summaryrefslogtreecommitdiff
path: root/src/Total/Term/CoDebruijn.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