yellowsquid/unify.git/src/Data, branch master [no description] http://git.yellowsquid.uk/yellowsquid/unify.git/atom?h=master 2024-01-22T12:05:20Z Fix invalid statement 2024-01-22T12:05:20Z Greg Brown greg.brown01@ed.ac.uk 2024-01-22T12:05:20Z urn:sha1:09cd77b9a880559f7f00f710d9a0b56df04fe807 Prove mgu has a unique factor. 2023-07-25T16:45:27Z Greg Brown greg.brown01@ed.ac.uk 2023-07-25T16:45:27Z urn:sha1:9c73520c5fe209cfd3d212b5891dfb8b677fb9d4 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 Add constructor for signature. 2023-07-12T13:44:40Z Greg Brown greg.brown01@ed.ac.uk 2023-07-12T13:44:40Z urn:sha1:890039d7dac42200ea280177d0dfba4792f30d93 Prove unification correct. 2023-07-12T13:02:42Z Greg Brown greg.brown01@ed.ac.uk 2023-07-12T13:02:42Z urn:sha1:fd658831ab53f07969524fee0257d086d6f79f5a Promote property equivalence to a record. 2023-07-11T16:22:14Z Greg Brown greg.brown01@ed.ac.uk 2023-07-11T16:22:14Z urn:sha1:66658a7102c5761fe6e4cfc5058f2fdafaa71b36 Improves inference for congruence. 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