Index
Symbols
A
-
Add
-
Add.
add -
Append
-
Append.
append -
Array
-
Array.
all -
Array.
allDiff -
Array.
allM -
Array.
any -
Array.
anyM -
Array.
append -
Array.
appendList -
Array.
attach -
Array.
attachWith -
Array.
back -
Array.
back! -
Array.
back? -
Array.
binInsert -
Array.
binInsertM -
Array.
binSearch -
Array.
binSearchContains -
Array.
concatMap -
Array.
concatMapM -
Array.
contains -
Array.
elem -
Array.
empty -
Array.
erase -
Array.
eraseIdx -
Array.
eraseReps -
Array.
extract -
Array.
filter -
Array.
filterM -
Array.
filterMap -
Array.
filterMapM -
Array.
filterPairsM -
Array.
filterSepElems -
Array.
filterSepElemsM -
Array.
find? -
Array.
findIdx? -
Array.
findIdxM? -
Array.
findM? -
Array.
findRev? -
Array.
findRevM? -
Array.
findSome! -
Array.
findSome? -
Array.
findSomeM? -
Array.
findSomeRev? -
Array.
findSomeRevM? -
Array.
flatMap -
Array.
flatMapM -
Array.
flatten -
Array.
foldl -
Array.
foldlM -
Array.
foldr -
Array.
foldrM -
Array.
forIn' -
Array.
forM -
Array.
forRevM -
Array.
get -
Array.
get! -
Array.
get? -
Array.
getD -
Array.
getEvenElems -
Array.
getIdx? -
Array.
getMax? -
Array.
groupByKey -
Array.
indexOf? -
Array.
insertAt -
Array.
insertAt! -
Array.
insertionSort -
Array.
isEmpty -
Array.
isEqv -
Array.
isPrefixOf -
Array.
map -
Array.
mapFinIdx -
Array.
mapFinIdxM -
Array.
mapIdx -
Array.
mapIdxM -
Array.
mapIndexed -
Array.
mapIndexedM -
Array.
mapM -
Array.
mapM' -
Array.
mapMono -
Array.
mapMonoM -
Array.
mk -
Array.
mkArray -
Array.
modify -
Array.
modifyM -
Array.
modifyOp -
Array.
ofFn -
Array.
ofSubarray -
Array.
partition -
Array.
pop -
Array.
popWhile -
Array.
push -
Array.
qsort -
Array.
qsortOrd -
Array.
range -
Array.
reduceGetElem -
Array.
reduceGetElem! -
Array.
reduceGetElem? -
Array.
reduceOption -
Array.
reverse -
Array.
sequenceMap -
Array.
set -
Array.
set! -
Array.
setD -
Array.
singleton -
Array.
size -
Array.
split -
Array.
swap -
Array.
swap! -
Array.
swapAt -
Array.
swapAt! -
Array.
take -
Array.
takeWhile -
Array.
toList -
Array.
toListAppend -
Array.
toListRev -
Array.
toPArray' -
Array.
toSubarray -
Array.
uget -
Array.
unattach -
Array.
unzip -
Array.
uset -
Array.
usize -
Array.
zip -
Array.
zipWith -
Array.
zipWithIndex -
ac_rfl
-
accessed
-
adaptExpander
-
add
-
addExtension
-
addHeartbeats
-
addMacroScope
-
admit
-
all
-
allDiff
-
allM
-
allTR
-
all_goals
(0) (1) -
and_intros
-
any
-
anyM
-
anyTR
-
any_goals
(0) (1) -
appDir
-
appPath
-
append
-
appendGoals
-
appendList
-
apply
(0) (1) -
apply?
-
applyEqLemma
-
applySimprocConst
-
apply_assumption
-
apply_ext_theorem
-
apply_mod_cast
-
apply_rfl
-
apply_rules
-
arg [@]i
-
args
-
arith
-
array
-
array_get_dec
-
asTask
-
assumption
-
assumption_mod_cast
-
atEnd
-
attach
-
attachWith
-
autoPromoteIndices
-
autoUnfold
B
-
BEq
-
BEq.
beq -
BaseIO
-
BaseIO.
asTask -
BaseIO.
bindTask -
BaseIO.
mapTask -
BaseIO.
mapTasks -
BaseIO.
toEIO -
BaseIO.
toIO -
Bool
-
Bool.
false -
Bool.
true -
Buffer
-
back
-
back!
-
back?
-
backward.
synthInstance. canonInstances -
below
-
beq
-
beta
-
binInsert
-
binInsertM
-
binSearch
-
binSearchContains
-
bindTask
-
bitwise
-
ble
-
blt
-
bootstrap.
inductiveCheckResultingUniverse -
bv_check
-
bv_decide
-
bv_decide?
-
bv_normalize
-
bv_omega
-
by_cases
-
byteIdx
-
byteSize
C
-
Char
-
Char.
isAlpha -
Char.
isAlphanum -
Char.
isDigit -
Char.
isLower -
Char.
isUpper -
Char.
isWhitespace -
Char.
mk -
CharLit
-
Child
-
Command
-
Config
-
calc
-
cancel
-
canonInstances
-
capitalize
-
case
-
case ...
=> ... -
case'
-
case' ...
=> ... -
caseStrongInductionOn
-
cases
-
casesOn
-
cast
-
catchExceptions
-
change
(0) (1) -
change ...
with ... -
charLitKind
-
checkCanceled
-
checkpoint
-
choiceKind
-
clear
-
closeMainGoal
-
closeMainGoalUsing
-
cmd
-
codepointPosToUtf16Pos
-
codepointPosToUtf16PosFrom
-
codepointPosToUtf8PosFrom
-
colEq
-
colGe
-
colGt
- comment
-
compare
-
components
-
concatMap
-
concatMapM
- configuration
-
congr
(0) (1) -
constructor
(0) (1) -
contains
-
contextual
-
contradiction
-
conv
-
conv => ...
-
conv'
(0) (1) -
createDir
-
createDirAll
-
createTempFile
-
crlfToLf
-
csize
- cumulativity
-
curr
-
currentDir
-
customEliminators
-
cwd
D
-
Decidable
-
Decidable.
isFalse -
Decidable.
isTrue -
DecidableEq
-
DecidableRel
-
DirEntry
-
Div
-
Div.
div -
Dvd
-
Dvd.
dvd -
Dynamic
-
Dynamic.
get? -
Dynamic.
mk -
data
-
dbg_cache
-
dbg_trace
-
decEq
-
decLe
-
decLt
-
decapitalize
-
decide
-
decreasing_tactic
-
decreasing_trivial
-
decreasing_with
-
dedicated
-
deepTerms
-
default
-
delta
(0) (1) -
digitChar
-
discharge
-
div
-
div2Induction
-
done
(0) (1) -
drop
-
dropRight
-
dropRightWhile
-
dropWhile
-
dsimp
(0) (1) -
dsimp!
-
dsimp?
-
dsimp?!
-
dsimpLocation'
-
dvd
E
-
EIO
-
EIO.
asTask -
EIO.
bindTask -
EIO.
catchExceptions -
EIO.
mapTask -
EIO.
mapTasks -
EIO.
toBaseIO -
EIO.
toIO -
EIO.
toIO' -
EST
-
Error
-
Even
-
Even.
plusTwo -
Even.
zero -
elabCasesTargets
-
elabDSimpConfigCore
-
elabSimpArgs
-
elabSimpConfig
-
elabSimpConfigCtxCore
-
elabTerm
-
elabTermEnsuringType
-
elabTermWithHoles
-
elem
-
elemsAndSeps
-
elimOffset
-
empty
-
endPos
-
endsWith
-
ensureHasNoMVars
-
enter
-
env
-
eprint
-
eprintln
-
eq_of_beq
-
eq_refl
-
erase
-
eraseIdx
-
eraseReps
-
erw
(0) (1) -
eta
-
etaStruct
-
exact
-
exact?
-
exact_mod_cast
-
exeExtension
-
exfalso
-
exists
-
exit
-
exitCode
-
expandMacro?
-
ext
(0) (1) -
ext1
-
extSeparator
-
extension
- extensionality
-
extract
F
-
FilePath
-
FileRight
-
fail
-
failIfUnchanged
-
fail_if_success
(0) (1) -
false_or_by_contra
-
fieldIdxKind
-
fileName
-
fileStem
-
filter
-
filterM
-
filterMap
-
filterMapM
-
filterPairsM
-
filterSepElems
-
filterSepElemsM
-
find
-
find?
-
findIdx?
-
findIdxM?
-
findLineStart
-
findM?
-
findRev?
-
findRevM?
-
findSome!
-
findSome?
-
findSomeM?
-
findSomeRev?
-
findSomeRevM?
-
first
(0) (1) -
firstDiffPos
-
flags
-
flatMap
-
flatMapM
-
flatten
-
flush
-
focus
(0) (1) -
fold
-
foldM
-
foldRev
-
foldRevM
-
foldTR
-
foldl
-
foldlM
-
foldr
-
foldrM
-
fopenErrorToString
-
forIn
-
forIn'
-
forM
-
forRevM
-
forward
-
fromExpr?
-
fromUTF8
-
fromUTF8!
-
fromUTF8?
-
front
-
fun
-
funext
(0) (1)
G
-
GetElem
-
GetElem.
getElem -
GetElem?
-
GetElem?.
getElem! -
GetElem?.
getElem? -
GetElem?.
toGetElem -
gcd
-
generalize
-
get
-
get!
-
get'
-
get?
-
getChar
-
getCurrMacroScope
-
getCurrNamespace
-
getCurrentDir
-
getD
-
getElem
-
getElem!
-
getElem!_def
-
getElem?
-
getElem?_def
-
getEnv
-
getEvenElems
-
getFVarId
-
getFVarIds
-
getGoals
-
getHygieneInfo
-
getId
-
getIdx?
-
getKind
-
getLine
-
getMainGoal
-
getMainModule
-
getMainTag
-
getMax?
-
getName
-
getNat
-
getNumHeartbeats
-
getPID
-
getRandomBytes
-
getScientific
-
getStderr
-
getStdin
-
getStdout
-
getString
-
getTaskState
-
getUnsolvedGoals
-
getUtf8Byte
-
get_elem_tactic
-
get_elem_tactic_trivial
- goal
-
ground
-
group
-
groupByKey
-
groupKind
-
guard_expr
-
guard_hyp
-
guard_target
H
-
HAdd
-
HAdd.
hAdd -
HAnd
-
HAnd.
hAnd -
HAppend
-
HAppend.
hAppend -
HDiv
-
HDiv.
hDiv -
HMod
-
HMod.
hMod -
HMul
-
HMul.
hMul -
HOr
-
HOr.
hOr -
HPow
-
HPow.
hPow -
HShiftLeft
-
HShiftLeft.
hShiftLeft -
HShiftRight
-
HShiftRight.
hShiftRight -
HSub
-
HSub.
hSub -
HXor
-
HXor.
hXor -
Handle
-
Hashable
-
Hashable.
hash -
HomogeneousPow
-
HomogeneousPow.
pow -
HygieneInfo
-
h
-
hAdd
-
hAnd
-
hAppend
-
hDiv
-
hMod
-
hMul
-
hOr
-
hPow
-
hShiftLeft
-
hShiftRight
-
hSub
-
hXor
-
hasDecl
-
hasFinished
-
hasNext
-
hasPrev
-
hash
-
have
-
have'
-
haveI
- hygiene
-
hygieneInfoKind
-
hygienic
I
-
IO
-
IO.
Error -
IO.
Error. alreadyExists -
IO.
Error. fopenErrorToString -
IO.
Error. hardwareFault -
IO.
Error. illegalOperation -
IO.
Error. inappropriateType -
IO.
Error. interrupted -
IO.
Error. invalidArgument -
IO.
Error. mkAlreadyExists -
IO.
Error. mkAlreadyExistsFile -
IO.
Error. mkEofError -
IO.
Error. mkHardwareFault -
IO.
Error. mkIllegalOperation -
IO.
Error. mkInappropriateType -
IO.
Error. mkInappropriateTypeFile -
IO.
Error. mkInterrupted -
IO.
Error. mkInvalidArgument -
IO.
Error. mkInvalidArgumentFile -
IO.
Error. mkNoFileOrDirectory -
IO.
Error. mkNoSuchThing -
IO.
Error. mkNoSuchThingFile -
IO.
Error. mkOtherError -
IO.
Error. mkPermissionDenied -
IO.
Error. mkPermissionDeniedFile -
IO.
Error. mkProtocolError -
IO.
Error. mkResourceBusy -
IO.
Error. mkResourceExhausted -
IO.
Error. mkResourceExhaustedFile -
IO.
Error. mkResourceVanished -
IO.
Error. mkTimeExpired -
IO.
Error. mkUnsatisfiedConstraints -
IO.
Error. mkUnsupportedOperation -
IO.
Error. noFileOrDirectory -
IO.
Error. noSuchThing -
IO.
Error. otherError -
IO.
Error. otherErrorToString -
IO.
Error. permissionDenied -
IO.
Error. protocolError -
IO.
Error. resourceBusy -
IO.
Error. resourceExhausted -
IO.
Error. resourceVanished -
IO.
Error. timeExpired -
IO.
Error. toString -
IO.
Error. unexpectedEof -
IO.
Error. unsatisfiedConstraints -
IO.
Error. unsupportedOperation -
IO.
Error. userError -
IO.
FS. DirEntry -
IO.
FS. DirEntry. mk -
IO.
FS. DirEntry. path -
IO.
FS. Handle -
IO.
FS. Handle. flush -
IO.
FS. Handle. getLine -
IO.
FS. Handle. isTty -
IO.
FS. Handle. lock -
IO.
FS. Handle. mk -
IO.
FS. Handle. putStr -
IO.
FS. Handle. putStrLn -
IO.
FS. Handle. read -
IO.
FS. Handle. readBinToEnd -
IO.
FS. Handle. readBinToEndInto -
IO.
FS. Handle. readToEnd -
IO.
FS. Handle. rewind -
IO.
FS. Handle. truncate -
IO.
FS. Handle. tryLock -
IO.
FS. Handle. unlock -
IO.
FS. Handle. write -
IO.
FS. Metadata -
IO.
FS. Metadata. mk -
IO.
FS. Mode -
IO.
FS. Mode. append -
IO.
FS. Mode. read -
IO.
FS. Mode. readWrite -
IO.
FS. Mode. write -
IO.
FS. Mode. writeNew -
IO.
FS. Stream -
IO.
FS. Stream. Buffer -
IO.
FS. Stream. Buffer. data -
IO.
FS. Stream. Buffer. mk -
IO.
FS. Stream. Buffer. pos -
IO.
FS. Stream. mk -
IO.
FS. Stream. ofBuffer -
IO.
FS. Stream. ofHandle -
IO.
FS. Stream. putStrLn -
IO.
FS. createDir -
IO.
FS. createDirAll -
IO.
FS. createTempFile -
IO.
FS. lines -
IO.
FS. readBinFile -
IO.
FS. readFile -
IO.
FS. realPath -
IO.
FS. removeDir -
IO.
FS. removeDirAll -
IO.
FS. removeFile -
IO.
FS. rename -
IO.
FS. withFile -
IO.
(0) (1)FS. withIsolatedStreams -
IO.
FS. withTempFile -
IO.
FS. writeBinFile -
IO.
FS. writeFile -
IO.
FileRight -
IO.
FileRight. flags -
IO.
FileRight. mk -
IO.
Process. Child -
IO.
Process. Child. kill -
IO.
Process. Child. mk -
IO.
Process. Child. takeStdin -
IO.
Process. Child. tryWait -
IO.
Process. Child. wait -
IO.
Process. Output -
IO.
Process. Output. mk -
IO.
Process. SpawnArgs -
IO.
Process. SpawnArgs. mk -
IO.
Process. Stdio -
IO.
Process. Stdio. inherit -
IO.
Process. Stdio. null -
IO.
Process. Stdio. piped -
IO.
Process. Stdio. toHandleType -
IO.
Process. StdioConfig -
IO.
Process. StdioConfig. mk -
IO.
Process. exit -
IO.
Process. getCurrentDir -
IO.
Process. getPID -
IO.
Process. output -
IO.
Process. run -
IO.
Process. setCurrentDir -
IO.
Process. spawn -
IO.
Ref -
IO.
addHeartbeats -
IO.
appDir -
IO.
appPath -
IO.
asTask -
IO.
bindTask -
IO.
cancel -
IO.
checkCanceled -
IO.
currentDir -
IO.
eprint -
IO.
eprintln -
IO.
getEnv -
IO.
getNumHeartbeats -
IO.
getRandomBytes -
IO.
getStderr -
IO.
getStdin -
IO.
getStdout -
IO.
getTaskState -
IO.
hasFinished -
IO.
iterate -
IO.
lazyPure -
IO.
mapTask -
IO.
mapTasks -
IO.
mkRef -
IO.
monoMsNow -
IO.
monoNanosNow -
IO.
ofExcept -
IO.
print -
IO.
println -
IO.
rand -
IO.
setAccessRights -
IO.
setRandSeed -
IO.
setStderr -
IO.
setStdin -
IO.
setStdout -
IO.
sleep -
IO.
toEIO -
IO.
userError -
IO.
wait -
IO.
waitAny -
IO.
withStderr -
IO.
withStdin -
IO.
withStdout -
Ident
-
Inhabited
-
Inhabited.
default -
Iterator
-
i
-
ibelow
-
identKind
- identifier
-
if ...
then ... else ... -
if h : ...
then ... else ... -
imax
-
implicitDefEqProofs
- impredicative
- inaccessible
- index
-
indexOf?
- indexed family
-
induction
-
inductionOn
-
inductive.
autoPromoteIndices -
inductiveCheckResultingUniverse
-
inferInstance
-
inferInstanceAs
-
infer_instance
-
injection
-
injections
-
insertAt
-
insertAt!
-
insertionSort
- instance synthesis
-
intercalate
-
interpolatedStrKind
-
interpolatedStrLitKind
-
intro
(0) (1) -
intro | ...
=> ... | ... => ... -
intros
-
iota
-
isAbsolute
-
isAlpha
-
isAlphanum
-
isDigit
-
isDir
-
isEmpty
-
isEqv
-
isInt
-
isLower
-
isNat
-
isOfKind
-
isPowerOfTwo
-
isPrefixOf
-
isRelative
-
isTty
-
isUpper
-
isValid
-
isValidChar
-
isValue
-
isWhitespace
-
iter
-
iterate
J
K
L
-
LE
-
LE.
le -
LT
-
LT.
lt -
LawfulBEq
-
LawfulBEq.
eq_of_beq -
LawfulBEq.
rfl -
LawfulGetElem
-
LawfulGetElem.
getElem!_def -
LawfulGetElem.
getElem?_def -
LeadingIdentBehavior
-
Lean.
Elab. Tactic. Tactic -
Lean.
Elab. Tactic. TacticM -
Lean.
Elab. Tactic. adaptExpander -
Lean.
Elab. Tactic. appendGoals -
Lean.
Elab. Tactic. closeMainGoal -
Lean.
Elab. Tactic. closeMainGoalUsing -
Lean.
Elab. Tactic. dsimpLocation' -
Lean.
Elab. Tactic. elabCasesTargets -
Lean.
Elab. Tactic. elabDSimpConfigCore -
Lean.
Elab. Tactic. elabSimpArgs -
Lean.
Elab. Tactic. elabSimpConfig -
Lean.
Elab. Tactic. elabSimpConfigCtxCore -
Lean.
Elab. Tactic. elabTerm -
Lean.
Elab. Tactic. elabTermEnsuringType -
Lean.
Elab. Tactic. elabTermWithHoles -
Lean.
Elab. Tactic. ensureHasNoMVars -
Lean.
Elab. Tactic. focus -
Lean.
Elab. Tactic. getCurrMacroScope -
Lean.
Elab. Tactic. getFVarId -
Lean.
Elab. Tactic. getFVarIds -
Lean.
Elab. Tactic. getGoals -
Lean.
Elab. Tactic. getMainGoal -
Lean.
Elab. Tactic. getMainModule -
Lean.
Elab. Tactic. getMainTag -
Lean.
Elab. Tactic. getUnsolvedGoals -
Lean.
Elab. Tactic. liftMetaMAtMain -
Lean.
Elab. Tactic. mkTacticAttribute -
Lean.
Elab. Tactic. orElse -
Lean.
Elab. Tactic. pruneSolvedGoals -
Lean.
Elab. Tactic. run -
Lean.
Elab. Tactic. runTermElab -
Lean.
Elab. Tactic. setGoals -
Lean.
Elab. Tactic. sortMVarIdArrayByIndex -
Lean.
Elab. Tactic. sortMVarIdsByIndex -
Lean.
Elab. Tactic. tacticElabAttribute -
Lean.
Elab. Tactic. tagUntaggedGoals -
Lean.
Elab. Tactic. tryCatch -
Lean.
Elab. Tactic. tryTactic -
Lean.
Elab. Tactic. tryTactic? -
Lean.
Elab. Tactic. withLocation -
Lean.
Elab. registerDerivingHandler -
Lean.
Macro. Exception. unsupportedSyntax -
Lean.
Macro. addMacroScope -
Lean.
Macro. expandMacro? -
Lean.
Macro. getCurrNamespace -
Lean.
Macro. hasDecl -
Lean.
Macro. resolveGlobalName -
Lean.
Macro. resolveNamespace -
Lean.
Macro. throwError -
Lean.
Macro. throwErrorAt -
Lean.
Macro. throwUnsupported -
Lean.
Macro. trace -
Lean.
Macro. withFreshMacroScope -
Lean.
MacroM -
Lean.
Meta. DSimp. Config -
Lean.
Meta. DSimp. Config. mk -
Lean.
Meta. Occurrences -
Lean.
Meta. Occurrences. all -
Lean.
Meta. Occurrences. neg -
Lean.
Meta. Occurrences. pos -
Lean.
Meta. Rewrite. Config -
Lean.
Meta. Rewrite. Config. mk -
Lean.
Meta. Rewrite. NewGoals -
Lean.
Meta. Simp. Config -
Lean.
Meta. Simp. Config. mk -
Lean.
Meta. Simp. neutralConfig -
Lean.
Meta. SimpExtension -
Lean.
Meta. TransparencyMode -
Lean.
Meta. TransparencyMode. all -
Lean.
Meta. TransparencyMode. default -
Lean.
Meta. TransparencyMode. instances -
Lean.
Meta. TransparencyMode. reducible -
Lean.
Meta. registerSimpAttr -
Lean.
Parser. LeadingIdentBehavior -
Lean.
Parser. LeadingIdentBehavior. both -
Lean.
Parser. LeadingIdentBehavior. default -
Lean.
Parser. LeadingIdentBehavior. symbol -
Lean.
SourceInfo -
Lean.
SourceInfo. none -
Lean.
SourceInfo. original -
Lean.
SourceInfo. synthetic -
Lean.
Syntax -
Lean.
Syntax. CharLit -
Lean.
Syntax. Command -
Lean.
Syntax. HygieneInfo -
Lean.
Syntax. Ident -
Lean.
Syntax. Level -
Lean.
Syntax. NameLit -
Lean.
Syntax. NumLit -
Lean.
Syntax. Prec -
Lean.
Syntax. Preresolved -
Lean.
Syntax. Preresolved. decl -
Lean.
Syntax. Preresolved. namespace -
Lean.
Syntax. Prio -
Lean.
Syntax. ScientificLit -
Lean.
Syntax. StrLit -
Lean.
Syntax. TSepArray -
Lean.
Syntax. TSepArray. mk -
Lean.
Syntax. Tactic -
Lean.
Syntax. Term -
Lean.
Syntax. atom -
Lean.
Syntax. getKind -
Lean.
Syntax. ident -
Lean.
Syntax. isOfKind -
Lean.
Syntax. missing -
Lean.
Syntax. node -
Lean.
Syntax. setKind -
Lean.
SyntaxNodeKind -
Lean.
TSyntax -
Lean.
TSyntax. getChar -
Lean.
TSyntax. getHygieneInfo -
Lean.
TSyntax. getId -
Lean.
TSyntax. getName -
Lean.
TSyntax. getNat -
Lean.
TSyntax. getScientific -
Lean.
TSyntax. getString -
Lean.
TSyntax. mk -
Lean.
TSyntaxArray -
Lean.
charLitKind -
Lean.
choiceKind -
Lean.
fieldIdxKind -
Lean.
groupKind -
Lean.
hygieneInfoKind -
Lean.
identKind -
Lean.
interpolatedStrKind -
Lean.
interpolatedStrLitKind -
Lean.
nameLitKind -
Lean.
nullKind -
Lean.
numLitKind -
Lean.
scientificLitKind -
Lean.
strLitKind -
Level
-
land
-
lazyPure
-
lcm
-
le
-
lean_is_array
-
lean_is_string
-
lean_string_object
(0) (1) -
lean_to_array
-
lean_to_string
-
left
(0) (1) -
length
-
let
-
let rec
-
let'
-
letI
- level
-
lhs
-
liftMetaMAtMain
-
lineEq
-
lines
-
linter.
unnecessarySimpa - literal
-
lock
-
log2
-
lor
-
lt
-
lt_wfRel
M
-
MacroM
-
Metadata
-
Mod
-
Mod.
mod -
Mode
-
Mul
-
Mul.
mul - main goal
-
map
-
mapFinIdx
-
mapFinIdxM
-
mapIdx
-
mapIdxM
-
mapIndexed
-
mapIndexedM
-
mapM
-
mapM'
-
mapMono
-
mapMonoM
-
mapTask
-
mapTasks
-
match
-
max
-
maxDischargeDepth
-
maxHeartbeats
-
maxSize
-
maxSteps
-
memoize
-
metadata
-
min
-
mk
-
mkAlreadyExists
-
mkAlreadyExistsFile
-
mkArray
-
mkEofError
-
mkFilePath
-
mkHardwareFault
-
mkIllegalOperation
-
mkInappropriateType
-
mkInappropriateTypeFile
-
mkInterrupted
-
mkInvalidArgument
-
mkInvalidArgumentFile
-
mkIterator
-
mkNoFileOrDirectory
-
mkNoSuchThing
-
mkNoSuchThingFile
-
mkOtherError
-
mkPermissionDenied
-
mkPermissionDeniedFile
-
mkProtocolError
-
mkRef
-
mkResourceBusy
-
mkResourceExhausted
-
mkResourceExhaustedFile
-
mkResourceVanished
-
mkStdGen
-
mkTacticAttribute
-
mkTimeExpired
-
mkUnsatisfiedConstraints
-
mkUnsupportedOperation
-
mod
-
modCore
-
modified
-
modify
-
modifyGet
-
modifyM
-
modifyOp
-
monoMsNow
-
monoNanosNow
-
mul
-
mvars
N
-
NameLit
-
Nat
-
Nat.
add -
Nat.
all -
Nat.
allM -
Nat.
allTR -
Nat.
any -
Nat.
anyM -
Nat.
anyTR -
Nat.
applyEqLemma -
Nat.
applySimprocConst -
Nat.
below -
Nat.
beq -
Nat.
bitwise -
Nat.
ble -
Nat.
blt -
Nat.
caseStrongInductionOn -
Nat.
casesOn -
Nat.
cast -
Nat.
decEq -
Nat.
decLe -
Nat.
decLt -
Nat.
digitChar -
Nat.
div -
Nat.
div. inductionOn -
Nat.
div2Induction -
Nat.
elimOffset -
Nat.
fold -
Nat.
foldM -
Nat.
foldRev -
Nat.
foldRevM -
Nat.
foldTR -
Nat.
forM -
Nat.
forRevM -
Nat.
fromExpr? -
Nat.
gcd -
Nat.
ibelow -
Nat.
imax -
Nat.
isPowerOfTwo -
Nat.
isValidChar -
Nat.
isValue -
Nat.
land -
Nat.
lcm -
Nat.
le -
Nat.
le. refl -
Nat.
le. step -
Nat.
log2 -
Nat.
lor -
Nat.
lt -
Nat.
lt_wfRel -
Nat.
max -
Nat.
min -
Nat.
mod -
Nat.
mod. inductionOn -
Nat.
modCore -
Nat.
mul -
Nat.
nextPowerOfTwo -
Nat.
noConfusion -
Nat.
noConfusionType -
Nat.
pow -
Nat.
pred -
Nat.
rec -
Nat.
recOn -
Nat.
reduceAdd -
Nat.
reduceBEq -
Nat.
reduceBNe -
Nat.
reduceBeqDiff -
Nat.
reduceBin -
Nat.
reduceBinPred -
Nat.
reduceBneDiff -
Nat.
reduceBoolPred -
Nat.
reduceDiv -
Nat.
reduceEqDiff -
Nat.
reduceGT -
Nat.
reduceGcd -
Nat.
reduceLT -
Nat.
reduceLTLE -
Nat.
reduceLeDiff -
Nat.
reduceMod -
Nat.
reduceMul -
Nat.
reduceNatEqExpr -
Nat.
reducePow -
Nat.
reduceSub -
Nat.
reduceSubDiff -
Nat.
reduceSucc -
Nat.
reduceUnary -
Nat.
repeat -
Nat.
repeatTR -
Nat.
repr -
Nat.
shiftLeft -
Nat.
shiftRight -
Nat.
strongInductionOn -
Nat.
sub -
Nat.
subDigitChar -
Nat.
succ -
Nat.
superDigitChar -
Nat.
testBit -
Nat.
toDigits -
Nat.
toDigitsCore -
Nat.
toFloat -
Nat.
toLevel -
Nat.
toSubDigits -
Nat.
toSubscriptString -
Nat.
toSuperDigits -
Nat.
toSuperscriptString -
Nat.
toUInt16 -
Nat.
toUInt32 -
Nat.
toUInt64 -
Nat.
toUInt8 -
Nat.
toUSize -
Nat.
xor -
Nat.
zero -
NatCast
-
NatCast.
natCast -
NatPow
-
NatPow.
pow -
NeZero
-
NeZero.
out -
Neg
-
Neg.
neg -
NewGoals
-
Nonempty
-
Nonempty.
intro -
NumLit
-
nameLitKind
- namespace
-
natCast
-
native_decide
-
neg
-
neutralConfig
-
newGoals
-
next
-
next ...
=> ... -
next'
-
nextPowerOfTwo
-
nextUntil
-
nextWhile
-
nextn
-
noConfusion
-
noConfusionType
-
nofun
-
nomatch
-
norm_cast
(0) (1) -
normalize
-
nullKind
-
numLitKind
O
P
-
PUnit
-
PUnit.
unit -
Pos
-
Pow
-
Pow.
pow -
Prec
-
Preresolved
-
Prio
-
Priority
-
Prop
- parameter
-
parent
- parser
-
partition
-
path
-
pathExists
-
pathSeparator
-
pathSeparators
-
pattern
- polymorphism
-
pop
-
popFront
-
popWhile
-
pos
-
posOf
-
pow
-
pp.
deepTerms -
pp.
deepTerms. threshold -
pp.
match -
pp.
maxSteps -
pp.
mvars -
pp.
proofs -
pp.
proofs. threshold -
pred
- predicative
-
prev
-
prevn
-
print
-
println
-
proj
- proof state
-
proofs
-
propext
- proposition
-
pruneSolvedGoals
-
ptrEq
-
push
-
push_cast
-
pushn
-
putStr
-
putStrLn
Q
-
qsort
-
qsortOrd
- quantification
-
quote
R
-
RandomGen
-
RandomGen.
next -
RandomGen.
range -
RandomGen.
split -
Ref
-
Repr
-
Repr.
reprPrec -
rand
-
randBool
-
randNat
-
range
-
raw
-
rcases
-
read
-
readBinFile
-
readBinToEnd
-
readBinToEndInto
-
readDir
-
readFile
-
readToEnd
-
realPath
-
rec
-
recOn
- recursor
-
reduce
-
reduceAdd
-
reduceAppend
-
reduceBEq
-
reduceBNe
-
reduceBeqDiff
-
reduceBin
-
reduceBinPred
-
reduceBneDiff
-
reduceBoolPred
-
reduceDiv
-
reduceEq
-
reduceEqDiff
-
reduceGE
-
reduceGT
-
reduceGcd
-
reduceGetElem
-
reduceGetElem!
-
reduceGetElem?
-
reduceLE
-
reduceLT
-
reduceLTLE
-
reduceLeDiff
-
reduceMk
-
reduceMod
-
reduceMul
-
reduceNatEqExpr
-
reduceNe
-
reduceOption
-
reducePow
-
reduceSub
-
reduceSubDiff
-
reduceSucc
-
reduceUnary
- reduction
-
ref
-
refine
-
refine'
-
registerDerivingHandler
-
registerSimpAttr
-
remainingBytes
-
remainingToString
-
removeDir
-
removeDirAll
-
removeFile
-
removeLeadingSpaces
-
rename
-
rename_i
-
repeat
(0) (1) -
repeat'
-
repeat1'
-
repeatTR
-
replace
-
repr
-
reprPrec
-
resolveGlobalName
-
resolveNamespace
-
revFind
-
revPosOf
-
reverse
-
revert
-
rewind
-
rewrite
(0) (1) -
rfl
(0) (1) -
rfl'
-
rhs
-
right
(0) (1) -
rintro
-
root
-
rotate_left
-
rotate_right
-
run
-
runEST
-
runST
-
runTermElab
-
run_tac
-
rw
(0) (1) -
rw?
-
rw_mod_cast
-
rwa
S
-
ST
-
ST.
Ref -
ST.
Ref. get -
ST.
Ref. mk -
ST.
Ref. modify -
ST.
Ref. modifyGet -
ST.
Ref. ptrEq -
ST.
Ref. set -
ST.
Ref. swap -
ST.
Ref. take -
ST.
Ref. toMonadStateOf -
ST.
mkRef -
ScientificLit
-
ShiftLeft
-
ShiftLeft.
shiftLeft -
ShiftRight
-
ShiftRight.
shiftRight -
SimpExtension
-
SizeOf
-
SizeOf.
sizeOf -
Sort
-
SourceInfo
-
SpawnArgs
-
StdGen
-
StdGen.
mk -
Stdio
-
StdioConfig
-
StrLit
-
Stream
-
String
-
String.
Iterator -
String.
Iterator. atEnd -
String.
Iterator. curr -
String.
Iterator. extract -
String.
Iterator. forward -
String.
Iterator. hasNext -
String.
Iterator. hasPrev -
String.
Iterator. mk -
String.
Iterator. next -
String.
Iterator. nextn -
String.
Iterator. pos -
String.
Iterator. prev -
String.
Iterator. prevn -
String.
Iterator. remainingBytes -
String.
Iterator. remainingToString -
String.
Iterator. setCurr -
String.
Iterator. toEnd -
String.
Pos -
String.
Pos. isValid -
String.
Pos. min -
String.
Pos. mk -
String.
all -
String.
any -
String.
append -
String.
atEnd -
String.
back -
String.
capitalize -
String.
codepointPosToUtf16Pos -
String.
codepointPosToUtf16PosFrom -
String.
codepointPosToUtf8PosFrom -
String.
contains -
String.
crlfToLf -
String.
csize -
String.
decEq -
String.
decapitalize -
String.
drop -
String.
dropRight -
String.
dropRightWhile -
String.
dropWhile -
String.
endPos -
String.
endsWith -
String.
extract -
String.
find -
String.
findLineStart -
String.
firstDiffPos -
String.
foldl -
String.
foldr -
String.
fromExpr? -
String.
fromUTF8 -
String.
fromUTF8! -
String.
fromUTF8? -
String.
front -
String.
get -
String.
get! -
String.
get' -
String.
get? -
String.
getUtf8Byte -
String.
hash -
String.
intercalate -
String.
isEmpty -
String.
isInt -
String.
isNat -
String.
isPrefixOf -
String.
iter -
String.
join -
String.
le -
String.
length -
String.
map -
String.
mk -
String.
mkIterator -
String.
modify -
String.
next -
String.
next' -
String.
nextUntil -
String.
nextWhile -
String.
offsetOfPos -
String.
posOf -
String.
prev -
String.
push -
String.
pushn -
String.
quote -
String.
reduceAppend -
String.
reduceBEq -
String.
reduceBNe -
String.
reduceBinPred -
String.
reduceBoolPred -
String.
reduceEq -
String.
reduceGE -
String.
reduceGT -
String.
reduceLE -
String.
reduceLT -
String.
reduceMk -
String.
reduceNe -
String.
removeLeadingSpaces -
String.
replace -
String.
revFind -
String.
revPosOf -
String.
set -
String.
singleton -
String.
split -
String.
splitOn -
String.
startsWith -
String.
substrEq -
String.
take -
String.
takeRight -
String.
takeRightWhile -
String.
takeWhile -
String.
toFileMap -
String.
toFormat -
String.
toInt! -
String.
toInt? -
String.
toList -
String.
toLower -
String.
toName -
String.
toNat! -
String.
toNat? -
String.
toSubstring -
String.
toSubstring' -
String.
toUTF8 -
String.
toUpper -
String.
trim -
String.
trimLeft -
String.
trimRight -
String.
utf16Length -
String.
utf16PosToCodepointPos -
String.
utf16PosToCodepointPosFrom -
String.
utf8ByteSize -
String.
utf8DecodeChar? -
String.
utf8EncodeChar -
String.
validateUTF8 -
Sub
-
Sub.
sub -
Subarray
-
Subarray.
all -
Subarray.
allM -
Subarray.
any -
Subarray.
anyM -
Subarray.
drop -
Subarray.
empty -
Subarray.
findRev? -
Subarray.
findRevM? -
Subarray.
findSomeRevM? -
Subarray.
foldl -
Subarray.
foldlM -
Subarray.
foldr -
Subarray.
foldrM -
Subarray.
forIn -
Subarray.
forM -
Subarray.
forRevM -
Subarray.
get -
Subarray.
get! -
Subarray.
getD -
Subarray.
mk -
Subarray.
popFront -
Subarray.
size -
Subarray.
split -
Subarray.
take -
Subarray.
toArray -
Syntax
-
SyntaxNodeKind
-
System.
FilePath -
System.
FilePath. addExtension -
System.
FilePath. components -
System.
FilePath. exeExtension -
System.
FilePath. extSeparator -
System.
FilePath. extension -
System.
FilePath. fileName -
System.
FilePath. fileStem -
System.
FilePath. isAbsolute -
System.
FilePath. isDir -
System.
FilePath. isRelative -
System.
FilePath. join -
System.
FilePath. metadata -
System.
FilePath. mk -
System.
FilePath. normalize -
System.
FilePath. parent -
System.
FilePath. pathExists -
System.
FilePath. pathSeparator -
System.
FilePath. pathSeparators -
System.
FilePath. readDir -
System.
FilePath. walkDir -
System.
FilePath. withExtension -
System.
FilePath. withFileName -
System.
mkFilePath -
s
-
s1
-
s2
-
save
-
scientificLitKind
-
semiOutParam
-
sequenceMap
-
set
-
set!
-
setAccessRights
-
setCurr
-
setCurrentDir
-
setD
-
setGoals
-
setKind
-
setRandSeed
-
setStderr
-
setStdin
-
setStdout
-
set_option
-
setsid
-
shiftLeft
-
shiftRight
-
show
-
show_term
-
simp
(0) (1) -
simp!
-
simp?
-
simp?!
-
simp_all
-
simp_all!
-
simp_all?
-
simp_all?!
-
simp_all_arith
-
simp_all_arith!
-
simp_arith
-
simp_arith!
-
simp_match
-
simp_wf
-
simpa
-
simpa!
-
simpa?
-
simpa?!
-
simprocs
-
singlePass
-
singleton
-
size
-
sizeOf
-
skip
(0) (1) -
skipAssignedInstances
-
sleep
-
solve
-
solve_by_elim
-
sorry
-
sortMVarIdArrayByIndex
-
sortMVarIdsByIndex
-
spawn
-
specialize
-
split
-
splitOn
-
start
-
start_le_stop
-
startsWith
-
stdNext
-
stdRange
-
stdSplit
-
stderr
-
stdin
-
stdout
-
stop
-
stop_le_array_size
-
strLitKind
-
strongInductionOn
-
sub
-
subDigitChar
-
subst
-
subst_eqs
-
subst_vars
-
substrEq
-
suffices
-
superDigitChar
-
swap
-
swap!
-
swapAt
-
swapAt!
-
symm
-
symm_saturate
-
synthInstance.
maxHeartbeats -
synthInstance.
maxSize - synthesis
T
-
TSepArray
-
TSyntax
-
TSyntaxArray
-
Tactic
-
TacticM
-
Task
-
Task.
Priority -
Task.
Priority. dedicated -
Task.
Priority. default -
Task.
Priority. max -
Task.
get -
Task.
pure -
Task.
spawn -
Term
-
ToString
-
ToString.
toString -
TransparencyMode
-
Type
-
TypeName
-
tactic
-
tactic'
-
tactic.
customEliminators -
tactic.
dbg_cache -
tactic.
hygienic -
tactic.
(0) (1)simp. trace -
tactic.
skipAssignedInstances -
tacticElabAttribute
-
tagUntaggedGoals
-
take
-
takeRight
-
takeRightWhile
-
takeStdin
-
takeWhile
-
testBit
-
threshold
-
throwError
-
throwErrorAt
-
throwUnsupported
-
toArray
-
toBaseIO
-
toDigits
-
toDigitsCore
-
toEIO
-
toEnd
-
toFileMap
-
toFloat
-
toFormat
-
toGetElem
-
toHandleType
-
toIO
-
toIO'
-
toInt!
-
toInt?
-
toLevel
-
toList
-
toListAppend
-
toListRev
-
toLower
-
toMonadStateOf
-
toName
-
toNat!
-
toNat?
-
toPArray'
-
toStdioConfig
-
toString
-
toSubDigits
-
toSubarray
-
toSubscriptString
-
toSubstring
-
toSubstring'
-
toSuperDigits
-
toSuperscriptString
-
toUInt16
-
toUInt32
-
toUInt64
-
toUInt8
-
toUSize
-
toUTF8
-
toUpper
-
trace
-
Lean.
Macro. trace -
tactic.
(0) (1)simp. trace
-
-
trace.
Meta. Tactic. simp. discharge -
trace.
Meta. Tactic. simp. rewrite -
trace_state
(0) (1) -
transparency
-
trim
-
trimLeft
-
trimRight
-
trivial
-
truncate
-
try
(0) (1) -
tryCatch
-
tryLock
-
tryTactic
-
tryTactic?
-
tryWait
-
type
- type constructor
U
-
Unit
-
Unit.
unit -
uget
-
unattach
-
unfold
(0) (1) -
unfoldPartialApp
-
unhygienic
-
unit
- universe
- universe polymorphism
-
unlock
-
unnecessarySimpa
-
unsupportedSyntax
-
unzip
-
user
-
userError
-
uset
-
usize
-
utf16Length
-
utf16PosToCodepointPos
-
utf16PosToCodepointPosFrom
-
utf8ByteSize
-
utf8DecodeChar?
-
utf8EncodeChar
V
-
val
-
valid
-
validateUTF8
W
-
wait
-
waitAny
-
walkDir
-
whnf
-
withExtension
-
withFile
-
withFileName
-
withFreshMacroScope
-
withIsolatedStreams
-
withLocation
-
withPosition
-
withPositionAfterLinebreak
-
withStderr
-
withStdin
-
withStdout
-
withTempFile
-
with_reducible
-
with_reducible_and_instances
-
with_unfolding_all
-
withoutPosition
-
write
-
writeBinFile
-
writeFile
X
-
xor
Subarray
```exceptions ```
Task
Task.bind, Task.map
{docstring Task.bind} {docstring Task.map}
```exceptions Task.bind Task.map ```
IO.Process
```exceptions ```
IO.Process.StdioConfig
```exceptions ```
String
String.dropSuffix?, String.stripSuffix, String.stripPrefix, String.dropPrefix?
{docstring String.dropSuffix?} {docstring String.stripSuffix} {docstring String.stripPrefix} {docstring String.dropPrefix?}
```exceptions String.dropSuffix? String.stripSuffix String.stripPrefix String.dropPrefix? ```
System
```exceptions ```
IO
IO.getTID
{docstring IO.getTID}
```exceptions IO.getTID ```
EIO
```exceptions ```
Task.Priority
```exceptions ```
IO.Process.Output
```exceptions ```
IO.FileRight
```exceptions ```
IO.Process.Child
```exceptions ```
Array
Array.insertIdxIfInBounds, Array.insertIdx.loop, Array.insertIdx, Array.findFinIdx?.loop, Array.eraseP, Array.pmap, Array.swapIfInBounds, Array.zipWithAll.go, Array.finRange, Array.eraseIdxIfInBounds, Array.«term__[:_]», Array.findFinIdx?, Array.insertIdx!, Array.eraseIdx!, Array.«term__[_:]», Array.setIfInBounds, Array.zipWithAll, Array.«term__[_:_]»
{docstring Array.insertIdxIfInBounds} {docstring Array.insertIdx.loop} {docstring Array.insertIdx} {docstring Array.findFinIdx?.loop} {docstring Array.eraseP} {docstring Array.pmap} {docstring Array.swapIfInBounds} {docstring Array.zipWithAll.go} {docstring Array.finRange} {docstring Array.eraseIdxIfInBounds} {docstring Array.«term__[:_]»} {docstring Array.findFinIdx?} {docstring Array.insertIdx!} {docstring Array.eraseIdx!} {docstring Array.«term__[_:]»} {docstring Array.setIfInBounds} {docstring Array.zipWithAll} {docstring Array.«term__[_:_]»}
```exceptions Array.insertIdxIfInBounds Array.insertIdx.loop Array.insertIdx Array.findFinIdx?.loop Array.eraseP Array.pmap Array.swapIfInBounds Array.zipWithAll.go Array.finRange Array.eraseIdxIfInBounds Array.«term__[:_]» Array.findFinIdx? Array.insertIdx! Array.eraseIdx! Array.«term__[_:]» Array.setIfInBounds Array.zipWithAll Array.«term__[_:_]» ```
IO.Process.Stdio
```exceptions ```
IO.FS.Stream.Buffer
```exceptions ```
IO.FS.Metadata
```exceptions ```
Unit
```exceptions ```
ST
```exceptions ```
IO.FS
IO.FS.createTempDir, IO.FS.withTempDir
{docstring IO.FS.createTempDir} {docstring IO.FS.withTempDir}
```exceptions IO.FS.createTempDir IO.FS.withTempDir ```
PUnit
```exceptions ```
IO.Process.SpawnArgs
```exceptions ```
Nat
Nat.caseStrongRecOn, Nat.reduceXor, Nat.reduceShiftRight, Nat.reduceOr, Nat.toInt16, Nat.toInt32, Nat.toISize, Nat.toInt8, Nat.reduceAnd, Nat.toInt64, Nat.strongRecOn, Nat.reduceShiftLeft
{docstring Nat.caseStrongRecOn} {docstring Nat.reduceXor} {docstring Nat.reduceShiftRight} {docstring Nat.reduceOr} {docstring Nat.toInt16} {docstring Nat.toInt32} {docstring Nat.toISize} {docstring Nat.toInt8} {docstring Nat.reduceAnd} {docstring Nat.toInt64} {docstring Nat.strongRecOn} {docstring Nat.reduceShiftLeft}
```exceptions Nat.caseStrongRecOn Nat.reduceXor Nat.reduceShiftRight Nat.reduceOr Nat.toInt16 Nat.toInt32 Nat.toISize Nat.toInt8 Nat.reduceAnd Nat.toInt64 Nat.strongRecOn Nat.reduceShiftLeft ```
IO.FS.DirEntry
```exceptions ```
IO.FS.Handle
```exceptions ```
Lean.Elab.Tactic
Lean.Elab.Tactic.tryCatchRestore, Lean.Elab.Tactic.withRWRulesSeq, Lean.Elab.Tactic.unfoldLocalDecl, Lean.Elab.Tactic.expandOptLocation, Lean.Elab.Tactic.expandLocation, Lean.Elab.Tactic.elabChange, Lean.Elab.Tactic.deltaLocalDecl, Lean.Elab.Tactic.addCheckpoints, Lean.Elab.Tactic.mkTacticInfo, Lean.Elab.Tactic.evalClassical, Lean.Elab.Tactic.withCaseRef, Lean.Elab.Tactic.isHoleRHS, Lean.Elab.Tactic.elabDecideConfig, Lean.Elab.Tactic.deltaTarget, Lean.Elab.Tactic.pushGoals, Lean.Elab.Tactic.renameInaccessibles, Lean.Elab.Tactic.commandConfigElab, Lean.Elab.Tactic.getNameOfIdent', Lean.Elab.Tactic.pushGoal, Lean.Elab.Tactic.elabAsFVar, Lean.Elab.Tactic.tactic.customEliminators, Lean.Elab.Tactic.popMainGoal, Lean.Elab.Tactic.getInductiveValFromMajor, Lean.Elab.Tactic.tacticToDischarge, Lean.Elab.Tactic.rewriteLocalDecl, Lean.Elab.Tactic.elabSimpConfigCore, Lean.Elab.Tactic.saveTacticInfoForToken, Lean.Elab.Tactic.focusAndDone, Lean.Elab.Tactic.unfoldTarget, Lean.Elab.Tactic.getMainTarget, Lean.Elab.Tactic.withSimpDiagnostics, Lean.Elab.Tactic.evalDecideCore.doElab, Lean.Elab.Tactic.checkCommandConfigElab, Lean.Elab.Tactic.dsimpLocation, Lean.Elab.Tactic.getMainDecl, Lean.Elab.Tactic.zetaDeltaLocalDecl, Lean.Elab.Tactic.elabTermForApply, Lean.Elab.Tactic.rewriteTarget, Lean.Elab.Tactic.evalDecideCore.doKernel, Lean.Elab.Tactic.configElab, Lean.Elab.Tactic.simpLocation, Lean.Elab.Tactic.refineCore, Lean.Elab.Tactic.evalDecideCore.diagnose, Lean.Elab.Tactic.throwNoGoalsToBeSolved, Lean.Elab.Tactic.closeUsingOrAdmit, Lean.Elab.Tactic.forEachVar, Lean.Elab.Tactic.checkConfigElab, Lean.Elab.Tactic.withTacticInfoContext, Lean.Elab.Tactic.withRestoreOrSaveFull, Lean.Elab.Tactic.logUnassignedAndAbort, Lean.Elab.Tactic.traceSimpCall, Lean.Elab.Tactic.zetaDeltaTarget, Lean.Elab.Tactic.mkSimpContext, Lean.Elab.Tactic.withMacroExpansion, Lean.Elab.Tactic.evalDecideCore, Lean.Elab.Tactic.withCollectingNewGoalsFrom, Lean.Elab.Tactic.withMainContext, Lean.Elab.Tactic.elabRewriteConfig, Lean.Elab.Tactic.mkInitialTacticInfo, Lean.Elab.Tactic.liftMetaFinishingTactic, Lean.Elab.Tactic.mkSimpOnly, Lean.Elab.Tactic.classical, Lean.Elab.Tactic.liftMetaTactic1, Lean.Elab.Tactic.isCheckpointableTactic, Lean.Elab.Tactic.saveState, Lean.Elab.Tactic.mkSimpCallStx, Lean.Elab.Tactic.filterOldMVars, Lean.Elab.Tactic.replaceMainGoal, Lean.Elab.Tactic.liftMetaTactic, Lean.Elab.Tactic.done, Lean.Elab.Tactic.simpOnlyBuiltins, Lean.Elab.Tactic.withoutRecover
{docstring Lean.Elab.Tactic.tryCatchRestore} {docstring Lean.Elab.Tactic.withRWRulesSeq} {docstring Lean.Elab.Tactic.unfoldLocalDecl} {docstring Lean.Elab.Tactic.expandOptLocation} {docstring Lean.Elab.Tactic.expandLocation} {docstring Lean.Elab.Tactic.elabChange} {docstring Lean.Elab.Tactic.deltaLocalDecl} {docstring Lean.Elab.Tactic.addCheckpoints} {docstring Lean.Elab.Tactic.mkTacticInfo} {docstring Lean.Elab.Tactic.evalClassical} {docstring Lean.Elab.Tactic.withCaseRef} {docstring Lean.Elab.Tactic.isHoleRHS} {docstring Lean.Elab.Tactic.elabDecideConfig} {docstring Lean.Elab.Tactic.deltaTarget} {docstring Lean.Elab.Tactic.pushGoals} {docstring Lean.Elab.Tactic.renameInaccessibles} {docstring Lean.Elab.Tactic.commandConfigElab} {docstring Lean.Elab.Tactic.getNameOfIdent'} {docstring Lean.Elab.Tactic.pushGoal} {docstring Lean.Elab.Tactic.elabAsFVar} {docstring Lean.Elab.Tactic.tactic.customEliminators} {docstring Lean.Elab.Tactic.popMainGoal} {docstring Lean.Elab.Tactic.getInductiveValFromMajor} {docstring Lean.Elab.Tactic.tacticToDischarge} {docstring Lean.Elab.Tactic.rewriteLocalDecl} {docstring Lean.Elab.Tactic.elabSimpConfigCore} {docstring Lean.Elab.Tactic.saveTacticInfoForToken} {docstring Lean.Elab.Tactic.focusAndDone} {docstring Lean.Elab.Tactic.unfoldTarget} {docstring Lean.Elab.Tactic.getMainTarget} {docstring Lean.Elab.Tactic.withSimpDiagnostics} {docstring Lean.Elab.Tactic.evalDecideCore.doElab} {docstring Lean.Elab.Tactic.checkCommandConfigElab} {docstring Lean.Elab.Tactic.dsimpLocation} {docstring Lean.Elab.Tactic.getMainDecl} {docstring Lean.Elab.Tactic.zetaDeltaLocalDecl} {docstring Lean.Elab.Tactic.elabTermForApply} {docstring Lean.Elab.Tactic.rewriteTarget} {docstring Lean.Elab.Tactic.evalDecideCore.doKernel} {docstring Lean.Elab.Tactic.configElab} {docstring Lean.Elab.Tactic.simpLocation} {docstring Lean.Elab.Tactic.refineCore} {docstring Lean.Elab.Tactic.evalDecideCore.diagnose} {docstring Lean.Elab.Tactic.throwNoGoalsToBeSolved} {docstring Lean.Elab.Tactic.closeUsingOrAdmit} {docstring Lean.Elab.Tactic.forEachVar} {docstring Lean.Elab.Tactic.checkConfigElab} {docstring Lean.Elab.Tactic.withTacticInfoContext} {docstring Lean.Elab.Tactic.withRestoreOrSaveFull} {docstring Lean.Elab.Tactic.logUnassignedAndAbort} {docstring Lean.Elab.Tactic.traceSimpCall} {docstring Lean.Elab.Tactic.zetaDeltaTarget} {docstring Lean.Elab.Tactic.mkSimpContext} {docstring Lean.Elab.Tactic.withMacroExpansion} {docstring Lean.Elab.Tactic.evalDecideCore} {docstring Lean.Elab.Tactic.withCollectingNewGoalsFrom} {docstring Lean.Elab.Tactic.withMainContext} {docstring Lean.Elab.Tactic.elabRewriteConfig} {docstring Lean.Elab.Tactic.mkInitialTacticInfo} {docstring Lean.Elab.Tactic.liftMetaFinishingTactic} {docstring Lean.Elab.Tactic.mkSimpOnly} {docstring Lean.Elab.Tactic.classical} {docstring Lean.Elab.Tactic.liftMetaTactic1} {docstring Lean.Elab.Tactic.isCheckpointableTactic} {docstring Lean.Elab.Tactic.saveState} {docstring Lean.Elab.Tactic.mkSimpCallStx} {docstring Lean.Elab.Tactic.filterOldMVars} {docstring Lean.Elab.Tactic.replaceMainGoal} {docstring Lean.Elab.Tactic.liftMetaTactic} {docstring Lean.Elab.Tactic.done} {docstring Lean.Elab.Tactic.simpOnlyBuiltins} {docstring Lean.Elab.Tactic.withoutRecover}
```exceptions Lean.Elab.Tactic.tryCatchRestore Lean.Elab.Tactic.withRWRulesSeq Lean.Elab.Tactic.unfoldLocalDecl Lean.Elab.Tactic.expandOptLocation Lean.Elab.Tactic.expandLocation Lean.Elab.Tactic.elabChange Lean.Elab.Tactic.deltaLocalDecl Lean.Elab.Tactic.addCheckpoints Lean.Elab.Tactic.mkTacticInfo Lean.Elab.Tactic.evalClassical Lean.Elab.Tactic.withCaseRef Lean.Elab.Tactic.isHoleRHS Lean.Elab.Tactic.elabDecideConfig Lean.Elab.Tactic.deltaTarget Lean.Elab.Tactic.pushGoals Lean.Elab.Tactic.renameInaccessibles Lean.Elab.Tactic.commandConfigElab Lean.Elab.Tactic.getNameOfIdent' Lean.Elab.Tactic.pushGoal Lean.Elab.Tactic.elabAsFVar Lean.Elab.Tactic.tactic.customEliminators Lean.Elab.Tactic.popMainGoal Lean.Elab.Tactic.getInductiveValFromMajor Lean.Elab.Tactic.tacticToDischarge Lean.Elab.Tactic.rewriteLocalDecl Lean.Elab.Tactic.elabSimpConfigCore Lean.Elab.Tactic.saveTacticInfoForToken Lean.Elab.Tactic.focusAndDone Lean.Elab.Tactic.unfoldTarget Lean.Elab.Tactic.getMainTarget Lean.Elab.Tactic.withSimpDiagnostics Lean.Elab.Tactic.evalDecideCore.doElab Lean.Elab.Tactic.checkCommandConfigElab Lean.Elab.Tactic.dsimpLocation Lean.Elab.Tactic.getMainDecl Lean.Elab.Tactic.zetaDeltaLocalDecl Lean.Elab.Tactic.elabTermForApply Lean.Elab.Tactic.rewriteTarget Lean.Elab.Tactic.evalDecideCore.doKernel Lean.Elab.Tactic.configElab Lean.Elab.Tactic.simpLocation Lean.Elab.Tactic.refineCore Lean.Elab.Tactic.evalDecideCore.diagnose Lean.Elab.Tactic.throwNoGoalsToBeSolved Lean.Elab.Tactic.closeUsingOrAdmit Lean.Elab.Tactic.forEachVar Lean.Elab.Tactic.checkConfigElab Lean.Elab.Tactic.withTacticInfoContext Lean.Elab.Tactic.withRestoreOrSaveFull Lean.Elab.Tactic.logUnassignedAndAbort Lean.Elab.Tactic.traceSimpCall Lean.Elab.Tactic.zetaDeltaTarget Lean.Elab.Tactic.mkSimpContext Lean.Elab.Tactic.withMacroExpansion Lean.Elab.Tactic.evalDecideCore Lean.Elab.Tactic.withCollectingNewGoalsFrom Lean.Elab.Tactic.withMainContext Lean.Elab.Tactic.elabRewriteConfig Lean.Elab.Tactic.mkInitialTacticInfo Lean.Elab.Tactic.liftMetaFinishingTactic Lean.Elab.Tactic.mkSimpOnly Lean.Elab.Tactic.classical Lean.Elab.Tactic.liftMetaTactic1 Lean.Elab.Tactic.isCheckpointableTactic Lean.Elab.Tactic.saveState Lean.Elab.Tactic.mkSimpCallStx Lean.Elab.Tactic.filterOldMVars Lean.Elab.Tactic.replaceMainGoal Lean.Elab.Tactic.liftMetaTactic Lean.Elab.Tactic.done Lean.Elab.Tactic.simpOnlyBuiltins Lean.Elab.Tactic.withoutRecover ```
IO.Error
```exceptions ```
Char
Char.reduceVal, Char.ofUInt8, Char.reduceOfNatAux, Char.reduceIsDigit, Char.reduceUnary, Char.reduceBEq, Char.reduceEq, Char.fromExpr?, Char.reduceIsWhitespace, Char.toNat, Char.toLower, Char.toUpper, Char.toUInt8, Char.reduceNe, Char.reduceIsUpper, Char.quoteCore.smallCharToHex, Char.quote, Char.le, Char.reduceIsAlpha, Char.reduceToNat, Char.reduceIsLower, Char.lt, Char.utf16Size, Char.reduceBNe, Char.isValidCharNat, Char.toString, Char.repr, Char.reduceToString, Char.reduceDefault, Char.reduceGT, Char.reduceLE, Char.ofNatAux, Char.reduceBinPred, Char.reduceToLower, Char.reduceLT, Char.isValue, Char.reduceGE, Char.utf8Size, Char.reduceIsAlphaNum, Char.reduceBoolPred, Char.quoteCore, Char.reduceToUpper, Char.ofNat
{docstring Char.reduceVal} {docstring Char.ofUInt8} {docstring Char.reduceOfNatAux} {docstring Char.reduceIsDigit} {docstring Char.reduceUnary} {docstring Char.reduceBEq} {docstring Char.reduceEq} {docstring Char.fromExpr?} {docstring Char.reduceIsWhitespace} {docstring Char.toNat} {docstring Char.toLower} {docstring Char.toUpper} {docstring Char.toUInt8} {docstring Char.reduceNe} {docstring Char.reduceIsUpper} {docstring Char.quoteCore.smallCharToHex} {docstring Char.quote} {docstring Char.le} {docstring Char.reduceIsAlpha} {docstring Char.reduceToNat} {docstring Char.reduceIsLower} {docstring Char.lt} {docstring Char.utf16Size} {docstring Char.reduceBNe} {docstring Char.isValidCharNat} {docstring Char.toString} {docstring Char.repr} {docstring Char.reduceToString} {docstring Char.reduceDefault} {docstring Char.reduceGT} {docstring Char.reduceLE} {docstring Char.ofNatAux} {docstring Char.reduceBinPred} {docstring Char.reduceToLower} {docstring Char.reduceLT} {docstring Char.isValue} {docstring Char.reduceGE} {docstring Char.utf8Size} {docstring Char.reduceIsAlphaNum} {docstring Char.reduceBoolPred} {docstring Char.quoteCore} {docstring Char.reduceToUpper} {docstring Char.ofNat}
```exceptions Char.reduceVal Char.ofUInt8 Char.reduceOfNatAux Char.reduceIsDigit Char.reduceUnary Char.reduceBEq Char.reduceEq Char.fromExpr? Char.reduceIsWhitespace Char.toNat Char.toLower Char.toUpper Char.toUInt8 Char.reduceNe Char.reduceIsUpper Char.quoteCore.smallCharToHex Char.quote Char.le Char.reduceIsAlpha Char.reduceToNat Char.reduceIsLower Char.lt Char.utf16Size Char.reduceBNe Char.isValidCharNat Char.toString Char.repr Char.reduceToString Char.reduceDefault Char.reduceGT Char.reduceLE Char.ofNatAux Char.reduceBinPred Char.reduceToLower Char.reduceLT Char.isValue Char.reduceGE Char.utf8Size Char.reduceIsAlphaNum Char.reduceBoolPred Char.quoteCore Char.reduceToUpper Char.ofNat ```
IO.Ref
```exceptions ```
IO.FS.Stream
```exceptions ```
ST.Ref
```exceptions ```
BaseIO
```exceptions ```
System.FilePath
```exceptions ```
- Tactics
Lean.Parser.Tactic.acNf0, Lean.Parser.Tactic.tacticAc_nf_, Lean.Parser.Tactic.classical
{docstring Lean.Parser.Tactic.acNf0} {docstring Lean.Parser.Tactic.tacticAc_nf_} {docstring Lean.Parser.Tactic.classical}
```exceptions Lean.Parser.Tactic.acNf0 Lean.Parser.Tactic.tacticAc_nf_ Lean.Parser.Tactic.classical ```