yellowsquid/correct-obs.git/src/Core/Term, branch master [no description] http://git.yellowsquid.uk/yellowsquid/correct-obs.git/atom?h=master 2023-04-08T13:30:55Z Reduce code duplication. 2023-04-08T13:30:55Z Chloe Brown chloe.brown.00@outlook.com 2023-04-08T13:30:55Z urn:sha1:12d5b7a16c443417daca46c5870d6b2660d90047 Prove many properties about substitutions. 2023-04-07T16:53:08Z Chloe Brown chloe.brown.00@outlook.com 2023-04-07T16:53:08Z urn:sha1:032a65f07bc5be170b1ccfe2338d4c9285e933c8 Migrate Substitution to use Thinned. 2023-04-06T16:12:38Z Chloe Brown chloe.brown.00@outlook.com 2023-04-06T16:12:38Z urn:sha1:4943ffb49405127ec3e8505c398b007dcd661dd0 Move Environment module. 2023-04-02T10:52:53Z Chloe Brown chloe.brown.00@outlook.com 2023-04-02T10:52:53Z urn:sha1:14279fa92481304e594e092e702f6925e7142ac5 Prove environment indexing preserves equality. 2023-04-02T08:45:55Z Chloe Brown chloe.brown.00@outlook.com 2023-04-02T08:45:55Z urn:sha1:f4bda78a3325c8fee491296b2cdcd79fb6f4f87c Define environment equality. 2023-04-01T14:13:36Z Chloe Brown chloe.brown.00@outlook.com 2023-04-01T14:13:36Z urn:sha1:a90932302afa9e13b8ed6f1159fbe604c89d453f Make environments do weakening lazily. 2023-04-01T12:58:46Z Chloe Brown chloe.brown.00@outlook.com 2023-04-01T12:58:46Z urn:sha1:f19665eac65f9a37dcde85eb58e7d4b5b4a22bcf This is in anticipation for defining well-formed thinnings. Fix record projection annotations. 2023-04-01T12:51:46Z Chloe Brown chloe.brown.00@outlook.com 2023-04-01T12:51:46Z urn:sha1:53ff29fda182629b9fd284b196ad67a47c95a777 Define Neutrals and Whnfs. 2023-04-01T12:30:46Z Chloe Brown chloe.brown.00@outlook.com 2023-04-01T12:16:22Z urn:sha1:c62b9753293389c37f29089a856a5d9a42ea23d5 Define Env indexing. 2023-03-31T17:14:53Z Chloe Brown chloe.brown.00@outlook.com 2023-03-31T17:14:53Z urn:sha1:fba865c2784d376f34dec543087d29db3d5090b7