- fvarId : Lean.FVarId
- userName : Lean.Name
- id : Lean.Name
- type : Lean.Expr
- proof : Lean.Expr
Equations
- Lean.Meta.SimpAll.instInhabitedEntry = { default := { fvarId := default, userName := default, id := default, type := default, proof := default } }
- modified : Bool
- mvarId : Lean.MVarId
- entries : Array Lean.Meta.SimpAll.Entry
- ctx : Lean.Meta.Simp.Context
@[inline]
Equations
- Lean.Meta.SimpAll.main = do Lean.Meta.SimpAll.initEntries let a ← Lean.Meta.SimpAll.loop if a = true then pure none else do let a ← get let mvarId : Lean.MVarId := a.mvarId let a ← get let entries : Array Lean.Meta.SimpAll.Entry := a.entries let discr ← liftM (Lean.Meta.assertHypotheses mvarId (Array.map (fun e => { userName := e.userName, type := e.type, value := e.proof }) entries)) let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (x, mvarId) => Lean.Internal.liftCoeM (Lean.Meta.tryClearMany mvarId (Array.map (fun e => e.fvarId) entries))
Equations
- Lean.Meta.simpAll mvarId ctx = Lean.Meta.withMVarContext mvarId (StateRefT'.run' Lean.Meta.SimpAll.main { modified := false, mvarId := mvarId, entries := #[], ctx := ctx })