Documentation

Cvc.Typed.Theory.Nullable.Regex

Regular expressions 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 regex term becomes nullable. The indexed reLoop and reRepeat have no lifted form, and the string-matching operators live in the string theory, so strInRegex? is generated there.

source
def Cvc.Typed.Term.reInter? [Ω] (lft rgt : Term (Option Regex)) :
Env (Term (Option Regex))

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

Equations
Instances For
    source
    def Cvc.Typed.Term.reOpt? [Ω] (re : Term (Option Regex)) :
    Env (Term (Option Regex))

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

    Equations
    Instances For
      source
      def Cvc.Typed.Term.reComplement? [Ω] (re : Term (Option Regex)) :
      Env (Term (Option Regex))

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

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

        reUnion? over two or more terms.

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

          reConcat? over two or more terms.

          Equations
          Instances For
            source
            def Cvc.Typed.Term.reDiff? [Ω] (lft rgt : Term (Option Regex)) :
            Env (Term (Option Regex))

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

            Equations
            Instances For
              source
              def Cvc.Typed.Term.reConcat? [Ω] (lft rgt : Term (Option Regex)) :
              Env (Term (Option Regex))

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

              Equations
              Instances For
                source
                def Cvc.Typed.Term.reUnion? [Ω] (lft rgt : Term (Option Regex)) :
                Env (Term (Option Regex))

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

                Equations
                Instances For
                  source
                  def Cvc.Typed.Term.reRange? [Ω] (lo hi : Term (Option String)) :
                  Env (Term (Option Regex))

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

                  Equations
                  Instances For
                    source
                    def Cvc.Typed.Term.reStar? [Ω] (re : Term (Option Regex)) :
                    Env (Term (Option Regex))

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

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

                      reInter? over two or more terms.

                      Equations
                      Instances For
                        source
                        def Cvc.Typed.Term.rePlus? [Ω] (re : Term (Option Regex)) :
                        Env (Term (Option Regex))

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

                        Equations
                        Instances For