# `#check` tactic #

This module defines a tactic version of the `#check` command. While `#check t` is similar to `have := t`, it is a little more convenient since it elaborates `t` in a more tolerant way and so it can be possible to get a result. For example, `#check` allows metavariables.

source
def Mathlib.Tactic.elabCheckTactic (tk : Lean.Syntax) (ignoreStuckTC : Bool) (term : Lean.Term) :
Lean.Elab.Tactic.TacticM Unit

Tactic version of `Lean.Elab.Command.elabCheck`. Elaborates `term` without modifying tactic/elab/meta state. Info messages are placed at `tk`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.«tactic#check__» :
Lean.ParserDescr

The `#check t` tactic elaborates the term `t` and then pretty prints it with its type as `e : ty`.

If `t` is an identifier, then it pretty prints a type declaration form for the global constant `t` instead. Use `#check (t)` to pretty print it as an elaborated expression.

Like the `#check` command, the `#check` tactic allows stuck typeclass instance problems. These become metavariables in the output.

Equations

- One or more equations did not get rendered due to their size.

Instances For