Strings 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.

def Cvc.Typed.Term.strReplaceRe? [Ω] (s : Term (Option String)) (re : Term (Option Regex)) (repl : Term (Option String)) : Env (Term (Option String))

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

Equations

• s.strReplaceRe? re repl = Cvc.Untyped.Term.strReplaceRe? s re repl

def Cvc.Typed.Term.strToRegex? [Ω] (s : Term (Option String)) : Env (Term (Option Regex))

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

Equations

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

def Cvc.Typed.Term.strToLower? [Ω] (s : Term (Option String)) : Env (Term (Option String))

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

Equations

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

def Cvc.Typed.Term.strContains? [Ω] (s sub : Term (Option String)) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.strSubstr? [Ω] (s : Term (Option String)) (idx len : Term (Option Int)) : Env (Term (Option String))

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

Equations

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

def Cvc.Typed.Term.strCharAt? [Ω] (s : Term (Option String)) (idx : Term (Option Int)) : Env (Term (Option String))

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

Equations

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

def Cvc.Typed.Term.strInRegex? [Ω] (s : Term (Option String)) (re : Term (Option Regex)) : Env (Term (Option Bool))

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

Equations

• s.strInRegex? re = Cvc.Untyped.Term.strInRegex? s re

def Cvc.Typed.Term.strReplaceAll? [Ω] (s pat repl : Term (Option String)) : Env (Term (Option String))

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

Equations

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

def Cvc.Typed.Term.strRev? [Ω] (s : Term (Option String)) : Env (Term (Option String))

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

Equations

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

def Cvc.Typed.Term.strIndexofRe? [Ω] (s : Term (Option String)) (re : Term (Option Regex)) (start : Term (Option Int)) : Env (Term (Option Int))

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

Equations

• s.strIndexofRe? re start = Cvc.Untyped.Term.strIndexofRe? s re start

def Cvc.Typed.Term.strConcat? [Ω] (lft rgt : Term (Option String)) : Env (Term (Option String))

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

Equations

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

def Cvc.Typed.Term.strToUpper? [Ω] (s : Term (Option String)) : Env (Term (Option String))

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

Equations

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

def Cvc.Typed.Term.strLt? [Ω] (lft rgt : Term (Option String)) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.strFromCode? [Ω] (code : Term (Option Int)) : Env (Term (Option String))

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

Equations

• code.strFromCode? = Cvc.Untyped.Term.strFromCode? code

def Cvc.Typed.Term.strIndexof? [Ω] (s sub : Term (Option String)) (start : Term (Option Int)) : Env (Term (Option Int))

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

Equations

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

def Cvc.Typed.Term.strToInt? [Ω] (s : Term (Option String)) : Env (Term (Option Int))

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

Equations

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

def Cvc.Typed.Term.strLe? [Ω] (lft rgt : Term (Option String)) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.strPrefix? [Ω] (pre s : Term (Option String)) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.strLength? [Ω] (s : Term (Option String)) : Env (Term (Option Int))

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

Equations

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

def Cvc.Typed.Term.strToCode? [Ω] (s : Term (Option String)) : Env (Term (Option Int))

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

Equations

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

def Cvc.Typed.Term.strReplace? [Ω] (s pat repl : Term (Option String)) : Env (Term (Option String))

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

Equations

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

def Cvc.Typed.Term.strFromInt? [Ω] (arg : Term (Option Int)) : Env (Term (Option String))

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

Equations

• arg.strFromInt? = Cvc.Untyped.Term.strFromInt? arg

def Cvc.Typed.Term.strUpdate? [Ω] (s : Term (Option String)) (idx : Term (Option Int)) (repl : Term (Option String)) : Env (Term (Option String))

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

Equations

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

def Cvc.Typed.Term.strReplaceReAll? [Ω] (s : Term (Option String)) (re : Term (Option Regex)) (repl : Term (Option String)) : Env (Term (Option String))

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

Equations

• s.strReplaceReAll? re repl = Cvc.Untyped.Term.strReplaceReAll? s re repl

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

strConcat? over two or more terms.

Equations

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

def Cvc.Typed.Term.strSuffix? [Ω] (suf s : Term (Option String)) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.strIsDigit? [Ω] (s : Term (Option String)) : Env (Term (Option Bool))

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

Equations

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