top_command (cmd_load_highlighting_info currentFile)
top_command (cmd_load currentFile [])
top_command (cmd_load_highlighting_info currentFile)
top_command (cmd_compile MAlonzo currentFile [])
-- Note that the previous fail does not unload the file
top_command cmd_constraints
top_command (cmd_load currentFile [])
top_command cmd_constraints
top_command cmd_metas
-- Note that cmd_make_case does not update the set of goals.
goal_command 0 cmd_make_case "n"
goal_command 0 (cmd_refine_or_intro False) "Just"
goal_command 7 (cmd_refine_or_intro False) ""
goal_command 4 cmd_auto ""
goal_command 3 (cmd_infer Instantiated) "D"
goal_command 7 (cmd_context Normalised) ""
goal_command 7 (cmd_goal_type Normalised) ""
goal_command 7 (cmd_goal_type_context Normalised) ""
goal_command 7 (cmd_goal_type_context_infer Normalised) "n"
goal_command 3 cmd_show_module_contents "D"
goal_command 3 (cmd_intro False) ""
goal_command 6 cmd_refine "Just"
goal_command 8 (cmd_compute False) "s′ z"
goal_command 8 (cmd_compute True) "s′ z"
goal_command 8 cmd_give "d"
-- Note that cmd_solveAll does not update the set of goals.
top_command cmd_solveAll
goal_command 1 cmd_give "s z"
top_command (cmd_compute_toplevel False "eval throw")
goal_command 1 cmd_give "Nothing"
goal_command 7 cmd_give "n"
top_command (cmd_infer_toplevel Normalised "eval throw")
top_command (cmd_compute_toplevel False "eval throw")
top_command (cmd_compute_toplevel True "s′ n")
top_command (cmd_compute_toplevel True "s′ z")
top_command (cmd_show_module_contents_toplevel "D")
top_command (cmd_compile MAlonzo currentFile [])
top_command (cmd_compile Epic currentFile [])