LeanPool.Polylean.ConjInvLength.Length #

source

def LeanPool.Polylean.Letter.int :

Letter → ℤ

Integer code for each letter.

Equations

Instances For

source

@[implicit_reducible]

instance LeanPool.Polylean.instPowWordNat :

Pow Word ℕ

Equations

LeanPool.Polylean.instPowWordNat = { pow := fun (w : LeanPool.Polylean.Word) (n : ℕ) => w.pow n }

source

@[reducible, inline]

abbrev LeanPool.Polylean.Wrd :

Type

Array-backed words used by the memoized length computation.

Equations

LeanPool.Polylean.Wrd = Array LeanPool.Polylean.Letter

Instances For

source

def LeanPool.Polylean.Word.wrd (w : Word) :

Wrd

Convert a list-backed word to an array-backed word.

Equations

w.wrd = List.toArray w

Instances For

source

def LeanPool.Polylean.Wrd.toString (w : Wrd) :

String

Render an array-backed word by concatenating rendered letters.

Equations

w.toString = Array.foldl (fun (x : String) (y : LeanPool.Polylean.Letter) => toString x ++ toString y) "" w

Instances For

source

@[implicit_reducible]

instance LeanPool.Polylean.Wrd.instToString :

ToString Wrd

Equations

LeanPool.Polylean.Wrd.instToString = { toString := LeanPool.Polylean.Wrd.toString }

source

def LeanPool.Polylean.Wrd.pow :

Wrd → ℕ → Wrd

Repeated concatenation of an array-backed word.

Equations

x✝.pow 0 = #[]
x✝.pow m.succ = x✝ ++ x✝.pow m

Instances For

source

@[implicit_reducible]

instance LeanPool.Polylean.Wrd.instPowNat :

Pow Wrd ℕ

Equations

LeanPool.Polylean.Wrd.instPowNat = { pow := fun (w : LeanPool.Polylean.Wrd) (n : ℕ) => w.pow n }

source

def LeanPool.Polylean.Wrd.hashfn (w : Wrd) :

UInt64

Hash function for array-backed words.

Equations

w.hashfn = Array.foldl (fun (h : UInt64) (i : LeanPool.Polylean.Letter) => mixHash h (hash i)) 7 w

Instances For

source

@[implicit_reducible]

instance LeanPool.Polylean.Wrd.instHashable :

Hashable Wrd

Equations

LeanPool.Polylean.Wrd.instHashable = { hash := LeanPool.Polylean.Wrd.hashfn }

source

opaque LeanPool.Polylean.Wrd.normCache :

IO.Ref (Std.HashMap Wrd ℕ)

Cache for normalized word lengths.

source

@[irreducible]

def LeanPool.Polylean.Wrd.splits (l : Letter) (w : Wrd) :

Array { p : Wrd × Wrd // Array.size p.fst + Array.size p.snd < Array.size w }

All splits of an array-backed word around occurrences of a letter.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[irreducible]

def LeanPool.Polylean.Wrd.length (w : Wrd) :

IO ℕ

Memoized conjugation-invariant length candidate for array-backed words.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def LeanPool.Polylean.wordLength (w : Word) :

IO ℕ

Memoized length for list-backed words.

Equations

LeanPool.Polylean.wordLength w = w.wrd.length

Instances For

source

def LeanPool.Polylean.Wrd.conj :

Wrd → Letter → Wrd

Conjugate an array-backed word by a letter.

Equations

w.conj l = #[l] ++ w ++ #[l⁻¹ ]

Instances For

source

@[implicit_reducible]

instance LeanPool.Polylean.instPowWrdLetter :

Pow Wrd Letter

Equations

LeanPool.Polylean.instPowWrdLetter = { pow := fun (w : LeanPool.Polylean.Wrd) (l : LeanPool.Polylean.Letter) => w.conj l }