General documentation

index
foundational types
tactics

Library

Batteries (file)
Classes
Cast
Deprecated
Order
RatCast
SatisfiesM
CodeAction (file)
Attr
Basic
Deprecated
Match
Misc
Control
ForInStep (file)
Basic
Lemmas
Nondet
Basic
AlternativeMonad
LawfulMonadState
Lemmas
Monad
OptionT
Data
Array (file)
Init
Lemmas
Basic
Lemmas
Match
Merge
Monadic
Pairwise
Scan
BinaryHeap (file)
Basic
BinomialHeap (file)
Basic
Lemmas
BitVec (file)
Basic
Lemmas
Char (file)
AsciiCasing
Basic
DList (file)
Basic
Lemmas
Fin (file)
Basic
Fold
Lemmas
OfBits
HashMap (file)
Basic
List (file)
Init
Lemmas
ArrayMap
Basic
Count
Lemmas
Matcher
Monadic
Pairwise
Perm
Scan
MLList (file)
Basic
Heartbeats
IO
Nat (file)
Basic
Bisect
Bitwise
Digits
Gcd
Lemmas
RBMap (file)
Alter
Basic
Depth
Lemmas
WF
Random (file)
MersenneTwister
Range (file)
Lemmas
Rat (file)
Float
String (file)
AsciiCasing
Basic
Legacy
Lemmas
Matcher
UnionFind (file)
Basic
Lemmas
Vector (file)
Basic
Lemmas
Monadic
AssocList
Bool
ByteArray
ByteSlice
FloatArray
Int
NameSet
PairingHeap
RunningStats
Stream
UInt
Lean
IO
Process
Meta
Basic
DiscrTree
Expr
Inaccessible
InstantiateMVars
SavedState
Simp
UnusedNames
System
IO
Util
EnvSearch
AttributeExtra
EStateM
Except
Expr
Float
HashMap
HashSet
Json
LawfulMonad
LawfulMonadLift
MonadBacktrack
NameMapAttribute
PersistentHashMap
PersistentHashSet
Position
SatisfiesM
Syntax
TagAttribute
Linter (file)
UnnecessarySeqFocus
UnreachableTactic
Tactic
Lint (file)
Basic
Frontend
Misc
Simp
TypeClass
Alias
Basic
Case
Congr
Exact
GeneralizeProofs
HelpCmd
Init
Instances
Lemma
NoMatch
OpenPrivate
PermuteGoals
PrintDependents
PrintOpaques
PrintPrefix
SeqFocus
ShowUnused
SqueezeScope
Trans
Unreachable
Util
Cache
ExtendedBinder
LibraryNote
Panic
Pickle
ProofWanted
Logic
Init (file)
Control (file)
Lawful (file)
MonadAttach (file)
Instances
Lemmas
MonadLift (file)
Basic
Instances
Lemmas
Basic
Instances
Lemmas
Basic
EState
Except
ExceptCps
Id
MonadAttach
Option
Reader
State
StateCps
StateRef
Data (file)
Array (file)
Lex (file)
Basic
Lemmas
QSort (file)
Basic
Subarray (file)
Split
Attach
Basic
BasicAux
BinSearch
Bootstrap
Count
DecidableEq
Erase
Extract
FinRange
Find
GetLit
InsertIdx
InsertionSort
Lemmas
MapIdx
Mem
Monadic
OfFn
Perm
Range
Set
TakeDrop
Zip
BitVec (file)
Basic
BasicAux
Bitblast
Bootstrap
Decidable
Folds
Lemmas
ByteArray (file)
Basic
Bootstrap
Extra
Lemmas
Char (file)
Basic
Lemmas
Order
Ordinal
Dyadic (file)
Basic
Instances
Inv
Round
Fin (file)
Basic
Bitwise
Fold
Iterate
Lemmas
Log2
OverflowAware
FloatArray (file)
Basic
Format (file)
Basic
Instances
Macro
Syntax
Int (file)
Bitwise (file)
Basic
Lemmas
DivMod (file)
Basic
Bootstrap
Lemmas
Pow
Basic
Compare
Cooper
Gcd
Lemmas
LemmasAux
Linear
OfNat
Order
Pow
Iterators (file)
Combinators (file)
Monadic (file)
Attach
FilterMap
FlatMap
Take
ULift
Attach
FilterMap
FlatMap
Take
ULift
Consumers (file)
Monadic (file)
Access
Collect
Loop
Partial
Total
Access
Collect
Loop
Partial
Stream
Total
Internal (file)
LawfulMonadLiftFunction
Lemmas (file)
Combinators (file)
Monadic (file)
Attach
FilterMap
FlatMap
Take
ULift
Attach
FilterMap
FlatMap
Take
ULift
Consumers (file)
Monadic (file)
Collect
Loop
Access
Collect
Loop
Monadic
Basic
Producers (file)
Monadic (file)
List
List
Basic
Producers (file)
Monadic (file)
List
List
Basic
PostconditionMonad
ToIterator
List (file)
Nat (file)
BEq
Basic
Count
Erase
Find
InsertIdx
Modify
Pairwise
Perm
Range
Sublist
TakeDrop
Sort (file)
Basic
Impl
Lemmas
Attach
Basic
BasicAux
Control
Count
Erase
FinRange
Find
Impl
Lemmas
Lex
MapIdx
MinMax
Monadic
Notation
OfFn
Pairwise
Perm
Range
Sublist
TakeDrop
ToArray
ToArrayImpl
Zip
Nat (file)
Bitwise (file)
Basic
Lemmas
Div (file)
Basic
Lemmas
Power2 (file)
Basic
Lemmas
Basic
Compare
Control
Coprime
Dvd
Fold
Gcd
Lcm
Lemmas
Linear
Log2
MinMax
Mod
Order
SOM
Simproc
Option (file)
Array
Attach
Basic
BasicAux
Coe
Function
Instances
Lemmas
List
Monadic
Ord (file)
Array
Basic
BitVec
SInt
String
UInt
Vector
Order (file)
Classes
ClassesExtra
Factories
FactoriesExtra
Lemmas
LemmasExtra
Ord
PackageFactories
Range (file)
Polymorphic (file)
Internal
SignedBitVec
Basic
BitVec
Char
Fin
GetElemTactic
Instances
Int
IntLemmas
Iterators
Lemmas
Map
Nat
NatLemmas
PRange
RangeIterator
SInt
Stream
UInt
UpwardEnumerable
Basic
Lemmas
Rat (file)
Basic
Lemmas
SInt (file)
Basic
Bitwise
Float
Float32
Lemmas
Slice (file)
Array (file)
Basic
Iterator
Lemmas
List (file)
Basic
Iterator
Lemmas
Basic
Lemmas
Notation
Operations
String (file)
Lemmas (file)
Basic
Modify
Search
Splits
Pattern (file)
Basic
Char
Pred
String
Basic
Bootstrap
Decode
Defs
Extra
Grind
Iterator
Legacy
Modify
PosRaw
Search
Slice
Stream
Substring
TakeDrop
Termination
ToSlice
Subtype (file)
Basic
Order
OrderExtra
Sum (file)
Basic
Lemmas
ToString (file)
Basic
Macro
Name
UInt (file)
Basic
BasicAux
Bitwise
Lemmas
Log2
Vector (file)
Algebra
Attach
Basic
Count
DecidableEq
Erase
Extract
FinRange
Find
InsertIdx
Lemmas
Lex
MapIdx
Monadic
OfFn
Perm
Range
Stream
Zip
AC
BEq
Bool
Cast
Float
Float32
Function
Hashable
LawfulHashable
NeZero
OfScientific
PLift
Prod
Queue
RArray
Random
Repr
Stream
ULift
Zero
Grind (file)
Module (file)
Basic
Envelope
NatModuleNorm
OfNatModule
Ordered (file)
Field
Int
Linarith
Module
Order
Rat
Ring
Ring (file)
Basic
CommSemiringAdapter
CommSolver
Envelope
Field
OfScientific
ToInt
AC
Annotated
Attr
Cases
Config
Ext
FieldNormNum
Injective
Interactive
Lemmas
Lint
Norm
Offset
Order
PP
Propagator
Tactics
ToInt
ToIntLemmas
Util
GrindInstances (file)
Ring (file)
BitVec
Fin
Int
Nat
Rat
SInt
UInt
Nat
ToInt
Internal (file)
Order (file)
Basic
Lemmas
Tactic
Meta (file)
Defs
Omega (file)
Coeffs
Constraint
Int
IntList
LinearCombo
Logic
Sym (file)
Lemmas
System (file)
FilePath
IO
IOError
Platform
Promise
ST
Uri
BinderNameHint
BinderPredicates
ByCases
Classical
Coe
Conv
Core
Dynamic
Ext
GetElem
Guard
Hints
LawfulBEqTactics
MacroTrace
MetaTypes
MethodSpecsSimp
Notation
NotationExtra
Prelude
PropLemmas
RCases
ShareCommon
SimpLemmas
Simproc
SizeOf
SizeOfLemmas
Syntax
Tactics
TacticsExtra
Task
Try
Util
WF
WFComputable
WFExtrinsicFix
WFTactics
While
Lean
Compiler
IR
Basic
CompilerM
Format
LCNF
Basic
CompilerM
ConfigOptions
LCtx
PassManager
PhaseExt
Types
BorrowedAnnotation
ExportAttr
ExternAttr
ImplementedByAttr
InitAttr
InlineAttrs
MetaAttr
ModPkgExt
NameMangling
NoncomputableAttr
Old
Specialize
Data
Json (file)
FromToJson (file)
Basic
Extra
Basic
Elab
Parser
Printer
Stream
Lsp (file)
Basic
BasicAux
CancelParams
Capabilities
Client
CodeActions
Communication
Diagnostics
Extra
InitShutdown
Internal
Ipc
LanguageFeatures
TextSync
Utf16
Window
Workspace
NameMap
Basic
Array
AssocList
DeclarationRange
Format
JsonRpc
KVMap
LBool
LOption
Name
NameTrie
OpenDecl
Options
PersistentArray
PersistentHashMap
PersistentHashSet
Position
PrefixTree
RArray
SMap
SSet
Trie
DocString (file)
Add
Extension
Formatter
Links
Markdown
Parser
Syntax
Types
Elab
Command (file)
Scope
Do (file)
Basic
Legacy
Switch
InfoTree (file)
InlayHints
Main
Types
PreDefinition
TerminationHint
Quotation
Precheck
Util
Tactic
Grind
Annotated
Basic
BuiltinTactic
Config
ElabTerm
Ext
Generalize
Induction
Location
RCases
RenameInaccessibles
Repeat
Simp
SimpTrace
Term (file)
TermElabM
App
Arg
Attributes
AutoBound
AuxDef
Binders
BindersUtil
BuiltinNotation
BuiltinTerm
Config
DeclModifiers
DeclarationRange
DocString
ElabRules
ErrorUtils
Eval
Exception
Import
Level
MacroArgUtil
Match
MatchAltView
Open
PatternVar
RecAppSyntax
SetOption
Syntax
SyntheticMVars
Util
WhereFinally
Language
Lean
Types
Basic
LibrarySuggestions
Basic
Linter
Basic
Deprecated
MissingDocs
UnusedVariables
Util
Meta
Constructions
CtorIdx
SparseCasesOn
DiscrTree (file)
Basic
Main
Types
Util
Match
MatcherApp
Basic
Basic
CaseArraySizes
CaseValues
MVarRenaming
Match
MatchEqsExt
MatchPatternAttr
MatcherInfo
NamedPatterns
SimpH
SolveOverlap
Value
Tactic
Simp (file)
Arith (file)
Int (file)
Basic
Simp
Nat (file)
Basic
Simp
Util
BuiltinSimprocs (file)
Array
BitVec
Char
Core
CtorIdx
Fin
Int
List
MethodSpecs
Nat
SInt
String
UInt
Util
Attr
Diagnostics
LoopProtection
Main
RegisterCommand
Rewrite
SimpAll
SimpCongrTheorems
SimpTheorems
Simproc
Types
Acyclic
Apply
Assert
Assumption
AuxLemma
Cases
Cleanup
Clear
Congr
Constructor
Contradiction
ElimInfo
ExposeNames
Ext
FVarSubst
FunIndCollect
FunIndInfo
Generalize
Induction
Injection
Intro
Refl
Rename
Repeat
Replace
Revert
Subst
TryThis
UnifyEq
Util
ACLt
AbstractMVars
AbstractNestedProofs
AppBuilder
Basic
BinderNameHint
Check
Closure
Coe
CoeAttr
CollectFVars
CollectMVars
CompletionName
CongrTheorems
CtorRecognizer
DecLevel
Diagnostics
Eqns
Eval
ForEachExpr
FunInfo
GeneralizeTelescope
GeneralizeVars
GetUnfoldableConst
GlobalInstances
HasNotBit
HaveTelescope
Hint
InferType
Instances
IntInstTesters
KAbstract
KExprMap
LetToHave
LitValues
MatchUtil
MethodSpecs
MonadSimp
NatInstTesters
Offset
PPGoal
ProdN
RecExt
RecursorInfo
Reduce
ReduceEval
SameCtorUtils
Sorry
Structure
SynthInstance
Transform
TransparencyMode
TryThis
WHNF
Parser
Tactic (file)
Doc
Term (file)
Basic
Doc
Attr
Basic
Command
Do
Extension
Extra
Level
Module
StrInterpolation
Syntax
Types
ParserCompiler (file)
Attribute
PrettyPrinter (file)
Delaborator (file)
Attributes
Basic
Builtins
FieldNotation
Options
SubExpr
TopDownAnalyze
Basic
Formatter
Parenthesizer
Server
CodeActions (file)
Attr
Basic
Provider
FileWorker
Utils
Rpc
Basic
RequestHandling
AsyncList
FileSource
InfoUtils
RequestCancellation
Requests
ServerTask
Snapshots
Utils
Util
CollectAxioms
CollectFVars
CollectLevelMVars
CollectLevelParams
CollectLooseBVars
CollectMVars
Diff
FindExpr
FindLevelMVar
FindMVar
FoldConsts
ForEachExpr
ForEachExprWhere
Heartbeats
InstantiateLevelParams
LeanOptions
MonadBacktrack
MonadCache
NumObjs
OccursCheck
PPExt
Path
Profile
PtrSet
RecDepth
Recognizers
ReplaceExpr
ReplaceLevel
SafeExponentiation
ShareCommon
Sorry
SortExprs
Trace
Widget
Basic
InteractiveCode
InteractiveDiagnostic
InteractiveGoal
TaggedText
Types
UserWidget
AddDecl
Attributes
AuxRecursor
BuiltinDocAttr
Class
CoreM
Declaration
DeclarationRange
DefEqAttrib
EnvExtension
Environment
ErrorExplanation
Exception
Expr
ExtraModUses
HeadIndex
Hygiene
IdentifierSuggestion
ImportingFlag
InternalExceptionId
KeyedDeclsAttribute
Level
LoadDynlib
LocalContext
Log
Message
MetavarContext
Modifiers
MonadEnv
Namespace
PrivateName
ProjFns
ReducibilityAttrs
ReservedNameAction
ResolveName
ScopedEnvExtension
Setup
Structure
SubExpr
Syntax
ToExpr
ToLevel
Std
Data
DHashMap
Internal
AssocList
Basic
Iterator
Lemmas
Defs
HashesTo
Index
Model
Raw
RawLemmas
WF
AdditionalOperations
Basic
DecidableEquiv
Iterator
IteratorLemmas
Lemmas
Raw
RawDef
RawLemmas
DTreeMap
Internal
WF
Defs
Lemmas
Balanced
Balancing
Cell
Def
Model
Operations
Ordered
Queries
Raw
Basic
AdditionalOperations
Basic
HashMap (file)
AdditionalOperations
Basic
DecidableEquiv
Iterator
IteratorLemmas
Lemmas
Raw
RawLemmas
HashSet
Basic
Internal
List
Associative
Defs
Cut
Iterators (file)
Combinators (file)
Monadic (file)
Drop
DropWhile
StepSize
TakeWhile
Zip
Drop
DropWhile
StepSize
TakeWhile
Zip
Lemmas (file)
Combinators (file)
Monadic (file)
Drop
DropWhile
FilterMap
TakeWhile
Zip
Drop
DropWhile
TakeWhile
Zip
Consumers (file)
Monadic (file)
Collect
Loop
Collect
Loop
Equivalence (file)
Basic
HetT
StepCongr
Producers (file)
Monadic (file)
Array
Empty
List
Array
Empty
Range
Repeat
Slice
Monadic
Producers (file)
Monadic (file)
Array
Empty
Array
Empty
Range
Repeat
Slice
TreeMap
Raw
Basic
AdditionalOperations
Basic
TreeSet
Basic
ByteSlice
Do (file)
SPred (file)
Notation (file)
Basic
DerivedLaws
Laws
SPred
SVal
Triple (file)
Basic
SpecLemmas
WP (file)
Basic
Monad
SimpLemmas
PostCond
PredTrans
Internal
Parsec (file)
Basic
ByteArray
String
Sync
Basic
Mutex
Tactic
Do
ProofMode
Syntax
Time
Date (file)
Unit
Basic
Day
Month
Week
Weekday
Year
Basic
PlainDate
ValidDate
DateTime (file)
PlainDateTime
Timestamp
Format (file)
Basic
Internal (file)
Bounded
UnitVal
Notation
Spec
Time (file)
Unit
Basic
Hour
Millisecond
Minute
Nanosecond
Second
Basic
HourMarker
PlainTime
Zoned (file)
Database (file)
Basic
TZdb
TzIf
Windows
DateTime
Offset
TimeZone
ZoneRules
ZonedDateTime
Duration

Color scheme