Equations
- Lean.Meta.unfold e declName = (fun pre => do let a ← Lean.Meta.getUnfoldEqnFor? declName match a with | some unfoldThm => do let a ← Lean.Meta.getSimpUnfoldContext Lean.Meta.Simp.main e a { pre := pre unfoldThm, post := fun e => pure (Lean.Meta.Simp.Step.done { expr := e, proof? := none }), discharge? := fun e => pure none } | x => do let a ← liftM (Lean.Meta.deltaExpand e fun a => a == declName) pure { expr := a, proof? := none }) Lean.Meta.unfold.pre
Equations
- Lean.Meta.unfold.pre unfoldThm e = do let a ← Lean.Meta.withReducible (Lean.Meta.Simp.tryLemma? e { keys := #[], levelParams := #[], proof := Lean.mkConst unfoldThm, priority := 1000, post := true, perm := false, name? := some unfoldThm } fun x => pure none) let _do_jp : Unit → Lean.Meta.SimpM Lean.Meta.Simp.Step := fun y => pure (Lean.Meta.Simp.Step.visit { expr := e, proof? := none }) match a with | none => do let y ← pure () _do_jp y | some r => pure (Lean.Meta.Simp.Step.done r)
Equations
- Lean.Meta.unfoldTarget mvarId declName = Lean.Meta.withMVarContext mvarId do let target ← Lean.Meta.getMVarType' mvarId let r ← Lean.Meta.unfold target declName Lean.Meta.applySimpResultToTarget mvarId target r
def
Lean.Meta.unfoldLocalDecl
(mvarId : Lean.MVarId)
(fvarId : Lean.FVarId)
(declName : Lean.Name)
:
Equations
- Lean.Meta.unfoldLocalDecl mvarId fvarId declName = Lean.Meta.withMVarContext mvarId do let localDecl ← Lean.Meta.getLocalDecl fvarId let a ← Lean.Meta.instantiateMVars (Lean.LocalDecl.type localDecl) let r ← Lean.Meta.unfold a declName let discr ← Lean.Meta.applySimpResultToLocalDecl mvarId fvarId r match discr with | some (x, mvarId) => pure mvarId | x => panicWithPosWithDecl "Lean.Meta.Tactic.Unfold" "Lean.Meta.unfoldLocalDecl" 39 70 "unreachable code has been reached"