The type_check tactic

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

def tacticType_check_ : Lean.ParserDescr

type_check e type checks the term e and prints its type to the infoview.

Equations

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