hs-to-coq icon indicating copy to clipboard operation
hs-to-coq copied to clipboard

Published 20 hours ago • verified publisher icon antalsz

Termination edits for "Default" functions

Open sweirich opened this issue 5 years ago • 0 comments

Now that we have an edit to change the type of a definition to include a "Default" constraint, we have to think about the interaction with termination edits.

In particular, they don't work together --- the type change confuses things. For an example where this is necessary see collectNAnnBndrs in CoreSyn.

sweirich avatar Jun 25 '19 10:06 sweirich