Documentation

Iris.Std.TC

source
class inductive Iris.Std.TCFalse :
Type

Type class version of False, i.e. a type class with no instances.

    Instances
      source
      class inductive Iris.Std.TCTrue :
      Type

      Type class version of True, i.e. a type class with a trivial instance without arguments.

      Instances
        source
        instance Iris.Std.instTCTrue :
        TCTrue
        Equations
        source
        class inductive Iris.Std.TCOr (T : Sort u_1) (U : Sort u_2) :
        Sort (max (max 1 u_1) u_2)

        Type class version of Or, i.e. a type class for which an instance exists if an instance of any of the listed type classes is present.

        Instances
          source
          instance Iris.Std.instTCOr {T : Sort u_1} {U : Sort u_2} [t : T] :
          TCOr T U
          Equations
          source
          instance Iris.Std.instTCOr_1 {U : Sort u_1} {T : Sort u_2} [u : U] :
          TCOr T U
          Equations
          source
          class inductive Iris.Std.TCIte :
          Bool → Sort u → Sort v → Type (max u v)

          Type class version of Ite, i.e. a type class for which an instance exists if the boolean condition is true and an instance of T is present or the condition is false and an instance of U is present.

          Note that type class instance search requires the condition to be fully reduced.

          Instances
            source
            instance Iris.Std.instTCIteTrue {T : Sort u_1} {U : Sort u_2} [t : T] :
            TCIte true T U
            Equations
            source
            instance Iris.Std.instTCIteFalse {U : Sort u_1} {T : Sort u_2} [u : U] :
            TCIte false T U
            Equations