yellowsquid/church-eval.git/src/Total, branch better-thinning [no description] http://git.yellowsquid.uk/yellowsquid/church-eval.git/atom?h=better-thinning 2023-06-15T15:09:42Z WIP : use smarter weakenings. 2023-06-15T15:09:42Z Chloe Brown chloe.brown.00@outlook.com 2023-06-15T15:09:42Z urn:sha1:cedc6109895a53ce6ed667e0391b232bf5463387 Use co-deBruijn syntax in logical relation proof. 2023-06-09T15:00:39Z Chloe Brown chloe.brown.00@outlook.com 2023-06-09T15:00:39Z urn:sha1:f910e142ce7c10f8244ecfa40e41756fb8c8a53f Many proofs are still missing. Because they are erased, the program still runs fine without them. Use CoDebruijn syntax at top level. 2023-06-08T16:17:04Z Chloe Brown chloe.brown.00@outlook.com 2023-06-08T16:17:04Z urn:sha1:d5794f15b40ef4c683d713ffad027e94f2caf17e Fully expand thinnings. 2023-06-08T13:23:29Z Chloe Brown chloe.brown.00@outlook.com 2023-06-08T13:23:29Z urn:sha1:c64650ee0f41a1ebe45cf92c9b999f39825e9f5e This makes adding CoDebruijn syntax simpler. If carrying the lengths of contexts around is too inefficient, I can always switch back to truncated thinnings. Add a pretty printer. 2023-06-06T14:13:22Z Chloe Brown chloe.brown.00@outlook.com 2023-06-06T14:13:22Z urn:sha1:6590816a835110b8181472a5116dd4ecf67c957c Write an encoding for data types. 2023-06-06T11:25:26Z Chloe Brown chloe.brown.00@outlook.com 2023-06-06T11:25:26Z urn:sha1:bf07a9fe3ee4ff06fe186e33221f7f91871b9217 Give a logical relation template. 2023-06-01T16:07:41Z Chloe Brown chloe.brown.00@outlook.com 2023-06-01T16:07:41Z urn:sha1:d5f8497dbb6de72d9664f48d6acbc9772de77be3 Define terms with substitution as an operation. 2023-06-01T10:54:49Z Chloe Brown chloe.brown.00@outlook.com 2023-06-01T10:54:49Z urn:sha1:3eb03e2347b35432f7eae7d6847ec9ecf1dff19e