generated from omelkonian/agda-minimal-backend
-
Notifications
You must be signed in to change notification settings - Fork 3
Open
Labels
enhancementNew feature or requestNew feature or request
Description
The CertiCoq evaluator requires constructors to be fully-applied.
To comply, the backend currently eta-expands constructor applications, but this verified transformation is already provided by the MetaCoq project.
Once we get the plumbing with the rest of the pipeline going, this transformation should be dropped from the backend to use the verified one instead.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
enhancementNew feature or requestNew feature or request