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