LeanPool.Polylean.ConjInvLength.MemoLength

opaque LeanPool.Polylean.normCache : IO.Ref (Std.HashMap Word ℕ)

Cache for memoized word lengths.

@[irreducible]

def LeanPool.Polylean.memoLength : Word → IO ℕ

Memoized list-backed conjugation-invariant length candidate.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.memoLength [] = do let cache ← ST.Ref.get LeanPool.Polylean.normCache match cache.get? [] with | some n => pure n | none => pure 0