Lean.Meta.Tactic.Assert

source

def Lean.Meta.assert (mvarId : Lean.MVarId) (name : Lean.Name) (type : Lean.Expr) (val : Lean.Expr) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.assert mvarId name type val = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `assert let tag ← Lean.Meta.getMVarTag mvarId let target ← Lean.Meta.getMVarType mvarId let newType : Lean.Expr := Lean.mkForall name Lean.BinderInfo.default type target let newMVar ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar newType tag Lean.Meta.assignExprMVar mvarId (Lean.mkApp newMVar val) pure (Lean.Expr.mvarId! newMVar)

source

def Lean.Meta.define (mvarId : Lean.MVarId) (name : Lean.Name) (type : Lean.Expr) (val : Lean.Expr) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.define mvarId name type val = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `define let tag ← Lean.Meta.getMVarTag mvarId let target ← Lean.Meta.getMVarType mvarId let newType : Lean.Expr := Lean.mkLet name type val target let newMVar ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar newType tag Lean.Meta.assignExprMVar mvarId newMVar pure (Lean.Expr.mvarId! newMVar)

source

def Lean.Meta.assertExt (mvarId : Lean.MVarId) (name : Lean.Name) (type : Lean.Expr) (val : Lean.Expr) (hName : optParam Lean.Name `h) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.assertExt mvarId name type val hName = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `assert let tag ← Lean.Meta.getMVarTag mvarId let target ← Lean.Meta.getMVarType mvarId let u ← Lean.Meta.getLevel type let hType : Lean.Expr := Lean.mkApp3 (Lean.mkConst `Eq [u]) type (Lean.mkBVar 0) val let newType : Lean.Expr := Lean.mkForall name Lean.BinderInfo.default type (Lean.mkForall hName Lean.BinderInfo.default hType target) let newMVar ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar newType tag let rflPrf ← Lean.Meta.mkEqRefl val Lean.Meta.assignExprMVar mvarId (Lean.mkApp2 newMVar val rflPrf) pure (Lean.Expr.mvarId! newMVar)

source

structure Lean.Meta.AssertAfterResult :

Type

fvarId : Lean.FVarId
mvarId : Lean.MVarId
subst : Lean.Meta.FVarSubst

source

def Lean.Meta.assertAfter (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (val : Lean.Expr) :

Lean.MetaM Lean.Meta.AssertAfterResult

Equations

Lean.Meta.assertAfter mvarId fvarId userName type val = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `assertAfter let tag ← Lean.Meta.getMVarTag mvarId let target ← Lean.Meta.getMVarType mvarId let localDecl ← Lean.Meta.getLocalDecl fvarId let lctx ← Lean.getLCtx let localInsts ← Lean.Meta.getLocalInstances let fvarIds : Array Lean.FVarId := Lean.LocalContext.foldl lctx (fun fvarIds decl => Array.push fvarIds (Lean.LocalDecl.fvarId decl)) #[] (Lean.LocalDecl.index localDecl + 1) let xs : Array Lean.Expr := Array.map Lean.mkFVar fvarIds let targetNew ← Lean.Meta.mkForallFVars xs target false false let targetNew : Lean.Expr := Lean.mkForall userName Lean.BinderInfo.default type targetNew let lctxNew : Lean.LocalContext := Array.foldl (fun lctxNew fvarId => Lean.LocalContext.erase lctxNew fvarId) lctx fvarIds 0 (Array.size fvarIds) let localInstsNew : Array Lean.LocalInstance := Array.filter (fun inst => !Array.contains fvarIds (Lean.Expr.fvarId! inst.fvar)) localInsts 0 (Array.size localInsts) let mvarNew ← Lean.Meta.mkFreshExprMVarAt lctxNew localInstsNew targetNew Lean.MetavarKind.syntheticOpaque tag 0 let args : Array Lean.Expr := Array.map Lean.mkFVar (Array.filter (fun fvarId => !Lean.LocalDecl.isLet (Lean.LocalContext.get! lctx fvarId)) fvarIds 0 (Array.size fvarIds)) let args : Array Lean.Expr := #[val] ++ args Lean.Meta.assignExprMVar mvarId (Lean.mkAppN mvarNew args) let discr ← Lean.Meta.intro1P (Lean.Expr.mvarId! mvarNew) let x : Lean.FVarId × Lean.MVarId := discr match x with | (fvarIdNew, mvarIdNew) => do let discr ← Lean.Meta.introNP mvarIdNew (Array.size fvarIds) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (fvarIdsNew, mvarIdNew) => let subst := Nat.fold (fun i subst => Lean.Meta.FVarSubst.insert subst (Array.getOp fvarIds i) (Lean.mkFVar (Array.getOp fvarIdsNew i))) (Array.size fvarIds) { map := ∅ }; pure { fvarId := fvarIdNew, mvarId := mvarIdNew, subst := subst }

source

structure Lean.Meta.Hypothesis :

Type

userName : Lean.Name
type : Lean.Expr
value : Lean.Expr

source

def Lean.Meta.assertHypotheses (mvarId : Lean.MVarId) (hs : Array Lean.Meta.Hypothesis) :

Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Equations

Lean.Meta.assertHypotheses mvarId hs = if Array.isEmpty hs = true then pure (#[], mvarId) else Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `assertHypotheses let tag ← Lean.Meta.getMVarTag mvarId let target ← Lean.Meta.getMVarType mvarId let targetNew : Lean.Expr := Array.foldr (fun h targetNew => Lean.mkForall h.userName Lean.BinderInfo.default h.type targetNew) target hs (Array.size hs) let mvarNew ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar targetNew tag let val : Lean.Expr := Array.foldl (fun val h => Lean.mkApp val h.value) mvarNew hs 0 (Array.size hs) Lean.Meta.assignExprMVar mvarId val Lean.Meta.introNP (Lean.Expr.mvarId! mvarNew) (Array.size hs)