Load and type-check an Agda file. Returns goals, errors, and warnings.

This must be called before other commands. Call again after edits to refresh.

Args: file_path: Absolute path to the .agda file

Get type/definition info for a symbol at a position.

Args: file_path: Absolute path to the .agda file line: Line number (1-based) character: Column number (1-based)

Go to the definition of a symbol at a position.

Args: file_path: Absolute path to the .agda file line: Line number (1-based) character: Column number (1-based)

Infer the type of an expression in the context of a loaded file.

Args: file_path: Absolute path to the .agda file (for scope) expr: The expression to type-check (e.g. "add", "suc zero")

Normalize (evaluate) an expression.

Args: file_path: Absolute path to the .agda file (for scope) expr: The expression to evaluate (e.g. "add 2 3")

Case split on a variable in a goal. Returns the new clauses.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) variable: The variable name to split on

Get the type and context of a specific goal/hole.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output)

Try to automatically solve a goal.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output)

Explain where a name is brought into scope.

Args: file_path: Absolute path to the .agda file name: The name to look up (e.g. "ℕ", "suc", "add")

Fill a goal/hole with a complete solution.

Agda will check the expression and, if correct, replace the hole in the source file. Call agda_load afterwards to refresh goals.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: The expression to fill the hole with

Fill a goal/hole with an elaborated solution.

Like agda_give, but returns the fully elaborated (normalized) expression. Call agda_load afterwards to refresh goals.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: The expression to fill the hole with

Refine a goal by filling it with an expression that may create new subgoals.

If expr is empty, Agda tries to refine using the goal type. Call agda_load afterwards to refresh goals.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: Expression to refine with (can be empty)

Introduce a constructor or lambda abstraction in a goal.

Tries to fill the hole with an appropriate constructor or lambda. Call agda_load afterwards to refresh goals.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output)

Refine or introduce in a goal (auto-chooses the best action).

Combines refine and intro: tries to refine with the expression if given, otherwise introduces a constructor or lambda. Call agda_load afterwards to refresh goals.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: Expression to refine with (can be empty for intro)

Get the type of a specific goal/hole (without context).

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output)

Get the context (available bindings) at a specific goal/hole.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output)

Get goal type, context, and the inferred type of an expression.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: Expression whose type to infer in this goal's context

Get goal type, context, and check an expression against the goal type.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: Expression to check against the goal type

Infer the type of an expression in the context of a specific goal.

Unlike agda_infer which works at top level, this infers within a goal's local context (with access to locally-bound variables).

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: The expression to type-check

Normalize (evaluate) an expression in the context of a specific goal.

Unlike agda_compute which works at top level, this evaluates within a goal's local context.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: The expression to evaluate

Generate a helper function type signature for a goal.

The expression should be a partial application like "h x y" where h is the helper name and x, y are arguments. Agda will generate the type signature for h. If empty, uses whatever is in the goal.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) expr: Partial application (e.g. "helper x y")

Explain where a name is brought into scope, in the context of a goal.

Like agda_why_in_scope but with access to the goal's local scope.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) name: The name to look up

List the contents of a module, in the context of a goal.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output) module_name: The module or record name to inspect

Solve a single goal if its solution has been determined by unification.

Only works if the goal has been fully instantiated (e.g. by constraints). Call agda_load afterwards to refresh goals.

Args: file_path: Absolute path to the .agda file goal_id: The goal/hole number (from agda_load output)

Solve all goals whose solutions have been determined by unification.

Call agda_load afterwards to refresh goals.

Args: file_path: Absolute path to the .agda file

Try to automatically solve all visible goals.

Call agda_load afterwards to refresh goals.

Args: file_path: Absolute path to the .agda file

Show all current unsolved constraints.

Useful for debugging type errors or understanding what Agda is stuck on.

Args: file_path: Absolute path to the .agda file

Show all open meta-variables (goals) and their types.

Args: file_path: Absolute path to the .agda file

Search for definitions whose type mentions the given names.

Useful for finding relevant lemmas, functions, or constructors.

Args: file_path: Absolute path to the .agda file query: Space-separated names to search for in types

List the top-level names exported by a module.

Args: file_path: Absolute path to the .agda file module_name: The module name to inspect (e.g. "Data.Nat", "Data.List")