Documentation

Init.Control.Id

def Id (type : Type u) :
Equations
Instances For
    @[always_inline]
    Equations
    Equations
    Instances For
      @[inline]
      def Id.run {α : Type u_1} (x : Id α) :
      α
      Equations
      Instances For
        instance Id.instOfNatId {α : Type u_1} {n : Nat} [OfNat α n] :
        OfNat (Id α) n
        Equations