ExtendedLambdaCase.in

top_command (cmd_load currentFile [])

-- Normalise and display a lambda lifted  extended lambda
top_command (cmd_compute_toplevel False "f")

-- Refine for extended lambdas (issue 713)
goal_command 4 cmd_refine "λ { a {x} b → a }"

-- Case splitting for function with implicit argument
top_command (showImplicitArgs True)
goal_command 3 cmd_make_case "z"
goal_command 3 cmd_make_case "w"
top_command (showImplicitArgs False)

-- Case splitting with lambda lifted definition, hidden arguments
goal_command 2 cmd_make_case "x'"
top_command (cmd_load currentFile [])
top_command (showImplicitArgs True)
goal_command 2 cmd_make_case "x'"


-- Case splitting with lambda lifted definition
goal_command 1 cmd_make_case "x"

-- Case splitting for nested extended lambdas
goal_command 0 cmd_make_case "y"