Sequences over nullables, sort-erased

One lifted constructor per liftable operator, <id>?, each answering none unless every argument is some.

The sequence term becomes nullable, not its elements: (Nullable (Seq T)), not (Seq (Nullable T)).

def Cvc.Untyped.Term.seqContains? [Ω] (s sub : Term) : Env Term

seqContains lifted over nullables, strictly: none unless every argument is some.

Equations

• s.seqContains? sub = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_CONTAINS #[s, sub]

def Cvc.Untyped.Term.seqExtract? [Ω] (s idx len : Term) : Env Term

seqExtract lifted over nullables, strictly: none unless every argument is some.

Equations

• s.seqExtract? idx len = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_EXTRACT #[s, idx, len]

def Cvc.Untyped.Term.seqConcatN? [Ω] (terms : Terms) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env Term

seqConcat? over two or more terms.

Equations

• Cvc.Untyped.Term.seqConcatN? terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_CONCAT terms

def Cvc.Untyped.Term.seqPrefix? [Ω] (pre s : Term) : Env Term

seqPrefix lifted over nullables, strictly: none unless every argument is some.

Equations

• pre.seqPrefix? s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_PREFIX #[pre, s]

def Cvc.Untyped.Term.seqLength? [Ω] (s : Term) : Env Term

seqLength lifted over nullables, strictly: none unless every argument is some.

Equations

• s.seqLength? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_LENGTH #[s]

def Cvc.Untyped.Term.seqIndexof? [Ω] (s sub start : Term) : Env Term

seqIndexof lifted over nullables, strictly: none unless every argument is some.

Equations

• s.seqIndexof? sub start = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_INDEXOF #[s, sub, start]

def Cvc.Untyped.Term.seqRev? [Ω] (s : Term) : Env Term

seqRev lifted over nullables, strictly: none unless every argument is some.

Equations

• s.seqRev? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_REV #[s]

def Cvc.Untyped.Term.seqUnit? [Ω] (elm : Term) : Env Term

seqUnit lifted over nullables, strictly: none unless every argument is some.

Equations

• elm.seqUnit? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_UNIT #[elm]

def Cvc.Untyped.Term.seqConcat? [Ω] (lft rgt : Term) : Env Term

seqConcat lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.seqConcat? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_CONCAT #[lft, rgt]

def Cvc.Untyped.Term.seqSuffix? [Ω] (suf s : Term) : Env Term

seqSuffix lifted over nullables, strictly: none unless every argument is some.

Equations

• suf.seqSuffix? s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_SUFFIX #[suf, s]

def Cvc.Untyped.Term.seqNth? [Ω] (s idx : Term) : Env Term

seqNth lifted over nullables, strictly: none unless every argument is some.

Equations

• s.seqNth? idx = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_NTH #[s, idx]

def Cvc.Untyped.Term.seqAt? [Ω] (s idx : Term) : Env Term

seqAt lifted over nullables, strictly: none unless every argument is some.

Equations

• s.seqAt? idx = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_AT #[s, idx]

def Cvc.Untyped.Term.seqReplaceAll? [Ω] (s pat repl : Term) : Env Term

seqReplaceAll lifted over nullables, strictly: none unless every argument is some.

Equations

• s.seqReplaceAll? pat repl = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_REPLACE_ALL #[s, pat, repl]

def Cvc.Untyped.Term.seqUpdate? [Ω] (s idx repl : Term) : Env Term

seqUpdate lifted over nullables, strictly: none unless every argument is some.

Equations

• s.seqUpdate? idx repl = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_UPDATE #[s, idx, repl]

def Cvc.Untyped.Term.seqReplace? [Ω] (s pat repl : Term) : Env Term

seqReplace lifted over nullables, strictly: none unless every argument is some.

Equations

• s.seqReplace? pat repl = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SEQ_REPLACE #[s, pat, repl]