Documentation

Cvc.Typed.Theory.Nullable.FiniteField

Finite fields 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 field's size is an index on the sort, not an operator index, so every operator here lifts.

source
def Cvc.Typed.Term.ffNeg? [Ω] {k : Nat} (ff : Term (Option (FiniteField k))) :
Env (Term (Option (FiniteField k)))

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

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

    ffAdd? over two or more terms.

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

      ffBitsum? over two or more terms.

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

        ffMul? over two or more terms.

        Equations
        Instances For
          source
          def Cvc.Typed.Term.ffBitsum? [Ω] {k : Nat} (lft rgt : Term (Option (FiniteField k))) :
          Env (Term (Option (FiniteField k)))

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

          Equations
          Instances For
            source
            def Cvc.Typed.Term.ffMul? [Ω] {k : Nat} (lft rgt : Term (Option (FiniteField k))) :
            Env (Term (Option (FiniteField k)))

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

            Equations
            Instances For
              source
              def Cvc.Typed.Term.ffAdd? [Ω] {k : Nat} (lft rgt : Term (Option (FiniteField k))) :
              Env (Term (Option (FiniteField k)))

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

              Equations
              Instances For