yellowsquid/correct-obs.git/src/Core/Term, branch nameless [no description] http://git.yellowsquid.uk/yellowsquid/correct-obs.git/atom?h=nameless 2023-04-23T13:53:40Z Define shape views. 2023-04-23T13:53:40Z Chloe Brown chloe.brown.00@outlook.com 2023-04-23T13:53:40Z urn:sha1:8baf4268940277164f1462187501225033ec93c4 Define generic equality. 2023-04-16T18:30:00Z Chloe Brown chloe.brown.00@outlook.com 2023-04-16T18:30:00Z urn:sha1:ae80fe4d92ff37b3bdd1b9c34e277ec6c9d40eec Judgemental equality is a trivial instance. Prove weakening of type judgements. 2023-04-16T17:31:20Z Chloe Brown chloe.brown.00@outlook.com 2023-04-16T17:31:20Z urn:sha1:87eea439d8d8390c768498c2224268200373f629 This is a huge commit that has many more changes. I should split this up later. Prove weakening a thinned term is homomorphic. 2023-04-16T14:25:29Z Chloe Brown chloe.brown.00@outlook.com 2023-04-16T14:25:29Z urn:sha1:69d8b5c52f8685e3b6332b1fa9892d2f1060adc4 Prove whnfs do not reduce. 2023-04-16T13:50:55Z Chloe Brown chloe.brown.00@outlook.com 2023-04-16T13:50:55Z urn:sha1:5a53c75f533f2ae758635e1989c4e7fb2b6469d5 Define declarative typing rules. 2023-04-15T16:07:32Z Chloe Brown chloe.brown.00@outlook.com 2023-04-15T16:07:32Z urn:sha1:9e2bd48420feba7c7752fd98cdf10fb67f56edc8 Prove substitution respects the quotient. 2023-04-15T15:35:15Z Chloe Brown chloe.brown.00@outlook.com 2023-04-15T15:35:15Z urn:sha1:a38b0b5a6ee30e7dd22bc91765ba5361ed807dda Define Term substitution. 2023-04-15T15:16:35Z Chloe Brown chloe.brown.00@outlook.com 2023-04-15T15:16:35Z urn:sha1:5f83999f483e241158706522a35364ba32f7f203