yellowsquid/idris-soas.git/src/SOAS, branch main [no description] http://git.yellowsquid.uk/yellowsquid/idris-soas.git/atom?h=main 2024-02-02T13:33:09Z Define generic syntax construction. 2024-02-02T13:33:09Z Greg Brown greg.brown01@ed.ac.uk 2024-02-01T19:25:13Z urn:sha1:4b9b6b0211f6fb5691d67ca77ac09be888e569b7 Whilst it works (see `Example`), a generated data type would probably work better. Improve runtime behaviour of variables. 2024-02-02T13:33:09Z Greg Brown greg.brown01@ed.ac.uk 2024-02-01T16:33:26Z urn:sha1:fa4de437fa3861189b506538f6ca4a39771ecbbb Operations like `weakl`, `weakr` and `copair` now treat variables as integers at runtime, instead of treating them as unary naturals. Reimplent `lift` in terms of `copair`. Split monolithic file into modules. 2024-02-02T13:32:49Z Greg Brown greg.brown01@ed.ac.uk 2024-02-01T15:23:47Z urn:sha1:6dde244c14410ede6d41e9a8607016e23c19e320 Prove metatheory for generic initial algebras, instead of a clunky concrete one.