yellowsquid/idris-soat.git/src/Soat/Data, 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 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 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 Prove index property of shuffle. 2022-11-25T15:31:29Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T15:31:29Z urn:sha1:fec727c164f9f3967eb543406d082f89fe61c052 Prove curry and uncurry form an isomorphism. 2022-11-25T15:30:18Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T15:30:18Z urn:sha1:a7d205c7d156c81efb3590f30dce62939a9dd088 Define introductors for Pointwise. 2022-11-25T15:29:32Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T15:29:32Z urn:sha1:d55bab90ca4455dbd9406a1ca7dd4d74d1a39a36 refactor: add structural comments. 2022-11-25T15:28:55Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T15:28:55Z urn:sha1:e8b8d6063adb69188c0b971dc641fabf3fdb53cc Define index on Pointwise. 2022-11-25T15:28:16Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T15:28:16Z urn:sha1:effca509eb470faa515bdb7e61cdaddc80ed37ff Define wrap and unwrap. 2022-11-25T15:26:32Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T15:26:32Z urn:sha1:c13a509f5bbbe07d1e8899134a5385e1b72a9625 Prove properties about map. 2022-11-25T15:25:52Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T15:25:52Z urn:sha1:6df261f1c09a4f4df9030375c6874f5c4c8e8f83