Documentation

Init.Control.Id

source
noncomputable def Id (type : Type u) :
Type u
Equations
  • Id type = type
source
instance Id.instMonadId :
Monad Id
Equations
source
def Id.hasBind :
Bind Id
Equations
source
@[inline]
def Id.run {α : Type u_1} (x : Id α) :
α
Equations
source
instance Id.instOfNatId {α : Type u_1} {n : Nat} [inst : OfNat α n] :
OfNat (Id α) n
Equations