General documentation

index
foundational types

Library

Aesop (file)
Builder
Apply
Basic
Cases
Constructors
Default
Forward
NormSimp
Tactic
Unfold
BuiltinRules (file)
ApplyHyps
Assumption
DestructProducts
Ext
Intros
Rfl
Split
Subst
Frontend
Extension (file)
Init
Attribute
Basic
Command
RuleExpr
Saturate
Tactic
Index (file)
Basic
Options (file)
Internal
Public
Rule (file)
Basic
Name
RuleSet (file)
Filter
Member
Name
RuleTac (file)
Forward (file)
Basic
Apply
Basic
Cases
ElabRuleTerm
FVarIdSubst
GoalDiff
Preprocess
Tactic
Script
Check
CtorNames
GoalWithMVars
Main
OptimizeSyntax
SScript
ScriptM
SpecificTactics
Step
StructureDynamic
StructureStatic
Tactic
TacticState
UScript
UScriptToSScript
Util
Search
Expansion (file)
Basic
Norm
Simp
Queue (file)
Class
ExpandSafePrefix
Main
RuleSelection
SearchM
Stats
Basic
Extension
Report
Tree (file)
AddRapp
Check
Data
ExtractProof
ExtractScript
Free
RunMetaM
State
Tracing
Traversal
TreeM
UnsafeQueue
Util
Tactic (file)
Ext
Unfold
Basic
EqualUpToIds
UnionFind
UnorderedArraySet
Check
Constants
ElabM
Exception
Main
Nanos
Percent
RulePattern
Saturate
Tracing
Batteries
Classes
Order
RatCast
CodeAction (file)
Attr
Basic
Deprecated
Misc
Control
ForInStep
Basic
Lemmas
Nondet
Basic
Data
Array
Init
Lemmas
Basic
Merge
BinomialHeap
Basic
Fin
Basic
Lemmas
List
Init
Lemmas
Basic
Count
Lemmas
OfFn
Pairwise
Perm
MLList
Basic
Nat
Basic
Gcd
RBMap
Alter
Basic
WF
Rat
Basic
Lemmas
String
Basic
Sum
Basic
Lemmas
Lean
Meta
Basic
DiscrTree
Expr
Inaccessible
InstantiateMVars
SavedState
UnusedNames
AttributeExtra
Except
Expr
Float
HashSet
MonadBacktrack
NameMap
NameMapAttribute
PersistentHashMap
PersistentHashSet
Position
Syntax
TagAttribute
Linter (file)
UnnecessarySeqFocus
UnreachableTactic
Tactic
Lint (file)
Basic
Frontend
Misc
Simp
TypeClass
Alias
Basic
Classical
Congr
Exact
Init
OpenPrivate
PermuteGoals
SeqFocus
Trans
Unreachable
Where
Util
Cache
ExtendedBinder
LibraryNote
ProofWanted
Logic
WF
ImportGraph
Imports
RequiredModules
Init (file)
Control (file)
Lawful (file)
Basic
Instances
Basic
EState
Except
ExceptCps
Id
Option
Reader
State
StateCps
StateRef
Data (file)
Array (file)
Subarray (file)
Split
Attach
Basic
BasicAux
BinSearch
Bootstrap
DecidableEq
GetLit
InsertionSort
Lemmas
Mem
QSort
TakeDrop
BitVec (file)
Basic
Bitblast
Folds
Lemmas
ByteArray (file)
Basic
Char (file)
Basic
Lemmas
Fin (file)
Basic
Bitwise
Fold
Iterate
Lemmas
Log2
FloatArray (file)
Basic
Format (file)
Basic
Instances
Macro
Syntax
Int (file)
Bitwise (file)
Lemmas
Basic
DivMod
DivModLemmas
Gcd
Lemmas
LemmasAux
Order
Pow
List (file)
Nat (file)
Basic
Count
Erase
Find
Pairwise
Range
Sublist
TakeDrop
Sort (file)
Basic
Impl
Lemmas
Attach
Basic
BasicAux
Control
Count
Erase
Find
Impl
Lemmas
MinMax
Monadic
Notation
Pairwise
Perm
Range
Sublist
TakeDrop
Zip
Nat (file)
Bitwise (file)
Basic
Lemmas
Basic
Compare
Control
Div
Dvd
Gcd
Lcm
Lemmas
Linear
Log2
MinMax
Mod
Power2
SOM
Simproc
Option (file)
Attach
Basic
BasicAux
Instances
Lemmas
List
String (file)
Basic
Extra
Lemmas
ToString (file)
Basic
Macro
UInt (file)
Basic
Bitwise
Lemmas
Log2
AC
BEq
Basic
Bool
Cast
Channel
Float
Hashable
NeZero
OfScientific
Ord
PLift
Prod
Queue
Random
Range
Repr
Stream
Subtype
Sum
ULift
Zero
Grind (file)
Cases
Lemmas
Norm
Tactics
Omega (file)
Coeffs
Constraint
Int
IntList
LinearCombo
Logic
System (file)
FilePath
IO
IOError
Mutex
Platform
Promise
ST
Uri
BinderPredicates
ByCases
Classical
Coe
Conv
Core
Dynamic
Ext
GetElem
Guard
Hints
MacroTrace
Meta
MetaTypes
Notation
NotationExtra
Prelude
PropLemmas
RCases
ShareCommon
SimpLemmas
Simproc
SizeOf
SizeOfLemmas
Tactics
TacticsExtra
Util
WF
WFTactics
Lake (file)
Build (file)
Actions
Basic
Common
Data
Executable
Facets
Fetch
Imports
Index
Info
Job
Key
Library
Module
Package
Run
Store
Targets
Topological
Trace
CLI
Actions
Build
Error
Config (file)
Context
Defaults
Dependency
Env
ExternLib
ExternLibConfig
FacetConfig
Glob
InstallPath
LeanConfig
LeanExe
LeanExeConfig
LeanLib
LeanLibConfig
Module
Monad
Opaque
Package
Script
TargetConfig
Workspace
WorkspaceConfig
DSL (file)
Attributes
AttributesCore
Config
DeclUtil
Extensions
Meta
Package
Require
Script
Targets
Load
Config
Toml (file)
Data
DateTime
Dict
Value
Elab (file)
Expression
Value
Grammar
Load
ParserUtil
Util
Binder
Casing
Compare
Cycle
DRBMap
EStateT
EquipT
Error
Exit
Family
FilePath
Git
IO
JsonObject
Lift
List
Lock
Log
Message
Name
NativeLib
Opaque
OrdHashSet
OrderedTagAttribute
Proc
RBArray
Store
StoreInsts
Sugar
Task
Version
Reservoir
Version
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
Elab
FromToJson
Parser
Printer
Stream
Lsp (file)
Basic
Capabilities
Client
CodeActions
Communication
Diagnostics
Extra
InitShutdown
Internal
Ipc
LanguageFeatures
TextSync
Utf16
Workspace
Xml (file)
Basic
Parser
Array
AssocList
Format
FuzzyMatching
HashMap
HashSet
JsonRpc
KVMap
LBool
LOption
Name
NameMap
NameTrie
OpenDecl
Options
PersistentArray
PersistentHashMap
PersistentHashSet
Position
PrefixTree
RBMap
RBTree
Rat
SMap
SSet
Trie
DocString (file)
Extension
Elab (file)
Deriving (file)
BEq
Basic
DecEq
FromToJson
Hashable
Inhabited
Nonempty
Ord
Repr
SizeOf
TypeName
Util
InfoTree (file)
Main
Types
PreDefinition (file)
Nonrec
Eqns
Structural (file)
BRecOn
Basic
Eqns
FindRecArg
IndGroupInfo
IndPred
Main
Preprocess
RecArgInfo
SmartUnfolding
WF (file)
Basic
Eqns
Fix
GuessLex
Ite
Main
PackMutual
Preprocess
Rel
Basic
EqUnfold
Eqns
Main
MkInhabitant
TerminationArgument
TerminationHint
Quotation (file)
Precheck
Util
Tactic (file)
BVDecide (file)
Frontend (file)
BVDecide (file)
Reflect
ReifiedBVExpr
ReifiedBVLogical
ReifiedBVPred
SatAtBVLogical
Attr
BVCheck
BVTrace
LRAT
Normalize
LRAT (file)
Trim
External
Conv (file)
Basic
Change
Congr
Delta
Pattern
Rewrite
Simp
Unfold
Omega (file)
Core
Frontend
MinNatAbs
OmegaM
Basic
BoolToPropSimps
BuiltinTactic
Cache
Calc
Change
Config
Congr
Delta
DiscrTreeKey
Doc
ElabTerm
Ext
FalseOrByContra
Generalize
Guard
Induction
Injection
LibrarySearch
Location
Match
Meta
NormCast
RCases
Repeat
Rewrite
Rewrites
Rfl
ShowTerm
Simp
SimpTrace
Simpa
Simproc
SolveByElim
Split
Symm
Unfold
App
Arg
Attributes
AutoBound
AuxDef
BinderPredicates
Binders
BindersUtil
BuiltinCommand
BuiltinNotation
BuiltinTerm
Calc
CheckTactic
Command
ComputedFields
Config
DeclModifiers
DeclNameGen
DeclUtil
Declaration
DeclarationRange
DefView
Do
ElabRules
Eval
Exception
Extra
Frontend
GenInjective
GuardMsgs
Import
Inductive
InheritDoc
LetRec
Level
Macro
MacroArgUtil
MacroRules
Match
MatchAltView
MatchExpr
Mixfix
MutualDef
Notation
Open
ParseImportsFast
PatternVar
Print
RecAppSyntax
SetOption
StructInst
Structure
Syntax
SyntheticMVars
Term
Time
Util
Language
Lean (file)
Types
Basic
Linter (file)
Basic
Builtin
ConstructorAsVariable
Deprecated
MissingDocs
Omit
UnusedVariables
Util
Meta (file)
ArgsPacker (file)
Basic
Constructions (file)
BRecOn
CasesOn
NoConfusion
RecOn
Match (file)
MatcherApp
Basic
Transform
Basic
CaseArraySizes
CaseValues
Match
MatchEqs
MatchEqsExt
MatchPatternAttr
MatcherInfo
Value
Tactic (file)
AC (file)
Main
Grind (file)
Attr
Cases
Core
Injection
Preprocessor
RevertAll
Types
Util
LinearArith (file)
Nat (file)
Basic
Simp
Solver
Basic
Main
Simp
Solver
Simp (file)
BuiltinSimprocs (file)
Array
BitVec
Char
Core
Fin
Int
List
Nat
String
UInt
Util
Attr
Diagnostics
Main
RegisterCommand
Rewrite
SimpAll
SimpCongrTheorems
SimpTheorems
Simproc
Types
Acyclic
Apply
Assert
Assumption
AuxLemma
Backtrack
Cases
Cleanup
Clear
Congr
Constructor
Contradiction
Delta
ElimInfo
FVarSubst
FunInd
Generalize
IndependentOf
Induction
Injection
Intro
LibrarySearch
NormCast
Refl
Rename
Repeat
Replace
Revert
Rewrite
Rewrites
Rfl
SolveByElim
Split
SplitIf
Subst
Symm
TryThis
Unfold
UnifyEq
Util
ACLt
AbstractMVars
AbstractNestedProofs
AppBuilder
Basic
Canonicalizer
Check
CheckTactic
Closure
Coe
CoeAttr
CollectFVars
CollectMVars
CompletionName
CongrTheorems
CtorRecognizer
DecLevel
Diagnostics
DiscrTree
DiscrTreeTypes
Eqns
Eval
ExprDefEq
ExprLens
ExprTraverse
ForEachExpr
FunInfo
GeneralizeTelescope
GeneralizeVars
GetUnfoldableConst
GlobalInstances
IndPredBelow
Inductive
InferType
Injective
Instances
Iterator
KAbstract
KExprMap
LazyDiscrTree
LevelDefEq
LitValues
MatchUtil
NatInstTesters
Offset
PPGoal
PProdN
RecursorInfo
Reduce
ReduceEval
SizeOf
Structure
SynthInstance
Transform
TransparencyMode
UnificationHint
WHNF
Parser (file)
Tactic (file)
Doc
Attr
Basic
Command
Do
Extension
Extra
Level
Module
StrInterpolation
Syntax
Term
Types
ParserCompiler (file)
Attribute
PrettyPrinter (file)
Delaborator (file)
Attributes
Basic
Builtins
FieldNotation
Options
SubExpr
TopDownAnalyze
Basic
Formatter
Parenthesizer
Server (file)
CodeActions (file)
Attr
Basic
Provider
FileWorker (file)
RequestHandling
SetupFile
Utils
WidgetRequests
Rpc (file)
Basic
Deriving
RequestHandling
AsyncList
Completion
CompletionItemData
FileSource
GoTo
ImportCompletion
InfoUtils
References
Requests
Snapshots
Utils
Watchdog
Util (file)
CollectAxioms
CollectFVars
CollectLevelMVars
CollectLevelParams
CollectMVars
Diff
FileSetupInfo
FindExpr
FindLevelMVar
FindMVar
FoldConsts
ForEachExpr
ForEachExprWhere
HasConstCache
Heartbeats
InstantiateLevelParams
LakePath
LeanOptions
MonadBacktrack
MonadCache
NumApps
NumObjs
OccursCheck
PPExt
Path
Paths
Profile
Profiler
PtrSet
RecDepth
Recognizers
ReplaceExpr
ReplaceLevel
SCC
SafeExponentiation
SearchPath
ShareCommon
Sorry
TestExtern
Trace
Widget (file)
Basic
Diff
InteractiveCode
InteractiveDiagnostic
InteractiveGoal
TaggedText
Types
UserWidget
AddDecl
Attributes
AuxRecursor
BuiltinDocAttr
Class
CoreM
Declaration
DeclarationRange
Environment
Eval
Exception
Expr
HeadIndex
Hygiene
ImportingFlag
InternalExceptionId
KeyedDeclsAttribute
LabelAttribute
LazyInitExtension
Level
LoadDynlib
LocalContext
Log
Message
MetavarContext
Modifiers
MonadEnv
ProjFns
ReducibilityAttrs
ReservedNameAction
ResolveName
Runtime
ScopedEnvExtension
Structure
SubExpr
Syntax
ToExpr
LeanSearchClient (file)
Basic
LoogleSyntax
Syntax
Mathlib
Algebra
Algebra
Subalgebra
Basic
Operations
Prod
Tower
Basic
Bilinear
Defs
Equiv
Hom
NonUnitalHom
Operations
Opposite
Pi
Prod
Rat
RestrictScalars
Tower
Associated
Basic
BigOperators
Group
Finset
List
Multiset
GroupWithZero
Action
Finset
Ring (file)
List
Multiset
Associated
Expect
Fin
Finprod
Finsupp
Intervals
NatAntidiagonal
Option
Pi
RingEquiv
WithTop
Category
Grp
Basic
ForgetCorepresentable
Injective
Limits
Preadditive
ZModuleEquivalence
ModuleCat
Basic
EpiMono
Injective
MonCat
Basic
Limits
Ring
Basic
Colimits
Constructions
Instances
Limits
CharP
Algebra
Basic
Defs
ExpChar
Lemmas
Two
CharZero
Defs
Lemmas
DirectSum
Basic
Finsupp
Module
Divisibility
Basic
Units
EuclideanDomain
Basic
Defs
Field
Int
Field
Basic
Defs
Equiv
IsField
Opposite
Rat
Subfield
FreeMonoid
Basic
GCDMonoid
Basic
Finset
Multiset
Group
Action
Basic
Defs
End
Faithful
Opposite
Pi
Pretransitive
Prod
TypeTags
Units
Commute
Basic
Defs
Hom
Units
Equiv
Basic
Fin
Basic
Tuple
Hom
Basic
CompTypeclasses
Defs
End
Instances
Invertible
Basic
Defs
Pi
Basic
Lemmas
Pointwise
Finset
Basic
Set
Basic
Semiconj
Basic
Defs
Units
Subgroup
Actions
Basic
Defs
Finite
MulOpposite
Order
Pointwise
ZPowers
Submonoid
Basic
Defs
DistribMulAction
Membership
MulOpposite
Operations
Pointwise
Subsemigroup
Basic
Defs
Membership
Operations
UniqueProds
Basic
Units (file)
Basic
Defs
Equiv
Hom
WithOne
Defs
Aut
Basic
Center
Commutator
Conj
Defs
Embedding
Even
Ext
FiniteSupport
Indicator
InjSurj
Int
Nat
NatPowAssoc
Opposite
Prod
Support
TypeTags
ULift
ZeroOne
GroupPower
IterateHom
GroupWithZero
Action
Basic
Defs
End
Opposite
Pi
Prod
Units
Units
Basic
Equiv
Lemmas
Basic
Center
Commute
Defs
Divisibility
Hom
Indicator
InjSurj
Invertible
NeZero
NonZeroDivisors
Opposite
Pi
Prod
Semiconj
ULift
WithZero
Module
Equiv
Basic
Defs
Opposite
LinearMap
Defs
End
Star
Submodule
Basic
Bilinear
EqLocus
Equiv
IterateMapComap
Ker
Lattice
LinearMap
Localization
Map
Pointwise
Range
RestrictScalars
Basic
BigOperators
CharacterModule
Defs
End
FinitePresentation
Hom
Injective
LocalizedModule
LocalizedModuleIntegers
Opposite
Opposites
Pi
Prod
Projective
Rat
ULift
MonoidAlgebra
Basic
Defs
Degree
Division
NoZeroDivisors
Support
MvPolynomial
Basic
CommRing
Degrees
Equiv
Rename
Variables
NoZeroSMulDivisors
Basic
Defs
Order
Antidiag
Prod
Archimedean
Basic
BigOperators
Group
Finset
List
Multiset
Ring
Finset
List
Multiset
CauSeq
Basic
Completion
Field
Canonical
Basic
Defs
Basic
Defs
InjSurj
Power
Rat
Group
Pointwise
Bounds
Unbundled
Abs
Basic
Int
Abs
Action
Basic
Defs
InjSurj
Instances
Lattice
MinMax
Nat
OrderIso
PiLex
PosPart
Synonym
Units
GroupWithZero
Action
Synonym
Unbundled (file)
Lemmas
Canonical
Synonym
Hom
Basic
Monoid
Ring
Interval
Set
Group
Instances
Monoid
Finset
Module
Defs
OrderedSMul
Pointwise
Monoid
Canonical
Defs
Unbundled
Basic
Defs
ExistsOfLE
MinMax
OrderDual
Pow
TypeTags
WithTop
Basic
Defs
NatCast
OrderDual
Prod
TypeTags
Units
WithTop
Nonneg
Field
Floor
Ring
Positive
Ring
Ring
Unbundled
Basic
Nonneg
Rat
Abs
Basic
Canonical
Cast
Defs
InjSurj
Int
Nat
Pow
Rat
WithTop
Sub
Unbundled
Basic
Basic
Defs
WithTop
AbsoluteValue
AddGroupWithTop
Floor
Invertible
Kleene
Pi
SuccPred
ToIntervalMod
ZeroLEOne
PUnitInstances
Algebra
Module
Polynomial
Degree
Definitions
Lemmas
TrailingDegree
AlgebraMap
Basic
BigOperators
CancelLeads
Coeff
Derivative
Div
EraseLead
Eval
FieldDivision
Induction
Inductions
Monic
Monomial
Reverse
RingDivision
Roots
Prime
Defs
Lemmas
Regular
Basic
Pow
SMul
Ring
Action
Basic
Group
Subobjects
Divisibility
Basic
Hom
Basic
Defs
Pointwise
Set
Subring
Basic
Subsemiring
Basic
AddAut
Aut
Basic
Center
Centralizer
Commute
CompTypeclasses
Defs
Equiv
Fin
Idempotents
InjSurj
Int
Invertible
Nat
NegOnePow
Opposite
Parity
Pi
Prod
Rat
Regular
Semiconj
ULift
Units
Star
Basic
BigOperators
Module
Pi
Prod
Rat
SelfAdjoint
AddTorsor
Exact
FreeAlgebra
GeomSum
ModEq
NeZero
Notation
Opposites
Periodic
Quotient
SMulWithZero
CategoryTheory
Adjunction
Basic
FullyFaithful
Limits
Bicategory
Basic
Strict
Category
Basic
Cat
Init
Preorder
ULift
Comma
StructuredArrow (file)
Basic
Arrow
Basic
Over
ConcreteCategory
Basic
Bundled
BundledHom
EpiMono
ReflectsIso
Filtered
Basic
FinCategory
AsType
Basic
Functor
Basic
Category
Const
Currying
EpiMono
FullyFaithful
Hom
ReflectsIso
LiftingProperties
Adjunction
Basic
Limits
ConcreteCategory
Basic
Constructions
EpiMono
FunctorCategory
Basic
Preserves
Shapes
BinaryProducts
Biproducts
Products
Pullbacks
Terminal
Zero
Basic
Finite
Limits
Shapes
Pullback
Cospan
HasPullback
Iso
Mono
PullbackCone
BinaryProducts
Biproducts
Equalizers
FiniteLimits
FiniteProducts
Images
IsTerminal
Kernels
Products
StrictInitial
StrongEpi
Terminal
WidePullbacks
ZeroMorphisms
ZeroObjects
Cones
Creates
ExactFunctor
Filtered
HasLimits
IsLimit
Opposites
Types
TypesFiltered
Yoneda
Linear
Basic
MorphismProperty
Basic
Composition
Concrete
Factorization
Pi
Basic
Preadditive
AdditiveFunctor
Basic
Biproducts
FunctorCategory
Injective
Projective
Products
Basic
Unitor
Balanced
CommSq
Conj
DiscreteCategory
Endomorphism
EpiMono
EqToHom
Equivalence
EssentialImage
EssentiallySmall
FullSubcategory
Groupoid
HomCongr
Iso
IsomorphismClasses
NatIso
NatTrans
Opposites
PEmpty
PUnit
Skeletal
Thin
Types
Whiskering
Yoneda
Combinatorics
Quiver
Basic
Path
Push
Symmetric
Control
Monad
Basic
Traversable
Basic
Applicative
Basic
Combinators
EquivFunctor
Functor
ULift
Data
Array
Defs
Bool
Basic
Set
Countable
Basic
Defs
DFinsupp
Basic
Encodable
Lex
NeLocus
Order
ENNReal
Basic
Inv
Lemmas
Operations
Real
ENat
Basic
Lattice
Fin
Tuple
Basic
Basic
VecNotation
Finite
Basic
Card
Defs
Powerset
Prod
Set
Sigma
Sum
Vector
Finset
Attr
Basic
Card
Density
Fold
Image
Lattice
Max
NAry
NatAntidiagonal
NoncommProd
Option
Order
Pairwise
Pi
Piecewise
Powerset
Preimage
Prod
Sigma
Sort
Sum
Sym
Union
Finsupp
Antidiagonal
Basic
Defs
Encodable
Fin
Fintype
Indicator
Lex
Multiset
Order
ToDFinsupp
Fintype
Basic
BigOperators
Card
Fin
Lattice
List
Option
Pi
Powerset
Prod
Quotient
Sigma
Sum
Units
Vector
FunLike
Basic
Embedding
Equiv
Int
Cast
Basic
Defs
Field
Lemmas
Prod
Order
Basic
Lemmas
Units
Bitwise
CharZero
ConditionallyCompleteOrder
Defs
DivMod
GCD
Interval
LeastGreatest
Lemmas
ModEq
Notation
Sqrt
SuccPred
List
Perm (file)
Basic
Lattice
Subperm
Basic
Chain
Count
Cycle
Dedup
Defs
Duplicate
FinRange
Forall2
GetD
Indexes
Infix
InsertIdx
InsertNth
Join
Lattice
Lex
MinMax
Monad
NatAntidiagonal
Nodup
NodupEquivFin
OfFn
Pairwise
Palindrome
Permutation
Prime
ProdSigma
Range
Rotate
Sort
Sublists
Sym
TFAE
Zip
Matrix
Basic
Basis
Block
Notation
RowCol
Multiset
Antidiagonal
Basic
Bind
Dedup
FinsetOps
Fold
Lattice
NatAntidiagonal
Nodup
OrderedMonoid
Pi
Powerset
Range
Sections
Sort
Sum
Sym
NNRat
Defs
Lemmas
Order
NNReal
Basic
Defs
Nat
Cast
Order
Basic
Field
Ring
Basic
Commute
Defs
Field
NeZero
Prod
WithTop
Choose
Basic
Sum
Factorial
Basic
Factorization
Basic
Defs
Induction
GCD
Basic
BigOperators
Order
Lemmas
Prime
Basic
Defs
Infinite
BinaryRec
Bits
Bitwise
Count
Defs
Digits
Factors
Find
Lattice
Log
ModEq
Multiplicity
Notation
Pairing
PartENat
Periodic
PrimeFin
Set
Size
Sqrt
SuccPred
Totient
WithBot
Option
Basic
Defs
NAry
Ordering
Basic
PNat
Basic
Defs
Equiv
Prod
Basic
Lex
PProd
Rat
Cast
CharZero
Defs
Lemmas
Order
BigOperators
Defs
Floor
Init
Lemmas
Real
Archimedean
Basic
Pointwise
Star
Set
Pairwise
Basic
Pointwise
BigOperators
Finite
Interval
ListOfFn
SMul
Accumulate
Basic
BoolIndicator
Card
Constructions
Countable
Defs
Finite
Function
Functor
Image
Lattice
List
Monotone
NAry
Notation
Operations
Prod
Semiring
Sigma
Subset
Subsingleton
SymmDiff
UnionLift
SetLike
Basic
Setoid
Basic
Sigma
Basic
Lex
String
Defs
Sum
Basic
Order
Sym
Sym2 (file)
Init
Order
Basic
Tree
Basic
Vector
Basic
Defs
ZMod
Basic
Defs
IntUnitsPower
Bracket
Opposite
Part
Quot
SProd
Subtype
TypeMax
ULift
Dynamics
FixedPoints
Basic
PeriodicPts
GroupTheory
Commutator
Basic
Congruence
Basic
Defs
Hom
Opposite
Coset
Basic
Card
Defs
GroupAction
DomAct
Basic
SubMulAction (file)
Pointwise
Basic
ConjAct
Defs
Hom
Quotient
Ring
MonoidLocalization
Away
Basic
MonoidWithZero
OreLocalization
Basic
OreSet
Perm
Basic
QuotientGroup
Basic
Defs
Finite
Subgroup
Center
Centralizer
Submonoid
Center
Centralizer
Subsemigroup
Center
Centralizer
Archimedean
Divisible
Finiteness
Index
OrderOfElement
Init (file)
Algebra
Classes
Logic
Lean
Elab
Tactic
Basic
Term
Expr
Basic
ExtraRecognizers
Rat
ReplaceRec
Meta (file)
Basic
CongrTheorems
Simp
PrettyPrinter
Delaborator
EnvExtension
Name
LinearAlgebra
Basis
Basic
Cardinality
Defs
DirectSum
Finsupp
TensorProduct
FreeModule
Finite
Basic
Basic
Matrix
ToLin
Trace
TensorProduct
Basic
Basis
RightExactness
Tower
BilinearMap
DFinsupp
Finsupp
FinsuppVectorSpace
Isomorphisms
LinearIndependent
LinearPMap
Pi
Prod
Quotient
Span
StdBasis
Logic
Embedding
Basic
Set
Encodable
Basic
Equiv
Basic
Defs
Fin
List
Nat
Option
PartialEquiv
Set
TransferInstance
Function
Basic
CompTypeclasses
Conjugate
Defs
Iterate
ULift
Nontrivial
Basic
Defs
Small
Basic
Defs
Set
Basic
Denumerable
ExistsUnique
IsEmpty
Lemmas
Nonempty
OpClass
Pairwise
Relation
Relator
Unique
UnivLE
NumberTheory
Padics
PadicVal
Defs
Divisors
Order
Bounds
Basic
Defs
Image
OrderIso
CompactlyGenerated
Basic
CompleteLattice (file)
Finset
ConditionallyCompleteLattice
Basic
Finset
Group
Indexed
Filter
AtTopBot (file)
Archimedean
Field
Group
Monoid
Ring
Bases
Basic
Cofinite
CountableInter
Curry
Defs
EventuallyConst
Extr
Interval
Ker
Lift
NAry
Pi
Pointwise
Prod
SmallSets
Subsingleton
Tendsto
Ultrafilter
Fin
Basic
Heyting
Basic
Hom
Basic
Bounded
CompleteLattice
Lattice
Order
Set
Interval
Finset
Basic
Defs
Fin
Nat
Set
Basic
Disjoint
Image
Infinite
OrdConnected
OrderEmbedding
OrderIso
Pi
ProjIcc
UnorderedInterval
WithBotTop
Multiset
Monotone
Basic
RelIso
Basic
Set
SuccPred
Archimedean
Basic
CompleteLinearOrder
Limit
Relation
UpperLower
Basic
Antichain
Antisymmetrization
Atoms
Basic
BooleanAlgebra
Bounded
BoundedOrder
Chain
Circular
Closure
Compare
CompleteBooleanAlgebra
CompleteLatticeIntervals
Copy
Cover
Defs
Directed
Disjoint
FixedPoints
GaloisConnection
InitialSeg
Iterate
Lattice
LatticeIntervals
Max
MinMax
Minimal
ModularLattice
Nat
Notation
OmegaCompletePartialOrder
OrderIsoNat
Part
PartialSups
PiLex
PropInstances
RelClasses
ScottContinuity
SetNotation
SupClosed
SupIndep
SymmDiff
Synonym
TypeTags
ULift
WellFounded
WellFoundedSet
WithBot
Zorn
ZornAtoms
RingTheory
Adjoin
Basic
Congruence
Basic
Defs
Opposite
Coprime
Basic
Lemmas
Flat
Basic
Stability
Ideal
Basic
Colon
Defs
IsPrimary
Lattice
Maps
Maximal
Operations
Prime
Quotient
QuotientOperations
Span
LocalProperties
Basic
LocalRing
MaximalIdeal
Basic
Defs
RingHom
Basic
Defs
Basic
Defs
Localization
Away
Basic
Algebra
AtPrime
BaseChange
Basic
Defs
Finiteness
FractionRing
Ideal
Integer
Module
Submodule
Nilpotent
Defs
Lemmas
NonUnitalSubring
Basic
NonUnitalSubsemiring
Basic
OreLocalization
Basic
OreSet
Ring
Polynomial
Basic
Content
Quotient
RingHom
Finite
TensorProduct
Basic
TwoSidedIdeal
Basic
Lattice
Operations
AlgebraTower
EuclideanDomain
Finiteness
IsPrimary
IsTensorProduct
JacobsonIdeal
Multiplicity
Noetherian
OrzechProperty
PrincipalIdealDomain
RingHomProperties
UniqueFactorizationDomain
SetTheory
Cardinal
Aleph
Arithmetic
Basic
Cofinality
ENat
Finite
Ordinal
PartENat
SchroederBernstein
ToNat
UnivLE
Ordinal
Arithmetic
Basic
Enum
Exponential
FixedPoint
Principal
Tactic
Attr
Core
Register
Bound
Attribute
Init
CC (file)
Addition
Datatypes
Lemmas
CancelDenoms
Core
CategoryTheory
Reassoc
Slice
Continuity (file)
Init
Finiteness
Attr
FunProp (file)
Attr
Core
Decl
Elab
FunctionData
Mor
RefinedDiscrTree
StateList
Theorems
ToBatteries
Types
GCongr (file)
Core
CoreAttrs
ForwardAttr
Linarith (file)
Oracle
SimplexAlgorithm (file)
Datatypes
Gauss
PositiveVector
SimplexAlgorithm
Datatypes
Frontend
Lemmas
Parsing
Preprocessing
Verification
LinearCombination (file)
Lemmas
Linter (file)
DocPrime
FlexibleLinter
GlobalAttributeIn
HashCommandLinter
HaveLetLinter
Header
Lint
MinImports
Multigoal
OldObtain
PPRoundtrip
RefineLinter
Style
TextBased
UnusedTactic
Monotonicity
Attr
Basic
Nontriviality (file)
Core
NormNum (file)
Basic
Core
DivMod
Eq
Ineq
Inv
OfScientific
Pow
Result
Positivity (file)
Basic
Core
Relation
Rfl
Symm
Trans
Ring (file)
Basic
PNat
RingNF
Simps
Basic
NotationClass
ToAdditive (file)
Frontend
Widget
Calc
CongrM
Conv
SelectInsertParamsClass
SelectPanelUtils
Abel
AdaptationNote
Algebraize
ApplyAt
ApplyCongr
ApplyFun
ApplyWith
Basic
ByContra
Cases
CasesM
Check
Choose
ClearExcept
ClearExclamation
Clear_
Coe
Common
ComputeDegree
CongrExclamation
CongrM
Constructor
Contrapose
Conv
Convert
Core
DeclarationNames
DefEqTransformations
DeprecateMe
DeriveToExpr
Eqns
ExistsI
ExtendDoc
ExtractGoal
ExtractLets
FBinop
FailIfNoProgress
FieldSimp
FinCases
Find
GeneralizeProofs
Group
GuardGoalNums
GuardHypNums
HaveI
HelpCmd
HigherOrder
Hint
InferParam
Inhabit
IntervalCases
IrreducibleDef
Lemma
Lift
MinImports
MkIffOfInductiveProp
Module
NoncommRing
NthRewrite
Observe
PPWithUniv
ProjectionNotation
Propose
PushNeg
RSuffices
Recover
Rename
RenameBVar
Says
ScopedNS
Set
SetLike
SimpIntro
SimpRw
SplitIfs
Spread
StacksAttribute
Subsingleton
Substs
SuccessIfFailWithMsg
SudoSetOption
SuppressCompilation
SwapVar
TFAE
Tauto
TermCongr
ToExpr
ToLevel
Trace
TryThis
TypeCheck
TypeStar
UnsetOption
Use
Variable
WLOG
Zify
Topology
Algebra
Group
Basic
Quotient
Order
Archimedean
Compact
Field
Group
Ring
Basic
UniformGroup (file)
Basic
Defs
ConstMulAction
Constructions
Field
GroupWithZero
Monoid
MulAction
Star
UniformMulAction
Bornology
Basic
Constructions
Compactness
Compact
Lindelof
LocallyCompact
SigmaCompact
Connected
Basic
Clopen
LocallyConnected
PathConnected
TotallyDisconnected
ContinuousMap
Basic
Defs
Defs
Basic
Filter
Induced
Sequences
EMetricSpace
Basic
Defs
Diam
Pi
Hom
ContinuousEval
ContinuousEvalConst
Instances
AddCircle
Discrete
Int
Real
ZMultiples
Maps
Basic
OpenQuotient
MetricSpace
Pseudo
Basic
Constructions
Defs
Lemmas
Pi
Basic
Bounded
Cauchy
Defs
ProperSpace
Metrizable
Basic
Order (file)
Basic
Bornology
Compact
DenselyOrdered
IntermediateValue
IsLUB
LeftRight
LeftRightNhds
LocalExtr
Monotone
OrderClosed
ProjIcc
Separation (file)
Basic
Sets
Opens
UniformSpace
AbstractCompletion
Basic
Cauchy
Compact
CompleteSeparated
Completion
Equicontinuity
Equiv
OfFun
Pi
Separation
UniformConvergence
UniformConvergenceTopology
UniformEmbedding
Bases
Basic
Clopen
CompactOpen
Constructions
ContinuousOn
DenseEmbedding
DiscreteSubset
GDelta
Homeomorph
Inseparable
Irreducible
IsLocalHomeomorph
LocallyFinite
NhdsSet
PartialHomeomorph
RestrictGen
SeparatedMap
Support
UnitInterval
Util
AddRelatedDecl
AssertExists
AssertExistsExt
AtomM
CompileInductive
CountHeartbeats
Delaborators
DischargerAsTactic
MemoFix
Notation3
Qq
SynthesizeUsing
Tactic
WhatsNew
WithWeakNamespace
ModuleLocalProperties (file)
MissingLemmas
FlatIff
LocalizaedIsTensorProduct
LocalizedModule
Range
Submodule
TensorProduct
Units
Basic
Defs
FinitePresentation
Flat
Isom
SpanIsom
ProofWidgets
Component
Basic
MakeEditLink
OfRpcMethod
Data
Html
Cancellable
Compat
Util
Qq (file)
ForLean
Do
ReduceEval
ToExpr
AssertInstancesCommute
Delab
Macro
Match
MetaM
SortLocalDecls
Typ
Std (file)
Data (file)
DHashMap (file)
Internal
AssocList
Basic
Lemmas
List
Associative
Defs
HashesTo
Pairwise
Sublist
Defs
Index
Model
Raw
RawLemmas
WF
AdditionalOperations
Basic
Lemmas
Raw
RawDef
RawLemmas
HashMap (file)
AdditionalOperations
Basic
Lemmas
Raw
RawLemmas
HashSet (file)
Basic
Lemmas
Raw
RawLemmas
Internal (file)
Parsec (file)
Basic
ByteArray
String
Sat (file)
AIG (file)
RefVecOperator (file)
Fold
Map
Zip
Basic
CNF
Cached
CachedGates
CachedGatesLemmas
CachedLemmas
If
LawfulOperator
LawfulVecOperator
Lemmas
RefVec
Relabel
RelabelNat
CNF (file)
Basic
Dimacs
Literal
Relabel
RelabelFin
Tactic (file)
BVDecide (file)
Bitblast (file)
BVExpr (file)
Circuit (file)
Impl (file)
Operations
Add
Append
Eq
Extract
GetLsbD
Mul
Not
Replicate
RotateLeft
RotateRight
ShiftLeft
ShiftRight
SignExtend
Ult
ZeroExtend
Carry
Const
Expr
Pred
Var
Lemmas (file)
Operations
Add
Append
Eq
Extract
GetLsbD
Mul
Not
Replicate
RotateLeft
RotateRight
ShiftLeft
ShiftRight
SignExtend
Ult
ZeroExtend
Basic
Carry
Const
Expr
Pred
Var
Basic
BoolExpr (file)
Basic
Circuit
LRAT (file)
Internal
Formula (file)
Class
Implementation
Instance
Lemmas
RatAddResult
RatAddSound
RupAddResult
RupAddSound
Actions
Assignment
CNF
Clause
Convert
Entails
LRATChecker
LRATCheckerSound
PosFin
Actions
Checker
Parser
Normalize (file)
BitVec
Bool
Canonicalize
Equal
Prop
Reflect
Syntax

Color scheme