summaryrefslogtreecommitdiff
path: root/src/SOAS/Strength.idr
AgeCommit message (Collapse)Author
2024-02-02Define generic syntax construction.mainGreg Brown
Whilst it works (see `Example`), a generated data type would probably work better.
2024-02-02Split monolithic file into modules.Greg Brown
Prove metatheory for generic initial algebras, instead of a clunky concrete one.