WG211/M19Carette

When a programming language doesn't have the features you want, WG2.11 people always do the same thing: implement a PL on top of them to get the job done.

Here we find Agda's facilities for creating and manipulating theories (whether as records or modules) wanting, so we set about to fix the problem. First, by creating a completely undisciplined prototype to hash out the requirements, then a second version will hopefully emerge that is 'sensible'.

(joint work with Musa Al-hassy and Wolfram Kahl)