yellowsquid/unify.git/src/Data/Fin, branch master [no description] http://git.yellowsquid.uk/yellowsquid/unify.git/atom?h=master 2023-07-25T15:32:51Z Remove SFin. 2023-07-25T15:32:51Z Greg Brown greg.brown01@ed.ac.uk 2023-07-25T15:32:51Z urn:sha1:c305e99c3f0866d2aa4fb0431b06fc398663bd94 Delete unused modules. Restructure some proofs to reduce the number of lemmas. Minor changes for use by other projects. 2023-07-16T14:19:15Z Greg Brown greg.brown01@ed.ac.uk 2023-07-16T14:19:15Z urn:sha1:bb4e7c82b7ecd93b7241be5fcc547cfd282a8908 Begin big unification proof. 2023-07-11T15:25:24Z Greg Brown greg.brown01@ed.ac.uk 2023-07-11T15:25:24Z urn:sha1:60df32ffd5b88498e4634649509bbd0810421004 Use new notion of Fin to reduce casts. 2023-07-11T12:54:54Z Greg Brown greg.brown01@ed.ac.uk 2023-07-11T12:54:54Z urn:sha1:60d5896ab7939ae42cf7744f93e8eaefa0675854 Describe unification. 2023-07-10T12:37:56Z Greg Brown greg.brown01@ed.ac.uk 2023-07-10T12:37:56Z urn:sha1:ce546fe96974cb7aa3b09c729f33ac6ba5169299 Add occurs check for terms. 2023-07-07T16:40:03Z Greg Brown greg.brown01@ed.ac.uk 2023-07-07T16:40:03Z urn:sha1:d42c29c3ded0e48021b24295c925b88232df6b75 Define zippers and prove no cycles exist. 2023-06-30T19:45:33Z Greg Brown greg.brown01@ed.ac.uk 2023-06-30T19:45:33Z urn:sha1:8c529393421843a7ccad041d2f29fa90b46bf6b6 Define thinning and thickening. 2023-06-30T17:34:49Z Greg Brown greg.brown01@ed.ac.uk 2023-06-30T17:34:49Z urn:sha1:621f6221048213dc4d359581197988050af99d0d