Equations
- Lean.Expr.ReplaceImpl.Cache.new e = let size := 1 <<< min (max e.approxDepth.toUSize 1) 13 - 1; { size := size, keysResults := mkArray (2 * size).toNat (unsafeCast ()) }
Instances For
@[inline]
Equations
- c.keyIdx key = ptrAddrUnsafe key % c.size
Instances For
@[inline]
unsafe def
Lean.Expr.ReplaceImpl.Cache.resultIdx
(c : Lean.Expr.ReplaceImpl.Cache)
(key : Lean.Expr)
:
Instances For
@[inline]
unsafe def
Lean.Expr.ReplaceImpl.Cache.hasResultFor
(c : Lean.Expr.ReplaceImpl.Cache)
(key : Lean.Expr)
:
Equations
- c.hasResultFor key = let_fun this := ⋯; ptrEq (unsafeCast key) c.keysResults[c.keyIdx key]
Instances For
@[inline]
unsafe def
Lean.Expr.ReplaceImpl.Cache.getResultFor
(c : Lean.Expr.ReplaceImpl.Cache)
(key : Lean.Expr)
:
Equations
- c.getResultFor key = let_fun this := ⋯; unsafeCast c.keysResults[c.resultIdx key]
Instances For
unsafe def
Lean.Expr.ReplaceImpl.Cache.store
(c : Lean.Expr.ReplaceImpl.Cache)
(key : Lean.Expr)
(result : Lean.Expr)
:
Equations
- c.store key result = { size := c.size, keysResults := (c.keysResults.uset (c.keyIdx key) (unsafeCast key) ⋯).uset (c.resultIdx key) (unsafeCast result) ⋯ }
Instances For
@[reducible, inline]
Instances For
@[inline]
Equations
- Lean.Expr.ReplaceImpl.cache key result = do modify fun (x : Lean.Expr.ReplaceImpl.Cache) => x.store key result pure result
Instances For
@[specialize #[]]
unsafe def
Lean.Expr.ReplaceImpl.replaceUnsafeM
(f? : Lean.Expr → Option Lean.Expr)
(e : Lean.Expr)
:
Equations
Instances For
@[specialize #[]]
unsafe def
Lean.Expr.ReplaceImpl.replaceUnsafeM.visit
(f? : Lean.Expr → Option Lean.Expr)
(e : Lean.Expr)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[inline]
unsafe def
Lean.Expr.ReplaceImpl.replaceUnsafe
(f? : Lean.Expr → Option Lean.Expr)
(e : Lean.Expr)
:
Equations
Instances For
@[implemented_by Lean.Expr.ReplaceImpl.replaceUnsafe]
Equations
- Lean.Expr.replace f? e = Lean.Expr.replaceNoCache f? e