1
top_command (cmd_load currentFile [])
3
top_command (cmd_compute_toplevel False "f")
5
goal_command 4 cmd_refine "λ { a {x} b → a }"
7
top_command (showImplicitArgs True)
8
goal_command 3 cmd_make_case "z"
9
goal_command 3 cmd_make_case "w"
10
top_command (showImplicitArgs False)
12
goal_command 2 cmd_make_case "x'"
13
top_command (cmd_load currentFile [])
14
top_command (showImplicitArgs True)
15
goal_command 2 cmd_make_case "x'"
18
goal_command 1 cmd_make_case "x"
20
goal_command 0 cmd_make_case "y"