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
BigOperators
Multiset
Basic
Lemmas
Basic
Finprod
Finsupp
Intervals
NatAntidiagonal
Option
Order
Pi
Ring
RingEquiv
CharZero
Defs
Infinite
Lemmas
DirectSum
Basic
Divisibility
Basic
Units
EuclideanDomain
Basic
Defs
Instances
Field
Basic
Defs
Opposite
Power
FreeMonoid
Basic
Count
GCDMonoid
Basic
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
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
Ring
Units
Homology
ComplexShape
Module
Submodule
Basic
Lattice
Basic
BigOperators
Equiv
Hom
LinearMap
Opposites
Pi
PointwisePi
Prod
ULift
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
Monoid
Cancel
Basic
Defs
Canonical
Defs
WithZero
Basic
Defs
Basic
Defs
Lemmas
MinMax
NatCast
OrderDual
Prod
ToMulBot
TypeTags
Units
WithTop
Positive
Field
Ring
Ring
Abs
Canonical
CharZero
Cone
Defs
InjSurj
Lemmas
WithTop
Sub
Basic
Canonical
Defs
WithTop
AbsoluteValue
Archimedean
EuclideanAbsoluteValue
Floor
Invertible
LatticeGroup
Pi
Pointwise
SMul
WithZero
ZeroLEOne
Regular
Basic
Pow
SMul
Ring
AddAut
Aut
Basic
Commute
CompTypeclasses
Defs
Divisibility
Equiv
Fin
Idempotents
InjSurj
Opposite
OrderSynonym
Pi
Prod
Regular
Semiconj
ULift
Units
Star
Basic
BigOperators
Pi
Pointwise
Prod
Unitary
Tropical
Basic
BigOperators
Lattice
Abs
Associated
Bounds
CovariantAndContravariant
Free
GeomSum
GradedMonoid
HierarchyDesign
IndicatorFunction
Invertible
IsPrimePow
NeZero
Opposites
PEmptyInstances
PUnitInstances
Parity
Quandle
Quotient
SMulWithZero
Support
CategoryTheory
Category
Basic
KleisliCat
RelCat
ConcreteCategory
Bundled
Functor
Basic
Category
Default
FullyFaithful
Functorial
EssentialImage
FullSubcategory
Iso
NatIso
NatTrans
Thin
Whiskering
Combinatorics
Additive
Energy
Hall
Finite
Quiver
Arborescence
Basic
Cast
ConnectedComponent
Path
Push
SingleObj
Subquiver
Symmetric
SetFamily
Compression
Down
Shadow
DoubleCounting
Pigeonhole
Control
EquivFunctor (file)
Instances
Functor (file)
Multivariate
Monad
Basic
Traversable
Basic
Equiv
Instances
Lemmas
Applicative
Basic
Fix
Random
SimpSet
ULift
Writer
Data
Array
Basic
Defs
Bitvec
Core
Bool
AllAny
Basic
Count
Set
Countable
Basic
Defs
Small
DList
Basic
Instances
Dfinsupp
Basic
NeLocus
ENat
Basic
Lattice
Equiv
Functor
Fin
Tuple
Basic
Monotone
Sort
Basic
Fin2
Interval
SuccPred
VecNotation
Finite
Basic
Defs
Set
Finset
Basic
Card
Fin
Fold
Image
Lattice
LocallyFinite
NAry
NatAntidiagonal
NoncommProd
Option
Order
Pairwise
Pi
PiInduction
Powerset
Preimage
Prod
Sigma
Slice
Sort
Sum
Finsupp
Defs
Fin
Fintype
Indicator
NeLocus
Order
Pointwise
Fintype
Basic
BigOperators
Card
Fin
Lattice
List
Option
Order
Parity
Pi
Powerset
Prod
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
LazyList (file)
Basic
List
BigOperators
Basic
Lemmas
AList
Basic
Card
Chain
Count
Cycle
Dedup
Defs
Destutter
Duplicate
FinRange
Forall2
Func
Infix
Join
Lattice
Lemmas
Lex
MinMax
NatAntidiagonal
Nodup
NodupEquivFin
OfFn
Pairwise
Palindrome
Perm
Permutation
Prime
ProdSigma
Range
Rdrop
Rotate
Sections
Sigma
Sort
Sublists
TFAE
Zip
Matrix
DMatrix
Multiset
Antidiagonal
Basic
Bind
Dedup
FinsetOps
Fold
Lattice
NatAntidiagonal
Nodup
Pi
Powerset
Range
Sections
Sort
Sum
Nat
Cast
Basic
Defs
Field
Prod
WithTop
Choose
Basic
Bounds
Dvd
Factorial
Basic
BigOperators
GCD
Basic
BigOperators
Order
Basic
Lemmas
Basic
Bits
Bitwise
Dist
EvenOddRec
Factors
Fib
ForSqrt
Hyperoperation
Interval
Lattice
Log
ModEq
PSub
Pairing
Parity
Pow
Prime
PrimeFin
Set
Size
Sqrt
SuccPred
Units
Upto
WithBot
Num
Basic
Bitwise
Option
Basic
Defs
NAry
PFunctor
Univariate
Basic
PNat
Basic
Defs
Find
Interval
Prime
Xgcd
PSigma
Order
Pi
Algebra
Lex
Prod
Basic
Lex
PProd
TProd
Rat
Basic
BigOperators
Cast
Defs
Encodable
Floor
Init
Lemmas
Order
Sqrt
Real
Basic
CauSeq
CauSeqCompletion
Sign
Seq
Computation
Set
Intervals
Basic
Disjoint
Group
Infinite
Instances
IsoIoo
Monoid
Monotone
OrdConnected
OrdConnectedComponent
OrderIso
Pi
ProjIcc
SurjOn
UnorderedInterval
WithBotTop
Pointwise
Basic
BigOperators
Finite
Iterate
ListOfFn
SMul
Support
Accumulate
Basic
BoolIndicator
Constructions
Countable
Enumerate
Equitable
Finite
Function
Functor
Image
Lattice
NAry
Opposite
Pairwise
Prod
Semiring
Sigma
UnionLift
SetLike
Basic
Setoid
Basic
Sigma
Basic
Lex
Order
Stream
Defs
Init
String
Defs
Lemmas
Sum
Basic
Order
Sym
Basic
Sym2
TypeVec (file)
Attr
Vector (file)
Basic
Mem
Zip
W
Basic
Constructions
ZMod
Defs
BinaryHeap
Bracket
Bundle
ByteArray
Char
Erased
FinEnum
HashMap
KVMap
Opposite
PEquiv
Part
Quot
Rel
Semiquot
Sign
Subtype
TwoPointing
UInt
ULift
UnionFind
Deprecated
Group
Ring
Subgroup
Submonoid
Dynamics
FixedPoints
Basic
PeriodicPts
GroupTheory
GroupAction
SubMulAction (file)
Pointwise
Basic
BigOperators
ConjAct
Defs
Embedding
FixingSubgroup
Group
Opposite
Option
Pi
Prod
Sigma
Sum
Support
Units
Perm
Basic
List
Support
ViaEmbedding
Subgroup
Actions
Basic
Finite
MulOpposite
Saturated
Simple
Zpowers
Submonoid
Basic
Center
Centralizer
Membership
Operations
Subsemigroup
Basic
Center
Centralizer
Membership
Operations
Archimedean
Congruence
Coset
EckmannHilton
FreeGroup
IsFreeGroup
MonoidLocalization
SemidirectProduct
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
Rat
Basic
Sigma
Basic
Subtype
Basic
Prod
Quot
Meta
WellFoundedTactics
Align
CcLemmas
Classical
Core
Function
Logic
Propext
Quot
Set
ZeroOne
Lean
Expr (file)
Basic
ReplaceRec
Traverse
Meta (file)
Simp
EnvExtension
Exception
LocalContext
Message
Logic
Embedding
Basic
Set
Encodable
Basic
Lattice
Equiv
Basic
Defs
Embedding
Fin
List
LocalEquiv
MfldSimpsAttr
Nat
Option
Set
Function
Basic
Conjugate
Iterate
Small
Basic
List
Basic
Denumerable
IsEmpty
Lemmas
Nonempty
Nontrivial
Pairwise
Relation
Relator
Unique
Mathport
Attributes
Notation
Rename
Syntax
NumberTheory
ClassNumber
AdmissibleAbsoluteValue
Divisors
FrobeniusNumber
Order
Atoms (file)
Finite
Bounds
Basic
OrderIso
ConditionallyCompleteLattice
Basic
Finset
Group
Extension
Linear
Filter
Archimedean
AtTopBot
Bases
Basic
Cofinite
CountableInter
Curry
Extr
IndicatorFunction
Interval
Lift
ModEq
NAry
Pi
Pointwise
Prod
SmallSets
Ultrafilter
Heyting
Basic
Boundary
Regular
Hom
Basic
Bounded
Order
Set
Monotone
Basic
Extension
Monovary
Odd
Union
RelIso
Basic
Group
Set
SuccPred
Basic
IntervalSucc
Limit
Relation
Antichain
Antisymmetrization
Basic
BooleanAlgebra
Bounded
BoundedOrder
Chain
Circular
Closure
Compare
CompleteBooleanAlgebra
CompleteLattice
CompleteLatticeIntervals
Concept
Copy
Cover
Directed
Disjoint
Disjointed
FixedPoints
GaloisConnection
GameAdd
Grade
InitialSeg
Iterate
Lattice
LatticeIntervals
LocallyFinite
Max
MinMax
ModularLattice
OmegaCompletePartialOrder
OrdContinuous
OrderIsoNat
PartialSups
PropInstances
RelClasses
SemiconjSup
SupIndep
SymmDiff
Synonym
WellFounded
WithBot
Zorn
ZornAtoms
RingTheory
Coprime
Basic
Lemmas
OreLocalization
OreSet
Subsemiring
Basic
Congruence
Fintype
NonZeroDivisors
Prime
RingInvo
SetTheory
Cardinal
SchroederBernstein
Tactic
Linarith (file)
Datatypes
Elimination
Frontend
Lemmas
Parsing
Preprocessing
Verification
Nontriviality (file)
Core
NormCast (file)
Tactic
NormNum (file)
Basic
Core
Positivity (file)
Basic
Core
Relation
Rfl
Symm
Trans
Ring (file)
Basic
RingNF
Sat
FromLRAT
Simps
Basic
NotationClass
Zify (file)
Attr
Abel
Alias
ApplyFun
ApplyWith
Basic
ByContra
Cache
Cases
CasesM
Choose
Classical
Clear!
ClearExcept
Clear_
Coe
Constructor
Contrapose
Conv
Convert
Core
Existsi
Expect
FinCases
Find
GeneralizeProofs
GuardGoalNums
GuardHypNums
Have
HelpCmd
InferParam
Inhabit
IntervalCases
IrreducibleDef
LeftRight
LibrarySearch
Lift
LinearCombination
MkIffOfInductiveProp
ModCases
NthRewrite
PermuteGoals
Polyrith
PrintPrefix
PushNeg
Reassoc
Recover
Rename
RenameBVar
Replace
RestateAxiom
RunCmd
ScopedNS
Set
SimpIntro
SimpRw
SolveByElim
SplitIfs
Spread
Substs
SudoSetOption
SwapVar
TagAttr
Tauto
ToAdditive
Trace
TypeCheck
UnsetOption
Use
Testing
SlimCheck
Gen
Sampleable
Testable
Topology
Bornology
Basic
Constructions
Hom
Basic
LocallyFinite
Maps
NhdsSet
Order
Util
AtomM
Export
IncludeStr
MemoFix
Simp
Syntax
SynthesizeUsing
Tactic
Time
WhatsNew
WithWeakNamespace
Std (file)
Classes
BEq
Cast
Dvd
LawfulMonad
Order
SetNotation
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
Rat (file)
Basic
Lemmas
AssocList
BinomialHeap
Char
DList
Ord
PairingHeap
String
Lean
Meta
AssertHypotheses
Basic
Clear
DiscrTree
Expr
Inaccessible
InstantiateMVars
LCtx
SavedState
UnusedNames
AttributeExtra
Command
Delaborator
Expr
HashMap
HashSet
MonadBacktrack
NameMapAttribute
Parser
PersistentHashMap
PersistentHashSet
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
HaveI
NoMatch
OpenPrivate
RCases
SeqFocus
ShowTerm
SimpTrace
Simpa
SqueezeScope
TryThis
Unreachable
Util
ExtendedBinder
LibraryNote
TermUnsafe
Logic