yellowsquid/idris-soat.git/src/Soat/SecondOrder, branch master [no description] http://git.yellowsquid.uk/yellowsquid/idris-soat.git/atom?h=master 2022-12-02T14:14:44Z WIP: Frex is free 2022-12-02T14:14:44Z Greg Brown greg.brown01@ed.ac.uk 2022-12-02T14:14:44Z urn:sha1:2bd69bf893b7e1ebe4186639526451caf2083b12 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 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 refactor: expand flip in most places. 2022-11-25T15:59:28Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T15:59:28Z urn:sha1:f335074a07d0a7aa8332d384757929f8c65dc4cd Provide more bundles from algebras. 2022-11-25T15:40:44Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T15:40:44Z urn:sha1:bfac93dbe8c98d193feb165a088c6a7c79382d27 refactor: rename Homomorphism.f -> func. 2022-11-25T15:24:17Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T15:24:17Z urn:sha1:02f72834f36dbb3ff362f3876ebf87a2cebec0a8 refactor: rename Algebra.rel -> relation. 2022-11-25T15:21:42Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T15:21:42Z urn:sha1:1f867019430517435433ec55ad42dbf6770fd4fd Make proofs relevant. 2022-11-25T14:30:36Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T14:30:36Z urn:sha1:865e9dbdd0a7ed2b0dad75f2c672ad84e9e85bcc Remove unnecessary pattern matching. 2022-11-25T14:23:42Z Greg Brown greg.brown01@ed.ac.uk 2022-11-25T14:23:42Z urn:sha1:7c8591b566baeb6af42a22b8979c53ebdcab5479