Documentation

Init.Coe

class Coe (α : Sort u) (β : Sort v) :

Sort (max (max 1 u) v)

coe : α → β

Instances

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

subtypeCoe

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 v → Sort (max 1 v)

coe : β

Instances

class CoeT (α : Sort u) :

α → Sort v → Sort (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

boolToSort

def coeNotation :

Lean.ParserDescr

Equations

coeNotation = Lean.ParserDescr.node `coeNotation 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↑") (Lean.ParserDescr.cat `term 1024))

instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [inst : Coe β δ] [inst : CoeTC α β] :

CoeTC α δ

Equations

coeTrans = { coe := fun a => Coe.coe (CoeTC.coe a) }

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 β δ] :

Equations

coeOfHeafOfTCOfTail = { coe := fun a => CoeTail.coe (CoeTC.coe (CoeHead.coe a)) }

instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} [inst : CoeHead α β] [inst : CoeTC β δ] :

Equations

coeOfHeadOfTC = { coe := fun a => CoeTC.coe (CoeHead.coe a) }

instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} [inst : CoeTail β δ] [inst : CoeTC α β] :

Equations

coeOfTCOfTail = { coe := fun a => CoeTail.coe (CoeTC.coe a) }

instance coeOfHead {α : Sort u} {β : Sort v} [inst : CoeHead α β] :

Equations

coeOfHead = { coe := fun a => CoeHead.coe a }

instance coeOfTail {α : Sort u} {β : Sort v} [inst : CoeTail α β] :

Equations

coeOfTail = { coe := fun a => CoeTail.coe a }

instance coeOfTC {α : Sort u} {β : Sort v} [inst : CoeTC α β] :

Equations

coeOfTC = { coe := fun a => CoeTC.coe a }

instance coeOfHTCT {α : Sort u} {β : Sort v} [inst : CoeHTCT α β] (a : α) :

CoeT α a β

Equations

coeOfHTCT a = { coe := CoeHTCT.coe a }

instance coeOfDep {α : Sort u} {β : Sort v} (a : α) [inst : CoeDep α a β] :

CoeT α a β

Equations

coeOfDep a = { coe := CoeDep.coe a }

instance coeId {α : Sort u} (a : α) :

CoeT α a α

Equations

coeId a = { coe := a }

instance coeSortToCoeTail {α : Sort u_1} {β : Sort u_2} [inst : CoeSort α β] :

Equations

coeSortToCoeTail = { coe := CoeSort.coe }

@[inline]

instance boolToProp :

Equations

boolToProp = { coe := fun b => b = true }

instance boolToSort :

CoeSort Bool Prop

Equations

boolToSort = { coe := fun b => b = true }

instance decPropToBool (p : Prop) [inst : Decidable p] :

CoeDep Prop p Bool

Equations

decPropToBool p = { coe := decide p }

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 u → Type v} {n : Type u → Type w} {α : Type u} {β : Type u} [inst : MonadLiftT m n] [inst : (a : α) → CoeT α a β] [inst : Monad n] (x : m α) :

n β

Equations

Lean.Internal.liftCoeM x = do let a ← liftM x pure a

@[inline]

def Lean.Internal.coeM {m : Type u → Type v} {α : Type u} {β : Type u} [inst : (a : α) → CoeT α a β] [inst : Monad m] (x : m α) :

m β

Equations

Lean.Internal.coeM x = do let a ← x pure a

instance instCoeDep {α : Sort u_1} {β : α → Sort u_2} [inst : CoeFun α β] (a : α) :

CoeDep α a (β a)

Equations

instCoeDep a = { coe := a }

instance instCoeTail {α : Sort u_1} {β : Sort u_2} [inst : CoeFun α fun x => β] :

Equations

instCoeTail = { coe := fun a => a }

instance instCoeTail_1 {α : Sort u_1} {β : Sort u_2} [inst : CoeSort α β] :

Equations

instCoeTail_1 = { coe := fun a => a }