summaryrefslogtreecommitdiff
path: root/src/Total/NormalForm.idr
AgeCommit message (Expand)Author
2023-06-15WIP : use smarter weakenings.better-thinningChloe Brown
2023-06-09Use co-deBruijn syntax in logical relation proof.masterChloe Brown
2023-06-08Fully expand thinnings.Chloe Brown
2023-06-06Write an encoding for data types.Chloe Brown
2023-06-01Give a logical relation template.Chloe Brown
2023-06-01Define terms with substitution as an operation.Chloe Brown