@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Instances For
Equations
- Lean.Expr.ReplaceLevelImpl.cache i key result = do modify fun (s : Lean.Expr.ReplaceLevelImpl.State) => { keys := s.keys.uset i key ⋯, results := s.results.uset i result ⋯ } pure result
Instances For
unsafe def
Lean.Expr.ReplaceLevelImpl.replaceUnsafeM
(f? : Lean.Level → Option Lean.Level)
(size : USize)
(e : Lean.Expr)
:
Equations
Instances For
unsafe def
Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit
(f? : Lean.Level → Option Lean.Level)
(size : USize)
(e : Lean.Expr)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
unsafe def
Lean.Expr.ReplaceLevelImpl.replaceUnsafe
(f? : Lean.Level → Option Lean.Level)
(e : Lean.Expr)
:
Equations
Instances For
@[implemented_by Lean.Expr.ReplaceLevelImpl.replaceUnsafe]