| Commit message (Collapse) | Author | Files | Lines |
|
|
|
|
|
statements. Also misc. cleanups.
|
|
learnt that I probably need to take a different approach. In particular, should first make the constants completely monomorphic, and then work on full proper type inference, rather than the heuristic approach taken here.
|
|
rules. Removing for now.
|
|
handling universes. Commit for release 0.1.0!
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Definition of function composition and properties.
|
|
Definition of function composition and properties.
|
|
|
|
|
|
|
|
type family decorations implicit.
|
|
|
|
|
|
|
|
derivation of "A:U" from "a:A".
|
|
|
|
|
|
be needed or useful later. Added [comp] attribute to be used by simplification met methods.
|
|
|
|
|
|
powerful derive method. Used these to rewrite proofs.
|
|
|
|
|
|
|
|
Added type formation rules expressing necessity of the conditions.
|
|
simplifier. Proved simplification rule for dependent fst.
|
|
|
|
|
|
|
|
formulation in the HoTT book.
|
|
|