RedPRL/sml-redprl

Inductive types in multiverses

Closed this issue · 0 comments

favonia commented

Support the inductive types in the discrete universes. Support the discrete tag. This is a major extension to the theory.