# Documentation

Lean.Meta.Check

This is not the Kernel type checker, but an auxiliary method for checking whether terms produced by tactics and isDefEq are type correct.

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

Given two expressions a and b, this method tries to annotate terms with pp.explicit := true to expose "implicit" differences. For example, suppose a and b are of the form

@HashMap Nat Nat eqInst hasInst1
@HashMap Nat Nat eqInst hasInst2


By default, the pretty printer formats both of them as HashMap Nat Nat. So, counterintuitive error messages such as

error: application type mismatch
HashMap.insert m
argument
m
has type
HashMap Nat Nat
but is expected to have type
HashMap Nat Nat


would be produced. By adding pp.explicit := true, we can generate the more informative error

error: application type mismatch
HashMap.insert m
argument
m
has type
@HashMap Nat Nat eqInst hasInst1
but is expected to have type
@HashMap Nat Nat eqInst hasInst2


Remark: this method implements a simple heuristic, we should extend it as we find other counterintuitive error messages.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.mkHasTypeButIsExpectedMsg (givenType : Lean.Expr) (expectedType : Lean.Expr) :

Return error message "has type{givenType}\nbut is expected to have type{expectedType}"

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

Throw an exception if e is not type correct.

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

Return true if e is type correct.

Equations