Stream: Coq devs & plugin devs

Topic: Systematically refolding named fix/cofix

Hugo Herbelin (Jan 31 2024 at 09:41):

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:

• the kernel would have to check that the alt_forms are convertible to the Fix expressions themselves
• the reduction would replace the recursive occurrences by alt_forms (if present) instead of by the Fix expressions themselves

For 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