Operator unfolding when applied to enough arguments#431
Conversation
When declaring an operator, it is now possible to specify which arguments are mandatory before an operator application is automtically unfolded during simplification. Syntax is: ``` op name (x1 : t1) (xp : tp) / (x_p+1 : t_p+1) ... = ... ``` where the optional `/` indicated that the operator `name` will be automatically unfolded when applied to at least `p` arguments.
|
Will you be looking for a review related to maintained proofs? I have a couple where this looks like it could be massively useful. (The Conversely, it looks like this will make a lot of proofs a lot less pleasant to step through and learn from unless some operators are made opaque or manually |
|
Just saw the updated description. This helps a bit. The question still stands, though. |
|
The PR does not change the default behaviour, so it is safe w.r.t. existing proofs. The next step would be to mark some operators of the standard library as auto-unfoldable. Not that this should be done only for cases where you do not want the folded version of the operator (e.g. |
2 participants
Operator unfolding when applied to enough arguments
When declaring an operator, it is now possible to specify which
arguments are mandatory before an operator application is
automtically unfolded during simplification.
Syntax is:
where the optional
/indicated that the operatornamewillbe automatically unfolded when applied to at least
parguments.