Modify name of induction scheme hypotheses #20813
Conversation
coqbot-app
bot
added
the
needs: full CI
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
dhalilov
force-pushed
the
better-names-for-induction-principle-cases
branch
from
fea4334 to
76dcadd
Compare
coqbot-app
bot
added
the
needs: full CI
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
ppedrot
added
kind: enhancement
|
In addition to overlays, this will also need a changelog. |
ppedrot
left a comment
ppedrot
left a comment
There was a problem hiding this comment.
Looks desirable to me, both codewise and in terms of feature.
…generated schemes)
coqbot-app
bot
added
the
needs: full CI
| (srefl : P a (srefl a)) (a0 : A) (s : seq a a0) => | ||
| match s :> seq a a0 as s0 in (seq _ a1) return (P a1 s0) with | ||
| | srefl _ => f | ||
| | srefl _ => srefl |
There was a problem hiding this comment.
Expressions like this look confusing to me, with two of the srefls being constructors, and the other two being the argument (IIUC). It seems to me that this makes it harder for the reader to quickly see what is going on, especially if the expression appears further from the argument list. Is this really an improvement? What about calling the argument something like srefl' instead?
There was a problem hiding this comment.
This change was made partially with the intent of using those names to generate goal names (see #20809), and in that use case it would not make much sense to write [true']: instead of [true]: as a goal selector.
There was a problem hiding this comment.
I'd argue this is a printer issue, we should disambiguate the constructor names when there are bound variables that clash with it.
…generated schemes)
…nerated schemes)
dhalilov
force-pushed
the
better-names-for-induction-principle-cases
branch
from
0327afd to
0cc933b
Compare
|
@ppedrot this PR is ready for a full CI run |
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
(CI failure looks unrelated, also fails on master) |
ppedrot
removed
needs: overlay
|
This got a green light at the Rocq call, so I guess we can just @coqbot merge now |
|
@ppedrot: Please take care of the following overlays:
|
…ciple-cases Adapt to rocq-prover/rocq#20813 (Update default hypothesis name in generated schemes)
…nciple-cases Adapt to rocq-prover/rocq#20813 (Update default hypothesese names in generated schemes)
…0824 Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
4 participants
Moves away from generated names
f,f0, etc., and instead uses the constructor names for the hypotheses of the induction scheme.Overlays: