Equations
Equations
- Lean.Meta.registerGetEqnsFn f = do let a ← Lean.initializing let _do_jp : PUnit → IO Unit := fun y => ST.Ref.modify Lean.Meta.getEqnsFnsRef fun a => f :: a if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← throw (IO.userError "failed to register equation getter, this kind of extension can only be registered during initialization") _do_jp y
Equations
- Lean.Meta.getEqnsFor? declName = do let a ← ST.Ref.get Lean.Meta.getEqnsFnsRef let r ← let col := a; forIn col { fst := none, snd := PUnit.unit } fun f r => let r := r.snd; do let a ← f declName match a with | some r => pure (ForInStep.done { fst := some (some r), snd := PUnit.unit }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM (Option (Array Lean.Name)) := fun y => pure none match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a
Equations
Equations
- Lean.Meta.registerGetUnfoldEqnFn f = do let a ← Lean.initializing let _do_jp : PUnit → IO Unit := fun y => ST.Ref.modify Lean.Meta.getUnfoldEqnFnsRef fun a => f :: a if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← throw (IO.userError "failed to register equation getter, this kind of extension can only be registered during initialization") _do_jp y
Equations
- Lean.Meta.getUnfoldEqnFor? declName = do let a ← ST.Ref.get Lean.Meta.getUnfoldEqnFnsRef let r ← let col := a; forIn col { fst := none, snd := PUnit.unit } fun f r => let r := r.snd; do let a ← f declName match a with | some r => pure (ForInStep.done { fst := some (some r), snd := PUnit.unit }) | x => do pure PUnit.unit pure (ForInStep.yield { fst := none, snd := PUnit.unit }) let x : PUnit := r.snd let _do_jp : PUnit → Lean.MetaM (Option Lean.Name) := fun y => pure none match r.fst with | none => do let y ← pure PUnit.unit _do_jp y | some a => pure a