top_command    (cmd_load currentFile [])

-- "f" is not in scope in toplevel, so these do not work

-- top_command (cmd_compute_toplevel DefaultCompute "f r")
-- top_command (cmd_compute_toplevel IgnoreAbstract "f s")
-- top_command (cmd_infer_toplevel Normalised "f s")

-- Should compute to "a"
goal_command 0 (cmd_compute DefaultCompute) "f s"
goal_command 0 (cmd_compute IgnoreAbstract) "f s"

-- Inferred type should be "A"
goal_command 0 (cmd_goal_type_context_infer Normalised) "f s"

goal_command 1 (cmd_compute IgnoreAbstract) "\ r -> f (t r)"
goal_command 1 (cmd_goal_type_context_infer Normalised) "\ r -> f (t r)"

goal_command 2 (cmd_give "x")

goal_command 3 (cmd_give "r")
