Try it out at https://atennapel.github.io/coc-os

Run CLI REPL:

yarn install
yarn start

Typecheck file:

yarn install
yarn start filename

Currently done:

• dependent functions (pi types)
• dependent pairs (sigma types)
• an heterogenous equality type with definitional uniqueness of identity proofs (UIP)
• booleans with an induction primitive
• type-in-type
• indexed descriptions ala "Gentle Art of Levitation"
• generic constructors from "Generic Constructors and Eliminators from Descriptions"
• generic eliminators from "Generic Constructors and Eliminators from Descriptions" (just for boolean-tagged datatypes for now)
• named holes (_name)
• generic eliminators for Fin tagged datatypes
• explicit erasure annotations

Not yet done:

• CEK machine for erased terms
• hash-based content-addressed references
• IO monad for system calls

Future work:

• levitation of Desc
• inductive-recursive types
• inductive-inductive types
• predicative universe hierarchy

TODO:
- add native unit type (for better printing, () : {})
- make erased language bigger (ifs, fix, etc.) in order to reduce ugly lambda encodings
- implement instance search
- implement pruning
- specialize meta when checking pair
- allow second component of pair to be erased
- fix infinite loop in postponements
- fix _ being used in elaboration
- allow erased FArg, Rec and HRec
- allow meta as head of glued value
- glued lets
- support some impredicative instantiation
- add a way to not mention type in argument of pi/sigma etc.

QUESTIONS:
- how to levitate in my core theory?
- is a first-order Arg description useful? (IFArg)
- can we erase Unit index in Desc?

LIBRARIES:
- find alternate definitions of symm, trans, eqRefl and uip, to allow for erasure of the proofs
- write more prelude functions
- write Desc using Desc