General documentation

index
foundational types

Library

Init (file)
Control (file)
Basic
EState
Except
ExceptCps
Id
Lawful
Option
Reader
State
StateCps
StateRef
Data (file)
Array (file)
Basic
BasicAux
BinSearch
DecidableEq
InsertionSort
Mem
QSort
Subarray
ByteArray (file)
Basic
Char (file)
Basic
Fin (file)
Basic
Log2
FloatArray (file)
Basic
Format (file)
Basic
Instances
Macro
Syntax
Int (file)
Basic
List (file)
Basic
BasicAux
Control
Nat (file)
Basic
Bitwise
Control
Div
Gcd
Linear
Log2
Power2
SOM
Option (file)
Basic
BasicAux
Instances
String (file)
Basic
Extra
ToString (file)
Basic
Macro
UInt (file)
Basic
Log2
AC
Basic
Channel
Float
Hashable
OfScientific
Ord
Prod
Queue
Random
Range
Repr
Stream
System (file)
FilePath
IO
IOError
Mutex
Platform
Promise
ST
Uri
Classical
Coe
Conv
Core
Dynamic
Hints
Meta
Notation
NotationExtra
Prelude
ShareCommon
SimpLemmas
SizeOf
SizeOfLemmas
Tactics
Util
WF
WFTactics
Lean (file)
Compiler (file)
IR (file)
Basic
Borrow
Boxing
Checker
CompilerM
CtorLayout
ElimDeadBranches
ElimDeadVars
EmitC
EmitUtil
ExpandResetReuse
Format
FreeVars
LiveVars
NormIds
PushProj
RC
ResetReuse
SimpCase
Sorry
UnboxResult
LCNF (file)
Simp (file)
Basic
Config
ConstantFold
DefaultAlt
DiscrM
FunDeclInfo
InlineCandidate
InlineProj
JpCases
Main
SimpM
SimpValue
Used
AlphaEqv
AuxDeclCache
BaseTypes
Basic
Bind
CSE
Check
Closure
CompatibleTypes
CompilerM
ConfigOptions
DeclHash
DependsOn
ElimDead
ElimDeadBranches
FVarUtil
FixedParams
FloatLetIn
ForEachExpr
InferType
Internalize
JoinPoints
LCtx
LambdaLifting
Level
Main
MonadScope
MonoTypes
OtherDecl
PassManager
Passes
PhaseExt
PrettyPrinter
PullFunDecls
PullLetDecls
ReduceArity
ReduceJpArity
Renaming
ScopeM
SpecInfo
Specialize
Testing
ToDecl
ToExpr
ToLCNF
ToMono
Types
Util
AtMostOnce
BorrowedAnnotation
CSimpAttr
ClosedTermCache
ConstFolding
ExportAttr
ExternAttr
FFI
ImplementedByAttr
InitAttr
InlineAttrs
Main
NameMangling
NeverExtractAttr
NoncomputableAttr
Old
Options
Specialize
Data (file)
Json (file)
Basic
FromToJson
Parser
Printer
Stream
Lsp (file)
Basic
Capabilities
Client
CodeActions
Communication
Diagnostics
Extra
InitShutdown
Internal
Ipc
LanguageFeatures
TextSync
Utf16
Workspace
Xml (file)
Basic
Parser
AssocList
Format
FuzzyMatching
HashMap
HashSet
JsonRpc
KVMap
LBool
LOption
Name
NameMap
NameTrie
Occurrences
OpenDecl
Options
Parsec
PersistentArray
PersistentHashMap
PersistentHashSet
Position
PrefixTree
RBMap
RBTree
Rat
SMap
SSet
Trie
Elab (file)
Deriving (file)
BEq
Basic
DecEq
FromToJson
Hashable
Inhabited
Nonempty
Ord
Repr
SizeOf
TypeName
Util
InfoTree (file)
Main
Types
PreDefinition (file)
Structural (file)
BRecOn
Basic
Eqns
FindRecArg
IndPred
Main
Preprocess
SmartUnfolding
WF (file)
Eqns
Fix
Ite
Main
PackDomain
PackMutual
Rel
TerminationHint
Basic
Eqns
Main
MkInhabitant
Quotation (file)
Precheck
Util
Tactic (file)
Conv (file)
Basic
Change
Congr
Delta
Pattern
Rewrite
Simp
Unfold
Basic
BuiltinTactic
Cache
Calc
Config
Congr
Delta
ElabTerm
Generalize
Induction
Injection
Location
Match
Meta
Rewrite
Simp
Split
Unfold
App
Arg
Attributes
AutoBound
AuxDef
Binders
BindersUtil
BuiltinCommand
BuiltinNotation
BuiltinTerm
Calc
Command
ComputedFields
Config
DeclModifiers
DeclUtil
Declaration
DeclarationRange
DefView
Do
ElabRules
Eval
Exception
Extra
Frontend
GenInjective
Import
Inductive
InheritDoc
LetRec
Level
Macro
MacroArgUtil
MacroRules
Match
MatchAltView
Mixfix
MutualDef
Notation
Open
ParseImportsFast
PatternVar
Print
RecAppSyntax
SetOption
StructInst
Structure
Syntax
SyntheticMVars
Term
Util
Linter (file)
Basic
Builtin
Deprecated
MissingDocs
UnusedVariables
Util
Meta (file)
Match (file)
Basic
CaseArraySizes
CaseValues
Match
MatchEqs
MatchEqsExt
MatchPatternAttr
MatcherInfo
Value
Tactic (file)
AC (file)
Main
LinearArith (file)
Nat (file)
Basic
Simp
Solver
Basic
Main
Simp
Solver
Simp (file)
Main
Rewrite
SimpAll
SimpCongrTheorems
SimpTheorems
Types
Acyclic
Apply
Assert
Assumption
AuxLemma
Cases
Cleanup
Clear
Congr
Constructor
Contradiction
Delta
ElimInfo
FVarSubst
Generalize
Induction
Injection
Intro
Refl
Rename
Replace
Revert
Rewrite
Split
SplitIf
Subst
Unfold
UnifyEq
Util
ACLt
AbstractMVars
AbstractNestedProofs
AppBuilder
Basic
CasesOn
Check
Closure
Coe
CollectFVars
CollectMVars
CongrTheorems
Constructions
DecLevel
DiscrTree
DiscrTreeTypes
Eqns
Eval
ExprDefEq
ExprLens
ExprTraverse
ForEachExpr
FunInfo
GeneralizeTelescope
GeneralizeVars
GetConst
GlobalInstances
IndPredBelow
Inductive
InferType
Injective
Instances
KAbstract
KExprMap
LevelDefEq
MatchUtil
Offset
PPGoal
RecursorInfo
Reduce
ReduceEval
SizeOf
Structure
SynthInstance
Transform
TransparencyMode
UnificationHint
WHNF
Parser (file)
Attr
Basic
Command
Do
Extension
Extra
Level
Module
StrInterpolation
Syntax
Tactic
Term
Types
ParserCompiler (file)
Attribute
PrettyPrinter (file)
Delaborator (file)
Basic
Builtins
Options
SubExpr
TopDownAnalyze
Basic
Formatter
Parenthesizer
Server (file)
FileWorker (file)
RequestHandling
Utils
WidgetRequests
Rpc (file)
Basic
Deriving
RequestHandling
AsyncList
CodeActions
Completion
FileSource
GoTo
InfoUtils
References
Requests
Snapshots
Utils
Watchdog
Util (file)
CollectFVars
CollectLevelParams
CollectMVars
FindExpr
FindLevelMVar
FindMVar
FoldConsts
ForEachExpr
ForEachExprWhere
HasConstCache
InstantiateLevelParams
MonadBacktrack
MonadCache
OccursCheck
PPExt
Path
Paths
Profile
RecDepth
Recognizers
ReplaceExpr
ReplaceLevel
SCC
ShareCommon
Sorry
Trace
Widget (file)
Basic
Diff
InteractiveCode
InteractiveDiagnostic
InteractiveGoal
TaggedText
UserWidget
Attributes
AuxRecursor
Class
CoreM
Declaration
DeclarationRange
DocString
Environment
Eval
Exception
Expr
HeadIndex
Hygiene
ImportingFlag
InternalExceptionId
KeyedDeclsAttribute
LazyInitExtension
Level
LoadDynlib
LocalContext
Log
Message
MetavarContext
Modifiers
MonadEnv
ProjFns
ReducibilityAttrs
ResolveName
Runtime
ScopedEnvExtension
Structure
SubExpr
Syntax
ToExpr
Mathlib (file)
Algebra
Algebra
Subalgebra
Basic
Pointwise
Tower
Basic
Bilinear
Equiv
Hom
Operations
Pi
Prod
RestrictScalars
Tower
Unitization
BigOperators
Multiset
Basic
Lemmas
Associated
Basic
Fin
Finprod
Finsupp
Intervals
NatAntidiagonal
Option
Order
Pi
Ring
RingEquiv
Category
GroupCat
Abelian
Basic
Biproducts
Colimits
EpiMono
EquivalenceGroupAddGroup
FilteredColimits
Images
Injective
Limits
Preadditive
ZModuleEquivalence
Zero
ModuleCat
Monoidal
Basic
Abelian
Adjunctions
Basic
Biproducts
EpiMono
Images
Kernels
Limits
Products
Projective
Tannaka
Mon
FilteredColimits
MonCat
Basic
Limits
Ring
Adjunctions
Basic
Colimits
Constructions
FilteredColimits
Instances
Limits
GroupWithZeroCat
CharP
Algebra
Basic
CharAndCard
ExpChar
Invertible
LocalRing
MixedCharZero
Pi
Quotient
Subring
Two
CharZero
Defs
Infinite
Lemmas
Quotient
ContinuedFractions
Computation
Basic
CorrectnessTerminating
Translations
Basic
ContinuantsRecurrence
ConvergentsEquiv
TerminatedStable
Translations
DirectSum
Algebra
Basic
Decomposition
Finsupp
Internal
Module
Ring
Divisibility
Basic
Units
EuclideanDomain
Basic
Defs
Instances
Field
Basic
Defs
Opposite
Power
ULift
FreeMonoid
Basic
Count
GCDMonoid
Basic
Div
Finset
Multiset
Group
WithOne
Basic
Defs
Units
Basic
Commutator
Commute
Conj
ConjFinite
Defs
Ext
InjSurj
Opposite
OrderSynonym
Pi
Prod
Semiconj
TypeTags
ULift
UniqueProds
Units
GroupPower
Basic
Identities
Lemmas
Order
Ring
GroupRingAction
Basic
Invariant
Subobjects
GroupWithZero
Units
Basic
Lemmas
Basic
Commute
Defs
Divisibility
InjSurj
Power
Semiconj
Hom
Equiv
Units
Basic
GroupWithZero
Basic
TypeTags
Aut
Centroid
Commute
Embedding
Freiman
Group
GroupAction
GroupInstances
Iterate
NonUnitalAlg
Ring
Units
Homology
ShortComplex
Basic
Homology
LeftHomology
RightHomology
ShortExact
Abelian
Preadditive
Additive
Augment
ComplexShape
Exact
Flip
Functor
HomologicalComplex
Homology
Homotopy
HomotopyCategory
ImageToKernel
Opposite
QuasiIso
Single
Lie
Basic
NonUnitalNonAssocAlgebra
Subalgebra
Module
Submodule
Basic
Bilinear
Lattice
Pointwise
Algebra
Basic
BigOperators
Bimodule
Equiv
GradedModule
Hom
Injective
LinearMap
LocalizedModule
Opposites
Pi
PointwisePi
Prod
Projective
Torsion
ULift
MonoidAlgebra
Basic
Degree
Division
Grading
Ideal
NoZeroDivisors
Support
ToDirectSum
Order
Field
Canonical
Basic
Defs
Basic
Defs
InjSurj
Pi
Power
Group
Abs
Bounds
Defs
DenselyOrdered
InjSurj
Instances
MinMax
OrderIso
Prod
TypeTags
Units
WithTop
Hom
Basic
Monoid
Ring
Monoid
Cancel
Basic
Defs
Canonical
Defs
WithZero
Basic
Defs
Basic
Defs
Lemmas
MinMax
NatCast
OrderDual
Prod
ToMulBot
TypeTags
Units
WithTop
Nonneg
Field
Floor
Ring
Positive
Field
Ring
Ring
Abs
Canonical
CharZero
Cone
Defs
InjSurj
Lemmas
WithTop
Sub
Basic
Canonical
Defs
WithTop
AbsoluteValue
Algebra
Archimedean
Chebyshev
EuclideanAbsoluteValue
Floor
Invertible
Kleene
LatticeGroup
Module
Pi
Pointwise
Rearrangement
SMul
ToIntervalMod
UpperLower
WithZero
ZeroLEOne
Polynomial
BigOperators
GroupRingAction
Regular
Basic
Pow
SMul
Ring
AddAut
Aut
Basic
BooleanRing
Commute
CompTypeclasses
Defs
Divisibility
Equiv
Fin
Idempotents
InjSurj
Opposite
OrderSynonym
Pi
Prod
Regular
Semiconj
ULift
Units
Star
Basic
BigOperators
CHSH
Free
Module
Pi
Pointwise
Prod
SelfAdjoint
StarAlgHom
Subalgebra
Unitary
Tropical
Basic
BigOperators
Lattice
Abs
AddTorsor
AlgebraicCard
Associated
Bounds
CovariantAndContravariant
CubicDiscriminant
DirectLimit
DualNumber
DualQuaternion
Free
FreeAlgebra
FreeNonUnitalNonAssocAlgebra
GeomSum
GradedMonoid
GradedMulAction
HierarchyDesign
IndicatorFunction
Invertible
IsPrimePow
LinearRecurrence
ModEq
NeZero
Opposites
PEmptyInstances
PUnitInstances
Parity
Periodic
QuadraticDiscriminant
Quandle
Quaternion
QuaternionBasis
Quotient
RingQuot
SMulWithZero
Squarefree
Support
TrivSqZeroExt
AlgebraicGeometry
PresheafedSpace (file)
HasColimits
PrimeSpectrum
Basic
IsOpenComapC
Maximal
Noetherian
ProjectiveSpectrum
Topology
SheafedSpace
Stalks
StructureSheaf
AlgebraicTopology
DoldKan
Compatibility
Decomposition
Degeneracies
EquivalenceAdditive
Faces
FunctorGamma
FunctorN
GammaCompN
Homotopies
HomotopyEquivalence
NCompGamma
NReflectsIso
Normalized
Notations
PInfty
Projections
SplitSimplicialObject
FundamentalGroupoid
Basic
FundamentalGroup
PUnit
AlternatingFaceMapComplex
CechNerve
ExtraDegeneracy
MooreComplex
Nerve
SimplexCategory
SimplicialObject
SimplicialSet
SplitSimplicialObject
TopologicalSimplex
Analysis
Analytic
Basic
Asymptotics
AsymptoticEquivalent
Asymptotics
SpecificAsymptotics
SuperpolynomialDecay
Theta
BoxIntegral
Box
Basic
SubboxInduction
Partition
Additive
Basic
Filter
Split
SubboxInduction
Tagged
Calculus
Conformal
InnerProduct
NormedSpace
Deriv
Add
AffineMap
Basic
Comp
Inv
Inverse
Linear
Mul
Polynomial
Pow
Prod
Slope
Star
Support
ZPow
FDeriv
Add
Basic
Bilinear
Comp
Equiv
Linear
Mul
Prod
RestrictScalars
Star
ContDiffDef
Darboux
DiffContOnCl
Dslope
FDerivMeasurable
FormalMultilinearSeries
IteratedDeriv
LocalExtr
MeanValue
TangentCone
Complex
UnitDisc
Basic
Arg
Basic
Circle
Conformal
Isometry
OperatorNorm
ReImTopology
Convex
Cone
Basic
Dual
SimplicialComplex
Basic
SpecificFunctions
Basic
Basic
Between
Body
Caratheodory
Combination
Complex
Contractible
Exposed
Extrema
Extreme
Function
Gauge
Hull
Independent
Jensen
Join
KreinMilman
Normed
PartitionOfUnity
Quasiconvex
Segment
Side
Slope
Star
StoneSeparation
Strict
StrictConvexBetween
StrictConvexSpace
Topology
Uniform
InnerProductSpace
Adjoint
Basic
ConformalLinearMap
Dual
GramSchmidtOrtho
LaxMilgram
Orthogonal
PiL2
Positive
Projection
Symmetric
LocallyConvex
AbsConvex
BalancedCoreHull
Basic
Bounded
ContinuousOfBounded
Polar
StrongTopology
WeakDual
WithSeminorms
Normed
Field
Basic
InfiniteSum
UnitBall
Group
AddCircle
AddTorsor
BallSphere
Basic
Completion
ControlledClosure
Hom
HomCompletion
InfiniteSum
Pointwise
Quotient
Seminorm
Order
Basic
Lattice
UpperLower
Ring
Seminorm
MulAction
NormedSpace
HahnBanach
Extension
Separation
Star
Basic
Mul
Multiplier
AddTorsor
AffineIsometry
BallAction
Banach
BanachSteinhaus
Basic
BoundedLinearMaps
CompactOperator
Complemented
Completion
ConformalLinearMap
ContinuousLinearMap
Dual
Extend
Extr
FiniteDimension
IndicatorFunction
Int
IsROrC
LinearIsometry
LpEquiv
MStructure
MazurUlam
Multilinear
OperatorNorm
PiLp
Pointwise
Ray
RieszLemma
Units
WeakDual
lpSpace
SpecialFunctions
Complex
Arg
Circle
Log
Log
Base
Basic
Monotone
Pow
Asymptotics
Complex
Continuity
NNReal
Real
Trigonometric
Angle
Basic
Chebyshev
Inverse
Exp
Polynomials
SpecificLimits
Basic
FloorPow
Normed
Hofer
MeanInequalities
MeanInequalitiesPow
PSeries
Quaternion
Seminorm
Subadditive
CategoryTheory
Abelian
DiagramLemmas
Four
Basic
Exact
Ext
FunctorCategory
Generator
Homology
Images
Injective
InjectiveResolution
LeftDerived
NonPreadditive
Opposite
Projective
Pseudoelements
RightDerived
Subobject
Transfer
Adjunction
AdjointFunctorTheorems
Basic
Comma
Evaluation
FullyFaithful
Limits
Mates
Opposites
Over
Reflective
Whiskering
Bicategory
Basic
Coherence
End
Free
Functor
LocallyDiscrete
SingleObj
Strict
Category
Cat (file)
Limit
Basic
Bipointed
GaloisConnection
Grpd
Init
KleisliCat
Pairwise
Pointed
Preorder
QuivCat
RelCat
TwoP
ULift
Closed
Monoidal
ConcreteCategory
Basic
Bundled
BundledHom
Elementwise
ReflectsIso
UnbundledHom
Endofunctor
Algebra
Functor
Basic
Category
Const
Currying
Default
EpiMono
Flat
FullyFaithful
Functorial
Hom
InvIsos
LeftDerived
ReflectsIso
Groupoid (file)
Basic
FreeGroupoid
VertexGroup
Idempotents
Basic
Biproducts
FunctorCategories
FunctorExtension
HomologicalComplex
Karoubi
KaroubiKaroubi
SimplicialObject
LiftingProperties
Adjunction
Basic
Limits
Constructions
Over
Connected
Products
BinaryProducts
EpiMono
Equalizers
Filtered
FiniteProductsOfBinaryProducts
LimitsOfProductsAndEqualizers
Pullbacks
WeaklyInitial
ZeroObjects
Preserves
Shapes
BinaryProducts
Biproducts
Equalizers
Images
Kernels
Products
Pullbacks
Terminal
Zero
Basic
Filtered
Finite
FunctorCategory
Limits
Opposites
Shapes
NormalMono
Basic
Equalizers
BinaryProducts
Biproducts
CommSq
Diagonal
DisjointCoproduct
Equalizers
Equivalence
FiniteLimits
FiniteProducts
FunctorCategory
Images
KernelPair
Kernels
Multiequalizer
Products
Pullbacks
Reflexive
RegularMono
SplitCoequalizer
StrictInitial
StrongEpi
Terminal
Types
WideEqualizers
WidePullbacks
ZeroMorphisms
ZeroObjects
Bicones
ColimitLimit
Comma
ConcreteCategory
ConeCategory
Cones
Connected
Creates
EssentiallySmall
ExactFunctor
Filtered
FilteredColimitCommutesFiniteLimit
Final
Fubini
FullSubcategory
FunctorCategory
HasLimits
IsLimit
KanExtension
Lattice
MonoCoprod
Opposites
Over
Pi
Presheaf
SmallComplete
Types
Unit
Yoneda
Linear
Basic
FunctorCategory
LinearFunctor
Yoneda
Localization
Construction
Opposite
Predicate
Monad
Adjunction
Algebra
Basic
Coequalizer
Kleisli
Limits
Products
Types
Monoidal
Free
Basic
Coherence
OfChosenFiniteProducts
Basic
Types
Basic
Category
CoherenceLemmas
Discrete
End
Functor
Functorial
Linear
NaturalTransformation
Preadditive
Tor
Transport
Pi
Basic
Preadditive
Yoneda
Basic
Injective
Limits
Projective
AdditiveFunctor
Basic
Biproducts
EilenbergMoore
EndoFunctor
FunctorCategory
Generator
HomOrthogonal
Injective
InjectiveResolution
LeftExact
OfBiproducts
Opposite
Projective
ProjectiveResolution
SingleObj
Products
Associator
Basic
Bifunctor
Shift
Basic
Sigma
Basic
Sites
Adjunction
Closed
Coherent
CoverLifting
CoverPreserving
Coverage
DenseSubsite
EffectiveEpimorphic
Grothendieck
InducedTopology
LeftExact
Limits
Plus
Pretopology
Pushforward
Sheaf
SheafOfTypes
Sheafification
Sieves
Spaces
Subsheaf
Whiskering
Subobject
Basic
Comma
FactorThru
Lattice
Limits
MonoOver
Types
WellPowered
Sums
Associator
Basic
Triangulated
Basic
Pretriangulated
Rotate
Triangulated
Action
Arrow
Balanced
CofilteredSystem
CommSq
Comma
Conj
ConnectedComponents
Core
DiscreteCategory
Elements
Elementwise
Endomorphism
EpiMono
EqToHom
Equivalence
EssentialImage
EssentiallySmall
Filtered
FinCategory
FintypeCat
FullSubcategory
Generator
GlueData
GradedObject
Grothendieck
IsConnected
Iso
IsomorphismClasses
MorphismProperty
NatIso
NatTrans
Noetherian
Opposites
Over
PEmpty
PUnit
PathCategory
Quotient
Simple
SingleObj
Skeletal
StructuredArrow
Subterminal
Thin
Types
Whiskering
Yoneda
Combinatorics
Additive
Energy
Etransform
PluenneckeRuzsa
RuzsaCovering
SalemSpencer
Derangements
Basic
Finite
Hall
Basic
Finite
Quiver
Arborescence
Basic
Cast
ConnectedComponent
Path
Push
SingleObj
Subquiver
Symmetric
SetFamily
Compression
Down
UV
HarrisKleitman
Intersecting
Kleitman
LYM
Shadow
SimpleGraph
Ends
Defs
Properties
Regularity
Energy
Equitabilise
Uniform
Triangle
Basic
Acyclic
AdjMatrix
Basic
Clique
Coloring
Connectivity
DegreeSum
Density
Finsubgraph
Hasse
IncMatrix
Init
Matching
Metric
Partition
Prod
StronglyRegular
Subgraph
Trails
Young
SemistandardTableau
YoungDiagram
Catalan
Colex
Composition
Configuration
DoubleCounting
HalesJewett
Hindman
Partition
Pigeonhole
Computability
Ackermann
DFA
Encoding
EpsilonNFA
Halting
Language
NFA
Partrec
PartrecCode
Primrec
Reduce
RegularExpressions
TMComputable
TMToPartrec
TuringMachine
Control
Bitraversable
Basic
Lemmas
EquivFunctor (file)
Instances
Functor (file)
Multivariate
Monad
Basic
Traversable
Basic
Equiv
Instances
Lemmas
Applicative
Basic
Bifunctor
Fix
Fold
LawfulFix
Random
SimpSet
ULift
Writer
Data
Analysis
Filter
Topology
Array
Basic
Defs
Bitvec
Basic
Core
Bool
AllAny
Basic
Count
Set
Complex
Basic
Cardinality
Determinant
Exponential
Module
Orientation
Countable
Basic
Defs
Small
DList
Basic
Instances
Dfinsupp
Basic
Interval
Lex
Multiset
NeLocus
Order
WellFounded
ENat
Basic
Lattice
Equiv
Functor
FP
Basic
Fin
Tuple
Basic
BubbleSortInduction
Monotone
NatAntidiagonal
Reflection
Sort
Basic
Fin2
Interval
SuccPred
VecNotation
Finite
Basic
Card
Defs
Set
Finset
Basic
Card
Fin
Finsupp
Fold
Functor
Image
Interval
Lattice
LocallyFinite
MulAntidiagonal
NAry
NatAntidiagonal
NoncommProd
Option
Order
PImage
Pairwise
Pi
PiInduction
Pointwise
Powerset
Preimage
Prod
Sigma
Slice
Sort
Sum
Sups
Sym
Finsupp
AList
Antidiagonal
Basic
BigOperators
Defs
Fin
Fintype
Indicator
Interval
Lex
Multiset
NeLocus
Order
Pointwise
Pwo
ToDfinsupp
WellFounded
Fintype
Basic
BigOperators
Card
CardEmbedding
Fin
Lattice
List
Option
Order
Parity
Perm
Pi
Powerset
Prod
Quotient
Sigma
Small
Sort
Sum
Units
Vector
FunLike
Basic
Embedding
Equiv
Fintype
Int
Cast
Basic
Defs
Field
Lemmas
Prod
Dvd
Basic
Pow
Order
Basic
Lemmas
Units
AbsoluteValue
Associated
Basic
Bitwise
CharZero
ConditionallyCompleteOrder
Div
GCD
Interval
LeastGreatest
Lemmas
Log
ModEq
NatPrime
Parity
Range
Sqrt
SuccPred
Units
IsROrC
Attr
Basic
Lemmas
LazyList (file)
Basic
List
BigOperators
Basic
Lemmas
AList
Basic
Card
Chain
Count
Cycle
Dedup
Defs
Destutter
Duplicate
FinRange
Forall2
Func
Indexes
Infix
Intervals
Join
Lattice
Lemmas
Lex
MinMax
NatAntidiagonal
Nodup
NodupEquivFin
OfFn
Pairwise
Palindrome
Perm
Permutation
Prime
ProdSigma
Range
Rdrop
Rotate
Sections
Sigma
Sort
Sublists
TFAE
ToFinsupp
Zip
ListM
Basic
BestFirst
DepthFirst
Heartbeats
Matrix
Basic
Basis
Block
CharP
DMatrix
DualNumber
Hadamard
Kronecker
Notation
PEquiv
Rank
Reflection
Multiset
Antidiagonal
Basic
Bind
Dedup
FinsetOps
Fintype
Fold
Functor
Interval
Lattice
LocallyFinite
NatAntidiagonal
Nodup
Pi
Powerset
Range
Sections
Sort
Sum
MvPolynomial
Basic
Cardinal
Comap
CommRing
Counit
Division
Equiv
Expand
Funext
Invertible
Monad
Polynomial
Rename
Supported
Variables
Nat
Cast
Basic
Defs
Field
Prod
WithTop
Choose
Basic
Bounds
Cast
Central
Dvd
Factorization
Multinomial
Sum
Vandermonde
Factorial
Basic
BigOperators
Cast
DoubleFactorial
Factorization
Basic
PrimePow
GCD
Basic
BigOperators
Order
Basic
Lemmas
Basic
Bits
Bitwise
Count
Digits
Dist
EvenOddRec
Factors
Fib
ForSqrt
Hyperoperation
Interval
Lattice
Log
ModEq
Multiplicity
PSub
Pairing
Parity
PartENat
Periodic
Pow
Prime
PrimeFin
PrimeNormNum
Set
Size
Sqrt
Squarefree
SuccPred
Totient
Units
Upto
WithBot
Num
Basic
Bitwise
Lemmas
Prime
Option
Basic
Defs
NAry
Ordmap
Ordnode
PFunctor
Multivariate
Basic
M
W
Univariate
Basic
M
PNat
Basic
Defs
Factors
Find
Interval
Prime
Xgcd
PSigma
Order
Pi
Algebra
Interval
Lex
Polynomial
Degree
CardPowDegree
Definitions
Lemmas
TrailingDegree
AlgebraMap
Basic
CancelLeads
Cardinal
Coeff
DenomsClearable
Derivative
Div
EraseLead
Eval
Expand
FieldDivision
HasseDeriv
Identities
Induction
Inductions
IntegralNormalization
Laurent
Lifts
Mirror
Module
Monic
Monomial
PartialFractions
Reverse
RingDivision
Splits
Taylor
Prod
Basic
Lex
PProd
TProd
QPF
Multivariate
Constructions
Comp
Const
Fix
Prj
Quot
Sigma
Basic
Univariate
Basic
Rat
Basic
BigOperators
Cast
Defs
Denumerable
Encodable
Floor
Init
Lemmas
NNRat
Order
Sqrt
Real
Basic
Cardinality
CauSeq
CauSeqCompletion
ConjugateExponents
ENNReal
ENatENNReal
EReal
GoldenRatio
Hyperreal
Irrational
NNReal
Pointwise
Sign
Sqrt
Seq
Computation
Parallel
Seq
WSeq
Set
Intervals
Basic
Disjoint
Group
Infinite
Instances
IsoIoo
Monoid
Monotone
OrdConnected
OrdConnectedComponent
OrderIso
Pi
ProjIcc
SurjOn
UnorderedInterval
WithBotTop
Pairwise
Basic
Lattice
Pointwise
Basic
BigOperators
Finite
Interval
Iterate
ListOfFn
SMul
Support
Accumulate
Basic
BoolIndicator
Constructions
Countable
Enumerate
Equitable
Finite
Function
Functor
Image
Lattice
List
MulAntidiagonal
NAry
Opposite
Prod
Semiring
Sigma
Sups
UnionLift
SetLike
Basic
Fintype
Setoid
Basic
Partition
Sigma
Basic
Interval
Lex
Order
Stream
Defs
Init
String
Basic
Defs
Lemmas
Sum
Basic
Interval
Order
Sym
Sym2 (file)
Init
Basic
Card
TypeVec (file)
Attr
Vector (file)
Basic
Mem
Zip
W
Basic
Cardinal
Constructions
ZMod
Algebra
Basic
Coprime
Defs
Parity
Quotient
BinaryHeap
Bracket
Bundle
ByteArray
Char
Erased
FinEnum
Finmap
HashMap
Holor
KVMap
Opposite
PEquiv
PFun
Part
Quot
Rel
SProd
Semiquot
Sign
Subtype
Tree
TwoPointing
TypeMax
UInt
ULift
UnionFind
Deprecated
Group
Ring
Subfield
Subgroup
Submonoid
Subring
Dynamics
Circle
RotationNumber
TranslationNumber
Ergodic
Conservative
Ergodic
MeasurePreserving
FixedPoints
Basic
Topology
Flow
Minimal
OmegaLimit
PeriodicPts
FieldTheory
Minpoly
Basic
Field
AxGrothendieck
Finiteness
IntermediateField
MvPolynomial
PerfectClosure
RatFunc
Separable
SeparableDegree
Subfield
Tower
Geometry
Euclidean
Angle
Unoriented
Affine
Basic
Conformal
Sphere
Basic
Power
SecondInter
Basic
Inversion
Manifold
ChartedSpace
ConformalGroupoid
LocalInvariantProperties
GroupTheory
GroupAction
SubMulAction (file)
Pointwise
Basic
BigOperators
ConjAct
Defs
Embedding
FixingSubgroup
Group
Opposite
Option
Pi
Prod
Quotient
Sigma
Sum
Support
Units
Perm
Cycle
Basic
Concrete
Type
Basic
Fin
List
Option
Sign
Subgroup
Support
ViaEmbedding
SpecificGroups
Alternating
Cyclic
Dihedral
Subgroup
Actions
Basic
Finite
MulOpposite
Pointwise
Saturated
Simple
ZPowers
Submonoid
Basic
Center
Centralizer
Inverses
Membership
Operations
Pointwise
Subsemigroup
Basic
Center
Centralizer
Membership
Operations
Abelianization
Archimedean
Commensurable
Commutator
CommutingProbability
Complement
Congruence
Coset
Divisible
DoubleCoset
EckmannHilton
Exponent
Finiteness
FreeAbelianGroup
FreeAbelianGroupFinsupp
FreeGroup
FreeProduct
Index
IsFreeGroup
MonoidLocalization
NielsenSchreier
Nilpotent
NoncommPiCoprod
OrderOfElement
PGroup
PresentedGroup
QuotientGroup
SemidirectProduct
Solvable
Sylow
Torsion
InformationTheory
Hamming
Init
Algebra
Classes
Functions
Order
Classes
Order
Control
Combinators
Data
Bool
Basic
Lemmas
Fin
Basic
Int
Basic
Bitwise
DivMod
Lemmas
Order
List
Basic
Instances
Lemmas
Nat
Basic
Bitwise
Div
GCD
Lemmas
Notation
Option
Init
Lemmas
Basic
Lemmas
Ordering
Basic
Lemmas
Rat
Basic
Sigma
Basic
Subtype
Basic
Prod
Quot
Meta
WellFoundedTactics
Align
CcLemmas
Classical
Core
Function
IteSimp
Logic
Propext
Quot
Set
ZeroOne
Lean
Elab
Tactic
Basic
Expr (file)
Basic
ReplaceRec
Traverse
Meta (file)
Basic
DiscrTree
Simp
CoreM
EnvExtension
Exception
Json
Linter
LocalContext
Message
Name
SMap
LinearAlgebra
AffineSpace
AffineEquiv
AffineMap
AffineSubspace
Basic
Basis
Combination
FiniteDimensional
Independent
Matrix
Midpoint
MidpointZero
Ordered
Pointwise
Restrict
Slope
Basis (file)
Bilinear
BilinearForm (file)
TensorProduct
Charpoly
Basic
ToMatrix
DirectSum
Finsupp
TensorProduct
FreeModule
Finite
Basic
Matrix
Rank
Basic
Determinant
IdealQuotient
PID
Rank
StrongRankCondition
Matrix
Charpoly
Basic
Coeff
LinearMap
Minpoly
AbsoluteValue
Adjugate
Basis
BilinearForm
Block
Circulant
Determinant
Diagonal
DotProduct
Dual
FiniteDimensional
GeneralLinearGroup
Hermitian
InvariantBasisNumber
IsDiag
MvPolynomial
Nondegenerate
NonsingularInverse
Orthogonal
Polynomial
Reindex
SesquilinearForm
SpecialLinearGroup
Symmetric
ToLin
ToLinearEquiv
Trace
Transvection
ZPow
Multilinear
Basic
Basis
FiniteDimensional
TensorProduct
ProjectiveSpace
Basic
Independence
Subspace
TensorProduct (file)
Matrix
AdicCompletion
Alternating
AnnihilatingPolynomial
Basic
BilinearMap
Coevaluation
Contraction
CrossProduct
Determinant
Dfinsupp
Dimension
Dual
FiniteDimensional
Finrank
Finsupp
FinsuppVectorSpace
FreeAlgebra
GeneralLinearGroup
InvariantBasisNumber
Isomorphisms
Lagrange
LinearIndependent
LinearPMap
Orientation
Pi
Prod
Projection
Quotient
QuotientPi
Ray
SModEq
SesquilinearForm
Span
StdBasis
SymplecticGroup
TensorProductBasis
Trace
UnitaryGroup
Vandermonde
Logic
Embedding
Basic
Set
Encodable
Basic
Lattice
Equiv
Basic
Defs
Embedding
Fin
Fintype
Functor
List
LocalEquiv
MfldSimpsAttr
Nat
Option
Set
TransferInstance
Function
Basic
Conjugate
Iterate
Small
Basic
List
Basic
Denumerable
Hydra
IsEmpty
Lemmas
Nonempty
Nontrivial
Pairwise
Relation
Relator
Unique
Mathport
Attributes
Notation
Rename
Syntax
MeasureTheory
Category
MeasCat
Constructions
BorelSpace
Basic
Complex
ContinuousLinearMap
Metrizable
Prod
Basic
Pi
Polish
Covering
Vitali
VitaliFamily
Decomposition
Jordan
SignedHahn
UnsignedHahn
Function
SpecialFunctions
Basic
Inner
IsROrC
StronglyMeasurable
Basic
Inner
AEEqFun
AEMeasurableOrder
AEMeasurableSequence
ConvergenceInMeasure
Egorov
EssSup
Floor
L1Space
LocallyIntegrable
LpOrder
LpSeminorm
LpSpace
SimpleFunc
SimpleFuncDense
Group
Action
Arithmetic
MeasurableEquiv
Measure
Pointwise
Prod
Integral
IntegrableOn
Lebesgue
LebesgueNormedSpace
MeanInequalities
RieszMarkovKakutani
Measure
Haar
Basic
OfBasis
AEDisjoint
AEMeasurable
Complex
Content
Doubling
GiryMonad
MeasureSpace
MeasureSpaceDef
MutuallySingular
NullMeasurable
OpenPos
OuterMeasure
Regular
Stieltjes
Sub
VectorMeasure
CardMeasurableSpace
Lattice
MeasurableSpace
MeasurableSpaceDef
PiSystem
Tactic
ModelTheory
Basic
Bundled
Definability
ElementaryMaps
Encoding
FinitelyGenerated
Graph
LanguageMap
Order
Quotients
Satisfiability
Semantics
Skolem
Substructures
Syntax
Types
Ultraproducts
NumberTheory
ClassNumber
AdmissibleAbs
AdmissibleAbsoluteValue
AdmissibleCardPowDegree
LegendreSymbol
MulCharacter
ZModChar
ModularForms
CongruenceSubgroups
Padics
Hensel
PadicIntegers
PadicNorm
PadicNumbers
PadicVal
RingHoms
Zsqrtd
Basic
ToReal
ADEInequality
ArithmeticFunction
Basic
Bernoulli
Divisors
Fermat4
FrobeniusNumber
LSeries
LucasLehmer
LucasPrimality
Multiplicity
PellMatiyasevic
Primorial
PythagoreanTriples
VonMangoldt
Order
Atoms (file)
Finite
Bounds
Basic
OrderIso
Category
DistLatCat
FinPartOrd
FrmCat
LatCat
LinOrdCat
NonemptyFinLinOrdCat
PartOrdCat
PreordCat
ConditionallyCompleteLattice
Basic
Finset
Group
Extension
Linear
Well
Filter
Archimedean
AtTopBot
Bases
Basic
Cofinite
CountableInter
Curry
ENNReal
Extr
FilterProduct
Germ
IndicatorFunction
Interval
Lift
ModEq
NAry
Partial
Pi
Pointwise
Prod
SmallSets
Ultrafilter
ZeroAndBoundedAtFilter
Heyting
Basic
Boundary
Hom
Regular
Hom
Basic
Bounded
CompleteLattice
Lattice
Order
Set
Monotone
Basic
Extension
Monovary
Odd
Union
Partition
Equipartition
Finpartition
RelIso
Basic
Group
Set
SuccPred
Basic
IntervalSucc
Limit
LinearLocallyFinite
Relation
UpperLower
Basic
Hom
LocallyFinite
Antichain
Antisymmetrization
Basic
BooleanAlgebra
Bounded
BoundedOrder
Chain
Circular
Closure
CompactlyGenerated
Compare
CompleteBooleanAlgebra
CompleteLattice
CompleteLatticeIntervals
Concept
Copy
CountableDenseLinearOrder
Cover
Directed
Disjoint
Disjointed
FixedPoints
GaloisConnection
GameAdd
Grade
Height
Ideal
InitialSeg
Interval
Iterate
JordanHolder
KrullDimension
Lattice
LatticeIntervals
LiminfLimsup
LocallyFinite
Max
MinMax
Minimal
ModularLattice
OmegaCompletePartialOrder
OrdContinuous
OrderIsoNat
PFilter
PartialSups
PrimeIdeal
PropInstances
RelClasses
SemiconjSup
SupIndep
SymmDiff
Synonym
WellFounded
WellFoundedSet
WithBot
Zorn
ZornAtoms
Probability
ProbabilityMassFunction
Basic
Constructions
Monad
Uniform
CondCount
ConditionalProbability
RepresentationTheory
Basic
Maschke
RingTheory
Adjoin
Basic
FG
Field
PowerBasis
Tower
Coprime
Basic
Ideal
Lemmas
DiscreteValuationRing
Basic
GradedAlgebra
Basic
HomogeneousIdeal
HomogeneousLocalization
Radical
Ideal
AssociatedPrime
Basic
Cotangent
IdempotentFG
LocalRing
MinimalPrime
Operations
Over
Prod
Quotient
QuotientOperations
Int
Basic
Localization
Away
Basic
AsSubring
AtPrime
Basic
Cardinality
FractionRing
Ideal
Integer
Integral
InvSubmonoid
LocalizationLocalization
Module
NumDen
Submodule
MvPolynomial
Basic
Homogeneous
Ideal
Symmetric
Tower
WeightedHomogeneous
NonUnitalSubsemiring
Basic
OreLocalization
Basic
OreSet
Polynomial
Eisenstein
Basic
Basic
Chebyshev
Content
Dickson
Opposites
Pochhammer
Quotient
ScaleRoots
Tower
Vieta
PowerSeries
Basic
WellKnown
Subring
Basic
Pointwise
Subsemiring
Basic
Pointwise
Valuation
Basic
ExtendToLocalization
Integers
Quotient
WittVector
WittPolynomial
AdjoinRoot
AlgebraTower
Algebraic
AlgebraicIndependent
Artinian
ChainOfDivisors
Congruence
EisensteinCriterion
EuclideanDomain
Filtration
FinitePresentation
FiniteType
Finiteness
Fintype
Flat
FractionalIdeal
FreeCommRing
FreeRing
HahnSeries
Henselian
IntegralClosure
IntegralDomain
IsTensorProduct
JacobsonIdeal
LaurentSeries
MatrixAlgebra
Multiplicity
Nakayama
Nilpotent
Noetherian
NonZeroDivisors
PolynomialAlgebra
PowerBasis
Prime
PrincipalIdealDomain
QuotientNilpotent
QuotientNoetherian
ReesAlgebra
RingInvo
SimpleModule
TensorProduct
UniqueFactorizationDomain
ZMod
SetTheory
Cardinal
Basic
Cofinality
Continuum
Divisibility
Finite
Ordinal
SchroederBernstein
Game
PGame
Ordinal
Arithmetic
Basic
CantorNormalForm
Exponential
FixedPoint
NaturalOps
Principal
Topology
ZFC
Basic
Ordinal
Lists
Tactic (file)
CategoryTheory
Coherence
Elementwise
Reassoc
Slice
Continuity (file)
Init
Linarith (file)
Datatypes
Elimination
Frontend
Lemmas
Parsing
Preprocessing
Verification
Measurability (file)
Init
Monotonicity (file)
Attr
Basic
Lemmas
Nontriviality (file)
Core
NormCast (file)
Tactic
NormNum (file)
Basic
Core
GCD
IsCoprime
NatFib
NatSqrt
Prime
Positivity (file)
Basic
Core
Qify (file)
Attr
Relation
Rfl
Symm
Trans
Ring (file)
Basic
RingNF
Sat
FromLRAT
Simps
Basic
NotationClass
Zify (file)
Attr
Abel
Alias
ApplyCongr
ApplyFun
ApplyWith
Backtracking
Basic
ByContra
Cache
CancelDenoms
Cases
CasesM
Choose
Classical
Clear!
ClearExcept
Clear_
Coe
Common
Congr!
Constructor
Contrapose
Conv
Convert
Core
DeriveFintype
DeriveToExpr
Eqns
Existsi
FBinop
FailIfNoProgress
FieldSimp
FinCases
Find
GeneralizeProofs
Group
GuardGoalNums
GuardHypNums
Have
HelpCmd
HigherOrder
InferParam
Inhabit
IntervalCases
IrreducibleDef
LabelAttr
LeftRight
LibrarySearch
Lift
LinearCombination
MkIffOfInductiveProp
ModCases
NthRewrite
PermuteGoals
Polyrith
PrintPrefix
ProjectionNotation
Propose
ProxyType
PushNeg
RSuffices
Recover
Rename
RenameBVar
Replace
RestateAxiom
Rewrites
RunCmd
ScopedNS
Set
SimpIntro
SimpRw
SlimCheck
SolveByElim
SplitIfs
Spread
Substs
SuccessIfFailWithMsg
SudoSetOption
SwapVar
TFAE
Tauto
ToAdditive
ToExpr
ToLevel
Trace
TryThis
TypeCheck
UnsetOption
Use
WLOG
Testing
SlimCheck
Gen
Sampleable
Testable
Topology
Algebra
Group
Basic
Compact
InfiniteSum
Basic
Module
Order
Real
Ring
Module
Basic
Determinant
FiniteDimension
LinearPMap
LocallyConvex
Multilinear
Simple
Star
StrongTopology
WeakDual
Nonarchimedean
AdicTopology
Bases
Basic
Order
Archimedean
Compact
ExtendFrom
ExtrClosure
Field
Filter
Floor
Group
IntermediateValue
LeftRight
LeftRightLim
LiminfLimsup
MonotoneContinuity
MonotoneConvergence
ProjIcc
T5
UpperLower
Ring
Basic
Ideal
Affine
Algebra
ConstMulAction
Constructions
ContinuousMonoidHom
Equicontinuity
Field
FilterBasis
GroupCompletion
GroupWithZero
Localization
Monoid
MulAction
OpenSubgroup
Polynomial
Semigroup
Star
StarSubalgebra
UniformConvergence
UniformField
UniformFilterBasis
UniformGroup
UniformMulAction
UniformRing
Valuation
ValuedField
WithZeroTopology
Bornology
Basic
Constructions
Hom
Category
CompHaus
Basic
Projective
Profinite
AsLimit
Basic
Projective
TopCat
Limits
Basic
Cofiltered
Konig
Products
Pullbacks
Adjunctions
Basic
EpiMono
OpenNhds
Opens
Born
Locale
TopCommRingCat
Compactification
OnePoint
ContinuousFunction
Algebra
Basic
Bounded
CocompactMap
Compact
LocallyConstant
Ordered
Polynomial
T0Sierpinski
FiberBundle
Basic
Constructions
IsHomeomorphicTrivialBundle
Trivialization
Hom
Open
Homotopy
Basic
Contractible
Equiv
HomotopyGroup
Path
Instances
AddCircle
Complex
Discrete
ENNReal
EReal
Int
Irrational
Matrix
NNReal
Nat
Rat
RatLemmas
Real
RealVectorSpace
Sign
TrivSqZeroExt
LocallyConstant
Algebra
Basic
MetricSpace
Algebra
Antilipschitz
Baire
Basic
CantorScheme
CauSeqFilter
Closeds
Completion
Contracting
EMetricParacompact
EMetricSpace
Equicontinuity
Gluing
GromovHausdorffRealized
HausdorffDistance
Holder
Infsep
IsometricSMul
Isometry
Kuratowski
Lipschitz
MetricSeparated
Metrizable
MetrizableUniformity
PartitionOfUnity
PiNat
Polish
ShrinkingLemma
ThickenedIndicator
Order (file)
Hom
Basic
Basic
Lattice
LowerTopology
Priestley
Sets
Closeds
Compacts
Opens
Order
Sheaves
SheafCondition
EqualizerProducts
OpensLeCover
PairwiseIntersections
Sites
UniqueGluing
Abelian
Forget
Functors
Init
Limits
LocalPredicate
PUnit
Presheaf
PresheafOfFunctions
Sheaf
SheafOfFunctions
Stalks
Spectral
Hom
UniformSpace
AbsoluteValue
AbstractCompletion
Basic
Cauchy
Compact
CompactConvergence
CompareReals
CompleteSeparated
Completion
Equicontinuity
Equiv
Matrix
Pi
Separation
UniformConvergence
UniformConvergenceTopology
UniformEmbedding
VectorBundle
Basic
Constructions
Bases
Basic
CompactOpen
Connected
Constructions
ContinuousOn
Covering
DenseEmbedding
DiscreteQuotient
ExtendFrom
ExtremallyDisconnected
Filter
GDelta
Homeomorph
Inseparable
IsLocallyHomeomorph
List
LocalAtTarget
LocalExtr
LocalHomeomorph
LocallyFinite
Maps
NhdsSet
NoetherianSpace
OmegaCompletePartialOrder
Paracompact
Partial
PartitionOfUnity
PathConnected
Perfect
QuasiSeparated
Semicontinuous
Separation
Sequences
ShrinkingLemma
Sober
StoneCech
SubsetProperties
Support
Tactic
TietzeExtension
UnitInterval
UrysohnsBounded
UrysohnsLemma
Util
AddRelatedDecl
AssertExists
AssertNoSorry
AtomM
CompileInductive
Export
IncludeStr
LongNames
MemoFix
Pickle
Qq
Syntax
SynthesizeUsing
Tactic
Time
WhatsNew
WithWeakNamespace
Qq (file)
ForLean
Do
ReduceEval
ToExpr
AssertInstancesCommute
Delab
Macro
Match
MetaM
SortLocalDecls
Typ
Std (file)
Classes
BEq
Cast
Dvd
LawfulMonad
Order
RatCast
SetNotation
CodeAction (file)
Attr
Basic
Misc
Control
ForInStep (file)
Basic
Lemmas
Data
Array
Init
Basic
Lemmas
Basic
Lemmas
Merge
Fin
Lemmas
HashMap (file)
Basic
WF
Int
Basic
DivMod
Lemmas
List
Init
Lemmas
Basic
Lemmas
Nat
Basic
Gcd
Lemmas
Option
Init
Lemmas
Basic
Lemmas
Prod
Lex
RBMap (file)
Alter
Basic
Lemmas
WF
Range
Lemmas
Rat (file)
Basic
Lemmas
String (file)
Basic
Lemmas
AssocList
BinomialHeap
Char
DList
Ord
PairingHeap
Lean
Meta
AssertHypotheses
Basic
Clear
DiscrTree
Expr
Inaccessible
InstantiateMVars
LCtx
SavedState
UnusedNames
AttributeExtra
Command
Delaborator
Expr
Format
HashMap
HashSet
InfoTree
MonadBacktrack
Name
NameMapAttribute
Parser
PersistentHashMap
PersistentHashSet
Position
Tactic
TagAttribute
Linter (file)
UnnecessarySeqFocus
UnreachableTactic
Tactic
Ext (file)
Attr
Lint (file)
Basic
Frontend
Misc
Simp
TypeClass
NormCast
Ext
Lemmas
Basic
ByCases
CoeExt
Congr
GuardExpr
GuardMsgs
HaveI
Instances
NoMatch
OpenPrivate
RCases
SeqFocus
ShowTerm
SimpTrace
Simpa
SqueezeScope
TryThis
Unreachable
Where
Util
ExtendedBinder
LibraryNote
TermUnsafe
Logic
WF