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

This module also defines the #check' tactic and command, which behaves like #check but only shows explicit arguments in the signature.

def Mathlib.Tactic.«command#check'_» : Lean.ParserDescr

The #check' command is like #check, but only prints explicit arguments in the signature (i.e., omitting implicit and typeclass arguments).

Equations

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

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

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

To display only explicit arguments in the type signature, see #check'.

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. In contrast to #check t, we only pretty-print explicit arguments, and omit implicit or type class arguments. Currently this only works when t is the name of a declaration.

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 other #check commands, 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.