Stream: Coq devs & plugin devs

Topic: Systematically refolding named fix/cofix


view this post on Zulip 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:

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