Documentation

Init.Coe

class CoeTC (α : Sort u) (β : Sort v) :
Sort (max (max 1 u) v)
  • coe : αβ

Auxiliary class that contains the transitive closure of Coe.

Instances
class CoeHead (α : Sort u) (β : Sort v) :
Sort (max (max 1 u) v)
  • coe : αβ
Instances
class CoeTail (α : Sort u) (β : Sort v) :
Sort (max (max 1 u) v)
  • coe : αβ
Instances
class CoeHTCT (α : Sort u) (β : Sort v) :
Sort (max (max 1 u) v)
  • coe : αβ

Auxiliary class that contains CoeHead + CoeTC + CoeTail.

Instances
class CoeDep (α : Sort u) :
αSort vSort (max 1 v)
  • coe : β
Instances
class CoeT (α : Sort u) :
αSort vSort (max 1 v)
  • coe : β
Instances
class CoeFun (α : Sort u) (γ : outParam (αSort v)) :
Sort (max (max 1 u) v)
  • coe : (a : α) → γ a
Instances
class CoeSort (α : Sort u) (β : outParam (Sort v)) :
Sort (max (max 1 u) v)
  • coe : αβ
Instances
instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [inst : Coe β δ] [inst : CoeTC α β] :
CoeTC α δ
Equations
instance coeBase {α : Sort u} {β : Sort v} [inst : Coe α β] :
CoeTC α β
Equations
  • coeBase = { coe := fun a => Coe.coe a }
instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} [inst : CoeHead α β] [inst : CoeTail δ γ] [inst : CoeTC β δ] :
CoeHTCT α γ
Equations
instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} [inst : CoeHead α β] [inst : CoeTC β δ] :
CoeHTCT α δ
Equations
instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} [inst : CoeTail β δ] [inst : CoeTC α β] :
CoeHTCT α δ
Equations
instance coeOfHead {α : Sort u} {β : Sort v} [inst : CoeHead α β] :
CoeHTCT α β
Equations
instance coeOfTail {α : Sort u} {β : Sort v} [inst : CoeTail α β] :
CoeHTCT α β
Equations
instance coeOfTC {α : Sort u} {β : Sort v} [inst : CoeTC α β] :
CoeHTCT α β
Equations
instance coeOfHTCT {α : Sort u} {β : Sort v} [inst : CoeHTCT α β] (a : α) :
CoeT α a β
Equations
instance coeOfDep {α : Sort u} {β : Sort v} (a : α) [inst : CoeDep α a β] :
CoeT α a β
Equations
instance coeId {α : Sort u} (a : α) :
CoeT α a α
Equations
instance coeSortToCoeTail {α : Sort u_1} {β : Sort u_2} [inst : CoeSort α β] :
CoeTail α β
Equations
  • coeSortToCoeTail = { coe := CoeSort.coe }
@[inline]
instance boolToProp :
Coe Bool Prop
Equations
instance boolToSort :
Equations
instance decPropToBool (p : Prop) [inst : Decidable p] :
CoeDep Prop p Bool
Equations
instance optionCoe {α : Type u} :
CoeTail α (Option α)
Equations
  • optionCoe = { coe := some }
instance subtypeCoe {α : Sort u} {p : αProp} :
CoeHead { x // p x } α
Equations
  • subtypeCoe = { coe := fun v => v.val }
@[inline]
def Lean.Internal.liftCoeM {m : Type uType v} {n : Type uType w} {α : Type u} {β : Type u} [inst : MonadLiftT m n] [inst : (a : α) → CoeT α a β] [inst : Monad n] (x : m α) :
n β
Equations
@[inline]
def Lean.Internal.coeM {m : Type uType v} {α : Type u} {β : Type u} [inst : (a : α) → CoeT α a β] [inst : Monad m] (x : m α) :
m β
Equations
instance instCoeDep {α : Sort u_1} {β : αSort u_2} [inst : CoeFun α β] (a : α) :
CoeDep α a (β a)
Equations
instance instCoeTail {α : Sort u_1} {β : Sort u_2} [inst : CoeFun α fun x => β] :
CoeTail α β
Equations
  • instCoeTail = { coe := fun a => a }
instance instCoeTail_1 {α : Sort u_1} {β : Sort u_2} [inst : CoeSort α β] :
CoeTail α β
Equations
  • instCoeTail_1 = { coe := fun a => a }