summaryrefslogtreecommitdiff
path: root/src/Total/Term.idr
AgeCommit message (Collapse)Author
2023-06-15WIP : use smarter weakenings.better-thinningChloe Brown
2023-06-09Use co-deBruijn syntax in logical relation proof.masterChloe Brown
Many proofs are still missing. Because they are erased, the program still runs fine without them.
2023-06-08Use CoDebruijn syntax at top level.Chloe Brown
2023-06-08Fully expand thinnings.Chloe Brown
This makes adding CoDebruijn syntax simpler. If carrying the lengths of contexts around is too inefficient, I can always switch back to truncated thinnings.
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