General documentation

index
foundational types
tactics

Library

Hale (file)
Aeson (file)
Data
Aeson (file)
Decode
Encode
Types
AnsiTerminal (file)
System
Console
ANSI
AutoUpdate (file)
Control
AutoUpdate
Base (file)
Control
Concurrent (file)
Chan
Green
MVar
QSem
QSemN
Scheduler
Applicative
Arrow
Category
Exception
Monad
Data
Functor
Compose
Const
Contravariant
Identity
Product
Sum
List (file)
NonEmpty
Bifunctor
Bits
Bool
Char
Complex
Either
Fixed
Foldable
Function
IORef
Ix
Maybe
Newtype
Ord
Proxy
Ratio
String
Traversable
Tuple
Unique
Void
System
Environment
Exit
IO
Base64 (file)
Data
ByteString
Base64
BsbHttpChunked (file)
Network
HTTP
Chunked
ByteString (file)
Data
ByteString (file)
Lazy (file)
Char8
Internal
Builder
Char8
Internal
Short
CaseInsensitive (file)
Data
CaseInsensitive
Conduit (file)
Data
Conduit (file)
Internal
Conduit
Pipe
Combinators
ConfiguratorPg (file)
Data
Configurator (file)
Types
Containers (file)
Data
Map (file)
Strict
IntMap
Set
Cookie (file)
Web
Cookie
DataDefault (file)
Data
Default
DataFrame (file)
DataFrame (file)
IO
CSV
Internal
Column
Types
Operations
Aggregation
Join
Sort
Statistics
Subset
Transform
Display
FastLogger (file)
System
Log
FastLogger
Hasql (file)
Database
PostgreSQL
LibPQ (file)
Types
Hasql
Connection
Decoders
Encoders
Pool
Session
Statement
Http2 (file)
Network
HTTP2
Frame
Decode
Encode
Types
HPACK
Decode
Encode
Huffman
Table
FlowControl
Server
Stream
Types
Http3 (file)
Network
HTTP3
QPACK
Decode
Encode
Table
Error
Frame
Server
HttpClient (file)
Network
HTTP
Client
Connection
Redirect
Request
Response
Types
HttpConduit (file)
Network
HTTP
Client
Conduit
Simple
HttpDate (file)
Network
HTTP
Date
HttpTypes (file)
Network
HTTP
Types
Header
Method
Status
URI
Version
IpRoute (file)
Data
IP
Jose (file)
Crypto
JOSE
FFI
JWK
JWS
JWT
Types
MimeTypes (file)
Network
Mime
Mtl (file)
Control
Monad
Except
Reader
State
Trans
Network (file)
Network
Socket (file)
Blocking
ByteString
EventDispatcher
FFI
Types
OptParse (file)
Options
Applicative (file)
Builder
Extra
Types
PostgREST (file)
PostgREST
ApiRequest
Preferences
Types
Auth (file)
Types
Cache
Sieve
Config (file)
Database
JSPath
PgVersion
Proxy
Error (file)
Types
Plan
CallPlan
MutatePlan
ReadPlan
Types
Query
SqlFragment
Response (file)
GucHeader
OpenAPI
Performance
SchemaCache (file)
Identifiers
Relationship
Representations
Routine
Table
Admin
App
AppState
CLI
Cors
Debounce
Listener
Logger
MainTx
MediaType
Metrics
Network
Observation
RangeQuery
TimeIt
Unix
Version
QUIC (file)
Network
QUIC
Client
Config
Connection
Server
Stream
Types
Recv (file)
Network
Socket
Recv
Req (file)
Network
HTTP
Req
ResourceT (file)
Control
Monad
Trans
Resource
STM (file)
Control
Concurrent
STM
TMVar
TQueue
TVar
Monad
STM
Scientific (file)
Data
Scientific
SimpleSendfile (file)
Network
Sendfile
StreamingCommons (file)
Data
Streaming
Network
TLS (file)
Network
TLS
Context
Types
Text (file)
Data
Text (file)
Encoding
Time (file)
Data
Time
Clock
TimeManager (file)
System
TimeManager
UnixCompat (file)
System
Posix
Compat
UnliftIO (file)
Control
Monad
IO
Unlift
Vault (file)
Data
Vault
Vector (file)
Data
Vector
WAI (file)
Network
Wai (file)
Internal
WaiAppStatic (file)
Network
Wai
Application
Static
WaiAppStatic
Storage
Filesystem
Types
WaiExtra (file)
Network
Wai
EventSource (file)
EventStream
Middleware
RequestLogger (file)
JSON
RequestSizeLimit (file)
Internal
AcceptOverride
AddHeaders
Approot
Autohead
CleanPath
CombineHeaders
ForceDomain
ForceSSL
Gzip
HealthCheckEndpoint
HttpAuth
Jsonp
Local
MethodOverride
MethodOverridePost
RealIp
Rewrite
Routed
Select
StreamFile
StripHeaders
Timeout
ValidateHeaders
Vhost
Test (file)
Internal
Header
Parse
Request
UrlMap
WaiHttp2Extra (file)
Network
Wai
Middleware
Push
Referer (file)
LRU
Manager
ParseURL
Types
WaiLogger (file)
Network
Wai
Logger
WaiWebSockets (file)
Network
Wai
Handler
WebSockets
Warp (file)
Network
Wai
Handler
Warp (file)
Conduit
Counter
Date
HashMap
Header
IO
Internal
PackInt
ReadInt
Request
Response
Run
SendFile
Settings
Types
WithApplication
WarpQUIC (file)
Network
Wai
Handler
WarpQUIC
WarpTLS (file)
Network
Wai
Handler
WarpTLS (file)
Internal
WebSockets (file)
Network
WebSockets
Connection
Frame
Handshake
Types
Word8 (file)
Data
Word8
Init (file)
Control (file)
Lawful (file)
MonadAttach (file)
Instances
Lemmas
MonadLift (file)
Basic
Instances
Lemmas
Basic
Instances
Lemmas
Basic
Do
EState
Except
ExceptCps
Id
MonadAttach
Option
Reader
State
StateCps
StateRef
Data (file)
Array (file)
Lex (file)
Basic
Lemmas
QSort (file)
Basic
Sort (file)
Basic
Lemmas
Subarray (file)
Split
Attach
Basic
BasicAux
BinSearch
Bootstrap
Count
DecidableEq
Erase
Extract
FinRange
Find
GetLit
InsertIdx
InsertionSort
Int
Lemmas
MapIdx
Mem
MinMax
Monadic
Nat
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
Repr
ToString
Iterators (file)
Combinators (file)
Monadic (file)
Append
Attach
FilterMap
FlatMap
Take
ULift
Append
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)
Append
Attach
FilterMap
FlatMap
Take
ULift
Append
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)
Int (file)
Sum
Nat (file)
BEq
Basic
Count
Erase
Find
InsertIdx
Modify
Pairwise
Perm
Range
Sublist
Sum
TakeDrop
Scan (file)
Basic
Lemmas
Sort (file)
Basic
Impl
Lemmas
SplitOn (file)
Basic
Lemmas
Attach
Basic
BasicAux
Control
ControlImpl
Count
Erase
FinRange
Find
Impl
Lemmas
Lex
MapIdx
MinMax
MinMaxIdx
MinMaxOn
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
ToString
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
MinMaxOn
Opposite
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
InternalLemmas
Lemmas
Notation
Operations
String (file)
Iter (file)
Basic
Intercalate
Lemmas (file)
Pattern (file)
Find (file)
Basic
Char
Pred
String
Split (file)
Basic
Char
Pred
String (file)
Basic
ForwardPattern
ForwardSearcher
TakeDrop (file)
Basic
Char
Pred
String
Basic
Char
Memcmp
Pred
Basic
FindPos
Hashable
Intercalate
IsEmpty
Iter
Iterate
Modify
Order
Search
Slice
Splits
StringOrder
TakeDrop
Pattern (file)
Basic
Char
Pred
String
Basic
Bootstrap
Decode
Defs
Extra
FindPos
Hashable
Iterate
Iterator
Legacy
Modify
OrderInstances
PosRaw
Search
Slice
Stream
Subslice
Substring
TakeDrop
Termination
ToSlice
Subtype (file)
Basic
Order
OrderExtra
Sum (file)
Basic
Lemmas
ToString (file)
Basic
Extra
Macro
Name
UInt (file)
Basic
BasicAux
Bitwise
Lemmas
Log2
Vector (file)
Algebra
Attach
Basic
Count
DecidableEq
Erase
Extract
FinRange
Find
InsertIdx
Int
Lemmas
Lex
MapIdx
Monadic
Nat
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)
Simp
SimprocDSL
Lemmas
System (file)
FilePath
IO
IOError
Platform
Promise
ST
Uri
BinderNameHint
BinderPredicates
ByCases
CbvSimproc
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
Lake (file)
Build (file)
Job (file)
Basic
Monad
Register
Target (file)
Basic
Fetch
Actions
Common
Context
Data
Executable
ExternLib
Facets
Fetch
Index
Info
Infos
InitFacets
InputFile
Key
Library
Module
ModuleArtifacts
Package
Run
Store
Targets
Topological
Trace
CLI
Actions
Config (file)
Artifact
Cache
ConfigDecl
ConfigTarget
Context
Defaults
Dependency
Dynlib
Env
ExternLib
ExternLibConfig
FacetConfig
Glob
InputFile
InputFileConfig
InstallPath
Kinds
LakeConfig
Lang
LeanConfig
LeanExe
LeanExeConfig
LeanLib
LeanLibConfig
Meta
MetaClasses
Module
Monad
Opaque
OutFormat
Package
PackageConfig
Pattern
Script
TargetConfig
Workspace
WorkspaceConfig
DSL (file)
Attributes
AttributesCore
Config
DeclUtil
Extensions
Key
Meta
Package
Require
Script
Syntax
Targets
VerLit
Toml (file)
Data (file)
DateTime
Dict
Value
Elab (file)
Expression
Value
Decode
Encode
Grammar
Load
ParserUtil
Util (file)
Binder
Casing
Cli
Cycle
Date
EStateT
EquipT
Error
Exit
Family
FilePath
Git
IO
JsonObject
Lift
Lock
Log
MainM
Message
Name
NativeLib
Opaque
OpaqueType
OrdHashSet
OrderedTagAttribute
Proc
RBArray
Reservoir
Store
StoreInsts
String
Task
Url
Version
Reservoir
Version
Lean (file)
Compiler (file)
IR (file)
Basic
Checker
CompilerM
EmitLLVM
EmitUtil
Format
LLVMBindings
Meta
NormIds
Sorry
ToIR
ToIRType
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
CoalesceRC
CompatibleTypes
CompilerM
ConfigOptions
DeclHash
DependsOn
ElimDead
ElimDeadBranches
EmitC
EmitUtil
ExpandResetReuse
ExplicitBoxing
ExplicitRC
ExtractClosed
FVarUtil
FixedParams
FloatLetIn
InferBorrow
InferType
Internalize
Irrelevant
JoinPoints
LCtx
LambdaLifting
Level
LiveVars
Main
MonadScope
MonoTypes
OtherDecl
PassManager
Passes
PhaseExt
PrettyPrinter
Probing
PropagateBorrow
PublicDeclsExt
PullFunDecls
PullLetDecls
PushProj
ReduceArity
ReduceJpArity
Renaming
ResetReuse
ScopeM
SimpCase
SimpleGroundExpr
SpecInfo
Specialize
SplitSCC
StructProjCases
ToDecl
ToExpr
ToImpure
ToImpureType
ToLCNF
ToMono
Toposort
Types
Util
Visibility
BorrowedAnnotation
CSimpAttr
ClosedTermCache
ExportAttr
ExternAttr
FFI
ImplementedByAttr
InitAttr
InlineAttrs
Main
MetaAttr
ModPkgExt
NameDemangling
NameMangling
NeverExtractAttr
NoncomputableAttr
Old
Options
Specialize
Data (file)
Iterators (file)
Producers (file)
PersistentHashMap
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 (file)
AdditionalOperations
Basic
Array
AssocList
DeclarationRange
EditDistance
Format
FuzzyMatching
JsonRpc
KVMap
LBool
LOption
Name
NameTrie
OpenDecl
Options
PersistentArray
PersistentHashMap
PersistentHashSet
Position
PrefixTree
RArray
RBMap
RBTree
SMap
SSet
Trie
DocString (file)
Add
Extension
Formatter
Links
Markdown
Parser
Syntax
Types
Elab (file)
BuiltinDo (file)
Basic
For
If
Jump
Let
Match
MatchExpr
Misc
TryCatch
Command (file)
Scope
WithWeakNamespace
Deriving (file)
BEq
Basic
DecEq
FromToJson
Hashable
Inhabited
LawfulBEq
Nonempty
Ord
ReflBEq
Repr
SizeOf
ToExpr
TypeName
Util
Do (file)
Basic
Control
InferControlInfo
Legacy
PatternVar
Switch
DocString (file)
Builtin (file)
Keywords
Parsing
Postponed
Scopes
InfoTree (file)
InlayHints
Main
Types
PreDefinition (file)
PartialFixpoint (file)
Eqns
Induction
Main
Structural (file)
BRecOn
Basic
Eqns
FindRecArg
IndGroupInfo
IndPred
Main
Preprocess
RecArgInfo
SmartUnfolding
WF (file)
Basic
Eqns
Fix
FloatRecApp
GuessLex
Main
PackMutual
Preprocess
Rel
Unfold
Basic
EqUnfold
Eqns
EqnsUtils
FixedParams
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
ApplyControlFlow
Basic
EmbeddedConstraint
Enums
IntToBitVec
Rewrite
ShortCircuit
Simproc
Structures
TypeAnalysis
Attr
BVCheck
BVTrace
LRAT
LRAT (file)
Trim
External
Conv (file)
Basic
Cbv
Change
Congr
Delta
Lets
Pattern
Rewrite
Simp
Unfold
Do (file)
ProofMode (file)
Assumption
Basic
Cases
Clear
Constructor
Delab
Exact
Exfalso
Focus
Frame
Have
Intro
LeftRight
MGoal
Pure
Refine
RenameI
Revert
Specialize
VCGen (file)
Basic
Split
SuggestInvariant
Attr
LetElim
Spec
Syntax
Grind (file)
Anchor
Annotated
Basic
BuiltinTactic
Config
Filter
Have
Lint
LintExceptions
Main
Param
RegisterSymSimp
ShowState
SimprocDSL
SimprocDSLBuiltin
Sym
Trace
Omega (file)
Core
Frontend
MinNatAbs
OmegaM
AsAuxLemma
Basic
BoolToPropSimps
BuiltinTactic
Calc
Cbv
CbvSimproc
Change
Classical
Config
ConfigSetter
Congr
Decide
Delta
DiscrTreeKey
Doc
ElabTerm
ExposeNames
Ext
FalseOrByContra
Generalize
Guard
Induction
Injection
Lets
LibrarySearch
Location
Match
Meta
Monotonicity
NormCast
RCases
RenameInaccessibles
Repeat
Rewrite
Rewrites
Rfl
Show
ShowTerm
Simp
SimpArith
SimpTrace
Simpa
Simproc
SolveByElim
Split
Symm
TreeTacAttr
Try
Unfold
Term (file)
TermElabM
App
Arg
AssertExists
Attributes
AutoBound
AuxDef
BinderPredicates
Binders
BindersUtil
BuiltinCommand
BuiltinEvalCommand
BuiltinNotation
BuiltinTerm
Calc
CheckTactic
Coinductive
ComputedFields
Config
DeclModifiers
DeclNameGen
DeclUtil
Declaration
DeclarationRange
DefView
DeprecatedArg
ElabRules
ErrorExplanation
ErrorUtils
Eval
Exception
Extra
Frontend
GenInjective
GuardMsgs
Idbg
Import
Inductive
InfoTrees
InheritDoc
LetRec
Level
Macro
MacroArgUtil
MacroRules
Match
MatchAltView
MatchExpr
Mixfix
MutualDef
MutualInductive
Notation
Open
Parallel
ParseImportsFast
PatternVar
Print
RecAppSyntax
RecommendedSpelling
SetOption
StructInst
StructInstHint
Structure
Syntax
SyntheticMVars
Task
Time
Util
WhereFinally
Language
Lean (file)
Types
Basic
Util
LibrarySuggestions (file)
Basic
Default
MePo
SineQuaNon
SymbolFrequency
Linter (file)
Basic
Builtin
Coe
ConstructorAsVariable
Deprecated
DocsOnAlt
List
MissingDocs
Omit
Sets
UnusedSimpArgs
UnusedVariables
Util
Meta (file)
ArgsPacker (file)
Basic
Constructions (file)
BRecOn
CasesOn
CasesOnSameCtor
CtorElim
CtorIdx
NoConfusion
RecOn
SparseCasesOn
SparseCasesOnEq
DiscrTree (file)
Basic
Main
Types
Util
Match (file)
MatcherApp (file)
Basic
Transform
AltTelescopes
Basic
CaseArraySizes
CaseValues
MVarRenaming
Match
MatchEqs
MatchEqsExt
MatchPatternAttr
MatcherInfo
NamedPatterns
Rewrite
SimpH
SolveOverlap
Value
Sym (file)
Simp (file)
App
Attr
CongrInfo
ControlFlow
Debug
Discharger
DiscrTree
EvalGround
Forall
Goal
Have
Lambda
Main
RegisterCommand
Result
Rewrite
SimpM
Simproc
Telescope
Theorems
Variant
AbstractS
AlphaShareBuilder
AlphaShareCommon
Apply
Canon
Eta
ExprPtr
Grind
InferType
InstantiateMVarsS
InstantiateS
Intro
IsClass
LitValues
LooseBVarsS
MaxFVar
Offset
Pattern
ProofInstInfo
ReplaceS
SymM
SynthInstance
Util
Tactic (file)
AC (file)
Main
Cbv (file)
BuiltinCbvSimprocs
Array
Core
String
CbvEvalExt
CbvSimproc
ControlFlow
Main
Opaque
TheoremsLookup
Util
Grind (file)
AC (file)
Action
DenoteExpr
Eq
Internalize
Inv
PP
Proof
Seq
ToExpr
Types
Util
Var
VarRename
Arith (file)
CommRing (file)
Action
DenoteExpr
EqCnstr
Functions
Internalize
Inv
MonadCanon
MonadRing
MonadSemiring
NonCommRingM
NonCommSemiringM
PP
Poly
Power
Proof
Reify
RingId
RingM
SafePoly
SemiringM
ToExpr
Types
VarRename
Cutsat (file)
Action
CommRing
DvdCnstr
EqCnstr
Inv
LeCnstr
MBTC
Model
Nat
Norm
Proof
ReorderVars
Search
SearchM
ToInt
ToIntInfo
Types
Util
Var
VarRename
Linear (file)
Action
Den
DenoteExpr
IneqCnstr
Internalize
Inv
LinearM
MBTC
Model
OfNatModule
PP
Proof
PropagateEq
Reify
Search
SearchM
StructId
ToExpr
Types
Util
Var
VarRename
EvalNum
FieldNormNum
Insts
IsRelevant
Main
Model
ModelUtil
Propagate
Simproc
Types
Util
Order (file)
Assert
Internalize
OrderM
Proof
StructId
Types
Util
Action
Anchor
Attr
Beta
Cases
CasesMatch
CastLike
CheckResult
CollectParams
Core
Ctor
CtorIdx
Diseq
EMatch
EMatchAction
EMatchTheorem
EMatchTheoremParam
EMatchTheoremPtr
EqResolution
Ext
ExtAttr
Extension
Filter
Finish
ForallProp
Injection
Injective
Internalize
Intro
Inv
LawfulEqCmp
Lookahead
MBTC
Main
MarkNestedSubsingletons
MatchCond
MatchDiscrOnly
OrderInsts
PP
Parser
Proj
Proof
ProofUtil
Propagate
PropagateInj
PropagatorAttr
ProveEq
ReflCmp
RegisterCommand
RevertAll
Simp
SimpUtil
Solve
Split
SynthInstance
Theorems
Types
Util
VarRename
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
Try (file)
Collect
Acyclic
Apply
Assert
Assumption
AuxLemma
Backtrack
Cases
CasesOnStuckLHS
Cleanup
Clear
Congr
Constructor
Contradiction
Delta
ElimInfo
ExposeNames
Ext
FVarSubst
FunInd
FunIndCollect
FunIndInfo
Generalize
IndependentOf
Induction
Injection
Intro
Lets
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
CasesInfo
Check
CheckTactic
Closure
Coe
CoeAttr
CollectFVars
CollectMVars
CompletionName
CongrTheorems
CtorIdxHInj
CtorRecognizer
DecLevel
Diagnostics
Eqns
Eval
ExprDefEq
ExprLens
ExprTraverse
ForEachExpr
FunInfo
GeneralizeTelescope
GeneralizeVars
GetUnfoldableConst
HasNotBit
HaveTelescope
Hint
IndPredBelow
Inductive
InferType
Injective
Instances
IntInstTesters
Iterator
KAbstract
KExprMap
LazyDiscrTree
LetToHave
LevelDefEq
LitValues
MatchUtil
MethodSpecs
MkIffOfInductiveProp
MonadSimp
NatInstTesters
NatTable
Native
Offset
Order
PPGoal
PProdN
ProdN
RecExt
RecursorInfo
Reduce
ReduceEval
SameCtorUtils
SizeOf
Sorry
SplitSparseCasesOn
StringLitProof
Structure
SynthInstance
Transform
TransparencyMode
TryThis
UnificationHint
WHNF
WrapInstance
Parser (file)
Module (file)
Syntax
Tactic (file)
Doc
Term (file)
Basic
Doc
Attr
Basic
Command
Do
Extension
Extra
Level
StrInterpolation
Syntax
Types
ParserCompiler (file)
Attribute
PrettyPrinter (file)
Delaborator (file)
Attributes
Basic
Builtins
DeclWithSig
FieldNotation
Options
SubExpr
TopDownAnalyze
Basic
Formatter
Parenthesizer
Server (file)
CodeActions (file)
Attr
Basic
Provider
UnknownIdentifier
Completion (file)
CompletionCollectors
CompletionInfoSelection
CompletionItemCompression
CompletionResolution
CompletionUtils
EligibleHeaderDecls
ImportCompletion
SyntheticCompletion
FileWorker (file)
ExampleHover
InlayHints
RequestHandling
SemanticHighlighting
SetupFile
SignatureHelp
Utils
WidgetRequests
Rpc (file)
Basic
Deriving
RequestHandling
Test (file)
Cancel
Refs
Runner
AsyncList
FileSource
GoTo
InfoUtils
Logging
ProtocolOverview
References
RequestCancellation
Requests
ServerTask
Snapshots
Utils
Watchdog
Util (file)
CollectAxioms
CollectFVars
CollectLevelMVars
CollectLevelParams
CollectLooseBVars
CollectMVars
Diff
FVarSubset
FindExpr
FindLevelMVar
FindMVar
FoldConsts
ForEachExpr
ForEachExprWhere
HasConstCache
Heartbeats
InstantiateLevelParams
LakePath
LeanOptions
MonadBacktrack
MonadCache
NumApps
NumObjs
OccursCheck
PPExt
ParamMinimizer
Path
Profile
Profiler
PtrSet
RecDepth
Recognizers
ReplaceExpr
ReplaceLevel
Reprove
SCC
SafeExponentiation
ShareCommon
Sorry
SortExprs
TestExtern
Trace
Widget (file)
Basic
Commands
Diff
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
LabelAttribute
Level
LoadDynlib
LocalContext
Log
Message
MetavarContext
Modifiers
MonadEnv
Namespace
OriginalConstKind
PrivateName
ProjFns
ReducibilityAttrs
Replay
ReservedNameAction
ResolveName
Runtime
ScopedEnvExtension
Setup
Shell
Structure
SubExpr
Syntax
ToExpr
ToLevel
Std (file)
Data (file)
DHashMap (file)
Internal
AssocList
Basic
Iterator
Lemmas
Defs
HashesTo
Index
Model
Raw
RawLemmas
WF
AdditionalOperations
Basic
DecidableEquiv
Iterator
IteratorLemmas
Lemmas
Raw
RawDecidableEquiv
RawDef
RawLemmas
DTreeMap (file)
Internal
WF
Defs
Lemmas
Balanced
Balancing
Cell
Def
Lemmas
Model
Operations
Ordered
Queries
Zipper
Raw (file)
AdditionalOperations
Basic
DecidableEquiv
Iterator
Lemmas
Slice
WF
AdditionalOperations
Basic
DecidableEquiv
Iterator
Lemmas
Slice
ExtDHashMap (file)
Basic
Lemmas
ExtDTreeMap (file)
Basic
Lemmas
ExtHashMap (file)
Basic
Lemmas
ExtHashSet (file)
Basic
Lemmas
ExtTreeMap (file)
Basic
Lemmas
ExtTreeSet (file)
Basic
Lemmas
HashMap (file)
AdditionalOperations
Basic
DecidableEquiv
Iterator
IteratorLemmas
Lemmas
Raw
RawDecidableEquiv
RawLemmas
HashSet (file)
Basic
DecidableEquiv
Iterator
IteratorLemmas
Lemmas
Raw
RawDecidableEquiv
RawLemmas
Internal
List
Associative
Defs
Cut
Iterators (file)
Combinators (file)
Monadic (file)
Drop
DropWhile
StepSize
TakeWhile
Zip
Drop
DropWhile
StepSize
TakeWhile
Zip
Consumers (file)
Monadic (file)
Set
Set
Lemmas (file)
Combinators (file)
Monadic (file)
Drop
DropWhile
FilterMap
TakeWhile
Zip
Drop
DropWhile
TakeWhile
Zip
Consumers (file)
Monadic (file)
Collect
Loop
Set
Collect
Loop
Set
Equivalence (file)
Basic
HetT
StepCongr
Producers (file)
Monadic (file)
Array
Empty
List
Vector
Array
Empty
Range
Repeat
Slice
Vector
Monadic
Producers (file)
Monadic (file)
Array
Empty
Vector
Array
Empty
Range
Repeat
Slice
Vector
String (file)
ToInt
ToNat
TreeMap (file)
Raw (file)
AdditionalOperations
Basic
DecidableEquiv
Iterator
Lemmas
Slice
WF
AdditionalOperations
Basic
DecidableEquiv
Iterator
Lemmas
Slice
TreeSet (file)
Raw (file)
Basic
DecidableEquiv
Iterator
Lemmas
Slice
WF
AdditionalOperations
Basic
DecidableEquiv
Iterator
Lemmas
Slice
ByteSlice
Do (file)
SPred (file)
Notation (file)
Basic
DerivedLaws
Laws
SPred
SVal
Triple (file)
Basic
SpecLemmas
WP (file)
Basic
Monad
SimpLemmas
PostCond
PredTrans
Internal (file)
Async (file)
Basic
ContextAsync
DNS
IO
Process
Select
Signal
System
TCP
Timer
UDP
Http (file)
Data (file)
Body (file)
Any
Basic
Empty
Full
Length
Stream
Headers (file)
Basic
Name
Value
URI (file)
Basic
Config
Encoding
Parser
Chunk
Extensions
Method
Request
Response
Status
Version
Internal (file)
Char
ChunkedBuffer
Encode
IndexMultiMap
LowerCase
String
Parsec (file)
Basic
ByteArray
String
UV (file)
DNS
Loop
Signal
System
TCP
Timer
UDP
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)
Barrier
Basic
Broadcast
CancellationContext
CancellationToken
Channel
Mutex
Notify
RecursiveMutex
SharedMutex
StreamMap
Tactic (file)
BVDecide (file)
Bitblast (file)
BVExpr (file)
Circuit (file)
Impl (file)
Operations
Add
Append
Clz
Cpop
Eq
Extract
GetLsbD
Mul
Neg
Not
Replicate
Reverse
RotateLeft
RotateRight
ShiftLeft
ShiftRight
Sub
Udiv
Ult
Umod
ZeroExtend
Carry
Const
Expr
Pred
Substructure
Var
Lemmas (file)
Operations
Add
Append
Clz
Cpop
Eq
Extract
GetLsbD
Mul
Neg
Not
Replicate
Reverse
RotateLeft
RotateRight
ShiftLeft
ShiftRight
Sub
Udiv
Ult
Umod
ZeroExtend
Basic
Carry
Const
Expr
Pred
Var
Basic
BoolExpr (file)
Basic
LRAT (file)
Internal
Formula (file)
Class
Implementation
Instance
Lemmas
RatAddResult
RatAddSound
RupAddResult
RupAddSound
Actions
Assignment
CNF
Clause
CompactLRATChecker
CompactLRATCheckerSound
Convert
Entails
LRATChecker
LRATCheckerSound
PosFin
Actions
Checker
Parser
Normalize (file)
BitVec
Bool
Canonicalize
Equal
Prop
Reflect
Syntax
Do (file)
ProofMode
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

Color scheme