yellowsquid/idris-soat.git/src/Soat/Data, branch refactor/strict [no description] http://git.yellowsquid.uk/yellowsquid/idris-soat.git/atom?h=refactor%2Fstrict 2022-12-06T13:33:06Z refactor: rename Soat.Data -> Data. 2022-12-06T13:33:06Z Greg Brown greg.brown01@ed.ac.uk 2022-12-06T13:33:06Z urn:sha1:1e64c562ad58d0fb264a11f11bc32b9311e728c4 Migrate to use idris-setoid library. 2022-12-06T13:22:10Z Greg Brown greg.brown01@ed.ac.uk 2022-12-06T13:22:10Z urn:sha1:522eb40ab39800f75daa704ae56c18953c4885e7 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