General documentation

index
foundational types

Library

Aesop (file)
Builder (file)
Apply
Basic
Cases
Constructors
Default
Forward
NormSimp
Tactic
Unfold
BuiltinRules (file)
ApplyHyps
Assumption
DestructProducts
Ext
Intros
Split
Subst
Check
Constants
Frontend (file)
Attribute
Basic
Command
ElabM
Extension (file)
Init
RuleExpr
Tactic
Index (file)
Basic
Main
Nanos
Options (file)
Internal
Public
Percent
Profiling
Rule (file)
Basic
Name
RuleSet
RuleTac (file)
Apply
Basic
Cases
Forward
Preprocess
Tactic
Script
Search
ExpandSafePrefix
Expansion (file)
Basic
Norm
Simp
Main
Queue (file)
Class
RuleSelection
SearchM
Tracing
Tree (file)
AddRapp
Check
Data
ExtractProof
ExtractScript
Free
RunMetaM
State
Tracing
Traversal
TreeM
UnsafeQueue
Util
Basic
EqualUpToIds
Tactic
UnionFind
UnorderedArraySet
Bookshelf (file)
Apostol (file)
Chapter_1_11
Chapter_I_03
🗎 Apostol (pdf)
Avigad (file)
Chapter_2
Chapter_3
Chapter_4
Chapter_5
Chapter_7
Chapter_8
Enderton (file)
Logic (file)
Chapter_1
🗎 Logic (pdf)
Set (file)
Chapter_1
Chapter_2
Chapter_3
Chapter_4
Chapter_6
OrderedPair
Relation
Fraleigh (file)
Chapter_1
Smullyan (file)
Aviary
Common (file)
List (file)
Basic
NonEmpty
Logic (file)
Basic
Nat (file)
Basic
Real (file)
Floor
Sequence (file)
Arithmetic
Geometric
🗎 Sequence (pdf)
Set (file)
Basic
Equinumerous
Function
Intervals
Peano
Init (file)
Classical
Coe
Control (file)
Basic
EState
Except
ExceptCps
Id
Lawful
Option
Reader
State
StateCps
StateRef
Conv
Core
Data (file)
AC
Array (file)
Basic
BasicAux
BinSearch
DecidableEq
InsertionSort
Mem
QSort
Subarray
Basic
ByteArray (file)
Basic
Channel
Char (file)
Basic
Fin (file)
Basic
Log2
Float
FloatArray (file)
Basic
Format (file)
Basic
Instances
Macro
Syntax
Hashable
Int (file)
Basic
List (file)
Basic
BasicAux
Control
Nat (file)
Basic
Bitwise
Control
Div
Gcd
Linear
Log2
Power2
SOM
OfScientific
Option (file)
Basic
BasicAux
Instances
Ord
Prod
Queue
Random
Range
Repr
Stream
String (file)
Basic
Extra
ToString (file)
Basic
Macro
UInt (file)
Basic
Log2
Dynamic
Hints
Meta
MetaTypes
Notation
NotationExtra
Prelude
ShareCommon
SimpLemmas
SizeOf
SizeOfLemmas
System (file)
FilePath
IO
IOError
Mutex
Platform
Promise
ST
Uri
Tactics
Util
WF
WFTactics
Lake (file)
Build (file)
Actions
Common
Context
Data
Executable
Facets
Imports
Index
Info
Job
Key
Library
Module
Monad
Package
Store
Targets
Topological
Trace
CLI
Actions
Config (file)
Context
Dependency
Env
ExternLib
ExternLibConfig
FacetConfig
Glob
InstallPath
LeanConfig
LeanExe
LeanExeConfig
LeanLib
LeanLibConfig
Module
Monad
Opaque
Package
Script
TargetConfig
Workspace
WorkspaceConfig
DSL (file)
Attributes
Config
DeclUtil
Extensions
Meta
Package
Require
Script
Targets
Load
Config
Util
Async
Binder
Casing
Compare
Cycle
DRBMap
EStateT
EquipT
Error
Exit
Family
Git
Lift
List
Log
Name
NativeLib
Opaque
OptionIO
OrdHashSet
OrderedTagAttribute
Platform
Proc
RBArray
Store
StoreInsts
Sugar
Task
Version
Lean (file)
Attributes
AuxRecursor
Class
Compiler (file)
AtMostOnce
BorrowedAnnotation
CSimpAttr
ClosedTermCache
ConstFolding
ExportAttr
ExternAttr
FFI
IR (file)
Basic
Borrow
Boxing
Checker
CompilerM
CtorLayout
ElimDeadBranches
ElimDeadVars
EmitC
EmitUtil
ExpandResetReuse
Format
FreeVars
LiveVars
NormIds
PushProj
RC
ResetReuse
SimpCase
Sorry
UnboxResult
ImplementedByAttr
InitAttr
InlineAttrs
LCNF (file)
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
Simp (file)
Basic
Config
ConstantFold
DefaultAlt
DiscrM
FunDeclInfo
InlineCandidate
InlineProj
JpCases
Main
SimpM
SimpValue
Used
SpecInfo
Specialize
Testing
ToDecl
ToExpr
ToLCNF
ToMono
Types
Util
Main
NameMangling
NeverExtractAttr
NoncomputableAttr
Old
Options
Specialize
CoreM
Data (file)
AssocList
Format
FuzzyMatching
HashMap
HashSet
Json (file)
Basic
FromToJson
Parser
Printer
Stream
JsonRpc
KVMap
LBool
LOption
Lsp (file)
Basic
Capabilities
Client
CodeActions
Communication
Diagnostics
Extra
InitShutdown
Internal
Ipc
LanguageFeatures
TextSync
Utf16
Workspace
Name
NameMap
NameTrie
OpenDecl
Options
Parsec
PersistentArray
PersistentHashMap
PersistentHashSet
Position
PrefixTree
RBMap
RBTree
Rat
SMap
SSet
Trie
Xml (file)
Basic
Parser
Declaration
DeclarationRange
DocString
Elab (file)
App
Arg
Attributes
AutoBound
AuxDef
Binders
BindersUtil
BuiltinCommand
BuiltinNotation
BuiltinTerm
Calc
Command
ComputedFields
Config
DeclModifiers
DeclUtil
Declaration
DeclarationRange
DefView
Deriving (file)
BEq
Basic
DecEq
FromToJson
Hashable
Inhabited
Nonempty
Ord
Repr
SizeOf
TypeName
Util
Do
ElabRules
Eval
Exception
Extra
Frontend
GenInjective
Import
Inductive
InfoTree (file)
Main
Types
InheritDoc
LetRec
Level
Macro
MacroArgUtil
MacroRules
Match
MatchAltView
Mixfix
MutualDef
Notation
Open
ParseImportsFast
PatternVar
PreDefinition (file)
Basic
Eqns
Main
MkInhabitant
Structural (file)
BRecOn
Basic
Eqns
FindRecArg
IndPred
Main
Preprocess
SmartUnfolding
WF (file)
Eqns
Fix
Ite
Main
PackDomain
PackMutual
Rel
TerminationHint
Print
Quotation (file)
Precheck
Util
RecAppSyntax
SetOption
StructInst
Structure
Syntax
SyntheticMVars
Tactic (file)
Basic
BuiltinTactic
Cache
Calc
Config
Congr
Conv (file)
Basic
Change
Congr
Delta
Pattern
Rewrite
Simp
Unfold
Delta
ElabTerm
Generalize
Induction
Injection
Location
Match
Meta
Rewrite
Simp
Split
Unfold
Term
Util
Environment
Eval
Exception
Expr
HeadIndex
Hygiene
ImportingFlag
InternalExceptionId
KeyedDeclsAttribute
LazyInitExtension
Level
Linter (file)
Basic
Builtin
Deprecated
MissingDocs
UnusedVariables
Util
LoadDynlib
LocalContext
Log
Message
Meta (file)
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
GetUnfoldableConst
GlobalInstances
IndPredBelow
Inductive
InferType
Injective
Instances
KAbstract
KExprMap
LevelDefEq
Match (file)
Basic
CaseArraySizes
CaseValues
Match
MatchEqs
MatchEqsExt
MatchPatternAttr
MatcherInfo
Value
MatchUtil
Offset
PPGoal
RecursorInfo
Reduce
ReduceEval
SizeOf
Structure
SynthInstance
Tactic (file)
AC (file)
Main
Acyclic
Apply
Assert
Assumption
AuxLemma
Cases
Cleanup
Clear
Congr
Constructor
Contradiction
Delta
ElimInfo
FVarSubst
Generalize
Induction
Injection
Intro
LinearArith (file)
Basic
Main
Nat (file)
Basic
Simp
Solver
Simp
Solver
Refl
Rename
Replace
Revert
Rewrite
Simp (file)
Main
Rewrite
SimpAll
SimpCongrTheorems
SimpTheorems
Types
Split
SplitIf
Subst
Unfold
UnifyEq
Util
Transform
TransparencyMode
UnificationHint
WHNF
MetavarContext
Modifiers
MonadEnv
Parser (file)
Attr
Basic
Command
Do
Extension
Extra
Level
Module
StrInterpolation
Syntax
Tactic
Term
Types
ParserCompiler (file)
Attribute
PrettyPrinter (file)
Basic
Delaborator (file)
Basic
Builtins
Options
SubExpr
TopDownAnalyze
Formatter
Parenthesizer
ProjFns
ReducibilityAttrs
ResolveName
Runtime
ScopedEnvExtension
Server (file)
AsyncList
CodeActions
Completion
FileSource
FileWorker (file)
RequestHandling
Utils
WidgetRequests
GoTo
InfoUtils
References
Requests
Rpc (file)
Basic
Deriving
RequestHandling
Snapshots
Utils
Watchdog
Structure
SubExpr
Syntax
ToExpr
Util (file)
CollectFVars
CollectLevelParams
CollectMVars
FindExpr
FindLevelMVar
FindMVar
FoldConsts
ForEachExpr
ForEachExprWhere
HasConstCache
InstantiateLevelParams
MonadBacktrack
MonadCache
OccursCheck
PPExt
Path
Paths
Profile
PtrSet
RecDepth
Recognizers
ReplaceExpr
ReplaceLevel
SCC
ShareCommon
Sorry
Trace
Widget (file)
Basic
Diff
InteractiveCode
InteractiveDiagnostic
InteractiveGoal
TaggedText
UserWidget
Mathlib
Algebra
Abs
BigOperators
Basic
Multiset
Basic
Lemmas
Option
Ring
Bounds
CharZero
Defs
Lemmas
CovariantAndContravariant
Divisibility
Basic
Units
EuclideanDomain
Defs
Instances
Field
Basic
Defs
IsField
Opposite
Group
Aut
Basic
Commute
Defs
Units
Defs
Embedding
Equiv
Basic
Hom
Basic
Defs
Instances
InjSurj
Opposite
OrderSynonym
Pi
Prod
Semiconj
Defs
Units
TypeTags
Units (file)
Equiv
Hom
WithOne
Defs
GroupPower
Basic
CovariantClass
IterateHom
Lemmas
Order
Ring
GroupRingAction
Basic
GroupWithZero
Basic
Bitwise
Commute
Defs
Divisibility
InjSurj
NeZero
Power
Semiconj
Units
Basic
Equiv
Lemmas
IndicatorFunction
Invertible
Basic
Defs
GroupWithZero
Module
Basic
NeZero
Opposites
Order
AbsoluteValue
Archimedean
Field
Basic
Defs
Power
Floor
Group
Abs
Defs
Instances
MinMax
OrderIso
Units
Hom
Basic
Invertible
Monoid
Basic
Canonical
Defs
Defs
Lemmas
MinMax
NatCast
OrderDual
TypeTags
Units
WithTop
WithZero
Basic
Defs
Positive
Ring
Ring
Abs
Canonical
CharZero
Defs
Lemmas
WithTop
Sub
Canonical
Defs
WithTop
WithZero
ZeroLEOne
Parity
Regular
Basic
Ring
Aut
Basic
Commute
CompTypeclasses
Defs
Divisibility
Basic
Equiv
Hom
Basic
Defs
InjSurj
Opposite
Pi
Regular
Semiconj
Units
SMulWithZero
Star
Basic
Support
Control
Applicative
Basic
EquivFunctor
Functor
Traversable
Basic
ULift
Data
Array
Defs
Bool
Basic
Set
Complex
Basic
Countable
Basic
Defs
ENat
Basic
Lattice
Fin
Basic
Tuple
Basic
VecNotation
Finite
Basic
Defs
Finset
Basic
Card
Fold
Image
Lattice
LocallyFinite
Option
Pairwise
Pi
Powerset
Preimage
Prod
Sigma
Sort
Sum
Finsupp
Defs
Fintype
Basic
BigOperators
Card
Lattice
Option
Pi
Powerset
Prod
Sigma
Sum
Vector
FunLike
Basic
Embedding
Equiv
HashMap
Int
Basic
Bitwise
Cast
Basic
Defs
Field
Lemmas
CharZero
Div
Dvd
Basic
LeastGreatest
Lemmas
Order
Basic
Lemmas
Units
List
Basic
BigOperators
Basic
Lemmas
Chain
Count
Dedup
Defs
Duplicate
Forall2
Infix
Join
Lattice
Lex
MinMax
Nodup
NodupEquivFin
OfFn
Pairwise
Perm
Permutation
Range
Sort
Sublists
Zip
MLList
Basic
Dedup
Multiset
Basic
Bind
Dedup
FinsetOps
Fold
Lattice
Nodup
Pi
Powerset
Range
Sort
Sum
Nat
Basic
Bits
Bitwise
Cast
Basic
Commute
Defs
Field
NeZero
Order
Choose
Basic
Factorial
Basic
ForSqrt
Interval
Lattice
Order
Basic
Lemmas
Pairing
PartENat
Pow
Set
Size
Sqrt
SuccPred
Units
Nondet
Basic
Num
Basic
Option
Basic
Defs
NAry
PNat
Basic
Defs
Part
Pi
Algebra
Lex
Prod
Basic
PProd
Quot
Rat
Basic
Cast
CharZero
Defs
Order
Defs
Floor
Init
Lemmas
Order
Real
Archimedean
Basic
CauSeq
CauSeqCompletion
Rel
SProd
Set
Basic
Countable
Finite
Function
Functor
Image
Intervals
Basic
Group
Image
Monoid
OrdConnected
UnorderedInterval
Lattice
List
NAry
Pairwise
Basic
Pointwise
Basic
Prod
Sigma
SetLike
Basic
Setoid
Basic
Partition
Sigma
Basic
String
Defs
Subtype
Sum
Basic
Order
Sym
Basic
Tree
ULift
Vector (file)
Basic
Dynamics
FixedPoints
Basic
GroupTheory
GroupAction
Defs
Group
Opposite
Pi
Prod
Units
Perm
Basic
Submonoid
Basic
Subsemigroup
Basic
Init
Algebra
Classes
Align
CCLemmas
Classical
Control
Combinators
Core
Data
Bool
Basic
Lemmas
Fin
Basic
Int
Basic
Bitwise
Order
List
Basic
Instances
Lemmas
Nat
Basic
Bitwise
Lemmas
Notation
Ordering
Basic
Quot
Sigma
Basic
Function
Logic
Meta
WellFoundedTactics
Order
Defs
LinearOrder
Propext
Quot
Set
ZeroOne
Lean
Data
NameMap
Elab
Tactic
Basic
Term
EnvExtension
Exception
Expr (file)
Basic
ReplaceRec
Traverse
Meta (file)
Basic
CongrTheorems
DiscrTree
Simp
Name
PrettyPrinter
Delaborator
SMap
Logic
Basic
Denumerable
Embedding
Basic
Set
Encodable
Basic
Equiv
Basic
Defs
Fin
List
Nat
Option
Set
Function
Basic
Conjugate
Iterate
IsEmpty
Nonempty
Nontrivial
Basic
Defs
Pairwise
Relation
Relator
Small
Basic
Defs
Unique
Mathport
Attributes
Notation
Rename
Order
Antichain
Antisymmetrization
Atoms (file)
Finite
Basic
BooleanAlgebra
BoundedOrder
Bounds
Basic
OrderIso
Chain
Compare
CompleteBooleanAlgebra
CompleteLattice
ConditionallyCompleteLattice
Basic
Finset
Cover
Directed
Disjoint
FixedPoints
GaloisConnection
Heyting
Basic
Hom
Basic
Bounded
CompleteLattice
Lattice
Order
Set
InitialSeg
Iterate
Lattice
LatticeIntervals
LocallyFinite
Max
MinMax
ModularLattice
Monotone
Basic
Partition
Finpartition
PropInstances
RelClasses
RelIso
Basic
Set
SuccPred
Basic
Limit
SupIndep
SymmDiff
Synonym
ULift
WellFounded
WithBot
Zorn
SetTheory
Cardinal
Basic
SchroederBernstein
Ordinal
Basic
Tactic
Abel
ApplyAt
ApplyCongr
ApplyFun
ApplyWith
Attr
Core
Register
Backtrack
Basic
ByContra
CancelDenoms
Core
Cases
CasesM
Choose
Classical
Clear!
ClearExcept
Clear_
Coe
Common
Congr!
Congrm
Constructor
Contrapose
Conv
Convert
Core
DefEqTransformations
DeriveToExpr
Eqns
Existsi
ExtractGoal
ExtractLets
FBinop
FailIfNoProgress
FieldSimp
Find
GCongr (file)
Core
ForwardAttr
GeneralizeProofs
GuardGoalNums
GuardHypNums
Have
HaveI
HelpCmd
HigherOrder
Hint
InferParam
Inhabit
IrreducibleDef
LibrarySearch
Lift
Linarith (file)
Datatypes
Elimination
Frontend
Lemmas
Parsing
Preprocessing
Verification
Lint
MkIffOfInductiveProp
Monotonicity
Attr
Nontriviality (file)
Core
NormNum (file)
Basic
Core
DivMod
Eq
Ineq
Inv
OfScientific
Pow
Result
NthRewrite
Observe
PPWithUniv
Positivity (file)
Basic
Core
ProjectionNotation
Propose
PushNeg
RSuffices
Recover
Relation
Rfl
Symm
Trans
Rename
RenameBVar
Replace
Rewrites
Ring (file)
Basic
PNat
RingNF
RunCmd
Says
ScopedNS
Set
SetLike
SimpIntro
SimpRw
Simps
Basic
NotationClass
SolveByElim
SplitIfs
Spread
Substs
SuccessIfFailWithMsg
SudoSetOption
SwapVar
Tauto
TermCongr
ToAdditive
ToExpr
ToLevel
Trace
TryThis
TypeCheck
UnsetOption
Use
Variable
WLOG
Zify
Util
AssertExists
AtomM
CompileInductive
CountHeartbeats
Delaborators
DischargerAsTactic
Imports
MemoFix
Qq
Syntax
SynthesizeUsing
Tactic
WhatsNew
WithWeakNamespace
Qq (file)
AssertInstancesCommute
Delab
ForLean
Do
ReduceEval
ToExpr
Macro
Match
MetaM
SortLocalDecls
Typ
Std (file)
Classes
BEq
Cast
Dvd
LawfulMonad
Order
RatCast
SetNotation
CodeAction (file)
Attr
Basic
Deprecated
Misc
Control
ForInStep (file)
Basic
Lemmas
Lemmas
Data
Array
Basic
Init
Basic
Lemmas
Lemmas
Match
Merge
AssocList
BinomialHeap (file)
Basic
Lemmas
BitVec (file)
Basic
Bitblast
Folds
Lemmas
Bool
Char
DList
Fin
Basic
Init
Lemmas
Iterate
Lemmas
HashMap (file)
Basic
Lemmas
WF
Int
Basic
DivMod
Lemmas
Json
List
Basic
Count
Init
Attach
Lemmas
Lemmas
Pairwise
MLList
Basic
Heartbeats
Nat
Basic
Bitwise
Gcd
Init
Lemmas
Lemmas
Option
Basic
Init
Lemmas
Lemmas
Ord
PairingHeap
Prod
Lex
RBMap (file)
Alter
Basic
Lemmas
WF
Range
Lemmas
Rat (file)
Basic
Lemmas
String (file)
Basic
Lemmas
Sum (file)
Basic
Lemmas
Lean
AttributeExtra
Command
CoreM
Delaborator
Elab
Tactic
Expr
Float
Format
HashMap
HashSet
InfoTree
Json
LocalContext
Meta
AssertHypotheses
Basic
Clear
DiscrTree
Expr
Inaccessible
InstantiateMVars
SavedState
Simp
UnusedNames
MonadBacktrack
Name
NameMapAttribute
Parser
PersistentHashMap
PersistentHashSet
Position
Tactic
TagAttribute
Util
EnvSearch
Path
Linter (file)
UnnecessarySeqFocus
UnreachableTactic
Logic
Tactic
Alias
Basic
ByCases
Case
Change
CoeExt
Congr
Exact
Ext (file)
Attr
GuardExpr
GuardMsgs
HaveI
Instances
LabelAttr
LeftRight
Lint (file)
Basic
Frontend
Misc
Simp
TypeClass
NoMatch
NormCast (file)
Ext
Lemmas
OpenPrivate
PermuteGoals
PrintDependents
PrintPrefix
RCases
Relation
Rfl
Symm
Replace
RunCmd
SeqFocus
ShowTerm
SimpTrace
Simpa
SqueezeScope
TryThis
Unreachable
Where
Test
Internal
DummyLabelAttr
Util
Cache
ExtendedBinder
LibraryNote
Pickle
ProofWanted
TermUnsafe
WF

Color scheme