Structures · Lean core
Coe
Coe α β is the typeclass for coercions from α to β. It can be transitively
chained with other Coe instances, and coercion is automatically used when
x has type α but it is used in a context where β is expected.
You can use the ↑x operator to explicitly trigger coercion.
- Defined in
- Init.Coe
- Shape
- 2 explicit arguments · adds coe
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every Coe is also a
Concrete types that are instances100
- Int
- Nat
- Real
- Rat
- Bool
- Complex
- NNReal
- ContinuousLinearMap
- ZMod
- ENNReal
- Polynomial
- Padic
- RatFunc
- WithVal
- NonemptyInterval
- LocallyConstant
- ENat
- PadicInt
- PNat
- GaussianInt
- FreeRing
- ArithmeticFunction
- Matrix.SpecialLinearGroup
- LieSubalgebra
- AddCommGrpCat
- PrimeSpectrum
- Ordinal.ToType
- SchwartzMap
- LinearEquiv
- AlternatingMap
- AddMonoidHom
- ContinuousAffineMap
- CommGrpCat
- GrpCat
- AddGrpCat
- String
- AlgHom
- PrincipalSeg
- MvPolynomial
- LieIdeal
- CommMonCat
- AddCommMonCat
- BialgHom
- PowerSeries
- Derivation
- LieDerivation
- LeftInvariantDerivation
- Complex.UnitClosedDisc
- CategoryTheory.Monad
- Pell.Solution₁
- CategoryTheory.Comonad
- PrimeMultiset
- List.Vector
- MonoidWithZeroHom
- MaximalSpectrum
- CochainComplex.HomComplex.Cocycle
- ContinuousLinearEquiv
- Complex.UnitDisc
- ClosedSubmodule
- AffineEquiv
- AffineIsometryEquiv
- RelEmbedding
- MeasureTheory.FiniteMeasure
- InitialSeg
- ZFSet
- DyckWord
- StarAlgHom
- ContinuousAlgHom
- Lean.Name
- PSet
- Std.TreeMap.Raw
- OpenNormalAddSubgroup
- OpenNormalSubgroup
- ByteArray
- FiniteIndexNormalSubgroup
- FiniteIndexNormalAddSubgroup
- Subarray
- SNum
- ClosedSubgroup
- ClosedAddSubgroup
- Std.Time.Week.Offset
- Std.Time.Second.Offset
- Std.Time.Minute.Offset
- Std.Time.Nanosecond.Offset
- FiniteGaloisIntermediateField
- Std.Time.Day.Offset
- Std.Time.Hour.Offset
- Lean.JsonNumber
- MeasureTheory.ProbabilityMeasure
- FirstOrder.Language.ElementarySubstructure
- Lean.Level
- MLList
- MulAlgebraNorm
- System.FilePath
- Std.Async.ContextAsync
- Stream'.Seq1
- Lean.Expr
- Lean.MVarId
- Lean.Syntax
- Lean.TSyntax
How is a type an instance?
Loading the hierarchy index…