summaryrefslogtreecommitdiff
path: root/src/Inky/Term.idr
AgeCommit message (Collapse)Author
2024-11-12Add more names. Names are good.Greg Brown
2024-11-12Add ability to desugar terms.Greg Brown
Remove `getChildren` construct---it's too niche for the core language.
2024-10-30Define well-formedness for types.Greg Brown
2024-10-29Print type checking errors.Greg Brown
2024-10-28Make everything relevant.Greg Brown
Too few proofs were relevant. Now they are.
2024-10-09Do a lot.Greg Brown
- Add type aliases. - Make `suc` a symbol. - Fix incorrect specification for `IsFunction`. - Write parser for terms. - Use `collie` to improve command line experience.
2024-09-30Make tags for tuples and cases unique.Greg Brown
2024-09-17Introduce names in contexts.Greg Brown
Introduce rows for n-ary sums and products. Remove union types.
2024-09-12Make naturals a fixpoint type.Greg Brown
This removes the need for a custom fold on naturals.
2024-09-11Define terms.Greg Brown