Documentation

Lean.Meta.Tactic.Assumption

def Lean.Meta.findLocalDeclWithType? (type : Lean.Expr) :

Lean.MetaM (Option Lean.FVarId)

Equations

Lean.Meta.findLocalDeclWithType? type = do let a ← Lean.getLCtx Lean.LocalContext.findDeclRevM? a fun localDecl => if Lean.LocalDecl.isAuxDecl localDecl = true then pure none else do let a ← Lean.Meta.isDefEq type (Lean.LocalDecl.type localDecl) if a = true then pure (some (Lean.LocalDecl.fvarId localDecl)) else pure none

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

Lean.MetaM Bool

Equations

Lean.Meta.assumptionCore mvarId = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `assumption let a ← Lean.Meta.getMVarType mvarId let a ← Lean.Meta.findLocalDeclWithType? a match a with | none => pure false | some fvarId => do Lean.Meta.assignExprMVar mvarId (Lean.mkFVar fvarId) pure true

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

Lean.MetaM Unit

Equations

Lean.Meta.assumption mvarId = do let a ← Lean.Meta.assumptionCore mvarId if a = true then pure PUnit.unit else Lean.Meta.throwTacticEx `assumption mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "") Lean.Syntax.missing