General documentation

index
foundational types

Library

Init (file)
Control (file)
Lawful (file)
Basic
Instances
Lemmas
Basic
EState
Except
ExceptCps
Id
Option
Reader
State
StateCps
StateRef
Data (file)
Array (file)
Lex (file)
Basic
Lemmas
Subarray (file)
Split
Attach
Basic
BasicAux
BinSearch
Bootstrap
Count
DecidableEq
Erase
Extract
FinRange
Find
GetLit
InsertIdx
InsertionSort
Lemmas
MapIdx
Mem
Monadic
OfFn
Perm
QSort
Range
Set
TakeDrop
Zip
BitVec (file)
Basic
BasicAux
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
DivMod (file)
Basic
Bootstrap
Lemmas
Basic
Cooper
DivModLemmas
Gcd
Lemmas
LemmasAux
Linear
Order
Pow
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
Basic
Lemmas
Basic
Compare
Control
Dvd
Fold
Gcd
Lcm
Lemmas
Linear
Log2
MinMax
Mod
Power2
SOM
Simproc
Option (file)
Attach
Basic
BasicAux
Instances
Lemmas
List
Monadic
Range (file)
Basic
Lemmas
SInt (file)
Basic
Bitwise
Float
Float32
Lemmas
String (file)
Basic
Extra
Lemmas
Sum (file)
Basic
Lemmas
ToString (file)
Basic
Macro
UInt (file)
Basic
BasicAux
Bitwise
Lemmas
Log2
Vector (file)
Attach
Basic
Count
DecidableEq
Erase
Extract
FinRange
InsertIdx
Lemmas
Lex
MapIdx
Monadic
OfFn
Range
Zip
AC
BEq
Basic
Bool
Cast
Channel
Float
Float32
Function
Hashable
NeZero
OfScientific
Ord
PLift
Prod
Queue
RArray
Random
Repr
Stream
Subtype
ULift
Zero
Grind (file)
Cases
Lemmas
Norm
Offset
PP
Propagator
Tactics
Util
Internal (file)
Order (file)
Basic
Lemmas
Tactic
Omega (file)
Coeffs
Constraint
Int
IntList
LinearCombo
Logic
System (file)
FilePath
IO
IOError
Mutex
Platform
Promise
ST
Uri
BinderNameHint
BinderPredicates
ByCases
Classical
Coe
Conv
Core
Dynamic
Ext
GetElem
Guard
Hints
MacroTrace
Meta
MetaTypes
Notation
NotationExtra
Prelude
PropLemmas
RCases
ShareCommon
SimpLemmas
Simproc
SizeOf
SizeOfLemmas
Syntax
Tactics
TacticsExtra
Try
Util
WF
WFTactics
While
Lake (file)
Build (file)
Job (file)
Basic
Monad
Register
Target (file)
Basic
Fetch
Actions
Common
Context
Data
Executable
Facets
Fetch
Imports
Index
Info
Key
Library
Module
Package
Run
Store
Targets
Topological
Trace
CLI
Actions
Build
Error
Config (file)
Context
Defaults
Dependency
Dynlib
Env
ExternLib
ExternLibConfig
FacetConfig
Glob
InstallPath
LeanConfig
LeanExe
LeanExeConfig
LeanLib
LeanLibConfig
Module
Monad
Opaque
OutFormat
Package
Script
TargetConfig
Workspace
WorkspaceConfig
DSL (file)
Attributes
AttributesCore
Config
DeclUtil
Extensions
Meta
Package
Require
Script
Targets
Load
Config
Manifest
Toml (file)
Data
DateTime
Dict
Value
Elab (file)
Expression
Value
Grammar
Load
ParserUtil
Util
Binder
Casing
Compare
Cycle
DRBMap
Date
EStateT
EquipT
Error
Exit
Family
FilePath
Git
IO
JsonObject
Lift
List
Lock
Log
Message
Name
NativeLib
Opaque
OpaqueType
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
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
CancelParams
Capabilities
Client
CodeActions
Communication
Diagnostics
Extra
InitShutdown
Internal
Ipc
LanguageFeatures
TextSync
Utf16
Workspace
Xml (file)
Basic
Parser
Array
AssocList
DeclarationRange
Format
FuzzyMatching
HashMap
HashSet
JsonRpc
KVMap
LBool
LOption
Name
NameMap
NameTrie
OpenDecl
Options
PersistentArray
PersistentHashMap
PersistentHashSet
Position
PrefixTree
RArray
RBMap
RBTree
SMap
SSet
Trie
DocString (file)
Extension
Elab (file)
Deriving (file)
BEq
Basic
DecEq
FromToJson
Hashable
Inhabited
Nonempty
Ord
Repr
SizeOf
ToExpr
TypeName
Util
InfoTree (file)
InlayHints
Main
Types
PreDefinition (file)
Nonrec
Eqns
PartialFixpoint (file)
Eqns
Induction
Main
Structural (file)
BRecOn
Basic
Eqns
FindRecArg
IndGroupInfo
IndPred
Main
Preprocess
RecArgInfo
SmartUnfolding
WF (file)
Basic
Eqns
Fix
FloatRecApp
GuessLex
Ite
Main
PackMutual
Preprocess
Rel
Unfold
Basic
EqUnfold
Eqns
Main
MkInhabitant
Mutual
TerminationHint
TerminationMeasure
Quotation (file)
Precheck
Util
Tactic (file)
BVDecide (file)
Frontend (file)
BVDecide (file)
Reflect
ReifiedBVExpr
ReifiedBVLogical
ReifiedBVPred
ReifiedLemmas
Reify
SatAtBVLogical
Normalize (file)
AC
AndFlatten
Basic
EmbeddedConstraint
Enums
IntToBitVec
Rewrite
Simproc
Structures
TypeAnalysis
Attr
BVCheck
BVTrace
LRAT
LRAT (file)
Trim
External
Conv (file)
Basic
Change
Congr
Delta
Pattern
Rewrite
Simp
Unfold
Omega (file)
Core
Frontend
MinNatAbs
OmegaM
AsAuxLemma
Basic
BoolToPropSimps
BuiltinTactic
Cache
Calc
Change
Classical
Config
Congr
Delta
DiscrTreeKey
Doc
ElabTerm
ExposeNames
Ext
FalseOrByContra
Generalize
Grind
Guard
Induction
Injection
LibrarySearch
Location
Match
Meta
Monotonicity
NormCast
RCases
Repeat
Rewrite
Rewrites
Rfl
ShowTerm
Simp
SimpArith
SimpTrace
Simpa
Simproc
SolveByElim
Split
Symm
TreeTacAttr
Try
Unfold
App
Arg
Attributes
AutoBound
AuxDef
BinderPredicates
Binders
BindersUtil
BuiltinCommand
BuiltinEvalCommand
BuiltinNotation
BuiltinTerm
Calc
CheckTactic
Command
ComputedFields
Config
DeclModifiers
DeclNameGen
DeclUtil
Declaration
DeclarationRange
DefView
Do
ElabRules
Eval
Exception
Extra
Frontend
GenInjective
GuardMsgs
Import
Inductive
InfoTrees
InheritDoc
LetRec
Level
Macro
MacroArgUtil
MacroRules
Match
MatchAltView
MatchExpr
Mixfix
MutualDef
MutualInductive
Notation
Open
ParseImportsFast
PatternVar
Print
RecAppSyntax
RecommendedSpelling
SetOption
StructInst
Structure
Syntax
SyntheticMVars
Term
Time
Util
Language
Lean (file)
Types
Basic
Util
Linter (file)
Basic
Builtin
ConstructorAsVariable
Deprecated
List
MissingDocs
Omit
UnusedVariables
Util
Meta (file)
ArgsPacker (file)
Basic
Constructions (file)
BRecOn
CasesOn
NoConfusion
RecOn
Match (file)
MatcherApp (file)
Basic
Transform
Basic
CaseArraySizes
CaseValues
Match
MatchEqs
MatchEqsExt
MatchPatternAttr
MatcherInfo
Value
Tactic (file)
AC (file)
Main
Grind (file)
Arith (file)
Cutsat (file)
DvdCnstr
EqCnstr
Inv
LeCnstr
Model
Proof
Search
SearchM
Types
Util
Var
Offset (file)
Main
Model
Proof
Types
Util
Internalize
Inv
Main
Model
ProofUtil
Types
Util
Attr
Beta
Canon
Cases
CasesMatch
Combinators
Core
Ctor
Diseq
EMatch
EMatchTheorem
ENodeKey
EqResolution
Ext
ForallProp
Injection
Internalize
Intro
Inv
Main
MarkNestedProofs
MatchCond
MatchDiscrOnly
PP
Parser
Proj
Proof
Propagate
PropagatorAttr
ProveEq
RevertAll
Simp
SimpUtil
Solve
Split
Types
Util
LinearArith (file)
Nat (file)
Basic
Simp
Solver
Basic
Main
Simp
Solver
Simp (file)
Arith (file)
Int (file)
Basic
Simp
Nat (file)
Basic
Simp
Util
BuiltinSimprocs (file)
Array
BitVec
Char
Core
Fin
Int
List
Nat
String
UInt
Util
Attr
Diagnostics
Main
RegisterCommand
Rewrite
SimpAll
SimpCongrTheorems
SimpTheorems
Simproc
Types
Try (file)
Collect
Acyclic
Apply
Assert
Assumption
AuxLemma
Backtrack
Cases
Cleanup
Clear
Congr
Constructor
Contradiction
Delta
ElimInfo
ExposeNames
Ext
FVarSubst
FunInd
FunIndCollect
FunIndInfo
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
BinderNameHint
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
IntInstTesters
Iterator
KAbstract
KExprMap
LazyDiscrTree
LevelDefEq
LitValues
MatchUtil
NatInstTesters
Offset
PPGoal
PProdN
RecursorInfo
Reduce
ReduceEval
SizeOf
Sorry
Structure
SynthInstance
Transform
TransparencyMode
UnificationHint
WHNF
Parser (file)
Tactic (file)
Doc
Term (file)
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 (file)
CodeActions (file)
Attr
Basic
Provider
Completion (file)
CompletionCollectors
CompletionInfoSelection
CompletionItemData
CompletionResolution
CompletionUtils
EligibleHeaderDecls
ImportCompletion
SyntheticCompletion
FileWorker (file)
InlayHints
RequestHandling
SemanticHighlighting
SetupFile
Utils
WidgetRequests
Rpc (file)
Basic
Deriving
RequestHandling
Test (file)
Cancel
Runner
AsyncList
FileSource
GoTo
InfoUtils
References
RequestCancellation
Requests
ServerTask
Snapshots
Utils
Watchdog
Util (file)
CollectAxioms
CollectFVars
CollectLevelMVars
CollectLevelParams
CollectMVars
Diff
FVarSubset
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
SortExprs
TestExtern
Trace
Widget (file)
Basic
Diff
InteractiveCode
InteractiveDiagnostic
InteractiveGoal
TaggedText
Types
UserWidget
AddDecl
Attributes
AuxRecursor
BuiltinDocAttr
Class
CoreM
Declaration
DeclarationRange
Environment
Exception
Expr
HeadIndex
Hygiene
ImportingFlag
InternalExceptionId
KeyedDeclsAttribute
LabelAttribute
Level
LoadDynlib
LocalContext
Log
Message
MetavarContext
Modifiers
MonadEnv
PremiseSelection
PrivateName
ProjFns
ReducibilityAttrs
Replay
ReservedNameAction
ResolveName
Runtime
ScopedEnvExtension
Structure
SubExpr
Syntax
ToExpr
ToLevel
Std (file)
Classes
Ord
Data (file)
DHashMap (file)
Internal
AssocList
Basic
Lemmas
List
Associative
Defs
HashesTo
Defs
HashesTo
Index
Model
Raw
RawLemmas
WF
AdditionalOperations
Basic
Lemmas
Raw
RawDef
RawLemmas
DTreeMap (file)
Internal
WF
Defs
Lemmas
Balanced
Balancing
Cell
Def
Model
Operations
Ordered
Queries
Raw
Basic
AdditionalOperations
Basic
HashMap (file)
AdditionalOperations
Basic
Lemmas
Raw
RawLemmas
HashSet (file)
Basic
Lemmas
Raw
RawLemmas
Internal
List
Associative
Defs
Cut
TreeMap (file)
Raw
Basic
AdditionalOperations
Basic
TreeSet (file)
Raw
Basic
AdditionalOperations
Basic
Internal (file)
Async (file)
Basic
Timer
Parsec (file)
Basic
ByteArray
String
UV (file)
Loop
Timer
Rat
Net (file)
Addr
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
Sync (file)
Channel
Mutex
Tactic (file)
BVDecide (file)
Bitblast (file)
BVExpr (file)
Circuit (file)
Impl (file)
Operations
Add
Append
Eq
Extract
GetLsbD
Mul
Neg
Not
Replicate
RotateLeft
RotateRight
ShiftLeft
ShiftRight
SignExtend
Sub
Udiv
Ult
Umod
ZeroExtend
Carry
Const
Expr
Pred
Var
Lemmas (file)
Operations
Add
Append
Eq
Extract
GetLsbD
Mul
Neg
Not
Replicate
RotateLeft
RotateRight
ShiftLeft
ShiftRight
SignExtend
Sub
Udiv
Ult
Umod
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
Time (file)
Date (file)
Unit
Basic
Day
Month
Week
Weekday
Year
Basic
PlainDate
ValidDate
DateTime (file)
PlainDateTime
Timestamp
Format (file)
Basic
Internal (file)
Bounded
UnitVal
Notation (file)
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
expdb (file)
Example
references (file)

Color scheme