proof-assistant

Description of the problem

as discussed in Zulip the documentation of Definition with Eval is unsatisfactory. A user might more look under Eval or eval to find ways to do e

A formula like forall x1. forall. x2. exists x3. phi gets resugared to, and hence pretty printed as, forall x1 x2 x3. phi. The bug is in the uncurry function in FStar.Syntax.Reguar.fs.

I won't have time to implement this, but it should be easy and it should provide a nice quality of life improvement.

Each goal buffer stars with a header line, like this:

1 focused subgoal
(shelved: 1) (ID 339)
  
  width : Z
  BW : Bitwidth width
  …

It would be nice to move that info to the modeline, next to the buffer name (*goals*). We can change the "lighter" of the

Eval cbn in 1 + 1.
Definition x :=
  Eval cbn in 1 + 1.
Definition y := 2.

The second Eval is not highlighted, and the second Definition is indented to match the second Eval.