Lean.Meta.Tactic.Apply

source

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

Lean.MetaM (Nat × Bool)

Equations

Lean.Meta.getExpectedNumArgsAux e = Lean.Meta.withDefault (Lean.Meta.forallTelescopeReducing e fun xs body => pure (Array.size xs, Lean.Expr.isMVar (Lean.Expr.getAppFn body)))

source

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

Lean.MetaM Nat

Equations

Lean.Meta.getExpectedNumArgs e = do let discr ← Lean.Meta.getExpectedNumArgsAux e let x : Nat × Bool := discr match x with | (numArgs, x) => pure numArgs

source

def Lean.Meta.synthAppInstances (tacticName : Lean.Name) (mvarId : Lean.MVarId) (newMVars : Array Lean.Expr) (binderInfos : Array Lean.BinderInfo) :

Lean.MetaM Unit

Equations

Lean.Meta.synthAppInstances tacticName mvarId newMVars binderInfos = Nat.forM (Array.size newMVars) fun i => if Lean.BinderInfo.isInstImplicit (Array.getOp binderInfos i) = true then let mvar := Array.getOp newMVars i; do let mvarType ← Lean.Meta.inferType mvar let mvarVal ← Lean.Meta.synthInstance mvarType none let a ← Lean.Meta.isDefEq mvar mvarVal if a = true then pure PUnit.unit else Lean.Meta.throwTacticEx tacticName mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "failed to assign synthesized instance") Lean.Syntax.missing else pure PUnit.unit

source

def Lean.Meta.appendParentTag (mvarId : Lean.MVarId) (newMVars : Array Lean.Expr) (binderInfos : Array Lean.BinderInfo) :

Lean.MetaM Unit

Equations

Lean.Meta.appendParentTag mvarId newMVars binderInfos = do let parentTag ← Lean.Meta.getMVarTag mvarId if (Array.size newMVars == 1) = true then Lean.Meta.setMVarTag (Lean.Expr.mvarId! (Array.getOp newMVars 0)) parentTag else if Lean.Name.isAnonymous parentTag = true then pure PUnit.unit else Nat.forM (Array.size newMVars) fun i => let newMVarId := Lean.Expr.mvarId! (Array.getOp newMVars i); do let a ← Lean.Meta.isExprMVarAssigned newMVarId if a = true then pure PUnit.unit else if Lean.BinderInfo.isInstImplicit (Array.getOp binderInfos i) = true then pure PUnit.unit else do let currTag ← Lean.Meta.getMVarTag newMVarId Lean.Meta.setMVarTag newMVarId (Lean.Meta.appendTag parentTag currTag)

source

def Lean.Meta.postprocessAppMVars (tacticName : Lean.Name) (mvarId : Lean.MVarId) (newMVars : Array Lean.Expr) (binderInfos : Array Lean.BinderInfo) :

Lean.MetaM Unit

Equations

Lean.Meta.postprocessAppMVars tacticName mvarId newMVars binderInfos = do Lean.Meta.synthAppInstances tacticName mvarId newMVars binderInfos Lean.Meta.appendParentTag mvarId newMVars binderInfos

source

inductive Lean.Meta.ApplyNewGoals :

Type

nonDependentFirst: Lean.Meta.ApplyNewGoals
nonDependentOnly: Lean.Meta.ApplyNewGoals
all: Lean.Meta.ApplyNewGoals

source

def Lean.Meta.apply (mvarId : Lean.MVarId) (e : Lean.Expr) :

Lean.MetaM (List Lean.MVarId)

Equations

Lean.Meta.apply mvarId e = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `apply let targetType ← Lean.Meta.getMVarType mvarId let eType ← Lean.Meta.inferType e let discr ← Lean.Meta.getExpectedNumArgsAux eType let x : Nat × Bool := discr match x with | (numArgs, hasMVarHead) => let _do_jp := fun numArgs y => do let discr ← Lean.Meta.forallMetaTelescopeReducing eType (some numArgs) Lean.MetavarKind.natural let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (newMVars, binderInfos, eType) => do let a ← Lean.Meta.isDefEq eType targetType let _do_jp : PUnit → Lean.MetaM (List Lean.MVarId) := fun y => do Lean.Meta.postprocessAppMVars `apply mvarId newMVars binderInfos let e ← Lean.Meta.instantiateMVars e Lean.Meta.assignExprMVar mvarId (Lean.mkAppN e newMVars) let newMVars ← Array.filterM (fun mvar => not <$> Lean.Meta.isExprMVarAssigned (Lean.Expr.mvarId! mvar)) newMVars 0 (Array.size newMVars) let otherMVarIds ← Lean.Meta.getMVarsNoDelayed e let newMVarIds ← Lean.Meta.reorderNonDependentFirst newMVars let otherMVarIds : Array Lean.MVarId := Array.filter (fun mvarId => !List.contains newMVarIds mvarId) otherMVarIds 0 (Array.size otherMVarIds) let result : List Lean.MVarId := newMVarIds ++ Array.toList otherMVarIds List.forM result Lean.Meta.headBetaMVarType pure result if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Meta.throwApplyError mvarId eType targetType _do_jp y; if hasMVarHead = true then do let y ← pure PUnit.unit _do_jp numArgs y else do let targetTypeNumArgs ← Lean.Meta.getExpectedNumArgs targetType let numArgs : Nat := numArgs - targetTypeNumArgs let y ← pure PUnit.unit _do_jp numArgs y

source

def Lean.Meta.splitAnd (mvarId : Lean.MVarId) :

Lean.MetaM (List Lean.MVarId)

Equations

Lean.Meta.splitAnd mvarId = Lean.Meta.saturate mvarId fun mvarId => Lean.observing? (Lean.Meta.apply mvarId (Lean.mkConst `And.intro))

source

def Lean.Meta.applyRefl (mvarId : Lean.MVarId) (msg : optParam Lean.MessageData (Function.comp Lean.MessageData.ofFormat Lean.format "refl failed")) :

Lean.MetaM Unit

Equations

Lean.Meta.applyRefl mvarId msg = Lean.Meta.withMVarContext mvarId do let discr ← Lean.observing? do let a ← Lean.Meta.mkFreshLevelMVar Lean.Meta.apply mvarId (Lean.mkConst `Eq.refl [a]) match discr with | some [] => pure PUnit.unit | x => Lean.Meta.throwTacticEx `refl mvarId msg Lean.Syntax.missing

source

def Lean.Meta.exfalso (mvarId : Lean.MVarId) (msg : optParam Lean.MessageData (Function.comp Lean.MessageData.ofFormat Lean.format "exfalso failed")) :

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.exfalso mvarId msg = Lean.Meta.withMVarContext mvarId do let discr ← Lean.observing? do let a ← Lean.Meta.mkFreshLevelMVar Lean.Meta.apply mvarId (Lean.mkConst `False.elim [a]) match discr with | some [mvarId] => pure mvarId | x => Lean.Meta.throwTacticEx `exfalso mvarId msg Lean.Syntax.missing