Documentation

Cvc.Srt.SrtBij

Relates Srt-s to Type-s #

Main class Srt.Bij (α : Type) associates srt : Srt to α. It guarantees this association works both ways by asking for a proof that α = srt.toType.

source
class Cvc.Srt.Bij (α : Type) :
Type

Denotes a "bijection" from the α type itself (not its values) to Srt.

"Bijection" here means that when A : SrtBij α, then A.srt.toType = α as guaranteed by valid.

  • srt : Srt

    Srt version of α.

  • h_bij : α = (srt α).toType

    Turning srt into a Type results in α.

Instances
    source
    @[reducible, inline]
    abbrev Cvc.getSrt (α : Type) [I : Srt.Bij α] :
    Srt

    Retrieves the Srt corresponding to a Type.

    Equations
    Instances For
      source
      instance Cvc.Srt.toBijType (srt : Srt) :
      Srt.Bij srt.toType
      Equations
      source
      @[reducible, inline]
      abbrev Cvc.Srt.ofType (α : Type) [I : Srt.Bij α] :
      Srt

      Retrieves the Srt corresponding to a Type.

      Equations
      Instances For
        source
        @[simp]
        theorem Cvc.Srt.toType_ofType (α : Type) [I : Srt.Bij α] :
        (ofType α).toType = α
        source
        @[simp]
        theorem Cvc.Srt.ofType_toType (srt : Srt) :
        ofType srt.toType = srt

        Instances for simple types #

        source
        instance Cvc.Srt.Bij.instUnit :
        Srt.Bij Unit
        Equations
        source
        instance Cvc.Srt.Bij.instBool :
        Srt.Bij Bool
        Equations
        source
        instance Cvc.Srt.Bij.instInt :
        Srt.Bij Int
        Equations
        source
        instance Cvc.Srt.Bij.instRat :
        Srt.Bij Rat
        Equations
        source
        instance Cvc.Srt.Bij.instString :
        Srt.Bij String
        Equations
        source
        instance Cvc.Srt.Bij.instRoundingMode :
        Srt.Bij RoundingMode
        Equations
        source
        instance Cvc.Srt.Bij.instRegex :
        Srt.Bij Cvc.Regex
        Equations

        Instances for non-Srt-parameterized types #

        source
        instance Cvc.Srt.Bij.instAnyFloat {exp sig : UInt32} :
        Srt.Bij (Cvc.AnyFloat exp sig)
        Equations
        source
        instance Cvc.Srt.Bij.instAbstract {k : Kind} :
        Srt.Bij (Cvc.Abstract k)
        Equations
        source
        instance Cvc.Srt.Bij.instFiniteField {n : Nat} :
        Srt.Bij (FiniteField n)
        Equations
        source
        instance Cvc.Srt.Bij.instBitVec {size : Nat} :
        Srt.Bij (BitVec size)
        Equations
        source
        instance Cvc.Srt.Bij.instUninterpreted {name : String} :
        Srt.Bij (Uninterpreted name)
        Equations

        Instances composite types #

        source
        instance Cvc.Srt.Bij.instArray {α : Type} [A : Srt.Bij α] :
        Srt.Bij (Array α)
        Equations
        source
        instance Cvc.Srt.Bij.instFunction {α β : Type} [A : Srt.Bij α] [B : Srt.Bij β] :
        Srt.Bij (α → β)
        Equations
        source
        instance Cvc.Srt.Bij.instProd {α β : Type} [A : Srt.Bij α] [B : Srt.Bij β] :
        Srt.Bij (α × β)
        Equations
        source
        instance Cvc.Srt.Bij.instTMap {α β : Type} [A : Srt.Bij α] [B : Srt.Bij β] :
        Srt.Bij (Cvc.TMap α β)
        Equations
        source
        instance Cvc.Srt.Bij.instBag {α : Type} [A : Srt.Bij α] :
        Srt.Bij (Cvc.Bag α)
        Equations
        source
        instance Cvc.Srt.Bij.instSet {α : Type} [A : Srt.Bij α] :
        Srt.Bij (Cvc.Set α)
        Equations

        Refinement of Srt.Bij to arithmetic sorts #

        source
        @[reducible, inline]
        abbrev Cvc.is_arith (α : Type) [Srt.Bij α] :
        Prop

        Proof that the sort associated to α is arithmetic.

        Equations
        Instances For
          source
          instance Cvc.instDecidableIs_arith {α : Type} [Srt.Bij α] :
          Decidable (Cvc.is_arith α)
          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[simp]
          theorem Cvc.is_arith_def (α : Type) [inst : Srt.Bij α] :
          Cvc.is_arith α → α = Int ∨ α = Rat
          source
          def Cvc.is_arith_srt_def (α : Type) [inst : Srt.Bij α] :
          Cvc.is_arith α → Srt.Bij.srt α = Srt.int ∨ Srt.Bij.srt α = Srt.real
          Equations
          • ⋯ = ⋯
          Instances For
            source
            class Cvc.Srt.Bij.Arith (α : Type) extends Cvc.Srt.Bij α :
            Type

            Extends Srt.Bij with a proof that α's Srt is arithmetic.

            Instances

              Instances for Int and Rat (Real) #

              source
              instance Cvc.Srt.Bij.Arith.instInt :
              Bij.Arith Int
              Equations
              source
              instance Cvc.Srt.Bij.Arith.instRat :
              Bij.Arith Rat
              Equations
              source
              theorem Cvc.Srt.Bij.Arith.int_or_rat (α : Type) [inst : Bij.Arith α] :
              α = Int ∨ α = Rat
              source
              def Cvc.Srt.Bij.Arith.int_or_rat' (α : Type) [inst : Bij.Arith α] :
              srt α = int ∨ srt α = real
              Equations
              • ⋯ = ⋯
              Instances For
                source
                def Cvc.Srt.Bij.Arith.inspect' {β : Prop} (α : Type) [inst : Bij.Arith α] (fInt : α = Int → β) (fRat : α = Rat → β) :
                β
                Equations
                • ⋯ = ⋯
                Instances For
                  source
                  def Cvc.Srt.Bij.Arith.inspect {α : Type} {β : Sort u} [inst : Bij.Arith α] (fInt : srt α = int → β) (fRat : srt α = real → β) :
                  β
                  Equations
                  Instances For