- coe : α → β
Instances
- Lean.Server.FileWorker.instCoeErrorElabTaskError
- Lean.Server.RequestError.instCoeErrorRequestError
- Lean.JsonRpc.instCoeResponseErrorMessage
- Lean.Parser.instCoeParserParserAliasValue
- Lean.JsonRpc.instCoeJsonNumberRequestID
- Lean.MessageData.instCoeFormatMessageData
- Lean.JsonRpc.instCoeRequestMessage
- Lean.MessageData.instCoeOptionExprMessageData
- Lean.instCoeSyntaxDataValue
- Lean.MessageData.instCoeSyntaxMessageData
- Lean.instCoeExprExprStructEq
- Lean.MessageData.instCoeExprMessageData
- IO.AsyncList.instCoeListAsyncList
- Lean.MessageData.instCoeListExprMessageData
- Lean.MessageData.instCoeListMessageData
- Array.instCoeSubarrayArray
- Lean.Json.instCoeRBNodeStringJsonStructured
- Lean.PrettyPrinter.Parenthesizer.instCoeParenthesizerParenthesizerAliasValue
- Lean.PrettyPrinter.Formatter.instCoeFormatterFormatterAliasValue
- Lean.JsonRpc.instCoeNotificationMessage
- Lean.instCoeNatDataValue
- Lean.Json.instCoeNatJson
- Lean.JsonNumber.instCoeNatJsonNumber
- instCoeNatInt
- Lean.Json.instCoeArrayJsonStructured
- Lean.Syntax.instCoeArraySyntaxSepArray
- Lean.MessageData.instCoeArrayExprMessageData
- Lean.MessageData.instCoeMVarIdMessageData
- boolToProp
- Lean.instCoeBoolDataValue
- Lean.Json.instCoeBoolJson
- Lean.JsonRpc.instCoeResponseMessage
- Lean.instCoeNameDataValue
- Lean.MessageData.instCoeNameMessageData
- instCoeStringError
- Lean.instCoeStringDataValue
- Lean.Json.instCoeStringJson
- Lean.Parser.instCoeStringParser
- Std.Format.instCoeStringFormat
- Lean.MessageData.instCoeStringMessageData
- Lean.JsonRpc.instCoeStringRequestID
- System.instCoeStringFilePath
- Lean.instCoeStringName
- Fin.coeToNat
- Lean.MessageData.instCoeLevelMessageData
- Lean.Rat.instCoeIntRat
- Lean.instCoeIntDataValue
- Lean.Json.instCoeIntJson
- Lean.JsonNumber.instCoeIntJsonNumber
- Lean.Parser.instCoeForAllParserParserAliasValue
- Lean.PrettyPrinter.Parenthesizer.instCoeForAllParenthesizerParenthesizerAliasValue
- Lean.PrettyPrinter.Formatter.instCoeForAllFormatterFormatterAliasValue
- Lean.Parser.instCoeForAllParserParserAliasValue_1
- Lean.PrettyPrinter.Parenthesizer.instCoeForAllParenthesizerParenthesizerAliasValue_1
- Lean.PrettyPrinter.Formatter.instCoeForAllFormatterFormatterAliasValue_1
- coe : α → β
Instances
- coe : α → β
- coe : α → β
- coe : β
Instances
- coe : α → β
Instances
Equations
- coeNotation = Lean.ParserDescr.node `coeNotation 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↑") (Lean.ParserDescr.cat `term 1024))
instance
coeOfHeafOfTCOfTail
{α : Sort u}
{β : Sort v}
{δ : Sort w}
{γ : Sort w'}
[inst : CoeHead α β]
[inst : CoeTail δ γ]
[inst : CoeTC β δ]
:
CoeHTCT α γ
Equations
- coeOfHeafOfTCOfTail = { coe := fun a => CoeTail.coe (CoeTC.coe (CoeHead.coe a)) }
instance
coeOfHeadOfTC
{α : Sort u}
{β : Sort v}
{δ : Sort w}
[inst : CoeHead α β]
[inst : CoeTC β δ]
:
CoeHTCT α δ
Equations
- coeOfHeadOfTC = { coe := fun a => CoeTC.coe (CoeHead.coe a) }
instance
coeOfTCOfTail
{α : Sort u}
{β : Sort v}
{δ : Sort w}
[inst : CoeTail β δ]
[inst : CoeTC α β]
:
CoeHTCT α δ
Equations
- coeOfTCOfTail = { coe := fun a => CoeTail.coe (CoeTC.coe a) }
@[inline]
Equations
- boolToProp = { coe := fun b => b = true }
Equations
- decPropToBool p = { coe := decide p }
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}
{β : outParam (α → Sort u_2)}
[inst : CoeFun α β]
(a : α)
:
CoeDep α a (β a)
Equations
- instCoeDep a = { coe := a }
Equations
- instCoeTail = { coe := fun a => a }