Email Gateway (Aug 22 2022 at 14:14): Email Gateway (Aug 22 2022 at 14:14):From: Lars Hupel <hupel@in.tum.de>
Dear Makarius,
the "proof outline" feature is very helpful. I have two suggestions for
improvements, and one item which could be worth thinking about:
1) Sometimes I define inductive predicates using "_" instead of
inventing a bogus variable name. When writing an inductive proof, I
usually do the same thing:
case (rec_comb Γ t css name Γ' cs u u' env _ rhs val)
The "proof outline" however will invent a funny name, like "uu". Is it
possible to also print "_" here? In my opinion it's much nicer to
explicitly state that a variable doesn't matter than to use a somehow
modified internal name.
2) Is it possible for the blue "i" icon in the gutter to disappear when
a proof body already exists? As it stands it is easily mistaken for a
hint given by "Auto Quickcheck" or "Auto Solve Direct".
3) I would assume that the mechanism is general enough to allow skeleton
generation for arbitrary initial methods. I'm mainly thinking about the
"standard" method here, but of course, this may also apply to others.
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC