lthms ⸮ is a user on mastodon.social. You can follow them or interact with them if you have an account anywhere in the fediverse.
If you don't, you can sign up here.
The #Coq equation plugin is pretty awesome:
Equations scopeLe (s s': Scope) : Prop :=
scopeLe None _ := True;
scopeLe _ All := True;
scopeLe (Only branches) (Only branches') := subset branches branches';
scopeLe _ _ := False.
@MartinShadok this one I don't know about. I will try to read more about it!
@lthms It's useful for recursive definitions. It's an equality of the form fix F = F (fix F). When you manipulate large definitions, such a lemma is very useful! And building it using tactics is a nightmare :-( So Equations really helps us there :-)
@MartinShadok this looks awesome. Especially if it works with cofixpoint.
Thanks for the hint!
@lthms I really appreciate the *_unfold generated lemma! :-) I totally agree :-)