To ensure refolding of named fix/cofix, I somehow arrived to the conclusion that the simplest way would be to add an optional extra information to Fix/CoFix constr nodes which informs that the fix/cofix has a toplevel definition.
A node would look like Fix ((decrs,i),((binder_names,alt_forms),types,body)
and:
alt_forms
are convertible to the Fix
expressions themselvesFix
expressions themselvesFor instance, for Nat.add
this would be Fix (([|0|],0),([|(Name add,Some Nat.add)|],[|nat->nat->nat|],[|...|])
.
Cross-posted with other details on CEP 45.
Last updated: Oct 13 2024 at 01:02 UTC