19 Commits (8a27ec29dedeec9640eb908c739b10f2978f21ee)

Author	SHA1	Message	Date
Amélia Liao	8a27ec29de	Fix recursive local lets	3 years ago
Amélia Liao	f745f7357d	fix composition for the universe	3 years ago
Amélia Liao	b4cf411a1b	more pain and suffering	3 years ago
Amélia Liao	d5c221c93d	some initial work on HITs	3 years ago
Amélia Liao	9c37655544	some fixes to inductive types	3 years ago
Amélia Liao	6827a8838c	Implement proper inductive types	3 years ago
Amélia Liao	7aa7a3fac8	Add where clauses	3 years ago
Amélia Liao	6d065cdddd	Use glued evaluation to get shorter normal forms	3 years ago
Amélia Liao	6d82ecd85f	Fix composition for pairs	3 years ago
Amélia Liao	e521e7f10e	Report unsolved metas & composition for the universe	3 years ago
Amélia Liao	8079ef845d	built-in bools (to be removed later)	3 years ago
Amélia Liao	e09d03572f	Add let definitions	3 years ago
Amélia Liao	1e6e17c3d8	Implement Glueing	3 years ago
Amélia Liao	eb83b77bf3	Implement cubical subtypes and composition	3 years ago
Amélia Liao	30b2984e1d	Implement partial elements and systems	3 years ago
Amélia Liao	134c24cb13	Implement dependent paths (PathP's)	3 years ago
Amélia Liao	818b816860	Wired in definitions for the interval algebra	3 years ago
Amélia Liao	9be5402444	Polish up the type checker	3 years ago
Amélia Liao	6eae8f2d2e	Implement MLTT elaborator w/ type inference	3 years ago