Documentation

Lean.Meta.Check

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

Equations

Lean.Meta.throwLetTypeMismatchMessage fvarId = do let lctx ← Lean.getLCtx match Lean.LocalContext.find? lctx fvarId with | some (Lean.LocalDecl.ldecl x x_1 n t v x_2) => do let vType ← Lean.Meta.inferType v Lean.throwError (Lean.toMessageData "invalid let declaration, term" ++ Lean.toMessageData (Lean.indentExpr v) ++ Lean.toMessageData "\nhas type" ++ Lean.toMessageData (Lean.indentExpr vType) ++ Lean.toMessageData "\nbut is expected to have type" ++ Lean.toMessageData (Lean.indentExpr t) ++ Lean.toMessageData "") | x => panicWithPosWithDecl "Lean.Meta.Check" "Lean.Meta.throwLetTypeMismatchMessage" 24 9 "unreachable code has been reached"

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

Lean.MetaM (Lean.Expr × Lean.Expr)

Equations

Lean.Meta.addPPExplicitToExposeDiff a b = (fun visit hasExplicitDiff? => do let a ← Lean.getOptions let a_1 ← Lean.getOptions if (Lean.KVMap.getBool a `pp.all || Lean.KVMap.getBool a_1 `pp.explicit) = true then pure (a, b) else do let a ← Lean.Meta.instantiateMVars a let a_2 ← Lean.Meta.instantiateMVars b visit a a_2) Lean.Meta.addPPExplicitToExposeDiff.visit Lean.Meta.addPPExplicitToExposeDiff.hasExplicitDiff?

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

Lean.MetaM (Lean.Expr × Lean.Expr)

partial def Lean.Meta.addPPExplicitToExposeDiff.hasExplicitDiff? (xs : Array Lean.Expr) (as : Array Lean.Expr) (bs : Array Lean.Expr) :

Lean.MetaM (Option (Array Lean.Expr × Array Lean.Expr))

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

Lean.MetaM Lean.MessageData

Equations

Lean.Meta.mkHasTypeButIsExpectedMsg givenType expectedType = tryCatch (do let givenTypeType ← Lean.Meta.inferType givenType let expectedTypeType ← Lean.Meta.inferType expectedType let discr ← Lean.Meta.addPPExplicitToExposeDiff givenType expectedType let x : Lean.Expr × Lean.Expr := discr match x with | (givenType, expectedType) => do let discr ← Lean.Meta.addPPExplicitToExposeDiff givenTypeType expectedTypeType let x : Lean.Expr × Lean.Expr := discr match x with | (givenTypeType, expectedTypeType) => pure (Lean.toMessageData "has type" ++ Lean.toMessageData (Lean.indentD (Lean.toMessageData "" ++ Lean.toMessageData givenType ++ Lean.toMessageData " : " ++ Lean.toMessageData givenTypeType ++ Lean.toMessageData "")) ++ Lean.toMessageData "\nbut is expected to have type" ++ Lean.toMessageData (Lean.indentD (Lean.toMessageData "" ++ Lean.toMessageData expectedType ++ Lean.toMessageData " : " ++ Lean.toMessageData expectedTypeType ++ Lean.toMessageData "")) ++ Lean.toMessageData "")) fun x => do let discr ← Lean.Meta.addPPExplicitToExposeDiff givenType expectedType let x : Lean.Expr × Lean.Expr := discr match x with | (givenType, expectedType) => pure (Lean.toMessageData "has type" ++ Lean.toMessageData (Lean.indentExpr givenType) ++ Lean.toMessageData "\nbut is expected to have type" ++ Lean.toMessageData (Lean.indentExpr expectedType) ++ Lean.toMessageData "")

def Lean.Meta.throwAppTypeMismatch {α : Type} (f : Lean.Expr) (a : Lean.Expr) (extraMsg : optParam Lean.MessageData (Lean.MessageData.ofFormat Lean.Format.nil)) :

Equations

Lean.Meta.throwAppTypeMismatch f a extraMsg = do let discr ← Lean.Meta.getFunctionDomain f let x : Lean.Expr × Lean.BinderInfo := discr match x with | (expectedType, binfo) => let e := Lean.mkApp f a; let _do_jp := fun e y => do let aType ← Lean.Meta.inferType a let a ← Lean.Meta.mkHasTypeButIsExpectedMsg aType expectedType Lean.throwError (Lean.toMessageData "application type mismatch" ++ Lean.toMessageData (Lean.indentExpr e) ++ Lean.toMessageData "\nargument" ++ Lean.toMessageData (Lean.indentExpr a) ++ Lean.toMessageData "\n" ++ Lean.toMessageData a ++ Lean.toMessageData ""); if Lean.BinderInfo.isExplicit binfo = true then do let y ← pure PUnit.unit _do_jp e y else let e := Lean.Expr.setAppPPExplicit e; do let y ← pure PUnit.unit _do_jp e y

def Lean.Meta.checkApp (f : Lean.Expr) (a : Lean.Expr) :

Lean.MetaM Unit

Equations

Lean.Meta.checkApp f a = do let fType ← Lean.Meta.inferType f let fType ← Lean.Meta.whnf fType match fType with | Lean.Expr.forallE x d x_1 x_2 => do let aType ← Lean.Meta.inferType a let a ← Lean.Meta.isDefEq d aType if a = true then pure PUnit.unit else Lean.Meta.throwAppTypeMismatch f a (Lean.MessageData.ofFormat Lean.Format.nil) | x => Lean.Meta.throwFunctionExpected (Lean.mkApp f a)

def Lean.Meta.check (e : Lean.Expr) :

Lean.MetaM Unit

Equations

Lean.Meta.check e = Lean.traceCtx `Meta.check (Lean.Meta.withTransparency Lean.Meta.TransparencyMode.all (Lean.Meta.checkAux e))

def Lean.Meta.isTypeCorrect (e : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.isTypeCorrect e = tryCatch (do Lean.Meta.check e pure true) fun ex => let cls := `Meta.typeError; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Bool := fun y => pure false if a = true then do let y ← Lean.addTrace cls (Lean.Exception.toMessageData ex) _do_jp y else do let y ← pure PUnit.unit _do_jp y