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.

source

def Lean.Meta.addPPExplicitToExposeDiff (a b : Expr) :

MetaM (Expr × Expr)

Given two expressions a and b, this method tries to annotate terms with pp.explicit := true and other pp options 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 simple heuristics; we should extend it as we find other counterintuitive error messages.

Equations

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

Instances For

source

def Lean.Meta.throwLetTypeMismatchMessage {α : Type} (fvarId : FVarId) :

MetaM α

Equations

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

Instances For

source

def Lean.Meta.mkUnfoldAxiomsNote (givenType expectedType : Expr) :

MetaM MessageData

Adds note about definitions not unfolded because of the module system, if any.

Equations

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

Instances For

source

def Lean.Meta.mkHasTypeButIsExpectedMsg (givenType expectedType : Expr) (trailing? : Option MessageData := none) (trailingExprs : Array Expr := #[]) :

MetaM MessageData

Return error message "has type{givenType}\nbut is expected to have type{expectedType}" Adds the type’s types unless they are defeq.

If trailing? is non-none, it is appended to the end of the message. This requires modifying the produced message, so prefer specifying trailing? over appending a message to the result of this function. Any expressions appearing in the trailing message should be included in trailingExprs.

Equations