def Lean.Grind.AC.Seq.length : Seq → Nat

def Lean.Grind.AC.Seq.isVar (s : Seq) : Bool

Returns true if s is a variable.

def Lean.Grind.AC.Seq.reverse (s : Seq) : Seq

Reverses the sequence

def Lean.Grind.AC.Seq.compare (s₁ s₂ : Seq) : Ordering

@[instance_reducible]

instance Lean.Grind.AC.instOrdSeq_lean : Ord Seq

@[instance_reducible]

instance Lean.Grind.AC.instAppendSeq_lean : Append Seq

@[instance_reducible]

def Lean.Grind.AC.instOfNatSeq_lean {n : Nat} : OfNat Seq n

inductive Lean.Grind.AC.SubseqResult : Type

Result type for s₁.subseq s₂

• false : SubseqResult

  s₁ is not a subsequence of s₂

• exact : SubseqResult

  s₁ == s₂

• prefix (s : Seq) : SubseqResult

  s₁ ++ s == s₂

• suffix (s : Seq) : SubseqResult

  s ++ s₁ == s₂

• middle (p s : Seq) : SubseqResult

  p ++ s₁ ++ s == s₂

def Lean.Grind.AC.Seq.subseq (s₁ s₂ : Seq) : SubseqResult

s₁.subseq s₂ checks whether s₁ is a subsequence of s₂

inductive Lean.Grind.AC.SubsetResult : Type

Result type for s₁.subset s₂

• false : SubsetResult

  s₁ is not a subset of s₂

• exact : SubsetResult

  s₁ == s₂

• strict (s : Seq) : SubsetResult

  s₁.union s == s₂

def Lean.Grind.AC.Seq.subset (s₁ s₂ : Seq) : SubsetResult

s₁.subset s₂ checks whether s₁ is a subset of s₂. It assumes s₁ and s₂ are sorted.

def Lean.Grind.AC.Seq.isSorted (s : Seq) : Bool

def Lean.Grind.AC.Seq.contains (s : Seq) (x : Var) : Bool

def Lean.Grind.AC.Seq.noAdjacentDuplicates (s : Seq) : Bool

@[irreducible]

def Lean.Grind.AC.Seq.sharesVar (s₁ s₂ : Seq) : Bool

Returns true if s₁ and s₂ have at least one variable in common. The function assumes both of them are sorted.

def Lean.Grind.AC.toSeq? (xs : List Var) : Option Seq

def Lean.Grind.AC.Seq.superposeAC? (s₁ s₂ : Seq) : Option (Seq × Seq × Seq)

Returns some (r₁, c, r₂) if s₁ == r₁.union c and s₂ == r₂.union c

It assumes s₁ and s₂ are sorted

def Lean.Grind.AC.Seq.superpose? (s₁ s₂ : Seq) : Option (Seq × Seq × Seq)

Returns some (p, c, s) if s₁ == p ++ c and s₂ == c ++ s

def Lean.Grind.AC.Seq.firstVar (s : Seq) : Var

def Lean.Grind.AC.Seq.startsWithVar (s : Seq) (x : Var) : Bool

def Lean.Grind.AC.Seq.lastVar (s : Seq) : Var

def Lean.Grind.AC.Seq.endsWithVar (s : Seq) (x : Var) : Bool