Documentation

Mathlib.Tactic.TypeCheck

The type_check tactic #

Define the type_check tactic: it type checks a given expression, and traces its type.

source
def tacticType_check_ :
Lean.ParserDescr

Type check the given expression, and trace its type.

Equations
    Instances For