Documentation

Cvc.Typed.Theory.Nullable.Defs

Nullable constructors, typed #

cvc5's Nullable is denoted by Lean's Option, so a nullable term is a Term (Option α) and the element it carries is a Term α. The index is what tells mkNull which sort to build, where the sort-erased version takes the element sort.

Constructors #

source
def Cvc.Typed.Term.mkNull' [Ω] (α : Type) [ToTyp α] :
Env (Term (Option α))

The null value at Option α.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Cvc.Typed.Term.mkNull [Ω] {α : Type} [ToTyp α] :
    Env (Term (Option α))

    The null value at Option α.

    Equations
    Instances For
      source
      def Cvc.Typed.Term.nullableSome [Ω] {α : Type} :
      Term α → Env (Term (Option α))

      The nullable value holding elem, nullable.some elem.

      Equations
      Instances For
        source
        def Cvc.Typed.Term.nullableVal [Ω] {α : Type} :
        Term (Option α) → Env (Term α)

        The element the nullable term nullable holds, nullable.val.

        Equations
        Instances For
          source
          def Cvc.Typed.Term.nullableIsNull [Ω] {α : Type} :
          Term (Option α) → Env (Term Bool)

          Whether the nullable term nullable is null, nullable.is_null.

          Equations
          Instances For
            source
            def Cvc.Typed.Term.nullableIsSome [Ω] {α : Type} :
            Term (Option α) → Env (Term Bool)

            Whether the nullable term nullable holds an element, nullable.is_some.

            Equations
            Instances For

              Values #

              source
              def Cvc.Typed.Term.isNullableValue [Ω] {α : Type} :
              Term (Option α) → Env Bool

              Whether a term is built by a nullable constructor, nullable.null or nullable.some.

              That is what getNullableElem? needs. Being nullable-sorted is not enough: a declared constant of nullable sort is built by neither.

              Equations
              Instances For
                source
                def Cvc.Typed.Term.getNullableElem? [Ω] {α : Type} :
                Term (Option α) → Env (Option (Term α))

                The element a nullable term denotes, or none if it denotes the null value.

                Equations
                Instances For
                  source
                  def Cvc.Typed.Term.mkNullableValue {α : Type} [Ω] [ToTyp α] [ValueToTerm α] (value : Option α) :
                  Env (Term (Option α))

                  The nullable term denoting an optional value.

                  Equations
                  Instances For
                    source
                    def Cvc.Typed.Term.getNullableValue {α : Type} [Ω] [TermToValue α] :
                    Term (Option α) → Env (Option α)

                    The optional value a nullable term denotes.

                    Equations
                    Instances For
                      source
                      @[instance_reducible]
                      instance Cvc.Typed.Term.instValueToTermOption {α : Type} [ToTyp α] [ValueToTerm α] :
                      ValueToTerm (Option α)
                      Equations
                      source
                      @[instance_reducible]
                      instance Cvc.Typed.Term.instTermToValueOption {α : Type} [TermToValue α] :
                      TermToValue (Option α)
                      Equations
                      source
                      def Cvc.Typed.Term.nullableCases? {α : Type} [Ω] (t : Term (Option α)) :
                      Env (Option (Option (Term α)))

                      A nullable literal's case: some none for null, some (some x) for some x.

                      none if the term is not a literal, such as a declared constant or an ite.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For