The behavior of Ctrl-Down is not user-friendly
On the following file, apply split_vc
on main and on subgoal 0, and prove subgoal 1 by calling a prover.
use int.Int
let f () : unit requires { 1 + 1 = 2 /\ 2 + 2 = 4 } = ()
let main () = f(); f(); f()
Assume that we want to save the proof of subgoal 0 for later. The navigation between goals with Ctrl-Up/Down becomes very painful. We can observe two issues:
- When selecting a subgoal of goal 0, pressing Ctrl-Down only cycles between subgoals 0.0 and 0.1, never reaching subgoal 2.
- When selecting subgoal 1, pressing Ctrl-Down jumps back up to 0.0 instead of going to 2.