#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.

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.

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.