Sequences over nullables, typed

Each lifted operator has its plain counterpart's signature with an Option around every argument and around the result, and nothing else changed. The lift is strict: none unless every argument is some.

The sequence term becomes nullable, not its elements — Option (Array α), not Array (Option α).

def Cvc.Typed.Term.seqUpdate? [Ω] {α : Type} (s : Term (Option (Array α))) (idx : Term (Option Int)) (repl : Term (Option (Array α))) : Env (Term (Option (Array α)))

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

Equations

• s.seqUpdate? idx repl = Cvc.Untyped.Term.seqUpdate? s idx repl

def Cvc.Typed.Term.seqIndexof? [Ω] {α : Type} (s sub : Term (Option (Array α))) (start : Term (Option Int)) : Env (Term (Option Int))

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

Equations

• s.seqIndexof? sub start = Cvc.Untyped.Term.seqIndexof? s sub start

def Cvc.Typed.Term.seqRev? [Ω] {α : Type} (s : Term (Option (Array α))) : Env (Term (Option (Array α)))

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

Equations

• s.seqRev? = Cvc.Untyped.Term.seqRev? s

def Cvc.Typed.Term.seqExtract? [Ω] {α : Type} (s : Term (Option (Array α))) (idx len : Term (Option Int)) : Env (Term (Option (Array α)))

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

Equations

• s.seqExtract? idx len = Cvc.Untyped.Term.seqExtract? s idx len

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

seqConcat? over two or more terms.

Equations

• Cvc.Typed.Term.seqConcatN? terms atLeastTwoElements = Cvc.Untyped.Term.seqConcatN? terms atLeastTwoElements

def Cvc.Typed.Term.seqReplaceAll? [Ω] {α : Type} (s pat repl : Term (Option (Array α))) : Env (Term (Option (Array α)))

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

Equations

• s.seqReplaceAll? pat repl = Cvc.Untyped.Term.seqReplaceAll? s pat repl

def Cvc.Typed.Term.seqPrefix? [Ω] {α : Type} (pre s : Term (Option (Array α))) : Env (Term (Option Bool))

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

Equations

• pre.seqPrefix? s = Cvc.Untyped.Term.seqPrefix? pre s

def Cvc.Typed.Term.seqAt? [Ω] {α : Type} (s : Term (Option (Array α))) (idx : Term (Option Int)) : Env (Term (Option (Array α)))

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

Equations

• s.seqAt? idx = Cvc.Untyped.Term.seqAt? s idx

def Cvc.Typed.Term.seqConcat? [Ω] {α : Type} (lft rgt : Term (Option (Array α))) : Env (Term (Option (Array α)))

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

Equations

• lft.seqConcat? rgt = Cvc.Untyped.Term.seqConcat? lft rgt

def Cvc.Typed.Term.seqUnit? [Ω] {α : Type} (elm : Term (Option α)) : Env (Term (Option (Array α)))

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

Equations

• elm.seqUnit? = Cvc.Untyped.Term.seqUnit? elm

def Cvc.Typed.Term.seqLength? [Ω] {α : Type} (s : Term (Option (Array α))) : Env (Term (Option Int))

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

Equations

• s.seqLength? = Cvc.Untyped.Term.seqLength? s

def Cvc.Typed.Term.seqReplace? [Ω] {α : Type} (s pat repl : Term (Option (Array α))) : Env (Term (Option (Array α)))

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

Equations

• s.seqReplace? pat repl = Cvc.Untyped.Term.seqReplace? s pat repl

def Cvc.Typed.Term.seqNth? [Ω] {α : Type} (s : Term (Option (Array α))) (idx : Term (Option Int)) : Env (Term (Option α))

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

Equations

• s.seqNth? idx = Cvc.Untyped.Term.seqNth? s idx

def Cvc.Typed.Term.seqContains? [Ω] {α : Type} (s sub : Term (Option (Array α))) : Env (Term (Option Bool))

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

Equations

• s.seqContains? sub = Cvc.Untyped.Term.seqContains? s sub

def Cvc.Typed.Term.seqSuffix? [Ω] {α : Type} (suf s : Term (Option (Array α))) : Env (Term (Option Bool))

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

Equations

• suf.seqSuffix? s = Cvc.Untyped.Term.seqSuffix? suf s