search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
95 stars 20 forks source link

Add simpl never when defining operations #411

Open CohenCyril opened 7 months ago

CohenCyril commented 7 months ago

https://github.com/math-comp/hierarchy-builder/blob/8b1725c9d99e2f0ce6514998b125706aaeb550ac/HB/structure.elpi#L240

Right now we accidentally rely on the fact that simpl will not unfold operators of a structure because it has to go through two delta expansions to see the match. We should make this future proof by adding an explicit no simpl.