summaryrefslogtreecommitdiff
path: root/src/Obs/Typing.idr
AgeCommit message (Collapse)Author
2023-01-01Index normal forms with relevance.Greg Brown
- Remove container types. - Replace sum types with booleans. - Remove type annotation from absurd. - Add original type as argument to cast. - Make if (was case) take a lambda for the return type.
2022-12-22Add Container types.Greg Brown
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-17Add type checking and inference.Greg Brown