General documentation

index
foundational types

Library

Init (file)
Control (file)
Lawful (file)
MonadLift (file)
Basic
Instances
Lemmas
Basic
Instances
Lemmas
Basic
EState
Except
ExceptCps
Id
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
Dyadic (file)
Basic
Instances
Inv
Round
Fin (file)
Basic
Bitwise
Fold
Iterate
Lemmas
Log2
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
Access
Collect
Loop
Partial
Stream
Internal (file)
LawfulMonadLiftFunction
Termination
Lemmas (file)
Combinators (file)
Monadic (file)
Attach
FilterMap
FlatMap
Take
ULift
Attach
FilterMap
FlatMap
Take
ULift
Consumers (file)
Monadic (file)
Collect
Loop
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
Basic
Compare
Control
Coprime
Dvd
Fold
Gcd
Lcm
Lemmas
Linear
Log2
MinMax
Mod
Order
Power2
SOM
Simproc
Option (file)
Array
Attach
Basic
BasicAux
Coe
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
GetElemTactic
Instances
Int
IntLemmas
Iterators
Lemmas
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
Splits
Pattern (file)
Basic
Char
Pred
String
Basic
Bootstrap
Decode
Defs
Extra
Iterator
Modify
PosRaw
Repr
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
Attr
Cases
Config
Ext
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
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
WFTactics
While
LeanLangur (file)
Basic

Color scheme