summaryrefslogtreecommitdiff
path: root/src/Obs/NormalForm.idr
AgeCommit message (Collapse)Author
2022-12-21Add sum types.Greg Brown
2022-12-21Improve parsing.Greg Brown
2022-12-20Add equality types and casts.Greg Brown
2022-12-18Add dependent sums.Greg Brown
2022-12-18Introduce better logging.Greg Brown
Led to immediate bug fixes for Pi types.
2022-12-18Add dependent products.Greg Brown
2022-12-18Add False type.Greg Brown
2022-12-18Add the True type.Greg Brown
2022-12-17Add totality annotations.Greg Brown
The parser is unfortunately not classified as total.
2022-12-17Define normal form.Greg Brown