Structures · Lean core
SizeOf
SizeOf is a typeclass automatically derived for every inductive type,
which equips the type with a "size" function to Nat.
The default instance defines each constructor to be 1 plus the sum of the
sizes of all the constructor fields.
This is used for proofs by well-founded induction, since every field of the
constructor has a smaller size than the constructor itself,
and in many cases this will suffice to do the proof that a recursive function
is only called on smaller values.
If the default proof strategy fails, it is recommended to supply a custom
size measure using the termination_by argument on the function definition.
- Defined in
- Init.SizeOf
- Shape
- One type argument · adds sizeOf
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every SizeOf is also a
Concrete types that are instances100
- Int
- Nat
- Real
- Rat
- Bool
- Complex
- BitVec
- ContinuousLinearMap
- Polynomial
- BoundedContinuousFunction
- CategoryTheory.Functor
- RatFunc
- UInt64
- UInt8
- UInt16
- UInt32
- Unitization
- IsDedekindDomain.HeightOneSpectrum.adicCompletion
- WithConv
- WithVal
- HahnSeries
- NumberField.InfinitePlace.Completion
- NonemptyInterval
- LocallyConstant
- USize
- QuadraticAlgebra
- Units
- WithLp
- MeasureTheory.SimpleFunc
- MonoidAlgebra
- AddMonoidAlgebra
- Finsupp
- DoubleCentralizer
- Zsqrtd
- CategoryTheory.Discrete
- ZNum
- SkewMonoidAlgebra
- ModuleCat
- AddUnits
- ContinuousMapZero
- CategoryTheory.Grp
- QuaternionAlgebra
- ZeroAtInftyContinuousMap
- Int32
- Int8
- Int64
- ContinuousAlternatingMap
- Int16
- DFinsupp
- WittVector
- TopologicalSpace.NonemptyCompacts
- ContinuousLinearMapWOT
- HomologicalComplex
- Action
- UpperSet
- LowerSet
- CategoryTheory.Mon
- ISize
- FundamentalGroupoid
- AlgebraicGeometry.Scheme
- Representation.IntertwiningMap
- AlgEquiv
- LieSubalgebra
- LieSubmodule
- Num
- RingQuot
- AddChar
- AddCommGrpCat
- MulActionHom
- AlgebraicGeometry.Scheme.IdealSheafData
- CategoryTheory.ObjectProperty.FullSubcategory
- CentroidHom
- PrimeSpectrum
- SimpleGraph
- TopCat
- SignType
- ContinuousMultilinearMap
- CompactlySupportedContinuousMap
- MeasureTheory.Measure
- TopologicalSpace.Opens
- SchwartzMap
- CategoryTheory.MonoidalOpposite
- MeasureTheory.VectorMeasure
- TopologicalSpace.Compacts
- LinearEquiv
- Digraph
- AlternatingMap
- IncidenceAlgebra
- AddMonoidHom
- Char
- Rep
- CategoryTheory.Quotient
- ContinuousAffineMap
- CommGrpCat
- PolynomialModule
- GrpCat
- AddSubgroup
- AddGrpCat
- SheafOfModules
- OneHom
How is a type an instance?
Loading the hierarchy index…