mercredi 6 janvier 2021

Is it possible in Agda to define a new data type with meta-programming using reflection?

According to Agda documentation, a new function can be declared and defined via reflection by applying unquoteDecl and unquoteDef to an appropriate tactic. Is this also possible for new data types and records? Or has Agda not implemented this feature yet?





Aucun commentaire:

Enregistrer un commentaire