Idea: `given` methods and `proven` proofs about ask HOT 3 CLOSED

Let me just quickly add in my support for 2. No feedback that my proof was really finished was indeed one thing that made me unsure when briefly playing around earlier today.

from ask.

Latest update. The given method is now implemented. I'm working on proven while rebuilding the prettyprinter with a tighter grip on whitespace. One annoyance is that if someone is silly enough to do

prove a & b by AndI where prove a ?
                          prove b ?

then solving the subgoals will make the main goal proven, necessitating a repair in the indentation. Options:

• Suck it up, detect the where-horizontal, rejig the whitespace.
• Ban the where-horizontal.
• Choose a 5 letter word to replace "proven", e.g. "happy" or "known" or "yaldi" or what?

Meanwhile, the question of whether proven-givens (also proven-from-Falses, proven-by-TrueIs) should be automatically inserted in empty prove-wheres but not in nonempty prove-wheres or provens, is really a tension between informative verbosity for beginners and clutter for the more advanced. If we do it, it should only be as an opt-in "beginner mode".

from ask.

1 & 2 have happened. 3 could still happen, but it seems like its at a priority below the threshold of action. So I'm closing this issue.

from ask.