yellowsquid/idris-soat.git/src/Soat, branch refactor/setoids [no description] http://git.yellowsquid.uk/yellowsquid/idris-soat.git/atom?h=refactor%2Fsetoids 2022-12-05T14:37:30Z WIP: port to library 2022-12-05T14:37:30Z Greg Brown greg.brown01@ed.ac.uk 2022-12-05T14:37:30Z urn:sha1:e8a5ba7c22c98d32671d02e41960598566bdcc58 Construct first-order algebraic coproducts. 2022-11-29T15:00:22Z Greg Brown greg.brown01@ed.ac.uk 2022-11-29T15:00:22Z urn:sha1:45e9bbec72bf338306d446012f077e195439aed0 refactor: introduce equational reasoning. 2022-11-29T14:57:58Z Greg Brown greg.brown01@ed.ac.uk 2022-11-29T14:57:58Z urn:sha1:3319050c0cb4c634d502e159da400b5a3cdcf828 Prove Pointwise forms a setoid. 2022-11-29T14:57:29Z Greg Brown greg.brown01@ed.ac.uk 2022-11-29T14:57:29Z urn:sha1:ce49914c213f798dd052229efe92633247fd4435 refactor: name arguments. 2022-11-29T14:54:22Z Greg Brown greg.brown01@ed.ac.uk 2022-11-29T14:54:22Z urn:sha1:07b5788d540bb81334389d68eeddfe81eadb1c90 Add a bundle for raw algebra with a relation. 2022-11-29T14:53:03Z Greg Brown greg.brown01@ed.ac.uk 2022-11-29T14:53:03Z urn:sha1:e8d6ac1f1d9c05b71bb9098a1590e29e5c93b0b8 Move indexed setoids and functions out of Soat. 2022-11-29T14:36:13Z Greg Brown greg.brown01@ed.ac.uk 2022-11-29T14:36:13Z urn:sha1:b21e69503571272a5f35cf84c731994f3e921a3a Extract setoids to a new module. 2022-11-29T14:24:17Z Greg Brown greg.brown01@ed.ac.uk 2022-11-29T14:24:17Z urn:sha1:d35c9f4eea009a5d3edd57c9165e49b8a7a66334 Prove the term algebras form an initial algebra. 2022-11-25T16:10:51Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T16:10:51Z urn:sha1:0b90e50d813a97aa3763e4aa209eaa3561fd401c Make implicit variables accessible for proofs. 2022-11-25T16:09:51Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T16:09:51Z urn:sha1:77af2f590343987071fc96da38d8fa399e513dc2