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