Index
A
-
Acc
-
Acc.
intro -
Add
-
Add.
mk -
Alternative
-
Alternative.
mk -
Append
-
Append.
mk -
Applicative
-
Applicative.
mk -
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
-
adapt
-
adaptExcept
-
adaptExpander
-
add
-
addCases
-
addExtension
-
addHeartbeats
-
addMacroScope
-
addNat
-
admit
-
all
-
allDiff
-
allM
-
allTR
-
all_goals
(0) (1) -
and
-
andM
-
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
-
asTask
-
assumption
-
assumption_mod_cast
-
atEnd
-
atLeastTwo
-
attach
-
attachWith
-
autoLift
-
autoParam
-
autoPromoteIndices
-
autoUnfold
B
-
BEq
-
BEq.
mk -
Backtrackable
-
BaseIO
-
BaseIO.
asTask -
BaseIO.
bindTask -
BaseIO.
mapTask -
BaseIO.
mapTasks -
BaseIO.
toEIO -
BaseIO.
toIO -
Bind
-
Bind.
bindLeft -
Bind.
kleisliLeft -
Bind.
kleisliRight -
Bind.
mk -
Bool
-
Bool.
and -
Bool.
atLeastTwo -
Bool.
decEq -
Bool.
false -
Bool.
not -
Bool.
or -
Bool.
toISize -
Bool.
toInt16 -
Bool.
toInt32 -
Bool.
toInt64 -
Bool.
toInt8 -
Bool.
toNat -
Bool.
toUInt16 -
Bool.
toUInt32 -
Bool.
toUInt64 -
Bool.
toUInt8 -
Bool.
toUSize -
Bool.
true -
Bool.
xor -
Buffer
-
back
-
back!
-
back?
-
backward.
synthInstance. canonInstances -
bdiv
-
below
-
beq
-
beta
-
binInsert
-
binInsertM
-
binSearch
-
binSearchContains
-
bind
-
bindCont
-
bindLeft
-
bindM
-
bindTask
-
bind_assoc
-
bind_map
-
bind_pure_comp
-
bitwise
-
ble
-
blt
-
bmod
-
bootstrap.
inductiveCheckResultingUniverse -
bv_check
-
bv_decide
-
bv_decide?
-
bv_normalize
-
bv_omega
-
byCases
-
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
-
castAdd
-
castLE
-
castLT
-
castSucc
-
catchExceptions
-
change
(0) (1) -
change ...
with ... -
charLitKind
-
checkCanceled
-
checkpoint
-
choice
-
choiceKind
-
clear
-
closeMainGoal
-
closeMainGoalUsing
-
cmd
-
codepointPosToUtf16Pos
-
codepointPosToUtf16PosFrom
-
codepointPosToUtf8PosFrom
-
colEq
-
colGe
-
colGt
- comment
-
comp_map
-
compare
-
complement
-
components
-
concatMap
-
concatMapM
-
cond
- configuration
-
congr
(0) (1) -
constructor
(0) (1) -
contains
-
contextual
-
contradiction
-
control
-
controlAt
-
conv
-
conv => ...
-
conv'
(0) (1) -
createDir
-
createDirAll
-
createTempFile
-
crlfToLf
-
csize
- cumulativity
-
curr
-
currentDir
-
customEliminators
-
cwd
D
-
Decidable
-
Decidable.
byCases -
Decidable.
decide -
Decidable.
isFalse -
Decidable.
isTrue -
DecidableEq
-
DecidableRel
-
DirEntry
-
Div
-
Div.
mk -
Dvd
-
Dvd.
mk -
Dynamic
-
Dynamic.
get? -
Dynamic.
mk -
data
-
dbg_cache
-
dbg_trace
-
decEq
-
decLe
-
decLt
-
decapitalize
- decidable
-
decidable_eq_none
-
decide
-
decreasing_tactic
-
decreasing_trivial
-
decreasing_with
-
dedicated
-
deepTerms
-
default
-
delta
(0) (1) -
digitChar
-
discard
-
discharge
-
div
-
div2Induction
-
done
(0) (1) -
down
-
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
-
EStateM
-
EStateM.
Backtrackable -
EStateM.
Backtrackable. mk -
EStateM.
Result -
EStateM.
Result. error -
EStateM.
Result. ok -
EStateM.
adaptExcept -
EStateM.
bind -
EStateM.
fromStateM -
EStateM.
get -
EStateM.
map -
EStateM.
modifyGet -
EStateM.
nonBacktrackable -
EStateM.
orElse -
EStateM.
orElse' -
EStateM.
pure -
EStateM.
run -
EStateM.
run' -
EStateM.
seqRight -
EStateM.
set -
EStateM.
throw -
EStateM.
tryCatch -
Empty
-
Empty.
elim -
Error
-
Even
-
Even.
plusTwo -
Even.
zero -
Except
-
Except.
bind -
Except.
error -
Except.
isOk -
Except.
map -
Except.
mapError -
Except.
ok -
Except.
orElseLazy -
Except.
pure -
Except.
toBool -
Except.
toOption -
Except.
tryCatch -
ExceptCpsT
-
ExceptCpsT.
lift -
ExceptCpsT.
run -
ExceptCpsT.
runCatch -
ExceptCpsT.
runK -
ExceptT
-
ExceptT.
adapt -
ExceptT.
bind -
ExceptT.
bindCont -
ExceptT.
lift -
ExceptT.
map -
ExceptT.
mk -
ExceptT.
pure -
ExceptT.
run -
ExceptT.
tryCatch -
ediv
-
elabCasesTargets
-
elabDSimpConfigCore
-
elabSimpArgs
-
elabSimpConfig
-
elabSimpConfigCtxCore
-
elabTerm
-
elabTermEnsuringType
-
elabTermWithHoles
-
elem
-
elemsAndSeps
-
elim
-
elim0
-
elimM
-
elimOffset
-
emod
-
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
-
Fin
-
Fin.
add -
Fin.
addCases -
Fin.
addNat -
Fin.
cases -
Fin.
cast -
Fin.
castAdd -
Fin.
castLE -
Fin.
castLT -
Fin.
castSucc -
Fin.
div -
Fin.
elim0 -
Fin.
foldl -
Fin.
foldlM -
Fin.
foldr -
Fin.
foldrM -
Fin.
fromExpr? -
Fin.
hIterate -
Fin.
hIterateFrom -
Fin.
induction -
Fin.
inductionOn -
Fin.
isValue -
Fin.
land -
Fin.
last -
Fin.
lastCases -
Fin.
log2 -
Fin.
lor -
Fin.
mk -
Fin.
mod -
Fin.
modn -
Fin.
mul -
Fin.
natAdd -
Fin.
ofNat' -
Fin.
pred -
Fin.
reduceAdd -
Fin.
reduceAddNat -
Fin.
reduceAnd -
Fin.
reduceBEq -
Fin.
reduceBNe -
Fin.
reduceBin -
Fin.
reduceBinPred -
Fin.
reduceBoolPred -
Fin.
reduceCastAdd -
Fin.
reduceCastLE -
Fin.
reduceCastLT -
Fin.
reduceCastSucc -
Fin.
reduceDiv -
Fin.
reduceEq -
Fin.
reduceFinMk -
Fin.
reduceGE -
Fin.
reduceGT -
Fin.
reduceLE -
Fin.
reduceLT -
Fin.
reduceLast -
Fin.
reduceMod -
Fin.
reduceMul -
Fin.
reduceNatAdd -
Fin.
reduceNatOp -
Fin.
reduceNe -
Fin.
reduceOfNat' -
Fin.
reduceOp -
Fin.
reduceOr -
Fin.
reducePred -
Fin.
reduceRev -
Fin.
reduceShiftLeft -
Fin.
reduceShiftRight -
Fin.
reduceSub -
Fin.
reduceSubNat -
Fin.
reduceSucc -
Fin.
reduceXor -
Fin.
rev -
Fin.
reverseInduction -
Fin.
shiftLeft -
Fin.
shiftRight -
Fin.
sub -
Fin.
subNat -
Fin.
succ -
Fin.
succRec -
Fin.
succRecOn -
Fin.
xor -
ForIn
-
ForIn'
-
ForIn'.
mk -
ForIn.
mk -
ForInStep
-
ForInStep.
done -
ForInStep.
yield -
ForM
-
ForM.
forIn -
ForM.
mk -
Functor
-
Functor.
discard -
Functor.
mapRev -
Functor.
mk -
fail
-
failIfUnchanged
-
fail_if_success
(0) (1) -
failure
-
false_or_by_contra
-
fdiv
-
fieldIdxKind
-
fieldNotation
-
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
-
fix
-
flags
-
flatMap
-
flatMapM
-
flatten
-
flush
-
fmod
-
focus
(0) (1) -
fold
-
foldM
-
foldRev
-
foldRevM
-
foldTR
-
foldl
-
foldlM
-
foldr
-
foldrM
-
fopenErrorToString
-
forIn
-
forIn'
-
forM
-
forRevM
-
format
-
forward
-
fromExpr
-
fromExpr?
-
fromStateM
-
fromUTF8
-
fromUTF8!
-
fromUTF8?
-
front
-
fst
-
fun
-
funext
(0) (1)
G
-
GetElem
-
GetElem.
mk -
GetElem?
-
GetElem?.
mk -
gcd
-
generalize
-
get
-
get!
-
get'
-
get?
-
getChar
-
getCurrMacroScope
-
getCurrNamespace
-
getCurrentDir
-
getD
-
getDM
-
getElem
-
getElem!
-
getElem!_def
-
getElem?
-
getElem?_def
-
getEnv
-
getEvenElems
-
getFVarId
-
getFVarIds
-
getGoals
-
getHygieneInfo
-
getId
-
getIdx?
-
getKind
-
getLine
-
getM
-
getMainGoal
-
getMainModule
-
getMainTag
-
getMax?
-
getModify
-
getName
-
getNat
-
getNumHeartbeats
-
getPID
-
getRandomBytes
-
getScientific
-
getStderr
-
getStdin
-
getStdout
-
getString
-
getTaskState
-
getThe
-
getUnsolvedGoals
-
getUtf8Byte
-
get_elem_tactic
-
get_elem_tactic_trivial
- goal
-
ground
-
group
-
groupByKey
-
groupKind
-
guard
-
guard_expr
-
guard_hyp
-
guard_target
H
-
HAdd
-
HAdd.
mk -
HAnd
-
HAnd.
mk -
HAppend
-
HAppend.
mk -
HDiv
-
HDiv.
mk -
HMod
-
HMod.
mk -
HMul
-
HMul.
mk -
HOr
-
HOr.
mk -
HPow
-
HPow.
mk -
HShiftLeft
-
HShiftLeft.
mk -
HShiftRight
-
HShiftRight.
mk -
HSub
-
HSub.
mk -
HXor
-
HXor.
mk -
Handle
-
Hashable
-
Hashable.
mk -
HomogeneousPow
-
HomogeneousPow.
mk -
HygieneInfo
-
h
-
hAdd
-
hAnd
-
hAppend
-
hDiv
-
hIterate
-
hIterateFrom
-
hMod
-
hMul
-
hOr
-
hPow
-
hShiftLeft
-
hShiftRight
-
hSub
-
hXor
-
hasBind
-
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 -
ISize
-
ISize.
add -
ISize.
complement -
ISize.
decEq -
ISize.
decLe -
ISize.
decLt -
ISize.
div -
ISize.
land -
ISize.
le -
ISize.
lor -
ISize.
lt -
ISize.
mk -
ISize.
mod -
ISize.
mul -
ISize.
neg -
ISize.
ofInt -
ISize.
ofNat -
ISize.
shiftLeft -
ISize.
shiftRight -
ISize.
size -
ISize.
sub -
ISize.
toBitVec -
ISize.
toInt -
ISize.
toInt32 -
ISize.
toInt64 -
ISize.
toNat -
ISize.
xor -
Id
-
Id.
hasBind -
Id.
run -
Ident
-
Inhabited
-
Inhabited.
mk -
Int
-
Int.
add -
Int.
bdiv -
Int.
bmod -
Int.
cast -
Int.
decEq -
Int.
ediv -
Int.
emod -
Int.
fdiv -
Int.
fmod -
Int.
fromExpr? -
Int.
gcd -
Int.
isPosValue -
Int.
lcm -
Int.
le -
Int.
lt -
Int.
mul -
Int.
natAbs -
Int.
neg -
Int.
negOfNat -
Int.
negSucc -
Int.
not -
Int.
ofNat -
Int.
pow -
Int.
reduceAbs -
Int.
reduceAdd -
Int.
reduceBEq -
Int.
reduceBNe -
Int.
reduceBdiv -
Int.
reduceBin -
Int.
reduceBinIntNatOp -
Int.
reduceBinPred -
Int.
reduceBmod -
Int.
reduceBoolPred -
Int.
reduceDiv -
Int.
reduceEq -
Int.
reduceFDiv -
Int.
reduceFMod -
Int.
reduceGE -
Int.
reduceGT -
Int.
reduceLE -
Int.
reduceLT -
Int.
reduceMod -
Int.
reduceMul -
Int.
reduceNatCore -
Int.
reduceNe -
Int.
reduceNeg -
Int.
reduceNegSucc -
Int.
reduceOfNat -
Int.
reducePow -
Int.
reduceSub -
Int.
reduceTDiv -
Int.
reduceTMod -
Int.
reduceToNat -
Int.
reduceUnary -
Int.
repr -
Int.
shiftRight -
Int.
sign -
Int.
sub -
Int.
subNatNat -
Int.
tdiv -
Int.
tmod -
Int.
toISize -
Int.
toInt16 -
Int.
toInt32 -
Int.
toInt64 -
Int.
toInt8 -
Int.
toNat -
Int.
toNat' -
Int16
-
Int16.
add -
Int16.
complement -
Int16.
decEq -
Int16.
decLe -
Int16.
decLt -
Int16.
div -
Int16.
land -
Int16.
le -
Int16.
lor -
Int16.
lt -
Int16.
mk -
Int16.
mod -
Int16.
mul -
Int16.
neg -
Int16.
ofInt -
Int16.
ofNat -
Int16.
shiftLeft -
Int16.
shiftRight -
Int16.
size -
Int16.
sub -
Int16.
toBitVec -
Int16.
toInt -
Int16.
(0) (1)toInt32 -
Int16.
toInt64 -
Int16.
toInt8 -
Int16.
toNat -
Int16.
xor -
Int32
-
Int32.
add -
Int32.
complement -
Int32.
decEq -
Int32.
decLe -
Int32.
decLt -
Int32.
div -
Int32.
land -
Int32.
le -
Int32.
lor -
Int32.
lt -
Int32.
mk -
Int32.
mod -
Int32.
mul -
Int32.
neg -
Int32.
ofInt -
Int32.
ofNat -
Int32.
shiftLeft -
Int32.
shiftRight -
Int32.
size -
Int32.
sub -
Int32.
toBitVec -
Int32.
toISize -
Int32.
toInt -
Int32.
toInt16 -
Int32.
toInt64 -
Int32.
toInt8 -
Int32.
toNat -
Int32.
xor -
Int64
-
Int64.
add -
Int64.
complement -
Int64.
decEq -
Int64.
decLe -
Int64.
decLt -
Int64.
div -
Int64.
land -
Int64.
le -
Int64.
lor -
Int64.
lt -
Int64.
mk -
Int64.
mod -
Int64.
mul -
Int64.
neg -
Int64.
ofInt -
Int64.
ofNat -
Int64.
shiftLeft -
Int64.
shiftRight -
Int64.
size -
Int64.
sub -
Int64.
toBitVec -
Int64.
toISize -
Int64.
toInt -
Int64.
toInt16 -
Int64.
toInt32 -
Int64.
toInt8 -
Int64.
toNat -
Int64.
xor -
Int8
-
Int8.
add -
Int8.
complement -
Int8.
decEq -
Int8.
decLe -
Int8.
decLt -
Int8.
div -
Int8.
land -
Int8.
le -
Int8.
lor -
Int8.
lt -
Int8.
mk -
Int8.
mod -
Int8.
mul -
Int8.
neg -
Int8.
ofInt -
Int8.
ofNat -
Int8.
shiftLeft -
Int8.
shiftRight -
Int8.
size -
Int8.
sub -
Int8.
toBitVec -
Int8.
toInt -
Int8.
toInt16 -
Int8.
(0) (1)toInt32 -
Int8.
toInt64 -
Int8.
toNat -
Int8.
xor -
IntCast
-
IntCast.
mk -
Iterator
-
i
-
ibelow
-
id_map
-
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
-
intCast
-
intercalate
-
interpolatedStrKind
-
interpolatedStrLitKind
-
intro
(0) (1) -
intro | ...
=> ... | ... => ... -
intros
-
invImage
-
iota
-
isAbsolute
-
isAlpha
-
isAlphanum
-
isDigit
-
isDir
-
isEmpty
-
isEqSome
-
isEqv
-
isInt
-
isLower
-
isLt
-
isNat
-
isNone
-
isOfKind
-
isOk
-
isPosValue
-
isPowerOfTwo
-
isPrefixOf
-
isRelative
-
isSome
-
isTty
-
isUpper
-
isValid
-
isValidChar
-
isValue
-
isWhitespace
-
iter
-
iterate
K
-
kill
-
kleisliLeft
-
kleisliRight
L
-
LE
-
LE.
mk -
LT
-
LT.
mk -
LawfulApplicative
-
LawfulApplicative.
mk -
LawfulBEq
-
LawfulBEq.
mk -
LawfulFunctor
-
LawfulFunctor.
mk -
LawfulGetElem
-
LawfulGetElem.
mk -
LawfulMonad
-
LawfulMonad.
mk -
LawfulMonad.
mk' -
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
-
List
-
List.
cons -
List.
nil -
land
-
last
-
lastCases
-
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
-
lift
-
liftMetaMAtMain
-
liftOrGet
-
liftWith
-
lineEq
-
lines
-
linter.
unnecessarySimpa - literal
-
lock
-
log2
-
lor
-
lt
-
lt_wfRel
M
-
MProd
-
MProd.
mk -
MacroM
-
Metadata
-
Mod
-
Mod.
mk -
Mode
-
Monad
-
Monad.
mk -
MonadControl
-
MonadControl.
mk -
MonadControlT
-
MonadControlT.
mk -
MonadExcept
-
MonadExcept.
mk -
MonadExcept.
ofExcept -
MonadExcept.
orElse -
MonadExcept.
orelse' -
MonadExceptOf
-
MonadExceptOf.
mk -
MonadFinally
-
MonadFinally.
mk -
MonadFunctor
-
MonadFunctor.
mk -
MonadFunctorT
-
MonadFunctorT.
mk -
MonadLift
-
MonadLift.
mk -
MonadLiftT
-
MonadLiftT.
mk -
MonadReader
-
MonadReader.
mk -
MonadReaderOf
-
MonadReaderOf.
mk -
MonadState
-
MonadState.
get -
MonadState.
mk -
MonadState.
modifyGet -
MonadStateOf
-
MonadStateOf.
mk -
MonadWithReader
-
MonadWithReader.
mk -
MonadWithReaderOf
-
MonadWithReaderOf.
mk -
Mul
-
Mul.
mk - main goal
-
map
-
mapA
-
mapConst
-
mapError
-
mapFinIdx
-
mapFinIdxM
-
mapIdx
-
mapIdxM
-
mapIndexed
-
mapIndexedM
-
mapM
-
mapM'
-
mapMono
-
mapMonoM
-
mapRev
-
mapTask
-
mapTasks
-
map_const
-
map_pure
-
match
-
max
-
maxDischargeDepth
-
maxHeartbeats
-
maxSize
-
maxSteps
-
memoize
-
merge
-
metadata
-
min
-
mk
-
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
-
modifyGetThe
-
modifyM
-
modifyOp
-
modifyThe
-
modn
-
monadLift
-
monadMap
-
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.
mk -
NatPow
-
NatPow.
mk -
NeZero
-
NeZero.
mk -
Neg
-
Neg.
mk -
NewGoals
-
Nonempty
-
Nonempty.
intro -
NumLit
-
nameLitKind
- namespace
-
natAbs
-
natAdd
-
natCast
-
native_decide
-
neg
-
negOfNat
-
neutralConfig
-
newGoals
-
next
-
next ...
=> ... -
next'
-
nextPowerOfTwo
-
nextUntil
-
nextWhile
-
nextn
-
noConfusion
-
noConfusionType
-
nofun
-
nomatch
-
nonBacktrackable
-
norm_cast
(0) (1) -
normalize
-
not
-
notM
-
nullKind
-
numLitKind
O
-
Occurrences
-
OfNat
-
OfNat.
mk -
OfScientific
-
OfScientific.
mk -
Option
-
Option.
all -
Option.
any -
Option.
attach -
Option.
attachWith -
Option.
bind -
Option.
bindM -
Option.
choice -
Option.
decidable_eq_none -
Option.
elim -
Option.
elimM -
Option.
filter -
Option.
forM -
Option.
format -
Option.
get -
Option.
get! -
Option.
getD -
Option.
getDM -
Option.
getM -
Option.
guard -
Option.
isEqSome -
Option.
isNone -
Option.
isSome -
Option.
join -
Option.
liftOrGet -
Option.
lt -
Option.
map -
Option.
mapA -
Option.
mapM -
Option.
max -
Option.
merge -
Option.
min -
Option.
none -
Option.
or -
Option.
orElse -
Option.
pbind -
Option.
pelim -
Option.
pmap -
Option.
repr -
Option.
sequence -
Option.
some -
Option.
toArray -
Option.
toList -
Option.
tryCatch -
Option.
unattach -
OptionT
-
OptionT.
bind -
OptionT.
fail -
OptionT.
lift -
OptionT.
mk -
OptionT.
orElse -
OptionT.
pure -
OptionT.
run -
OptionT.
tryCatch -
Ord
-
Ord.
mk -
Ordering
-
Ordering.
eq -
Ordering.
gt -
Ordering.
lt -
Output
-
obtain
-
occs
-
ofBuffer
-
ofExcept
-
ofFn
-
ofHandle
-
ofInt
-
ofNat
-
ofNat'
-
ofNat32
-
ofNatCore
-
ofNatTruncate
-
ofScientific
-
ofSubarray
-
offsetCnstrs
-
offsetOfPos
-
omega
-
open
-
optParam
-
optional
-
or
-
orElse
-
orElse'
-
orElseLazy
-
orM
-
orelse'
-
other
-
otherErrorToString
-
out
-
outParam
-
output
P
-
PEmpty
-
PEmpty.
elim -
PLift
-
PLift.
up -
PProd
-
PProd.
mk -
PSigma
-
PSigma.
mk -
PSum
-
PSum.
inl -
PSum.
inr -
PUnit
-
PUnit.
unit -
Pos
-
Pow
-
Pow.
mk -
Prec
-
Preresolved
-
Prio
-
Priority
-
Prod
-
Prod.
mk -
Prop
-
Pure
-
Pure.
mk - parameter
-
parent
- parser
-
partition
-
path
-
pathExists
-
pathSeparator
-
pathSeparators
-
pattern
-
pbind
-
pelim
- placeholder term
-
pmap
- polymorphism
-
pop
-
popFront
-
popWhile
-
pos
-
posOf
-
pow
-
pp.
deepTerms -
pp.
deepTerms. threshold -
pp.
fieldNotation -
pp.
match -
pp.
maxSteps -
pp.
mvars -
pp.
proofs -
pp.
proofs. threshold -
pred
- predicative
-
prev
-
prevn
-
print
-
println
-
proj
- proof state
-
proofs
-
property
-
propext
- proposition
-
pruneSolvedGoals
-
ptrEq
-
pure
-
pure_bind
-
pure_seq
-
push
-
push_cast
-
pushn
-
putStr
-
putStrLn
Q
-
qsort
-
qsortOrd
- quantification
-
quote
R
-
RandomGen
-
RandomGen.
mk -
ReaderM
-
ReaderT
-
ReaderT.
adapt -
ReaderT.
bind -
ReaderT.
failure -
ReaderT.
orElse -
ReaderT.
pure -
ReaderT.
read -
ReaderT.
run -
Ref
-
Repr
-
Repr.
mk -
Result
-
rand
-
randBool
-
randNat
-
range
-
raw
-
rcases
-
read
-
readBinFile
-
readBinToEnd
-
readBinToEndInto
-
readDir
-
readFile
-
readThe
-
readToEnd
-
realPath
-
rec
-
recOn
- recursor
-
reduce
-
reduceAbs
-
reduceAdd
-
reduceAddNat
-
reduceAnd
-
reduceAppend
-
reduceBEq
-
reduceBNe
-
reduceBdiv
-
reduceBeqDiff
-
reduceBin
-
reduceBinIntNatOp
-
reduceBinPred
-
reduceBmod
-
reduceBneDiff
-
reduceBoolPred
-
reduceCastAdd
-
reduceCastLE
-
reduceCastLT
-
reduceCastSucc
-
reduceDiv
-
reduceEq
-
reduceEqDiff
-
reduceFDiv
-
reduceFMod
-
reduceFinMk
-
reduceGE
-
reduceGT
-
reduceGcd
-
reduceGetElem
-
reduceGetElem!
-
reduceGetElem?
-
reduceLE
-
reduceLT
-
reduceLTLE
-
reduceLast
-
reduceLeDiff
-
reduceMk
-
reduceMod
-
reduceMul
-
reduceNatAdd
-
reduceNatCore
-
reduceNatEqExpr
-
reduceNatOp
-
reduceNe
-
reduceNeg
-
reduceNegSucc
-
reduceOfNat
-
reduceOfNat'
-
reduceOfNatCore
-
reduceOp
-
reduceOption
-
reduceOr
-
reducePow
-
reducePred
-
reduceRev
-
reduceShiftLeft
-
reduceShiftRight
-
reduceSub
-
reduceSubDiff
-
reduceSubNat
-
reduceSucc
-
reduceTDiv
-
reduceTMod
-
reduceToNat
-
reduceUnary
-
reduceXor
- reduction
-
ref
-
refine
-
refine'
-
registerDerivingHandler
-
registerSimpAttr
-
rel
-
remainingBytes
-
remainingToString
-
removeDir
-
removeDirAll
-
removeFile
-
removeLeadingSpaces
-
rename
-
rename_i
-
repeat
(0) (1) -
repeat'
-
repeat1'
-
repeatTR
-
replace
-
repr
-
reprPrec
-
resolveGlobalName
-
resolveNamespace
-
restore
-
restoreM
-
rev
-
revFind
-
revPosOf
-
reverse
-
reverseInduction
-
revert
-
rewind
-
rewrite
(0) (1) -
rfl
(0) (1) -
rfl'
-
rhs
-
right
(0) (1) -
rintro
-
root
-
rotate_left
-
rotate_right
-
run
-
run'
-
runCatch
-
runEST
-
runK
-
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 -
STWorld
-
STWorld.
mk -
ScientificLit
-
Seq
-
Seq.
mk -
SeqLeft
-
SeqLeft.
mk -
SeqRight
-
SeqRight.
mk -
ShiftLeft
-
ShiftLeft.
mk -
ShiftRight
-
ShiftRight.
mk -
Sigma
-
Sigma.
mk -
SimpExtension
-
SizeOf
-
SizeOf.
mk -
Sort
-
SourceInfo
-
SpawnArgs
-
StateCpsT
-
StateCpsT.
lift -
StateCpsT.
run -
StateCpsT.
run' -
StateCpsT.
runK -
StateM
-
StateRefT'
-
StateRefT'.
get -
StateRefT'.
lift -
StateRefT'.
modifyGet -
StateRefT'.
run -
StateRefT'.
run' -
StateRefT'.
set -
StateT
-
StateT.
bind -
StateT.
failure -
StateT.
get -
StateT.
lift -
StateT.
map -
StateT.
modifyGet -
StateT.
orElse -
StateT.
pure -
StateT.
run -
StateT.
run' -
StateT.
set -
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.
mk -
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 -
Subtype
-
Subtype.
mk -
Sum
-
Sum.
inl -
Sum.
inr -
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
-
seq
-
seqLeft
-
seqLeft_eq
-
seqRight
-
seqRight_eq
-
seq_assoc
-
seq_pure
-
sequence
-
sequenceMap
-
set
-
set!
-
setAccessRights
-
setCurr
-
setCurrentDir
-
setD
-
setGoals
-
setKind
-
setRandSeed
-
setStderr
-
setStdin
-
setStdout
-
set_option
-
setsid
-
shiftLeft
-
shiftRight
-
show
-
show_term
-
sign
-
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
-
snd
-
solve
-
solve_by_elim
-
sorry
-
sortMVarIdArrayByIndex
-
sortMVarIdsByIndex
-
spawn
-
specialize
-
split
-
splitOn
-
stM
-
start
-
start_le_stop
-
startsWith
-
stdNext
-
stdRange
-
stdSplit
-
stderr
-
stdin
-
stdout
-
stop
-
stop_le_array_size
-
strLitKind
-
strongInductionOn
-
sub
-
subDigitChar
-
subNat
-
subNatNat
-
subst
-
subst_eqs
-
subst_vars
-
substrEq
-
succ
-
succRec
-
succRecOn
-
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.
mk -
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
-
tdiv
- term
-
testBit
-
threshold
-
throw
-
throwError
-
throwErrorAt
-
throwThe
-
throwUnsupported
-
tmod
-
toApplicative
-
toArray
-
toBaseIO
-
toBind
-
toBitVec
-
toBool
-
toDigits
-
toDigitsCore
-
toEIO
-
toEnd
-
toFileMap
-
toFloat
-
toFloat32
-
toFormat
-
toFunctor
-
toGetElem
-
toHandleType
-
toIO
-
toIO'
-
toISize
-
toInt
-
toInt!
-
toInt16
-
toInt32
-
Bool.
toInt32 -
ISize.
toInt32 -
Int.
toInt32 -
Int16.
(0) (1)toInt32 -
Int64.
toInt32 -
Int8.
(0) (1)toInt32
-
-
toInt64
-
toInt8
-
toInt?
-
toLawfulApplicative
-
toLawfulFunctor
-
toLevel
-
toList
-
toListAppend
-
toListRev
-
toLower
-
toMonadStateOf
-
toName
-
toNat
-
toNat!
-
toNat'
-
toNat?
-
toOption
-
toPArray'
-
toPure
-
toSeq
-
toSeqLeft
-
toSeqRight
-
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
-
tryCatchThe
-
tryFinally'
-
tryLock
-
tryTactic
-
tryTactic?
-
tryWait
-
type
- type constructor
U
-
UInt16
-
UInt16.
add -
UInt16.
complement -
UInt16.
decEq -
UInt16.
decLe -
UInt16.
decLt -
UInt16.
div -
UInt16.
fromExpr -
UInt16.
land -
UInt16.
le -
UInt16.
log2 -
UInt16.
lor -
UInt16.
lt -
UInt16.
mk -
UInt16.
mod -
UInt16.
mul -
UInt16.
ofNat -
UInt16.
ofNatCore -
UInt16.
reduceAdd -
UInt16.
reduceDiv -
UInt16.
reduceGE -
UInt16.
reduceGT -
UInt16.
reduceLE -
UInt16.
reduceLT -
UInt16.
reduceMod -
UInt16.
reduceMul -
UInt16.
reduceOfNat -
UInt16.
reduceOfNatCore -
UInt16.
reduceSub -
UInt16.
reduceToNat -
UInt16.
shiftLeft -
UInt16.
shiftRight -
UInt16.
size -
UInt16.
sub -
UInt16.
toNat -
UInt16.
toUInt32 -
UInt16.
toUInt64 -
UInt16.
toUInt8 -
UInt16.
toUSize -
UInt16.
val -
UInt16.
xor -
UInt32
-
UInt32.
add -
UInt32.
complement -
UInt32.
decEq -
UInt32.
decLe -
UInt32.
decLt -
UInt32.
div -
UInt32.
fromExpr -
UInt32.
isValidChar -
UInt32.
land -
UInt32.
log2 -
UInt32.
lor -
UInt32.
mk -
UInt32.
mod -
UInt32.
mul -
UInt32.
ofNat -
UInt32.
ofNat' -
UInt32.
ofNatCore -
UInt32.
ofNatTruncate -
UInt32.
reduceAdd -
UInt32.
reduceDiv -
UInt32.
reduceGE -
UInt32.
reduceGT -
UInt32.
reduceLE -
UInt32.
reduceLT -
UInt32.
reduceMod -
UInt32.
reduceMul -
UInt32.
reduceOfNat -
UInt32.
reduceOfNatCore -
UInt32.
reduceSub -
UInt32.
reduceToNat -
UInt32.
shiftLeft -
UInt32.
shiftRight -
UInt32.
size -
UInt32.
sub -
UInt32.
toNat -
UInt32.
toUInt16 -
UInt32.
toUInt64 -
UInt32.
toUInt8 -
UInt32.
toUSize -
UInt32.
val -
UInt32.
xor -
UInt64
-
UInt64.
add -
UInt64.
complement -
UInt64.
decEq -
UInt64.
decLe -
UInt64.
decLt -
UInt64.
div -
UInt64.
fromExpr -
UInt64.
land -
UInt64.
le -
UInt64.
log2 -
UInt64.
lor -
UInt64.
lt -
UInt64.
mk -
UInt64.
mod -
UInt64.
mul -
UInt64.
ofNat -
UInt64.
ofNatCore -
UInt64.
reduceAdd -
UInt64.
reduceDiv -
UInt64.
reduceGE -
UInt64.
reduceGT -
UInt64.
reduceLE -
UInt64.
reduceLT -
UInt64.
reduceMod -
UInt64.
reduceMul -
UInt64.
reduceOfNat -
UInt64.
reduceOfNatCore -
UInt64.
reduceSub -
UInt64.
reduceToNat -
UInt64.
shiftLeft -
UInt64.
shiftRight -
UInt64.
size -
UInt64.
sub -
UInt64.
toFloat -
UInt64.
toFloat32 -
UInt64.
toNat -
UInt64.
toUInt16 -
UInt64.
toUInt32 -
UInt64.
toUInt8 -
UInt64.
toUSize -
UInt64.
val -
UInt64.
xor -
UInt8
-
UInt8.
add -
UInt8.
complement -
UInt8.
decEq -
UInt8.
decLe -
UInt8.
decLt -
UInt8.
div -
UInt8.
fromExpr -
UInt8.
land -
UInt8.
le -
UInt8.
log2 -
UInt8.
lor -
UInt8.
lt -
UInt8.
mk -
UInt8.
mod -
UInt8.
mul -
UInt8.
ofNat -
UInt8.
ofNatCore -
UInt8.
reduceAdd -
UInt8.
reduceDiv -
UInt8.
reduceGE -
UInt8.
reduceGT -
UInt8.
reduceLE -
UInt8.
reduceLT -
UInt8.
reduceMod -
UInt8.
reduceMul -
UInt8.
reduceOfNat -
UInt8.
reduceOfNatCore -
UInt8.
reduceSub -
UInt8.
reduceToNat -
UInt8.
shiftLeft -
UInt8.
shiftRight -
UInt8.
size -
UInt8.
sub -
UInt8.
toNat -
UInt8.
toUInt16 -
UInt8.
toUInt32 -
UInt8.
toUInt64 -
UInt8.
toUSize -
UInt8.
val -
UInt8.
xor -
ULift
-
ULift.
up -
USize
-
USize.
add -
USize.
complement -
USize.
decEq -
USize.
decLe -
USize.
decLt -
USize.
div -
USize.
fromExpr -
USize.
land -
USize.
le -
USize.
log2 -
USize.
lor -
USize.
lt -
USize.
mk -
USize.
mod -
USize.
mul -
USize.
ofNat -
USize.
ofNat32 -
USize.
ofNatCore -
USize.
reduceToNat -
USize.
repr -
USize.
shiftLeft -
USize.
shiftRight -
USize.
size -
USize.
sub -
USize.
toNat -
USize.
toUInt16 -
USize.
toUInt32 -
USize.
toUInt64 -
USize.
toUInt8 -
USize.
val -
USize.
xor -
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
W
-
WellFounded
-
WellFounded.
fix -
WellFounded.
intro -
WellFoundedRelation
-
WellFoundedRelation.
mk -
wait
-
waitAny
-
walkDir
-
wf
-
whnf
-
withExtension
-
withFile
-
withFileName
-
withFreshMacroScope
-
withIsolatedStreams
-
withLocation
-
withPosition
-
withPositionAfterLinebreak
-
withReader
-
withStderr
-
withStdin
-
withStdout
-
withTempFile
-
withTheReader
-
with_reducible
-
with_reducible_and_instances
-
with_unfolding_all
-
withoutPosition
-
write
-
writeBinFile
-
writeFile
X
Applicative
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
Array
Array.eraseIdx!, Array.eraseIdxIfInBounds, Array.eraseP, Array.finRange, Array.findFinIdx?, Array.findFinIdx?.loop, Array.insertIdx, Array.insertIdx!, Array.insertIdx.loop, Array.insertIdxIfInBounds, Array.lex, Array.pmap, Array.setIfInBounds, Array.swapIfInBounds, Array.toVector, Array.zipWithAll, Array.zipWithAll.go, Array.«term__[:_]», Array.«term__[_:]», Array.«term__[_:_]», Array.«term_~_»
{docstring Array.eraseIdx!} {docstring Array.eraseIdxIfInBounds} {docstring Array.eraseP} {docstring Array.finRange} {docstring Array.findFinIdx?} {docstring Array.findFinIdx?.loop} {docstring Array.insertIdx} {docstring Array.insertIdx!} {docstring Array.insertIdx.loop} {docstring Array.insertIdxIfInBounds} {docstring Array.lex} {docstring Array.pmap} {docstring Array.setIfInBounds} {docstring Array.swapIfInBounds} {docstring Array.toVector} {docstring Array.zipWithAll} {docstring Array.zipWithAll.go} {docstring Array.«term__[:_]»} {docstring Array.«term__[_:]»} {docstring Array.«term__[_:_]»} {docstring Array.«term_~_»}
```exceptions Array.eraseIdx! Array.eraseIdxIfInBounds Array.eraseP Array.finRange Array.findFinIdx? Array.findFinIdx?.loop Array.insertIdx Array.insertIdx! Array.insertIdx.loop Array.insertIdxIfInBounds Array.lex Array.pmap Array.setIfInBounds Array.swapIfInBounds Array.toVector Array.zipWithAll Array.zipWithAll.go Array.«term__[:_]» Array.«term__[_:]» Array.«term__[_:_]» Array.«term_~_» ```
BaseIO
```exceptions ```
Bind
```exceptions ```
BitVec
BitVec.abs, BitVec.adc, BitVec.adcb, BitVec.add, BitVec.allOnes, BitVec.and, BitVec.append, BitVec.carry, BitVec.cast, BitVec.concat, BitVec.cons, BitVec.decEq, BitVec.divRec, BitVec.divSubtractShift, BitVec.extractLsb, BitVec.extractLsb', BitVec.fill, BitVec.fromExpr?, BitVec.getLsb', BitVec.getLsb?, BitVec.getLsbD, BitVec.getMsb', BitVec.getMsb?, BitVec.getMsbD, BitVec.hash, BitVec.intMax, BitVec.intMin, BitVec.iunfoldr, BitVec.msb, BitVec.mul, BitVec.mulRec, BitVec.neg, BitVec.nil, BitVec.not, BitVec.ofBool, BitVec.ofBoolListBE, BitVec.ofBoolListLE, BitVec.ofInt, BitVec.ofNat, BitVec.ofNatLt, BitVec.or, BitVec.reduceAbs, BitVec.reduceAdd, BitVec.reduceAllOnes, BitVec.reduceAnd, BitVec.reduceAppend, BitVec.reduceBEq, BitVec.reduceBNe, BitVec.reduceBin, BitVec.reduceBinPred, BitVec.reduceBitVecOfFin, BitVec.reduceBitVecToFin, BitVec.reduceBoolPred, BitVec.reduceCast, BitVec.reduceDiv, BitVec.reduceEq, BitVec.reduceExtend, BitVec.reduceExtracLsb', BitVec.reduceGE, BitVec.reduceGT, BitVec.reduceGetBit, BitVec.reduceGetLsb, BitVec.reduceGetMsb, BitVec.reduceHShiftLeft, BitVec.reduceHShiftLeft', BitVec.reduceHShiftRight, BitVec.reduceHShiftRight', BitVec.reduceLE, BitVec.reduceLT, BitVec.reduceMod, BitVec.reduceMul, BitVec.reduceNe, BitVec.reduceNeg, BitVec.reduceNot, BitVec.reduceOfInt, BitVec.reduceOfNat, BitVec.reduceOr, BitVec.reduceReplicate, BitVec.reduceRotateLeft, BitVec.reduceRotateRight, BitVec.reduceSDiv, BitVec.reduceSLE, BitVec.reduceSLT, BitVec.reduceSMTSDiv, BitVec.reduceSMTUDiv, BitVec.reduceSMod, BitVec.reduceSRem, BitVec.reduceSShiftRight, BitVec.reduceSetWidth, BitVec.reduceSetWidth', BitVec.reduceShift, BitVec.reduceShiftLeft, BitVec.reduceShiftLeftShiftLeft, BitVec.reduceShiftLeftZeroExtend, BitVec.reduceShiftRightShiftRight, BitVec.reduceShiftShift, BitVec.reduceShiftWithBitVecLit, BitVec.reduceSignExtend, BitVec.reduceSub, BitVec.reduceToInt, BitVec.reduceToNat, BitVec.reduceUDiv, BitVec.reduceULE, BitVec.reduceULT, BitVec.reduceUMod, BitVec.reduceUShiftRight, BitVec.reduceUnary, BitVec.reduceXOr, BitVec.reduceZeroExtend, BitVec.replicate, BitVec.rotateLeft, BitVec.rotateLeftAux, BitVec.rotateRight, BitVec.rotateRightAux, BitVec.sdiv, BitVec.setWidth, BitVec.setWidth', BitVec.shiftConcat, BitVec.shiftLeft, BitVec.shiftLeftRec, BitVec.shiftLeftZeroExtend, BitVec.signExtend, BitVec.sle, BitVec.slt, BitVec.smod, BitVec.smtSDiv, BitVec.smtUDiv, BitVec.srem, BitVec.sshiftRight, BitVec.sshiftRight', BitVec.sshiftRightRec, BitVec.sub, BitVec.toHex, BitVec.toInt, BitVec.toNat, BitVec.truncate, BitVec.twoPow, BitVec.udiv, BitVec.ule, BitVec.ult, BitVec.umod, BitVec.unexpandBitVecOfNat, BitVec.unexpandBitVecOfNatLt, BitVec.ushiftRight, BitVec.ushiftRightRec, BitVec.xor, BitVec.zero, BitVec.zeroExtend, BitVec.«term__#'__», BitVec.«term__#__»
{docstring BitVec.abs} {docstring BitVec.adc} {docstring BitVec.adcb} {docstring BitVec.add} {docstring BitVec.allOnes} {docstring BitVec.and} {docstring BitVec.append} {docstring BitVec.carry} {docstring BitVec.cast} {docstring BitVec.concat} {docstring BitVec.cons} {docstring BitVec.decEq} {docstring BitVec.divRec} {docstring BitVec.divSubtractShift} {docstring BitVec.extractLsb} {docstring BitVec.extractLsb'} {docstring BitVec.fill} {docstring BitVec.fromExpr?} {docstring BitVec.getLsb'} {docstring BitVec.getLsb?} {docstring BitVec.getLsbD} {docstring BitVec.getMsb'} {docstring BitVec.getMsb?} {docstring BitVec.getMsbD} {docstring BitVec.hash} {docstring BitVec.intMax} {docstring BitVec.intMin} {docstring BitVec.iunfoldr} {docstring BitVec.msb} {docstring BitVec.mul} {docstring BitVec.mulRec} {docstring BitVec.neg} {docstring BitVec.nil} {docstring BitVec.not} {docstring BitVec.ofBool} {docstring BitVec.ofBoolListBE} {docstring BitVec.ofBoolListLE} {docstring BitVec.ofInt} {docstring BitVec.ofNat} {docstring BitVec.ofNatLt} {docstring BitVec.or} {docstring BitVec.reduceAbs} {docstring BitVec.reduceAdd} {docstring BitVec.reduceAllOnes} {docstring BitVec.reduceAnd} {docstring BitVec.reduceAppend} {docstring BitVec.reduceBEq} {docstring BitVec.reduceBNe} {docstring BitVec.reduceBin} {docstring BitVec.reduceBinPred} {docstring BitVec.reduceBitVecOfFin} {docstring BitVec.reduceBitVecToFin} {docstring BitVec.reduceBoolPred} {docstring BitVec.reduceCast} {docstring BitVec.reduceDiv} {docstring BitVec.reduceEq} {docstring BitVec.reduceExtend} {docstring BitVec.reduceExtracLsb'} {docstring BitVec.reduceGE} {docstring BitVec.reduceGT} {docstring BitVec.reduceGetBit} {docstring BitVec.reduceGetLsb} {docstring BitVec.reduceGetMsb} {docstring BitVec.reduceHShiftLeft} {docstring BitVec.reduceHShiftLeft'} {docstring BitVec.reduceHShiftRight} {docstring BitVec.reduceHShiftRight'} {docstring BitVec.reduceLE} {docstring BitVec.reduceLT} {docstring BitVec.reduceMod} {docstring BitVec.reduceMul} {docstring BitVec.reduceNe} {docstring BitVec.reduceNeg} {docstring BitVec.reduceNot} {docstring BitVec.reduceOfInt} {docstring BitVec.reduceOfNat} {docstring BitVec.reduceOr} {docstring BitVec.reduceReplicate} {docstring BitVec.reduceRotateLeft} {docstring BitVec.reduceRotateRight} {docstring BitVec.reduceSDiv} {docstring BitVec.reduceSLE} {docstring BitVec.reduceSLT} {docstring BitVec.reduceSMTSDiv} {docstring BitVec.reduceSMTUDiv} {docstring BitVec.reduceSMod} {docstring BitVec.reduceSRem} {docstring BitVec.reduceSShiftRight} {docstring BitVec.reduceSetWidth} {docstring BitVec.reduceSetWidth'} {docstring BitVec.reduceShift} {docstring BitVec.reduceShiftLeft} {docstring BitVec.reduceShiftLeftShiftLeft} {docstring BitVec.reduceShiftLeftZeroExtend} {docstring BitVec.reduceShiftRightShiftRight} {docstring BitVec.reduceShiftShift} {docstring BitVec.reduceShiftWithBitVecLit} {docstring BitVec.reduceSignExtend} {docstring BitVec.reduceSub} {docstring BitVec.reduceToInt} {docstring BitVec.reduceToNat} {docstring BitVec.reduceUDiv} {docstring BitVec.reduceULE} {docstring BitVec.reduceULT} {docstring BitVec.reduceUMod} {docstring BitVec.reduceUShiftRight} {docstring BitVec.reduceUnary} {docstring BitVec.reduceXOr} {docstring BitVec.reduceZeroExtend} {docstring BitVec.replicate} {docstring BitVec.rotateLeft} {docstring BitVec.rotateLeftAux} {docstring BitVec.rotateRight} {docstring BitVec.rotateRightAux} {docstring BitVec.sdiv} {docstring BitVec.setWidth} {docstring BitVec.setWidth'} {docstring BitVec.shiftConcat} {docstring BitVec.shiftLeft} {docstring BitVec.shiftLeftRec} {docstring BitVec.shiftLeftZeroExtend} {docstring BitVec.signExtend} {docstring BitVec.sle} {docstring BitVec.slt} {docstring BitVec.smod} {docstring BitVec.smtSDiv} {docstring BitVec.smtUDiv} {docstring BitVec.srem} {docstring BitVec.sshiftRight} {docstring BitVec.sshiftRight'} {docstring BitVec.sshiftRightRec} {docstring BitVec.sub} {docstring BitVec.toHex} {docstring BitVec.toInt} {docstring BitVec.toNat} {docstring BitVec.truncate} {docstring BitVec.twoPow} {docstring BitVec.udiv} {docstring BitVec.ule} {docstring BitVec.ult} {docstring BitVec.umod} {docstring BitVec.unexpandBitVecOfNat} {docstring BitVec.unexpandBitVecOfNatLt} {docstring BitVec.ushiftRight} {docstring BitVec.ushiftRightRec} {docstring BitVec.xor} {docstring BitVec.zero} {docstring BitVec.zeroExtend} {docstring BitVec.«term__#'__»} {docstring BitVec.«term__#__»}
```exceptions BitVec.abs BitVec.adc BitVec.adcb BitVec.add BitVec.allOnes BitVec.and BitVec.append BitVec.carry BitVec.cast BitVec.concat BitVec.cons BitVec.decEq BitVec.divRec BitVec.divSubtractShift BitVec.extractLsb BitVec.extractLsb' BitVec.fill BitVec.fromExpr? BitVec.getLsb' BitVec.getLsb? BitVec.getLsbD BitVec.getMsb' BitVec.getMsb? BitVec.getMsbD BitVec.hash BitVec.intMax BitVec.intMin BitVec.iunfoldr BitVec.msb BitVec.mul BitVec.mulRec BitVec.neg BitVec.nil BitVec.not BitVec.ofBool BitVec.ofBoolListBE BitVec.ofBoolListLE BitVec.ofInt BitVec.ofNat BitVec.ofNatLt BitVec.or BitVec.reduceAbs BitVec.reduceAdd BitVec.reduceAllOnes BitVec.reduceAnd BitVec.reduceAppend BitVec.reduceBEq BitVec.reduceBNe BitVec.reduceBin BitVec.reduceBinPred BitVec.reduceBitVecOfFin BitVec.reduceBitVecToFin BitVec.reduceBoolPred BitVec.reduceCast BitVec.reduceDiv BitVec.reduceEq BitVec.reduceExtend BitVec.reduceExtracLsb' BitVec.reduceGE BitVec.reduceGT BitVec.reduceGetBit BitVec.reduceGetLsb BitVec.reduceGetMsb BitVec.reduceHShiftLeft BitVec.reduceHShiftLeft' BitVec.reduceHShiftRight BitVec.reduceHShiftRight' BitVec.reduceLE BitVec.reduceLT BitVec.reduceMod BitVec.reduceMul BitVec.reduceNe BitVec.reduceNeg BitVec.reduceNot BitVec.reduceOfInt BitVec.reduceOfNat BitVec.reduceOr BitVec.reduceReplicate BitVec.reduceRotateLeft BitVec.reduceRotateRight BitVec.reduceSDiv BitVec.reduceSLE BitVec.reduceSLT BitVec.reduceSMTSDiv BitVec.reduceSMTUDiv BitVec.reduceSMod BitVec.reduceSRem BitVec.reduceSShiftRight BitVec.reduceSetWidth BitVec.reduceSetWidth' BitVec.reduceShift BitVec.reduceShiftLeft BitVec.reduceShiftLeftShiftLeft BitVec.reduceShiftLeftZeroExtend BitVec.reduceShiftRightShiftRight BitVec.reduceShiftShift BitVec.reduceShiftWithBitVecLit BitVec.reduceSignExtend BitVec.reduceSub BitVec.reduceToInt BitVec.reduceToNat BitVec.reduceUDiv BitVec.reduceULE BitVec.reduceULT BitVec.reduceUMod BitVec.reduceUShiftRight BitVec.reduceUnary BitVec.reduceXOr BitVec.reduceZeroExtend BitVec.replicate BitVec.rotateLeft BitVec.rotateLeftAux BitVec.rotateRight BitVec.rotateRightAux BitVec.sdiv BitVec.setWidth BitVec.setWidth' BitVec.shiftConcat BitVec.shiftLeft BitVec.shiftLeftRec BitVec.shiftLeftZeroExtend BitVec.signExtend BitVec.sle BitVec.slt BitVec.smod BitVec.smtSDiv BitVec.smtUDiv BitVec.srem BitVec.sshiftRight BitVec.sshiftRight' BitVec.sshiftRightRec BitVec.sub BitVec.toHex BitVec.toInt BitVec.toNat BitVec.truncate BitVec.twoPow BitVec.udiv BitVec.ule BitVec.ult BitVec.umod BitVec.unexpandBitVecOfNat BitVec.unexpandBitVecOfNatLt BitVec.ushiftRight BitVec.ushiftRightRec BitVec.xor BitVec.zero BitVec.zeroExtend BitVec.«term__#'__» BitVec.«term__#__» ```
Bool
Bool.toInt
{docstring Bool.toInt}
```exceptions Bool.toInt ```
Char
Char.fromExpr?, Char.isValidCharNat, Char.isValue, Char.le, Char.lt, Char.notLTAntisymm, Char.notLTTotal, Char.notLTTrans, Char.ofNat, Char.ofNatAux, Char.ofUInt8, Char.quote, Char.quoteCore, Char.quoteCore.smallCharToHex, Char.reduceBEq, Char.reduceBNe, Char.reduceBinPred, Char.reduceBoolPred, Char.reduceDefault, Char.reduceEq, Char.reduceGE, Char.reduceGT, Char.reduceIsAlpha, Char.reduceIsAlphaNum, Char.reduceIsDigit, Char.reduceIsLower, Char.reduceIsUpper, Char.reduceIsWhitespace, Char.reduceLE, Char.reduceLT, Char.reduceNe, Char.reduceOfNatAux, Char.reduceToLower, Char.reduceToNat, Char.reduceToString, Char.reduceToUpper, Char.reduceUnary, Char.reduceVal, Char.repr, Char.toLower, Char.toNat, Char.toString, Char.toUInt8, Char.toUpper, Char.utf16Size, Char.utf8Size
{docstring Char.fromExpr?} {docstring Char.isValidCharNat} {docstring Char.isValue} {docstring Char.le} {docstring Char.lt} {docstring Char.notLTAntisymm} {docstring Char.notLTTotal} {docstring Char.notLTTrans} {docstring Char.ofNat} {docstring Char.ofNatAux} {docstring Char.ofUInt8} {docstring Char.quote} {docstring Char.quoteCore} {docstring Char.quoteCore.smallCharToHex} {docstring Char.reduceBEq} {docstring Char.reduceBNe} {docstring Char.reduceBinPred} {docstring Char.reduceBoolPred} {docstring Char.reduceDefault} {docstring Char.reduceEq} {docstring Char.reduceGE} {docstring Char.reduceGT} {docstring Char.reduceIsAlpha} {docstring Char.reduceIsAlphaNum} {docstring Char.reduceIsDigit} {docstring Char.reduceIsLower} {docstring Char.reduceIsUpper} {docstring Char.reduceIsWhitespace} {docstring Char.reduceLE} {docstring Char.reduceLT} {docstring Char.reduceNe} {docstring Char.reduceOfNatAux} {docstring Char.reduceToLower} {docstring Char.reduceToNat} {docstring Char.reduceToString} {docstring Char.reduceToUpper} {docstring Char.reduceUnary} {docstring Char.reduceVal} {docstring Char.repr} {docstring Char.toLower} {docstring Char.toNat} {docstring Char.toString} {docstring Char.toUInt8} {docstring Char.toUpper} {docstring Char.utf16Size} {docstring Char.utf8Size}
```exceptions Char.fromExpr? Char.isValidCharNat Char.isValue Char.le Char.lt Char.notLTAntisymm Char.notLTTotal Char.notLTTrans Char.ofNat Char.ofNatAux Char.ofUInt8 Char.quote Char.quoteCore Char.quoteCore.smallCharToHex Char.reduceBEq Char.reduceBNe Char.reduceBinPred Char.reduceBoolPred Char.reduceDefault Char.reduceEq Char.reduceGE Char.reduceGT Char.reduceIsAlpha Char.reduceIsAlphaNum Char.reduceIsDigit Char.reduceIsLower Char.reduceIsUpper Char.reduceIsWhitespace Char.reduceLE Char.reduceLT Char.reduceNe Char.reduceOfNatAux Char.reduceToLower Char.reduceToNat Char.reduceToString Char.reduceToUpper Char.reduceUnary Char.reduceVal Char.repr Char.toLower Char.toNat Char.toString Char.toUInt8 Char.toUpper Char.utf16Size Char.utf8Size ```
Decidable
```exceptions ```
EIO
```exceptions ```
EStateM
```exceptions ```
EStateM.Backtrackable
```exceptions ```
EStateM.Result
```exceptions ```
Empty
```exceptions ```
Except
```exceptions ```
ExceptCpsT
```exceptions ```
ExceptT
```exceptions ```
Fin
```exceptions ```
Float
Float.abs, Float.acos, Float.acosh, Float.add, Float.asin, Float.asinh, Float.atan, Float.atan2, Float.atanh, Float.beq, Float.cbrt, Float.ceil, Float.cos, Float.cosh, Float.decLe, Float.decLt, Float.div, Float.exp, Float.exp2, Float.floor, Float.frExp, Float.isFinite, Float.isInf, Float.isNaN, Float.le, Float.log, Float.log10, Float.log2, Float.lt, Float.mul, Float.neg, Float.ofBinaryScientific, Float.ofBits, Float.ofInt, Float.ofNat, Float.ofScientific, Float.pow, Float.round, Float.scaleB, Float.sin, Float.sinh, Float.sqrt, Float.sub, Float.tan, Float.tanh, Float.toBits, Float.toFloat32, Float.toString, Float.toUInt16, Float.toUInt32, Float.toUInt64, Float.toUInt8, Float.toUSize
{docstring Float.abs} {docstring Float.acos} {docstring Float.acosh} {docstring Float.add} {docstring Float.asin} {docstring Float.asinh} {docstring Float.atan} {docstring Float.atan2} {docstring Float.atanh} {docstring Float.beq} {docstring Float.cbrt} {docstring Float.ceil} {docstring Float.cos} {docstring Float.cosh} {docstring Float.decLe} {docstring Float.decLt} {docstring Float.div} {docstring Float.exp} {docstring Float.exp2} {docstring Float.floor} {docstring Float.frExp} {docstring Float.isFinite} {docstring Float.isInf} {docstring Float.isNaN} {docstring Float.le} {docstring Float.log} {docstring Float.log10} {docstring Float.log2} {docstring Float.lt} {docstring Float.mul} {docstring Float.neg} {docstring Float.ofBinaryScientific} {docstring Float.ofBits} {docstring Float.ofInt} {docstring Float.ofNat} {docstring Float.ofScientific} {docstring Float.pow} {docstring Float.round} {docstring Float.scaleB} {docstring Float.sin} {docstring Float.sinh} {docstring Float.sqrt} {docstring Float.sub} {docstring Float.tan} {docstring Float.tanh} {docstring Float.toBits} {docstring Float.toFloat32} {docstring Float.toString} {docstring Float.toUInt16} {docstring Float.toUInt32} {docstring Float.toUInt64} {docstring Float.toUInt8} {docstring Float.toUSize}
```exceptions Float.abs Float.acos Float.acosh Float.add Float.asin Float.asinh Float.atan Float.atan2 Float.atanh Float.beq Float.cbrt Float.ceil Float.cos Float.cosh Float.decLe Float.decLt Float.div Float.exp Float.exp2 Float.floor Float.frExp Float.isFinite Float.isInf Float.isNaN Float.le Float.log Float.log10 Float.log2 Float.lt Float.mul Float.neg Float.ofBinaryScientific Float.ofBits Float.ofInt Float.ofNat Float.ofScientific Float.pow Float.round Float.scaleB Float.sin Float.sinh Float.sqrt Float.sub Float.tan Float.tanh Float.toBits Float.toFloat32 Float.toString Float.toUInt16 Float.toUInt32 Float.toUInt64 Float.toUInt8 Float.toUSize ```
ForIn
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
ForIn'
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
ForInStep
ForInStep.value
{docstring ForInStep.value}
```exceptions ForInStep.value ```
ForM
```exceptions ```
Function
Function.comp, Function.const, Function.curry, Function.uncurry
{docstring Function.comp} {docstring Function.const} {docstring Function.curry} {docstring Function.uncurry}
```exceptions Function.comp Function.const Function.curry Function.uncurry ```
Functor
```exceptions ```
IO
IO.getTID
{docstring IO.getTID}
```exceptions IO.getTID ```
IO.Error
```exceptions ```
IO.FS
IO.FS.createTempDir, IO.FS.withTempDir
{docstring IO.FS.createTempDir} {docstring IO.FS.withTempDir}
```exceptions IO.FS.createTempDir IO.FS.withTempDir ```
IO.FS.DirEntry
```exceptions ```
IO.FS.Handle
```exceptions ```
IO.FS.Metadata
```exceptions ```
IO.FS.Stream
```exceptions ```
IO.FS.Stream.Buffer
```exceptions ```
IO.FileRight
```exceptions ```
IO.Process
```exceptions ```
IO.Process.Child
```exceptions ```
IO.Process.Output
```exceptions ```
IO.Process.SpawnArgs
```exceptions ```
IO.Process.Stdio
```exceptions ```
IO.Process.StdioConfig
```exceptions ```
IO.Ref
```exceptions ```
ISize
```exceptions ```
Id
```exceptions ```
Int
Int.«term-[_+1]»
{docstring Int.«term-[_+1]»}
```exceptions Int.«term-[_+1]» ```
Int16
```exceptions ```
Int32
```exceptions ```
Int64
```exceptions ```
Int8
```exceptions ```
IntCast
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
LawfulApplicative
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
LawfulFunctor
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
LawfulMonad
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
Lean.Elab.Tactic
Lean.Elab.Tactic.addCheckpoints, Lean.Elab.Tactic.checkCommandConfigElab, Lean.Elab.Tactic.checkConfigElab, Lean.Elab.Tactic.classical, Lean.Elab.Tactic.closeUsingOrAdmit, Lean.Elab.Tactic.commandConfigElab, Lean.Elab.Tactic.configElab, Lean.Elab.Tactic.deltaLocalDecl, Lean.Elab.Tactic.deltaTarget, Lean.Elab.Tactic.done, Lean.Elab.Tactic.dsimpLocation, Lean.Elab.Tactic.elabAsFVar, Lean.Elab.Tactic.elabChange, Lean.Elab.Tactic.elabDecideConfig, Lean.Elab.Tactic.elabGrindConfig, Lean.Elab.Tactic.elabGrindPattern, Lean.Elab.Tactic.elabRewriteConfig, Lean.Elab.Tactic.elabSimpArgs.toZetaDeltaSet, Lean.Elab.Tactic.elabSimpConfigCore, Lean.Elab.Tactic.elabTermForApply, Lean.Elab.Tactic.evalApplyRfl, Lean.Elab.Tactic.evalClassical, Lean.Elab.Tactic.evalDecideCore, Lean.Elab.Tactic.evalDecideCore.diagnose, Lean.Elab.Tactic.evalDecideCore.doElab, Lean.Elab.Tactic.evalDecideCore.doKernel, Lean.Elab.Tactic.expandLocation, Lean.Elab.Tactic.expandOptLocation, Lean.Elab.Tactic.filterOldMVars, Lean.Elab.Tactic.focusAndDone, Lean.Elab.Tactic.forEachVar, Lean.Elab.Tactic.getInductiveValFromMajor, Lean.Elab.Tactic.getMainDecl, Lean.Elab.Tactic.getMainTarget, Lean.Elab.Tactic.getNameOfIdent', Lean.Elab.Tactic.grind, Lean.Elab.Tactic.isCheckpointableTactic, Lean.Elab.Tactic.isHoleRHS, Lean.Elab.Tactic.liftMetaFinishingTactic, Lean.Elab.Tactic.liftMetaTactic, Lean.Elab.Tactic.liftMetaTactic1, Lean.Elab.Tactic.logUnassignedAndAbort, Lean.Elab.Tactic.mkInitialTacticInfo, Lean.Elab.Tactic.mkSimpCallStx, Lean.Elab.Tactic.mkSimpContext, Lean.Elab.Tactic.mkSimpOnly, Lean.Elab.Tactic.mkTacticInfo, Lean.Elab.Tactic.popMainGoal, Lean.Elab.Tactic.pushGoal, Lean.Elab.Tactic.pushGoals, Lean.Elab.Tactic.refineCore, Lean.Elab.Tactic.renameInaccessibles, Lean.Elab.Tactic.replaceMainGoal, Lean.Elab.Tactic.rewriteLocalDecl, Lean.Elab.Tactic.rewriteTarget, Lean.Elab.Tactic.saveState, Lean.Elab.Tactic.saveTacticInfoForToken, Lean.Elab.Tactic.simpLocation, Lean.Elab.Tactic.simpOnlyBuiltins, Lean.Elab.Tactic.tactic.customEliminators, Lean.Elab.Tactic.tacticToDischarge, Lean.Elab.Tactic.throwNoGoalsToBeSolved, Lean.Elab.Tactic.traceSimpCall, Lean.Elab.Tactic.tryCatchRestore, Lean.Elab.Tactic.unfoldLocalDecl, Lean.Elab.Tactic.unfoldTarget, Lean.Elab.Tactic.withCaseRef, Lean.Elab.Tactic.withCollectingNewGoalsFrom, Lean.Elab.Tactic.withMacroExpansion, Lean.Elab.Tactic.withMainContext, Lean.Elab.Tactic.withRWRulesSeq, Lean.Elab.Tactic.withRestoreOrSaveFull, Lean.Elab.Tactic.withSimpDiagnostics, Lean.Elab.Tactic.withTacticInfoContext, Lean.Elab.Tactic.withoutRecover, Lean.Elab.Tactic.zetaDeltaLocalDecl, Lean.Elab.Tactic.zetaDeltaTarget
{docstring Lean.Elab.Tactic.addCheckpoints} {docstring Lean.Elab.Tactic.checkCommandConfigElab} {docstring Lean.Elab.Tactic.checkConfigElab} {docstring Lean.Elab.Tactic.classical} {docstring Lean.Elab.Tactic.closeUsingOrAdmit} {docstring Lean.Elab.Tactic.commandConfigElab} {docstring Lean.Elab.Tactic.configElab} {docstring Lean.Elab.Tactic.deltaLocalDecl} {docstring Lean.Elab.Tactic.deltaTarget} {docstring Lean.Elab.Tactic.done} {docstring Lean.Elab.Tactic.dsimpLocation} {docstring Lean.Elab.Tactic.elabAsFVar} {docstring Lean.Elab.Tactic.elabChange} {docstring Lean.Elab.Tactic.elabDecideConfig} {docstring Lean.Elab.Tactic.elabGrindConfig} {docstring Lean.Elab.Tactic.elabGrindPattern} {docstring Lean.Elab.Tactic.elabRewriteConfig} {docstring Lean.Elab.Tactic.elabSimpArgs.toZetaDeltaSet} {docstring Lean.Elab.Tactic.elabSimpConfigCore} {docstring Lean.Elab.Tactic.elabTermForApply} {docstring Lean.Elab.Tactic.evalApplyRfl} {docstring Lean.Elab.Tactic.evalClassical} {docstring Lean.Elab.Tactic.evalDecideCore} {docstring Lean.Elab.Tactic.evalDecideCore.diagnose} {docstring Lean.Elab.Tactic.evalDecideCore.doElab} {docstring Lean.Elab.Tactic.evalDecideCore.doKernel} {docstring Lean.Elab.Tactic.expandLocation} {docstring Lean.Elab.Tactic.expandOptLocation} {docstring Lean.Elab.Tactic.filterOldMVars} {docstring Lean.Elab.Tactic.focusAndDone} {docstring Lean.Elab.Tactic.forEachVar} {docstring Lean.Elab.Tactic.getInductiveValFromMajor} {docstring Lean.Elab.Tactic.getMainDecl} {docstring Lean.Elab.Tactic.getMainTarget} {docstring Lean.Elab.Tactic.getNameOfIdent'} {docstring Lean.Elab.Tactic.grind} {docstring Lean.Elab.Tactic.isCheckpointableTactic} {docstring Lean.Elab.Tactic.isHoleRHS} {docstring Lean.Elab.Tactic.liftMetaFinishingTactic} {docstring Lean.Elab.Tactic.liftMetaTactic} {docstring Lean.Elab.Tactic.liftMetaTactic1} {docstring Lean.Elab.Tactic.logUnassignedAndAbort} {docstring Lean.Elab.Tactic.mkInitialTacticInfo} {docstring Lean.Elab.Tactic.mkSimpCallStx} {docstring Lean.Elab.Tactic.mkSimpContext} {docstring Lean.Elab.Tactic.mkSimpOnly} {docstring Lean.Elab.Tactic.mkTacticInfo} {docstring Lean.Elab.Tactic.popMainGoal} {docstring Lean.Elab.Tactic.pushGoal} {docstring Lean.Elab.Tactic.pushGoals} {docstring Lean.Elab.Tactic.refineCore} {docstring Lean.Elab.Tactic.renameInaccessibles} {docstring Lean.Elab.Tactic.replaceMainGoal} {docstring Lean.Elab.Tactic.rewriteLocalDecl} {docstring Lean.Elab.Tactic.rewriteTarget} {docstring Lean.Elab.Tactic.saveState} {docstring Lean.Elab.Tactic.saveTacticInfoForToken} {docstring Lean.Elab.Tactic.simpLocation} {docstring Lean.Elab.Tactic.simpOnlyBuiltins} {docstring Lean.Elab.Tactic.tactic.customEliminators} {docstring Lean.Elab.Tactic.tacticToDischarge} {docstring Lean.Elab.Tactic.throwNoGoalsToBeSolved} {docstring Lean.Elab.Tactic.traceSimpCall} {docstring Lean.Elab.Tactic.tryCatchRestore} {docstring Lean.Elab.Tactic.unfoldLocalDecl} {docstring Lean.Elab.Tactic.unfoldTarget} {docstring Lean.Elab.Tactic.withCaseRef} {docstring Lean.Elab.Tactic.withCollectingNewGoalsFrom} {docstring Lean.Elab.Tactic.withMacroExpansion} {docstring Lean.Elab.Tactic.withMainContext} {docstring Lean.Elab.Tactic.withRWRulesSeq} {docstring Lean.Elab.Tactic.withRestoreOrSaveFull} {docstring Lean.Elab.Tactic.withSimpDiagnostics} {docstring Lean.Elab.Tactic.withTacticInfoContext} {docstring Lean.Elab.Tactic.withoutRecover} {docstring Lean.Elab.Tactic.zetaDeltaLocalDecl} {docstring Lean.Elab.Tactic.zetaDeltaTarget}
```exceptions Lean.Elab.Tactic.addCheckpoints Lean.Elab.Tactic.checkCommandConfigElab Lean.Elab.Tactic.checkConfigElab Lean.Elab.Tactic.classical Lean.Elab.Tactic.closeUsingOrAdmit Lean.Elab.Tactic.commandConfigElab Lean.Elab.Tactic.configElab Lean.Elab.Tactic.deltaLocalDecl Lean.Elab.Tactic.deltaTarget Lean.Elab.Tactic.done Lean.Elab.Tactic.dsimpLocation Lean.Elab.Tactic.elabAsFVar Lean.Elab.Tactic.elabChange Lean.Elab.Tactic.elabDecideConfig Lean.Elab.Tactic.elabGrindConfig Lean.Elab.Tactic.elabGrindPattern Lean.Elab.Tactic.elabRewriteConfig Lean.Elab.Tactic.elabSimpArgs.toZetaDeltaSet Lean.Elab.Tactic.elabSimpConfigCore Lean.Elab.Tactic.elabTermForApply Lean.Elab.Tactic.evalApplyRfl Lean.Elab.Tactic.evalClassical Lean.Elab.Tactic.evalDecideCore Lean.Elab.Tactic.evalDecideCore.diagnose Lean.Elab.Tactic.evalDecideCore.doElab Lean.Elab.Tactic.evalDecideCore.doKernel Lean.Elab.Tactic.expandLocation Lean.Elab.Tactic.expandOptLocation Lean.Elab.Tactic.filterOldMVars Lean.Elab.Tactic.focusAndDone Lean.Elab.Tactic.forEachVar Lean.Elab.Tactic.getInductiveValFromMajor Lean.Elab.Tactic.getMainDecl Lean.Elab.Tactic.getMainTarget Lean.Elab.Tactic.getNameOfIdent' Lean.Elab.Tactic.grind Lean.Elab.Tactic.isCheckpointableTactic Lean.Elab.Tactic.isHoleRHS Lean.Elab.Tactic.liftMetaFinishingTactic Lean.Elab.Tactic.liftMetaTactic Lean.Elab.Tactic.liftMetaTactic1 Lean.Elab.Tactic.logUnassignedAndAbort Lean.Elab.Tactic.mkInitialTacticInfo Lean.Elab.Tactic.mkSimpCallStx Lean.Elab.Tactic.mkSimpContext Lean.Elab.Tactic.mkSimpOnly Lean.Elab.Tactic.mkTacticInfo Lean.Elab.Tactic.popMainGoal Lean.Elab.Tactic.pushGoal Lean.Elab.Tactic.pushGoals Lean.Elab.Tactic.refineCore Lean.Elab.Tactic.renameInaccessibles Lean.Elab.Tactic.replaceMainGoal Lean.Elab.Tactic.rewriteLocalDecl Lean.Elab.Tactic.rewriteTarget Lean.Elab.Tactic.saveState Lean.Elab.Tactic.saveTacticInfoForToken Lean.Elab.Tactic.simpLocation Lean.Elab.Tactic.simpOnlyBuiltins Lean.Elab.Tactic.tactic.customEliminators Lean.Elab.Tactic.tacticToDischarge Lean.Elab.Tactic.throwNoGoalsToBeSolved Lean.Elab.Tactic.traceSimpCall Lean.Elab.Tactic.tryCatchRestore Lean.Elab.Tactic.unfoldLocalDecl Lean.Elab.Tactic.unfoldTarget Lean.Elab.Tactic.withCaseRef Lean.Elab.Tactic.withCollectingNewGoalsFrom Lean.Elab.Tactic.withMacroExpansion Lean.Elab.Tactic.withMainContext Lean.Elab.Tactic.withRWRulesSeq Lean.Elab.Tactic.withRestoreOrSaveFull Lean.Elab.Tactic.withSimpDiagnostics Lean.Elab.Tactic.withTacticInfoContext Lean.Elab.Tactic.withoutRecover Lean.Elab.Tactic.zetaDeltaLocalDecl Lean.Elab.Tactic.zetaDeltaTarget ```
List
List.all, List.allM, List.and, List.any, List.anyM, List.append, List.appendTR, List.asString, List.attach, List.attachWith, List.beq, List.concat, List.contains, List.count, List.countP, List.countP.go, List.drop, List.dropLast, List.dropLastTR, List.dropWhile, List.elem, List.enum, List.enumFrom, List.enumFromTR, List.enumLE, List.erase, List.eraseDups, List.eraseDups.loop, List.eraseIdx, List.eraseIdxTR, List.eraseIdxTR.go, List.eraseP, List.erasePTR, List.erasePTR.go, List.eraseReps, List.eraseReps.loop, List.eraseTR, List.eraseTR.go, List.filter, List.filterAuxM, List.filterM, List.filterMap, List.filterMapM, List.filterMapM.loop, List.filterMapTR, List.filterMapTR.go, List.filterRevM, List.filterTR, List.filterTR.loop, List.finRange, List.find?, List.findIdx, List.findIdx.go, List.findIdx?, List.findM?, List.findSome?, List.findSomeM?, List.firstM, List.flatMap, List.flatMapTR, List.flatMapTR.go, List.flatten, List.flattenTR, List.foldl, List.foldlM, List.foldlRecOn, List.foldr, List.foldrM, List.foldrRecOn, List.foldrTR, List.forA, List.forIn', List.forIn'.loop, List.forM, List.format, List.get, List.get!, List.get?, List.getD, List.getLast, List.getLast!, List.getLast?, List.getLastD, List.groupByKey, List.hasDecEq, List.head, List.head!, List.head?, List.headD, List.indexOf, List.indexOf?, List.insert, List.insertIdx, List.insertIdxTR, List.insertIdxTR.go, List.intercalate, List.intercalateTR, List.intercalateTR.go, List.intersperse, List.intersperseTR, List.iota, List.iotaTR, List.iotaTR.go, List.isEmpty, List.isEqv, List.isPerm, List.isPrefixOf, List.isPrefixOf?, List.isSublist, List.isSuffixOf, List.isSuffixOf?, List.le, List.leftpad, List.leftpadTR, List.length, List.lengthTR, List.lengthTRAux, List.lex, List.lookup, List.lt, List.map, List.mapA, List.mapFinIdx, List.mapFinIdx.go, List.mapIdx, List.mapIdx.go, List.mapM, List.mapM', List.mapM.loop, List.mapMono, List.mapMonoM, List.mapTR, List.mapTR.loop, List.max?, List.maxNatAbs, List.merge, List.mergeSort, List.min?, List.minNatAbs, List.modify, List.modifyHead, List.modifyTR, List.modifyTR.go, List.modifyTailIdx, List.nonzeroMinimum, List.ofFn, List.or, List.partition, List.partition.loop, List.partitionM, List.partitionM.go, List.partitionMap, List.partitionMap.go, List.pmap, List.range, List.range', List.range'TR, List.range'TR.go, List.range.loop, List.reduceOption, List.reduceReplicate, List.removeAll, List.replace, List.replaceTR, List.replaceTR.go, List.replicate, List.replicateTR, List.replicateTR.loop, List.repr, List.repr', List.reverse, List.reverseAux, List.rightpad, List.rotateLeft, List.rotateRight, List.set, List.setTR, List.setTR.go, List.singleton, List.span, List.span.loop, List.splitAt, List.splitAt.go, List.splitBy, List.splitBy.loop, List.sum, List.tail, List.tail!, List.tail?, List.tailD, List.take, List.takeTR, List.takeTR.go, List.takeWhile, List.takeWhileTR, List.takeWhileTR.go, List.toArray, List.toArrayAux, List.toArrayImpl, List.toAssocList', List.toByteArray, List.toByteArray.loop, List.toFloatArray, List.toFloatArray.loop, List.toPArray', List.toPArray'.loop, List.toSMap, List.toSSet, List.toString, List.unattach, List.unzip, List.unzipTR, List.zip, List.zipWith, List.zipWithAll, List.zipWithTR, List.zipWithTR.go, List.«term_<+:_», List.«term_<+_», List.«term_<:+:_», List.«term_<:+_», List.«term_~_»
{docstring List.all} {docstring List.allM} {docstring List.and} {docstring List.any} {docstring List.anyM} {docstring List.append} {docstring List.appendTR} {docstring List.asString} {docstring List.attach} {docstring List.attachWith} {docstring List.beq} {docstring List.concat} {docstring List.contains} {docstring List.count} {docstring List.countP} {docstring List.countP.go} {docstring List.drop} {docstring List.dropLast} {docstring List.dropLastTR} {docstring List.dropWhile} {docstring List.elem} {docstring List.enum} {docstring List.enumFrom} {docstring List.enumFromTR} {docstring List.enumLE} {docstring List.erase} {docstring List.eraseDups} {docstring List.eraseDups.loop} {docstring List.eraseIdx} {docstring List.eraseIdxTR} {docstring List.eraseIdxTR.go} {docstring List.eraseP} {docstring List.erasePTR} {docstring List.erasePTR.go} {docstring List.eraseReps} {docstring List.eraseReps.loop} {docstring List.eraseTR} {docstring List.eraseTR.go} {docstring List.filter} {docstring List.filterAuxM} {docstring List.filterM} {docstring List.filterMap} {docstring List.filterMapM} {docstring List.filterMapM.loop} {docstring List.filterMapTR} {docstring List.filterMapTR.go} {docstring List.filterRevM} {docstring List.filterTR} {docstring List.filterTR.loop} {docstring List.finRange} {docstring List.find?} {docstring List.findIdx} {docstring List.findIdx.go} {docstring List.findIdx?} {docstring List.findM?} {docstring List.findSome?} {docstring List.findSomeM?} {docstring List.firstM} {docstring List.flatMap} {docstring List.flatMapTR} {docstring List.flatMapTR.go} {docstring List.flatten} {docstring List.flattenTR} {docstring List.foldl} {docstring List.foldlM} {docstring List.foldlRecOn} {docstring List.foldr} {docstring List.foldrM} {docstring List.foldrRecOn} {docstring List.foldrTR} {docstring List.forA} {docstring List.forIn'} {docstring List.forIn'.loop} {docstring List.forM} {docstring List.format} {docstring List.get} {docstring List.get!} {docstring List.get?} {docstring List.getD} {docstring List.getLast} {docstring List.getLast!} {docstring List.getLast?} {docstring List.getLastD} {docstring List.groupByKey} {docstring List.hasDecEq} {docstring List.head} {docstring List.head!} {docstring List.head?} {docstring List.headD} {docstring List.indexOf} {docstring List.indexOf?} {docstring List.insert} {docstring List.insertIdx} {docstring List.insertIdxTR} {docstring List.insertIdxTR.go} {docstring List.intercalate} {docstring List.intercalateTR} {docstring List.intercalateTR.go} {docstring List.intersperse} {docstring List.intersperseTR} {docstring List.iota} {docstring List.iotaTR} {docstring List.iotaTR.go} {docstring List.isEmpty} {docstring List.isEqv} {docstring List.isPerm} {docstring List.isPrefixOf} {docstring List.isPrefixOf?} {docstring List.isSublist} {docstring List.isSuffixOf} {docstring List.isSuffixOf?} {docstring List.le} {docstring List.leftpad} {docstring List.leftpadTR} {docstring List.length} {docstring List.lengthTR} {docstring List.lengthTRAux} {docstring List.lex} {docstring List.lookup} {docstring List.lt} {docstring List.map} {docstring List.mapA} {docstring List.mapFinIdx} {docstring List.mapFinIdx.go} {docstring List.mapIdx} {docstring List.mapIdx.go} {docstring List.mapM} {docstring List.mapM'} {docstring List.mapM.loop} {docstring List.mapMono} {docstring List.mapMonoM} {docstring List.mapTR} {docstring List.mapTR.loop} {docstring List.max?} {docstring List.maxNatAbs} {docstring List.merge} {docstring List.mergeSort} {docstring List.min?} {docstring List.minNatAbs} {docstring List.modify} {docstring List.modifyHead} {docstring List.modifyTR} {docstring List.modifyTR.go} {docstring List.modifyTailIdx} {docstring List.nonzeroMinimum} {docstring List.ofFn} {docstring List.or} {docstring List.partition} {docstring List.partition.loop} {docstring List.partitionM} {docstring List.partitionM.go} {docstring List.partitionMap} {docstring List.partitionMap.go} {docstring List.pmap} {docstring List.range} {docstring List.range'} {docstring List.range'TR} {docstring List.range'TR.go} {docstring List.range.loop} {docstring List.reduceOption} {docstring List.reduceReplicate} {docstring List.removeAll} {docstring List.replace} {docstring List.replaceTR} {docstring List.replaceTR.go} {docstring List.replicate} {docstring List.replicateTR} {docstring List.replicateTR.loop} {docstring List.repr} {docstring List.repr'} {docstring List.reverse} {docstring List.reverseAux} {docstring List.rightpad} {docstring List.rotateLeft} {docstring List.rotateRight} {docstring List.set} {docstring List.setTR} {docstring List.setTR.go} {docstring List.singleton} {docstring List.span} {docstring List.span.loop} {docstring List.splitAt} {docstring List.splitAt.go} {docstring List.splitBy} {docstring List.splitBy.loop} {docstring List.sum} {docstring List.tail} {docstring List.tail!} {docstring List.tail?} {docstring List.tailD} {docstring List.take} {docstring List.takeTR} {docstring List.takeTR.go} {docstring List.takeWhile} {docstring List.takeWhileTR} {docstring List.takeWhileTR.go} {docstring List.toArray} {docstring List.toArrayAux} {docstring List.toArrayImpl} {docstring List.toAssocList'} {docstring List.toByteArray} {docstring List.toByteArray.loop} {docstring List.toFloatArray} {docstring List.toFloatArray.loop} {docstring List.toPArray'} {docstring List.toPArray'.loop} {docstring List.toSMap} {docstring List.toSSet} {docstring List.toString} {docstring List.unattach} {docstring List.unzip} {docstring List.unzipTR} {docstring List.zip} {docstring List.zipWith} {docstring List.zipWithAll} {docstring List.zipWithTR} {docstring List.zipWithTR.go} {docstring List.«term_<+:_»} {docstring List.«term_<+_»} {docstring List.«term_<:+:_»} {docstring List.«term_<:+_»} {docstring List.«term_~_»}
```exceptions List.all List.allM List.and List.any List.anyM List.append List.appendTR List.asString List.attach List.attachWith List.beq List.concat List.contains List.count List.countP List.countP.go List.drop List.dropLast List.dropLastTR List.dropWhile List.elem List.enum List.enumFrom List.enumFromTR List.enumLE List.erase List.eraseDups List.eraseDups.loop List.eraseIdx List.eraseIdxTR List.eraseIdxTR.go List.eraseP List.erasePTR List.erasePTR.go List.eraseReps List.eraseReps.loop List.eraseTR List.eraseTR.go List.filter List.filterAuxM List.filterM List.filterMap List.filterMapM List.filterMapM.loop List.filterMapTR List.filterMapTR.go List.filterRevM List.filterTR List.filterTR.loop List.finRange List.find? List.findIdx List.findIdx.go List.findIdx? List.findM? List.findSome? List.findSomeM? List.firstM List.flatMap List.flatMapTR List.flatMapTR.go List.flatten List.flattenTR List.foldl List.foldlM List.foldlRecOn List.foldr List.foldrM List.foldrRecOn List.foldrTR List.forA List.forIn' List.forIn'.loop List.forM List.format List.get List.get! List.get? List.getD List.getLast List.getLast! List.getLast? List.getLastD List.groupByKey List.hasDecEq List.head List.head! List.head? List.headD List.indexOf List.indexOf? List.insert List.insertIdx List.insertIdxTR List.insertIdxTR.go List.intercalate List.intercalateTR List.intercalateTR.go List.intersperse List.intersperseTR List.iota List.iotaTR List.iotaTR.go List.isEmpty List.isEqv List.isPerm List.isPrefixOf List.isPrefixOf? List.isSublist List.isSuffixOf List.isSuffixOf? List.le List.leftpad List.leftpadTR List.length List.lengthTR List.lengthTRAux List.lex List.lookup List.lt List.map List.mapA List.mapFinIdx List.mapFinIdx.go List.mapIdx List.mapIdx.go List.mapM List.mapM' List.mapM.loop List.mapMono List.mapMonoM List.mapTR List.mapTR.loop List.max? List.maxNatAbs List.merge List.mergeSort List.min? List.minNatAbs List.modify List.modifyHead List.modifyTR List.modifyTR.go List.modifyTailIdx List.nonzeroMinimum List.ofFn List.or List.partition List.partition.loop List.partitionM List.partitionM.go List.partitionMap List.partitionMap.go List.pmap List.range List.range' List.range'TR List.range'TR.go List.range.loop List.reduceOption List.reduceReplicate List.removeAll List.replace List.replaceTR List.replaceTR.go List.replicate List.replicateTR List.replicateTR.loop List.repr List.repr' List.reverse List.reverseAux List.rightpad List.rotateLeft List.rotateRight List.set List.setTR List.setTR.go List.singleton List.span List.span.loop List.splitAt List.splitAt.go List.splitBy List.splitBy.loop List.sum List.tail List.tail! List.tail? List.tailD List.take List.takeTR List.takeTR.go List.takeWhile List.takeWhileTR List.takeWhileTR.go List.toArray List.toArrayAux List.toArrayImpl List.toAssocList' List.toByteArray List.toByteArray.loop List.toFloatArray List.toFloatArray.loop List.toPArray' List.toPArray'.loop List.toSMap List.toSSet List.toString List.unattach List.unzip List.unzipTR List.zip List.zipWith List.zipWithAll List.zipWithTR List.zipWithTR.go List.«term_<+:_» List.«term_<+_» List.«term_<:+:_» List.«term_<:+_» List.«term_~_» ```
MProd
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
Monad
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
MonadControl
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
MonadControlT
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
MonadExcept
```exceptions ```
MonadExceptOf
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
MonadFunctor
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
MonadFunctorT
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
MonadLift
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
MonadLiftT
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
MonadReader
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
MonadReaderOf
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
MonadState
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
MonadStateOf
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
Nat
Nat.caseStrongRecOn, Nat.reduceAnd, Nat.reduceOr, Nat.reduceShiftLeft, Nat.reduceShiftRight, Nat.reduceXor, Nat.strongRecOn, Nat.toFloat32, Nat.toISize, Nat.toInt16, Nat.toInt32, Nat.toInt64, Nat.toInt8
{docstring Nat.caseStrongRecOn} {docstring Nat.reduceAnd} {docstring Nat.reduceOr} {docstring Nat.reduceShiftLeft} {docstring Nat.reduceShiftRight} {docstring Nat.reduceXor} {docstring Nat.strongRecOn} {docstring Nat.toFloat32} {docstring Nat.toISize} {docstring Nat.toInt16} {docstring Nat.toInt32} {docstring Nat.toInt64} {docstring Nat.toInt8}
```exceptions Nat.caseStrongRecOn Nat.reduceAnd Nat.reduceOr Nat.reduceShiftLeft Nat.reduceShiftRight Nat.reduceXor Nat.strongRecOn Nat.toFloat32 Nat.toISize Nat.toInt16 Nat.toInt32 Nat.toInt64 Nat.toInt8 ```
Option
```exceptions ```
OptionT
```exceptions ```
Ord
Ord.arrayOrd, Ord.lex, Ord.lex', Ord.on, Ord.opposite, Ord.toBEq, Ord.toLE, Ord.toLT
{docstring Ord.arrayOrd} {docstring Ord.lex} {docstring Ord.lex'} {docstring Ord.on} {docstring Ord.opposite} {docstring Ord.toBEq} {docstring Ord.toLE} {docstring Ord.toLT}
```exceptions Ord.arrayOrd Ord.lex Ord.lex' Ord.on Ord.opposite Ord.toBEq Ord.toLE Ord.toLT ```
Ordering
Ordering.isEq, Ordering.isGE, Ordering.isGT, Ordering.isLE, Ordering.isLT, Ordering.isNe, Ordering.ofNat, Ordering.swap, Ordering.then, Ordering.toCtorIdx
{docstring Ordering.isEq} {docstring Ordering.isGE} {docstring Ordering.isGT} {docstring Ordering.isLE} {docstring Ordering.isLT} {docstring Ordering.isNe} {docstring Ordering.ofNat} {docstring Ordering.swap} {docstring Ordering.then} {docstring Ordering.toCtorIdx}
```exceptions Ordering.isEq Ordering.isGE Ordering.isGT Ordering.isLE Ordering.isLT Ordering.isNe Ordering.ofNat Ordering.swap Ordering.then Ordering.toCtorIdx ```
PEmpty
```exceptions ```
PLift
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
PProd
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
PSum
PSum.inhabitedLeft, PSum.inhabitedRight
{docstring PSum.inhabitedLeft} {docstring PSum.inhabitedRight}
```exceptions PSum.inhabitedLeft PSum.inhabitedRight ```
PUnit
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
Prod
Prod.allI, Prod.anyI, Prod.foldI, Prod.lex, Prod.lexLt, Prod.map, Prod.repr, Prod.rprod, Prod.swap
{docstring Prod.allI} {docstring Prod.anyI} {docstring Prod.foldI} {docstring Prod.lex} {docstring Prod.lexLt} {docstring Prod.map} {docstring Prod.repr} {docstring Prod.rprod} {docstring Prod.swap}
```exceptions Prod.allI Prod.anyI Prod.foldI Prod.lex Prod.lexLt Prod.map Prod.repr Prod.rprod Prod.swap ```
Pure
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
Quot
Quot.hrecOn, Quot.indep, Quot.lcInv, Quot.lift, Quot.liftOn, Quot.mk, Quot.rec, Quot.recOn, Quot.recOnSubsingleton, Quot.sound
{docstring Quot.hrecOn} {docstring Quot.indep} {docstring Quot.lcInv} {docstring Quot.lift} {docstring Quot.liftOn} {docstring Quot.mk} {docstring Quot.rec} {docstring Quot.recOn} {docstring Quot.recOnSubsingleton} {docstring Quot.sound}
```exceptions Quot.hrecOn Quot.indep Quot.lcInv Quot.lift Quot.liftOn Quot.mk Quot.rec Quot.recOn Quot.recOnSubsingleton Quot.sound ```
Quotient
Quotient.hrecOn, Quotient.lift, Quotient.liftOn, Quotient.liftOn₂, Quotient.lift₂, Quotient.mk, Quotient.mk', Quotient.rec, Quotient.recOn, Quotient.recOnSubsingleton, Quotient.recOnSubsingleton₂
{docstring Quotient.hrecOn} {docstring Quotient.lift} {docstring Quotient.liftOn} {docstring Quotient.liftOn₂} {docstring Quotient.lift₂} {docstring Quotient.mk} {docstring Quotient.mk'} {docstring Quotient.rec} {docstring Quotient.recOn} {docstring Quotient.recOnSubsingleton} {docstring Quotient.recOnSubsingleton₂}
```exceptions Quotient.hrecOn Quotient.lift Quotient.liftOn Quotient.liftOn₂ Quotient.lift₂ Quotient.mk Quotient.mk' Quotient.rec Quotient.recOn Quotient.recOnSubsingleton Quotient.recOnSubsingleton₂ ```
ReaderM
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
ReaderT
```exceptions ```
ST
```exceptions ```
ST.Ref
```exceptions ```
Seq
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
SeqLeft
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
SeqRight
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
Setoid
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
Sigma
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
Squash
Squash.lift, Squash.mk
{docstring Squash.lift} {docstring Squash.mk}
```exceptions Squash.lift Squash.mk ```
StateCpsT
```exceptions ```
StateM
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
StateRefT'
```exceptions ```
StateT
```exceptions ```
String
String.dropPrefix?, String.dropSuffix?, String.stripPrefix, String.stripSuffix
{docstring String.dropPrefix?} {docstring String.dropSuffix?} {docstring String.stripPrefix} {docstring String.stripSuffix}
```exceptions String.dropPrefix? String.dropSuffix? String.stripPrefix String.stripSuffix ```
Subarray
```exceptions ```
Subsingleton
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
Subtype
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
Sum
Sum.elim, Sum.getLeft, Sum.getLeft?, Sum.getRight, Sum.getRight?, Sum.inhabitedLeft, Sum.inhabitedRight, Sum.isLeft, Sum.isRight, Sum.map, Sum.repr, Sum.swap
{docstring Sum.elim} {docstring Sum.getLeft} {docstring Sum.getLeft?} {docstring Sum.getRight} {docstring Sum.getRight?} {docstring Sum.inhabitedLeft} {docstring Sum.inhabitedRight} {docstring Sum.isLeft} {docstring Sum.isRight} {docstring Sum.map} {docstring Sum.repr} {docstring Sum.swap}
```exceptions Sum.elim Sum.getLeft Sum.getLeft? Sum.getRight Sum.getRight? Sum.inhabitedLeft Sum.inhabitedRight Sum.isLeft Sum.isRight Sum.map Sum.repr Sum.swap ```
System
```exceptions ```
System.FilePath
```exceptions ```
System.Platform
System.Platform.getIsEmscripten, System.Platform.getIsOSX, System.Platform.getIsWindows, System.Platform.getNumBits, System.Platform.getTarget, System.Platform.isEmscripten, System.Platform.isOSX, System.Platform.isWindows, System.Platform.numBits, System.Platform.target
{docstring System.Platform.getIsEmscripten} {docstring System.Platform.getIsOSX} {docstring System.Platform.getIsWindows} {docstring System.Platform.getNumBits} {docstring System.Platform.getTarget} {docstring System.Platform.isEmscripten} {docstring System.Platform.isOSX} {docstring System.Platform.isWindows} {docstring System.Platform.numBits} {docstring System.Platform.target}
```exceptions System.Platform.getIsEmscripten System.Platform.getIsOSX System.Platform.getIsWindows System.Platform.getNumBits System.Platform.getTarget System.Platform.isEmscripten System.Platform.isOSX System.Platform.isWindows System.Platform.numBits System.Platform.target ```
Task
Task.bind, Task.map
{docstring Task.bind} {docstring Task.map}
```exceptions Task.bind Task.map ```
Task.Priority
```exceptions ```
Thunk
Thunk.bind, Thunk.get, Thunk.map, Thunk.pure
{docstring Thunk.bind} {docstring Thunk.get} {docstring Thunk.map} {docstring Thunk.pure}
```exceptions Thunk.bind Thunk.get Thunk.map Thunk.pure ```
UInt16
```exceptions ```
UInt32
```exceptions ```
UInt64
```exceptions ```
UInt8
```exceptions ```
ULift
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
USize
```exceptions ```
Unit
```exceptions ```
WellFoundedRelation
[anonymous]
{docstring [anonymous]}
```exceptions [anonymous] ```
_root_
And, AndOp, AndThen, BitVec, ByteArray, Coe, CoeDep, CoeFun, CoeHTC, CoeHTCT, CoeHead, CoeOTC, CoeOut, CoeSort, CoeT, CoeTC, CoeTail, Complement, DecidableLE, DecidableLT, DecidablePred, DoResultBC, DoResultPR, DoResultPRBC, DoResultSBC, EmptyCollection, Eq, EquivBEq, Equivalence, Exists, False, Float, Float32, FloatArray, FloatSpec, HAndThen, HEq, HOrElse, HasEquiv, HasSSubset, HasSubset, Iff, Insert, Inter, InvImage, LawfulHashable, LawfulSingleton, Max, Membership, Min, MonadEval, MonadEvalT, MonadShareCommon, Ne, NonScalar, NonemptyType, Not, Or, OrElse, OrOp, PNonScalar, PartialEquivBEq, Quot, Quotient, ReflBEq, ReprAtom, ReprTuple, SDiff, SSuperset, Sep, Setoid, ShareCommonM, ShareCommonT, Singleton, Squash, Stream, Subrelation, Subsingleton, Substring, Superset, Thunk, ToBool, ToStream, Trans, True, Union, Vector, Xor, absurd, acc_transGen_iff, addParenHeuristic, allocprof, and_and_and_comm, and_and_left, and_and_right, and_assoc, and_comm, and_congr, and_congr_left, and_congr_left', and_congr_left_eq, and_congr_left_iff, and_congr_right, and_congr_right', and_congr_right_eq, and_congr_right_iff, and_exists_self, and_false, and_iff_left, and_iff_left_iff_imp, and_iff_left_of_imp, and_iff_right, and_iff_right_iff_imp, and_iff_right_of_imp, and_imp, and_left_comm, and_not_self, and_not_self_iff, and_or_left, and_or_right, and_right_comm, and_rotate, and_self, and_self_iff, and_self_left, and_self_right, and_true, apply_dite, apply_ite, beq_eq_false_iff_ne, beq_false, beq_false_of_ne, beq_iff_eq, beq_of_eq, beq_self_eq_true, beq_self_eq_true', beq_true, bind_congr, bind_map_left, bind_pure, bind_pure_unit, bne, bne_comm, bne_eq_false_iff_eq, bne_iff_ne, bne_self_eq_false, bne_self_eq_false', bool, boolIfThenElse, boolPredToPred, boolRelToRel, boolToProp, boolToPropSimps, boolToSort, cast, cast_cast, cast_eq, cast_heq, coeFunNotation, coeNotation, coeSortNotation, commandDeclare_bitwise_uint_theorems__, commandDeclare_uint_simprocs_, commandDeclare_uint_theorems__, compareLex, compareOfLessAndBEq, compareOfLessAndEq, compareOn, cond_false, cond_true, congr, congrArg, congrFun, dbgSleep, dbgStackTrace, dbgTrace, dbgTraceIfShared, dbgTraceVal, decEq, decPropToBool, decidableGetElem?, decidable_of_bool, decidable_of_decidable_of_eq, decidable_of_decidable_of_iff, decidable_of_iff, decidable_of_iff', decide_eq_decide, decide_eq_false, decide_eq_false_iff_not, decide_eq_true, decide_eq_true_eq, decide_eq_true_iff, decide_false, decide_implies, decide_ite, decide_not, decide_true, dif_eq_if, dif_neg, dif_pos, dite, dite_cond_eq_false, dite_cond_eq_true, dite_congr, dite_else_false, dite_else_true, dite_eq_ite, dite_eq_left_iff, dite_eq_right_iff, dite_false, dite_iff_left_iff, dite_iff_right_iff, dite_not, dite_then_false, dite_then_true, dite_true, dreduceDIte, dreduceIte, emptyRelation, emptyWf, eqRec_heq, eq_comm, eq_false, eq_false', eq_false_of_decide, eq_false_of_ne_true, eq_iff_iff, eq_iff_true_of_subsingleton, eq_mp_eq_cast, eq_mpr_eq_cast, eq_of_heq, eq_self, eq_self_iff_true, eq_true, eq_true_eq_id, eq_true_of_decide, eq_true_of_ne_false, exists_and_left, exists_and_right, exists_and_self, exists_apply_eq_apply, exists_comm, exists_congr, exists_const, exists_eq, exists_eq', exists_eq_left, exists_eq_left', exists_eq_or_imp, exists_eq_right, exists_eq_right', exists_eq_right_right, exists_eq_right_right', exists_false, exists_idem, exists_imp, exists_or, exists_or_eq_left, exists_or_eq_left', exists_or_eq_right, exists_or_eq_right', exists_prop, exists_prop', exists_prop_congr, exists_prop_decidable, exists_prop_of_true, exists_true_left, exists₂_congr, exists₂_imp, exists₃_congr, exists₄_congr, exists₅_congr, false_and, false_eq_decide_iff, false_iff, false_iff_true, false_imp_iff, false_implies, false_ne_true, false_of_ne, false_of_true_eq_false, false_of_true_iff_false, false_or, flip, float32DecLe, float32DecLt, float32Spec, floatDecLe, floatDecLt, floatSpec, forIn'_eq_forIn, forall_and, forall_apply_eq_imp_iff, forall_apply_eq_imp_iff₂, forall_comm, forall_congr, forall_congr', forall_const, forall_eq, forall_eq', forall_eq_apply_imp_iff, forall_eq_or_imp, forall_exists_index, forall_false, forall_imp, forall_not_of_not_exists, forall_prop_congr_dom, forall_prop_decidable, forall_prop_domain_congr, forall_prop_of_false, forall_prop_of_true, forall_self_imp, forall₂_congr, forall₃_congr, forall₄_congr, forall₅_congr, funext_iff, ge_iff_le, getElem!_neg, getElem!_pos, getElem?_eq_none, getElem?_neg, getElem?_pos, getElem_congr, getElem_congr_coll, getElem_congr_idx, get_getElem?, gt_iff_lt, hash64, hash_eq, heq_comm, heq_eq_eq, heq_of_eq, heq_of_eqRec_eq, heq_of_eq_of_heq, heq_of_heq_of_eq, heq_self_iff_true, hexDigitRepr, id, id_def, id_eq, id_map', if_false, if_false_left, if_false_right, if_neg, if_pos, if_true, if_true_left, if_true_right, iff_and_self, iff_comm, iff_congr, iff_def, iff_def', iff_false, iff_false_intro, iff_false_left, iff_false_right, iff_iff_eq, iff_iff_implies_and_implies, iff_not_self, iff_of_eq, iff_of_false, iff_of_true, iff_or_self, iff_self, iff_self_and, iff_self_or, iff_true, iff_true_intro, iff_true_left, iff_true_right, imp_and, imp_congr, imp_congr_ctx, imp_congr_left, imp_congr_right, imp_false, imp_iff_not, imp_iff_right, imp_imp_imp, imp_intro, imp_not_comm, imp_not_self, imp_self, imp_true_iff, implies_congr, implies_congr_ctx, implies_dep_congr_ctx, implies_true, inline, instAddFloat, instAddFloat32, instAddISize, instAddInt16, instAddInt32, instAddInt64, instAddInt8, instAddNat, instAddUInt16, instAddUInt32, instAddUInt64, instAddUInt8, instAddUSize, instAlternativeOption, instAndOpISize, instAndOpInt16, instAndOpInt32, instAndOpInt64, instAndOpInt8, instAndOpUInt16, instAndOpUInt32, instAndOpUInt64, instAndOpUInt8, instAndOpUSize, instAppendSubarray, instAssociativeAnd, instAssociativeBoolAnd, instAssociativeBoolOr, instAssociativeOr, instBEqFloat, instBEqFloat32, instBEqOfDecidableEq, instBEqOrdering, instBEqProd, instCoeHTC, instCoeHTCOfCoeHeadOfCoeOTC, instCoeHTCOfCoeOTC, instCoeHTCT, instCoeHTCTIntOfIntCast, instCoeHTCTNatOfNatCast, instCoeHTCTOfCoeHTC, instCoeHTCTOfCoeTailOfCoeHTC, instCoeOTC, instCoeOTCOfCoeOut, instCoeOTCOfCoeTC, instCoeOutOfCoeFun, instCoeOutOfCoeSort, instCoeStringError, instCoeT, instCoeTC, instCoeTCOfCoe, instCoeTCOfCoe_1, instCoeTOfCoeDep, instCoeTOfCoeHTCT, instCoeTailIntOfIntCast, instCoeTailNatOfNatCast, instComplementISize, instComplementInt16, instComplementInt32, instComplementInt64, instComplementInt8, instComplementUInt16, instComplementUInt32, instComplementUInt64, instComplementUInt8, instComplementUSize, instDecidableAnd, instDecidableDite, instDecidableEqBitVec, instDecidableEqBool, instDecidableEqChar, instDecidableEqEmpty, instDecidableEqFin, instDecidableEqISize, instDecidableEqInt16, instDecidableEqInt32, instDecidableEqInt64, instDecidableEqInt8, instDecidableEqList, instDecidableEqNat, instDecidableEqOfIff, instDecidableEqPEmpty, instDecidableEqPLift, instDecidableEqPUnit, instDecidableEqPos, instDecidableEqProd, instDecidableEqString, instDecidableEqSum, instDecidableEqUInt16, instDecidableEqUInt32, instDecidableEqUInt64, instDecidableEqUInt8, instDecidableEqULift, instDecidableEqUSize, instDecidableEqVector, instDecidableFalse, instDecidableForall, instDecidableIff, instDecidableIte, instDecidableLeBitVec, instDecidableLeISize, instDecidableLeInt16, instDecidableLeInt32, instDecidableLeInt64, instDecidableLeInt8, instDecidableLePos, instDecidableLeUInt16, instDecidableLeUInt32, instDecidableLeUInt64, instDecidableLeUInt8, instDecidableLeUSize, instDecidableLtBitVec, instDecidableLtISize, instDecidableLtInt16, instDecidableLtInt32, instDecidableLtInt64, instDecidableLtInt8, instDecidableLtPos, instDecidableLtUInt16, instDecidableLtUInt32, instDecidableLtUInt64, instDecidableLtUInt8, instDecidableLtUSize, instDecidableNot, instDecidableOr, instDecidablePredComp, instDecidableRelLe, instDecidableRelLt, instDecidableTrue, instDivFloat, instDivFloat32, instDivISize, instDivInt16, instDivInt32, instDivInt64, instDivInt8, instDivUInt16, instDivUInt32, instDivUInt64, instDivUInt8, instDivUSize, instEquivBEqOfLawfulBEq, instForInOfForIn', instForInOfStream, instFunctorOption, instGetElem?OfGetElemOfDecidable, instHAdd, instHAddPos, instHAddPosChar, instHAddPosString, instHAndOfAndOp, instHAndThenOfAndThen, instHAppendOfAppend, instHDiv, instHMod, instHModUInt16Nat, instHModUInt32Nat, instHModUInt64Nat, instHModUInt8Nat, instHModUSizeNat, instHMul, instHOrElseOfOrElse, instHOrOfOrOp, instHPow, instHShiftLeftOfShiftLeft, instHShiftRightOfShiftRight, instHSub, instHSubPos, instHXorOfXor, instHasEquivOfSetoid, instHashable, instHashableArray, instHashableBool, instHashableByteArray, instHashableChar, instHashableFin, instHashableInt, instHashableList, instHashableNat, instHashableOption, instHashablePos, instHashableProd, instHashableString, instHashableSubtype, instHashableUInt16, instHashableUInt32, instHashableUInt64, instHashableUInt8, instHashableUSize, instHomogeneousPowFloat, instHomogeneousPowFloat32, instIdempotentOpAnd, instIdempotentOpBoolAnd, instIdempotentOpBoolOr, instIdempotentOpOr, instInhabitedBool, instInhabitedEIO, instInhabitedEST, instInhabitedExcept, instInhabitedExceptTOfMonad, instInhabitedFloat, instInhabitedFloat32, instInhabitedForInStep, instInhabitedForInStep_1, instInhabitedForall, instInhabitedForallOfMonad, instInhabitedISize, instInhabitedInt16, instInhabitedInt32, instInhabitedInt64, instInhabitedInt8, instInhabitedList, instInhabitedMProd, instInhabitedNat, instInhabitedNonScalar, instInhabitedNonemptyType, instInhabitedOfMonad, instInhabitedOption, instInhabitedOrdering, instInhabitedPNonScalar, instInhabitedPProd, instInhabitedPUnit, instInhabitedPos, instInhabitedProd, instInhabitedProp, instInhabitedReaderT, instInhabitedSort, instInhabitedStdGen, instInhabitedSubstring, instInhabitedTask, instInhabitedTrue, instInhabitedUInt16, instInhabitedUInt32, instInhabitedUInt64, instInhabitedUInt8, instInhabitedUSize, instIntCastInt, instLEBitVec, instLEFin, instLEFloat, instLEFloat32, instLEISize, instLEInt16, instLEInt32, instLEInt64, instLEInt8, instLENat, instLEPos, instLEUInt16, instLEUInt32, instLEUInt64, instLEUInt8, instLEUSize, instLTBitVec, instLTFin, instLTFloat, instLTFloat32, instLTISize, instLTInt16, instLTInt32, instLTInt64, instLTInt8, instLTNat, instLTOption, instLTPos, instLTUInt16, instLTUInt32, instLTUInt64, instLTUInt8, instLTUSize, instLawfulApplicativeExcept, instLawfulApplicativeOption, instLawfulBEq, instLawfulBEqBool, instLawfulBEqChar, instLawfulBEqString, instLawfulFunctorExcept, instLawfulFunctorOption, instLawfulGetElem, instLawfulHashableOfLawfulBEq, instLawfulIdentityAndTrue, instLawfulIdentityBoolAndTrue, instLawfulIdentityBoolOrFalse, instLawfulIdentityOrFalse, instLawfulMonadEStateM, instLawfulMonadExcept, instLawfulMonadOption, instLawfulMonadStateRefT', instMaxFloat, instMaxFloat32, instMaxISize, instMaxInt16, instMaxInt32, instMaxInt64, instMaxInt8, instMaxUInt16, instMaxUInt32, instMaxUInt64, instMaxUInt8, instMaxUSize, instMinFloat, instMinFloat32, instMinISize, instMinInt16, instMinInt32, instMinInt64, instMinInt8, instMinNat, instMinUInt16, instMinUInt32, instMinUInt64, instMinUInt8, instMinUSize, instModISize, instModInt16, instModInt32, instModInt64, instModInt8, instModUInt16, instModUInt32, instModUInt64, instModUInt8, instModUSize, instMonadBaseIO, instMonadControlExceptTOfMonad, instMonadControlOptionTOfMonad, instMonadControlReaderT, instMonadControlStateRefT', instMonadControlTOfMonadControl, instMonadControlTOfPure, instMonadEIO, instMonadEST, instMonadEvalOfMonadLift, instMonadEvalT, instMonadEvalTOfMonadEval, instMonadExceptOfEIO, instMonadExceptOfEST, instMonadExceptOfExcept, instMonadExceptOfExceptT, instMonadExceptOfExceptTOfMonad, instMonadExceptOfMonadExceptOf, instMonadExceptOfUnitOption, instMonadFinallyBaseIO, instMonadFinallyEIO, instMonadFinallyStateRefT', instMonadFunctorTOfMonadFunctor, instMonadLiftBaseIOEIO, instMonadLiftSTEST, instMonadLiftT, instMonadLiftTOfMonadLift, instMonadOption, instMonadReaderOfMonadReaderOf, instMonadReaderOfOfMonadLift, instMonadReaderOfReaderTOfMonad, instMonadST, instMonadStateOfMonadStateOf, instMonadStateOfOfMonadLift, instMonadStateOfStateTOfMonad, instMonadWithReaderOfMonadWithReaderOf, instMonadWithReaderOfOfMonadFunctor, instMonadWithReaderOfReaderT, instMulFloat, instMulFloat32, instMulISize, instMulInt16, instMulInt32, instMulInt64, instMulInt8, instMulNat, instMulUInt16, instMulUInt32, instMulUInt64, instMulUInt8, instMulUSize, instNatCastInt, instNatCastNat, instNatPowNat, instNeZeroNatIte, instNegFloat, instNegFloat32, instNegISize, instNegInt16, instNegInt32, instNegInt64, instNegInt8, instNonemptyDynamic, instNonemptyFloat, instNonemptyFloat32, instNonemptyForall, instNonemptyMProd, instNonemptyOfInhabited, instNonemptyOfMonad, instNonemptyPProd, instNonemptyProd, instNonemptyTask, instNonemptyTypeName, instOfNat, instOfNatFloat, instOfNatFloat32, instOfNatISize, instOfNatInt16, instOfNatInt32, instOfNatInt64, instOfNatInt8, instOfNatNat, instOfScientificFloat, instOfScientificFloat32, instOrElseEIO, instOrElseOfAlternative, instOrOpISize, instOrOpInt16, instOrOpInt32, instOrOpInt64, instOrOpInt8, instOrOpUInt16, instOrOpUInt32, instOrOpUInt64, instOrOpUInt8, instOrOpUSize, instOrdBool, instOrdChar, instOrdFin, instOrdInt, instOrdNat, instOrdOption, instOrdString, instOrdUInt16, instOrdUInt32, instOrdUInt64, instOrdUInt8, instOrdUSize, instPowNat, instPowOfHomogeneousPow, instRandomGenStdGen, instReprAtomBool, instReprAtomChar, instReprAtomFloat, instReprAtomFloat32, instReprAtomInt, instReprAtomNat, instReprAtomString, instReprAtomUInt16, instReprAtomUInt32, instReprAtomUInt64, instReprAtomUInt8, instReprAtomUSize, instReprBool, instReprChar, instReprDecidable, instReprEmpty, instReprExcept, instReprFin, instReprFloat, instReprFloat32, instReprId, instReprId_1, instReprInt, instReprIterator, instReprList, instReprListOfReprAtom, instReprNat, instReprOption, instReprPUnit, instReprPos, instReprProdOfReprTuple, instReprSSet, instReprSigma, instReprSourceInfo, instReprStdGen, instReprString, instReprSubarray, instReprSubstring, instReprSubtype, instReprSum, instReprTupleOfRepr, instReprTupleProdOfRepr, instReprUInt16, instReprUInt32, instReprUInt64, instReprUInt8, instReprULift, instReprUSize, instReprUnit, instReprVector, instSTWorldEST, instSTWorldOfMonadLift, instShiftLeftISize, instShiftLeftInt16, instShiftLeftInt32, instShiftLeftInt64, instShiftLeftInt8, instShiftLeftUInt16, instShiftLeftUInt32, instShiftLeftUInt64, instShiftLeftUInt8, instShiftLeftUSize, instShiftRightISize, instShiftRightInt16, instShiftRightInt32, instShiftRightInt64, instShiftRightInt8, instShiftRightUInt16, instShiftRightUInt32, instShiftRightUInt64, instShiftRightUInt8, instShiftRightUSize, instSizeOfDefault, instSizeOfForallUnit, instSizeOfNat, instStreamList, instStreamProd, instStreamRangeNat, instStreamSubarray, instStreamSubstringChar, instSubFloat, instSubFloat32, instSubISize, instSubInt16, instSubInt32, instSubInt64, instSubInt8, instSubNat, instSubUInt16, instSubUInt32, instSubUInt64, instSubUInt8, instSubUSize, instSubsingleton, instSubsingletonDecidable, instSubsingletonEmpty, instSubsingletonPEmpty, instSubsingletonPLift, instSubsingletonPUnit, instSubsingletonProd, instSubsingletonSquash, instSubsingletonStateM, instSubsingletonULift, instToBoolBool, instToBoolOption, instToFormatArray, instToFormatList, instToFormatOfToString, instToFormatOption, instToFormatPos, instToFormatProd, instToStreamArraySubarray, instToStreamList, instToStreamRange, instToStreamStringSubstring, instToStreamSubarray, instToStringBool, instToStringByteArray, instToStringChar, instToStringDecidable, instToStringExcept, instToStringFin, instToStringFloat, instToStringFloat32, instToStringFloatArray, instToStringFormat, instToStringISize, instToStringId, instToStringId_1, instToStringInt, instToStringInt16, instToStringInt32, instToStringInt64, instToStringInt8, instToStringIterator, instToStringList, instToStringNat, instToStringOption, instToStringPUnit, instToStringPos, instToStringProd, instToStringSigma, instToStringString, instToStringSubarray, instToStringSubstring, instToStringSubtype, instToStringSum, instToStringUInt16, instToStringUInt32, instToStringUInt64, instToStringUInt8, instToStringULift, instToStringUSize, instToStringUnit, instTransEq, instTransEq_1, instTransIff, instWellFoundedRelationOfSizeOf, instXorISize, instXorInt16, instXorInt32, instXorInt64, instXorInt8, instXorUInt16, instXorUInt32, instXorUInt64, instXorUInt8, instXorUSize, isExclusiveUnsafe, isSome_getElem?, isValidChar, ite, iteInduction, ite_cond_eq_false, ite_cond_eq_true, ite_congr, ite_else_decide_not_self, ite_else_decide_self, ite_else_not_self, ite_else_self, ite_eq_ite, ite_eq_left_iff, ite_eq_right_iff, ite_false, ite_id, ite_iff_ite, ite_iff_left_iff, ite_iff_right_iff, ite_not, ite_self, ite_then_decide_not_self, ite_then_decide_self, ite_then_not_self, ite_then_self, ite_true, lcCast, lcErased, lcProof, lcUnreachable, leOfOrd, le_of_eq_of_le, le_of_le_of_eq, le_usize_size, letFun, letFun_body_congr, letFun_congr, letFun_unused, letFun_val_congr, let_body_congr, let_congr, let_val_congr, lexOrd, liftExcept, liftM, liftOption, ltOfOrd, lt_of_eq_of_lt, lt_of_lt_of_eq, map_bind, map_congr, map_eq_pure_bind, maxOfLe, measure, minOfLe, mixHash, mkRecOn, monadFunctorRefl, monadLift_self, mt, namedPattern, neZero_iff, neZero_zero_iff_false, ne_comm, ne_eq, ne_false_of_eq_true, ne_false_of_self, ne_of_apply_ne, ne_of_beq_false, ne_of_mem_of_not_mem, ne_of_mem_of_not_mem', ne_self_iff_false, ne_true_of_eq_false, ne_true_of_not, neq_of_not_iff, noConfusionEnum, noConfusionTypeEnum, nonempty_of_exists, nonempty_prop, not_and, not_and', not_and_of_not_left, not_and_of_not_or_not, not_and_of_not_right, not_and_self, not_and_self_iff, not_congr, not_decide_eq_true, not_exists, not_exists_of_forall_not, not_false, not_false_eq_true, not_false_iff, not_forall_of_exists_not, not_iff_false_intro, not_iff_self, not_imp_of_and_not, not_not_em, not_not_intro, not_not_not, not_not_of_not_imp, not_of_iff_false, not_of_not_imp, not_or, not_or_intro, not_true, not_true_eq_false, observing, ofBoolUsing_eq_false, ofBoolUsing_eq_true, of_decide_eq_false, of_decide_eq_self_eq_true, of_decide_eq_true, of_eq_false, of_eq_true, of_iff_true, optParam_eq, optionCoe, or_and_left, or_and_right, or_assoc, or_comm, or_congr, or_congr_left, or_congr_right, or_false, or_iff_left, or_iff_left_iff_imp, or_iff_left_of_imp, or_iff_right, or_iff_right_iff_imp, or_iff_right_of_imp, or_imp, or_left_comm, or_or_distrib_left, or_or_distrib_right, or_or_or_comm, or_right_comm, or_rotate, or_self, or_self_iff, or_self_left, or_self_right, or_true, outOfBounds, outOfBounds_eq_default, panic, panicCore, panicWithPos, panicWithPosWithDecl, peirce', pi_congr, precArg, precLead, precMax, precMin, precMin1, prioDefault, prioHigh, prioLow, prioMid, proof_irrel, proof_irrel_heq, propext_iff, ptrAddrUnsafe, ptrEq, ptrEqList, pure_id_seq, rawNatLit, recSubsingleton, reduceCtorEq, reduceDIte, reduceIte, repr, reprArg, reprStr, rfl, seqLeft_eq_bind, seqRight_eq_bind, seq_eq_bind, seq_eq_bind_map, shareCommonM, sizeOfWFRel, sizeOf_default, sizeOf_nat, sizeOf_thunk, sorryAx, strictAnd, strictOr, stx!_, stx_?, subtypeCoe, tacticClean_wf, tacticDecreasing_tactic, tacticDecreasing_trivial, tacticDecreasing_trivial_pre_omega, tacticDecreasing_with_, tacticFunext___, tacticGet_elem_tactic, tacticGet_elem_tactic_trivial, tacticSimp_wf, term!_, termDepIfThenElse, termIfLet, termIfThenElse, termMax_prec, termPrintln!__, termS!_, termWithout_expected_type_, thunkCoe, timeit, toBoolUsing, toBoolUsing_eq_true, toLBoolM, toLOptionM, trivial, true_and, true_eq_decide_iff, true_eq_false_of_false, true_iff, true_iff_false, true_imp_iff, true_implies, true_ne_false, true_or, tryFinally, type_eq_of_heq, unexpandArrayEmpty, unexpandEqNDRec, unexpandEqRec, unexpandExists, unexpandGetElem, unexpandGetElem!, unexpandGetElem?, unexpandIte, unexpandListCons, unexpandListNil, unexpandListToArray, unexpandMkArray0, unexpandMkArray1, unexpandMkArray2, unexpandMkArray3, unexpandMkArray4, unexpandMkArray5, unexpandMkArray6, unexpandMkArray7, unexpandMkArray8, unexpandPSigma, unexpandProdMk, unexpandSigma, unexpandSubtype, unexpandTSepArray, unexpandTSyntax, unexpandTSyntaxArray, unexpandUnit, unsafeBaseIO, unsafeCast, unsafeEIO, unsafeIO, usize_size_eq, usize_size_le, usize_size_pos, withPtrAddr, withPtrAddrUnsafe, withPtrEq, withPtrEqDecEq, withPtrEqUnsafe, withShareCommon, «prec(_)», «prio(_)», «stx_*», «stx_+», «stx_,*,?», «stx_,*», «stx_,+,?», «stx_,+», «stx_<|>_», «tacticBy_cases_:_», «term#[_,]», «term%[_|_]», «term-_», «termExists_,_», «term[_]», «term_!=_», «term_$__», «term_%_», «term_&&&_», «term_&&_», «term_*>_», «term_*_», «term_++_», «term_+_», «term_-_», «term_/\_», «term_/_», «term_::_», «term_<$>_», «term_<&&>_», «term_<&>_», «term_<*>_», «term_<*_», «term_<->_», «term_<<<_», «term_<=<_», «term_<=_», «term_<_», «term_<|>_», «term_<|_», «term_<||>_», «term_=<<_», «term_==_», «term_=_», «term_>=>_», «term_>=_», «term_>>=_», «term_>>>_», «term_>>_», «term_>_», «term_\/_», «term_\_», «term_^^^_», «term_^_», «term__[_]'_», «term__[_]_!», «term__[_]_?», «term__[_]», «term_|>_», «term_||_», «term_|||_», «term_×'__1», «term_×'_», «term_×__1», «term_×_», «term_↔_», «term_∈_», «term_∉_», «term_∘_», «term_∣_», «term_∧_», «term_∨_», «term_∩_», «term_∪_», «term_≈_», «term_≠_», «term_≤_», «term_≥_», «term_⊂_», «term_⊃_», «term_⊆_», «term_⊇_», «term_⊕'_», «term_⊕_», «term{_:_//_}», «term{_}», «term{}», «term~~~_», «term¬_», «termΣ'_,_», «termΣ_,_», «term‹_›», «term∃_,_», «term∅»
{docstring And} {docstring AndOp} {docstring AndThen} {docstring BitVec} {docstring ByteArray} {docstring Coe} {docstring CoeDep} {docstring CoeFun} {docstring CoeHTC} {docstring CoeHTCT} {docstring CoeHead} {docstring CoeOTC} {docstring CoeOut} {docstring CoeSort} {docstring CoeT} {docstring CoeTC} {docstring CoeTail} {docstring Complement} {docstring DecidableLE} {docstring DecidableLT} {docstring DecidablePred} {docstring DoResultBC} {docstring DoResultPR} {docstring DoResultPRBC} {docstring DoResultSBC} {docstring EmptyCollection} {docstring Eq} {docstring EquivBEq} {docstring Equivalence} {docstring Exists} {docstring False} {docstring Float} {docstring Float32} {docstring FloatArray} {docstring FloatSpec} {docstring HAndThen} {docstring HEq} {docstring HOrElse} {docstring HasEquiv} {docstring HasSSubset} {docstring HasSubset} {docstring Iff} {docstring Insert} {docstring Inter} {docstring InvImage} {docstring LawfulHashable} {docstring LawfulSingleton} {docstring Max} {docstring Membership} {docstring Min} {docstring MonadEval} {docstring MonadEvalT} {docstring MonadShareCommon} {docstring Ne} {docstring NonScalar} {docstring NonemptyType} {docstring Not} {docstring Or} {docstring OrElse} {docstring OrOp} {docstring PNonScalar} {docstring PartialEquivBEq} {docstring Quot} {docstring Quotient} {docstring ReflBEq} {docstring ReprAtom} {docstring ReprTuple} {docstring SDiff} {docstring SSuperset} {docstring Sep} {docstring Setoid} {docstring ShareCommonM} {docstring ShareCommonT} {docstring Singleton} {docstring Squash} {docstring Stream} {docstring Subrelation} {docstring Subsingleton} {docstring Substring} {docstring Superset} {docstring Thunk} {docstring ToBool} {docstring ToStream} {docstring Trans} {docstring True} {docstring Union} {docstring Vector} {docstring Xor} {docstring absurd} {docstring acc_transGen_iff} {docstring addParenHeuristic} {docstring allocprof} {docstring and_and_and_comm} {docstring and_and_left} {docstring and_and_right} {docstring and_assoc} {docstring and_comm} {docstring and_congr} {docstring and_congr_left} {docstring and_congr_left'} {docstring and_congr_left_eq} {docstring and_congr_left_iff} {docstring and_congr_right} {docstring and_congr_right'} {docstring and_congr_right_eq} {docstring and_congr_right_iff} {docstring and_exists_self} {docstring and_false} {docstring and_iff_left} {docstring and_iff_left_iff_imp} {docstring and_iff_left_of_imp} {docstring and_iff_right} {docstring and_iff_right_iff_imp} {docstring and_iff_right_of_imp} {docstring and_imp} {docstring and_left_comm} {docstring and_not_self} {docstring and_not_self_iff} {docstring and_or_left} {docstring and_or_right} {docstring and_right_comm} {docstring and_rotate} {docstring and_self} {docstring and_self_iff} {docstring and_self_left} {docstring and_self_right} {docstring and_true} {docstring apply_dite} {docstring apply_ite} {docstring beq_eq_false_iff_ne} {docstring beq_false} {docstring beq_false_of_ne} {docstring beq_iff_eq} {docstring beq_of_eq} {docstring beq_self_eq_true} {docstring beq_self_eq_true'} {docstring beq_true} {docstring bind_congr} {docstring bind_map_left} {docstring bind_pure} {docstring bind_pure_unit} {docstring bne} {docstring bne_comm} {docstring bne_eq_false_iff_eq} {docstring bne_iff_ne} {docstring bne_self_eq_false} {docstring bne_self_eq_false'} {docstring bool} {docstring boolIfThenElse} {docstring boolPredToPred} {docstring boolRelToRel} {docstring boolToProp} {docstring boolToPropSimps} {docstring boolToSort} {docstring cast} {docstring cast_cast} {docstring cast_eq} {docstring cast_heq} {docstring coeFunNotation} {docstring coeNotation} {docstring coeSortNotation} {docstring commandDeclare_bitwise_uint_theorems__} {docstring commandDeclare_uint_simprocs_} {docstring commandDeclare_uint_theorems__} {docstring compareLex} {docstring compareOfLessAndBEq} {docstring compareOfLessAndEq} {docstring compareOn} {docstring cond_false} {docstring cond_true} {docstring congr} {docstring congrArg} {docstring congrFun} {docstring dbgSleep} {docstring dbgStackTrace} {docstring dbgTrace} {docstring dbgTraceIfShared} {docstring dbgTraceVal} {docstring decEq} {docstring decPropToBool} {docstring decidableGetElem?} {docstring decidable_of_bool} {docstring decidable_of_decidable_of_eq} {docstring decidable_of_decidable_of_iff} {docstring decidable_of_iff} {docstring decidable_of_iff'} {docstring decide_eq_decide} {docstring decide_eq_false} {docstring decide_eq_false_iff_not} {docstring decide_eq_true} {docstring decide_eq_true_eq} {docstring decide_eq_true_iff} {docstring decide_false} {docstring decide_implies} {docstring decide_ite} {docstring decide_not} {docstring decide_true} {docstring dif_eq_if} {docstring dif_neg} {docstring dif_pos} {docstring dite} {docstring dite_cond_eq_false} {docstring dite_cond_eq_true} {docstring dite_congr} {docstring dite_else_false} {docstring dite_else_true} {docstring dite_eq_ite} {docstring dite_eq_left_iff} {docstring dite_eq_right_iff} {docstring dite_false} {docstring dite_iff_left_iff} {docstring dite_iff_right_iff} {docstring dite_not} {docstring dite_then_false} {docstring dite_then_true} {docstring dite_true} {docstring dreduceDIte} {docstring dreduceIte} {docstring emptyRelation} {docstring emptyWf} {docstring eqRec_heq} {docstring eq_comm} {docstring eq_false} {docstring eq_false'} {docstring eq_false_of_decide} {docstring eq_false_of_ne_true} {docstring eq_iff_iff} {docstring eq_iff_true_of_subsingleton} {docstring eq_mp_eq_cast} {docstring eq_mpr_eq_cast} {docstring eq_of_heq} {docstring eq_self} {docstring eq_self_iff_true} {docstring eq_true} {docstring eq_true_eq_id} {docstring eq_true_of_decide} {docstring eq_true_of_ne_false} {docstring exists_and_left} {docstring exists_and_right} {docstring exists_and_self} {docstring exists_apply_eq_apply} {docstring exists_comm} {docstring exists_congr} {docstring exists_const} {docstring exists_eq} {docstring exists_eq'} {docstring exists_eq_left} {docstring exists_eq_left'} {docstring exists_eq_or_imp} {docstring exists_eq_right} {docstring exists_eq_right'} {docstring exists_eq_right_right} {docstring exists_eq_right_right'} {docstring exists_false} {docstring exists_idem} {docstring exists_imp} {docstring exists_or} {docstring exists_or_eq_left} {docstring exists_or_eq_left'} {docstring exists_or_eq_right} {docstring exists_or_eq_right'} {docstring exists_prop} {docstring exists_prop'} {docstring exists_prop_congr} {docstring exists_prop_decidable} {docstring exists_prop_of_true} {docstring exists_true_left} {docstring exists₂_congr} {docstring exists₂_imp} {docstring exists₃_congr} {docstring exists₄_congr} {docstring exists₅_congr} {docstring false_and} {docstring false_eq_decide_iff} {docstring false_iff} {docstring false_iff_true} {docstring false_imp_iff} {docstring false_implies} {docstring false_ne_true} {docstring false_of_ne} {docstring false_of_true_eq_false} {docstring false_of_true_iff_false} {docstring false_or} {docstring flip} {docstring float32DecLe} {docstring float32DecLt} {docstring float32Spec} {docstring floatDecLe} {docstring floatDecLt} {docstring floatSpec} {docstring forIn'_eq_forIn} {docstring forall_and} {docstring forall_apply_eq_imp_iff} {docstring forall_apply_eq_imp_iff₂} {docstring forall_comm} {docstring forall_congr} {docstring forall_congr'} {docstring forall_const} {docstring forall_eq} {docstring forall_eq'} {docstring forall_eq_apply_imp_iff} {docstring forall_eq_or_imp} {docstring forall_exists_index} {docstring forall_false} {docstring forall_imp} {docstring forall_not_of_not_exists} {docstring forall_prop_congr_dom} {docstring forall_prop_decidable} {docstring forall_prop_domain_congr} {docstring forall_prop_of_false} {docstring forall_prop_of_true} {docstring forall_self_imp} {docstring forall₂_congr} {docstring forall₃_congr} {docstring forall₄_congr} {docstring forall₅_congr} {docstring funext_iff} {docstring ge_iff_le} {docstring getElem!_neg} {docstring getElem!_pos} {docstring getElem?_eq_none} {docstring getElem?_neg} {docstring getElem?_pos} {docstring getElem_congr} {docstring getElem_congr_coll} {docstring getElem_congr_idx} {docstring get_getElem?} {docstring gt_iff_lt} {docstring hash64} {docstring hash_eq} {docstring heq_comm} {docstring heq_eq_eq} {docstring heq_of_eq} {docstring heq_of_eqRec_eq} {docstring heq_of_eq_of_heq} {docstring heq_of_heq_of_eq} {docstring heq_self_iff_true} {docstring hexDigitRepr} {docstring id} {docstring id_def} {docstring id_eq} {docstring id_map'} {docstring if_false} {docstring if_false_left} {docstring if_false_right} {docstring if_neg} {docstring if_pos} {docstring if_true} {docstring if_true_left} {docstring if_true_right} {docstring iff_and_self} {docstring iff_comm} {docstring iff_congr} {docstring iff_def} {docstring iff_def'} {docstring iff_false} {docstring iff_false_intro} {docstring iff_false_left} {docstring iff_false_right} {docstring iff_iff_eq} {docstring iff_iff_implies_and_implies} {docstring iff_not_self} {docstring iff_of_eq} {docstring iff_of_false} {docstring iff_of_true} {docstring iff_or_self} {docstring iff_self} {docstring iff_self_and} {docstring iff_self_or} {docstring iff_true} {docstring iff_true_intro} {docstring iff_true_left} {docstring iff_true_right} {docstring imp_and} {docstring imp_congr} {docstring imp_congr_ctx} {docstring imp_congr_left} {docstring imp_congr_right} {docstring imp_false} {docstring imp_iff_not} {docstring imp_iff_right} {docstring imp_imp_imp} {docstring imp_intro} {docstring imp_not_comm} {docstring imp_not_self} {docstring imp_self} {docstring imp_true_iff} {docstring implies_congr} {docstring implies_congr_ctx} {docstring implies_dep_congr_ctx} {docstring implies_true} {docstring inline} {docstring instAddFloat} {docstring instAddFloat32} {docstring instAddISize} {docstring instAddInt16} {docstring instAddInt32} {docstring instAddInt64} {docstring instAddInt8} {docstring instAddNat} {docstring instAddUInt16} {docstring instAddUInt32} {docstring instAddUInt64} {docstring instAddUInt8} {docstring instAddUSize} {docstring instAlternativeOption} {docstring instAndOpISize} {docstring instAndOpInt16} {docstring instAndOpInt32} {docstring instAndOpInt64} {docstring instAndOpInt8} {docstring instAndOpUInt16} {docstring instAndOpUInt32} {docstring instAndOpUInt64} {docstring instAndOpUInt8} {docstring instAndOpUSize} {docstring instAppendSubarray} {docstring instAssociativeAnd} {docstring instAssociativeBoolAnd} {docstring instAssociativeBoolOr} {docstring instAssociativeOr} {docstring instBEqFloat} {docstring instBEqFloat32} {docstring instBEqOfDecidableEq} {docstring instBEqOrdering} {docstring instBEqProd} {docstring instCoeHTC} {docstring instCoeHTCOfCoeHeadOfCoeOTC} {docstring instCoeHTCOfCoeOTC} {docstring instCoeHTCT} {docstring instCoeHTCTIntOfIntCast} {docstring instCoeHTCTNatOfNatCast} {docstring instCoeHTCTOfCoeHTC} {docstring instCoeHTCTOfCoeTailOfCoeHTC} {docstring instCoeOTC} {docstring instCoeOTCOfCoeOut} {docstring instCoeOTCOfCoeTC} {docstring instCoeOutOfCoeFun} {docstring instCoeOutOfCoeSort} {docstring instCoeStringError} {docstring instCoeT} {docstring instCoeTC} {docstring instCoeTCOfCoe} {docstring instCoeTCOfCoe_1} {docstring instCoeTOfCoeDep} {docstring instCoeTOfCoeHTCT} {docstring instCoeTailIntOfIntCast} {docstring instCoeTailNatOfNatCast} {docstring instComplementISize} {docstring instComplementInt16} {docstring instComplementInt32} {docstring instComplementInt64} {docstring instComplementInt8} {docstring instComplementUInt16} {docstring instComplementUInt32} {docstring instComplementUInt64} {docstring instComplementUInt8} {docstring instComplementUSize} {docstring instDecidableAnd} {docstring instDecidableDite} {docstring instDecidableEqBitVec} {docstring instDecidableEqBool} {docstring instDecidableEqChar} {docstring instDecidableEqEmpty} {docstring instDecidableEqFin} {docstring instDecidableEqISize} {docstring instDecidableEqInt16} {docstring instDecidableEqInt32} {docstring instDecidableEqInt64} {docstring instDecidableEqInt8} {docstring instDecidableEqList} {docstring instDecidableEqNat} {docstring instDecidableEqOfIff} {docstring instDecidableEqPEmpty} {docstring instDecidableEqPLift} {docstring instDecidableEqPUnit} {docstring instDecidableEqPos} {docstring instDecidableEqProd} {docstring instDecidableEqString} {docstring instDecidableEqSum} {docstring instDecidableEqUInt16} {docstring instDecidableEqUInt32} {docstring instDecidableEqUInt64} {docstring instDecidableEqUInt8} {docstring instDecidableEqULift} {docstring instDecidableEqUSize} {docstring instDecidableEqVector} {docstring instDecidableFalse} {docstring instDecidableForall} {docstring instDecidableIff} {docstring instDecidableIte} {docstring instDecidableLeBitVec} {docstring instDecidableLeISize} {docstring instDecidableLeInt16} {docstring instDecidableLeInt32} {docstring instDecidableLeInt64} {docstring instDecidableLeInt8} {docstring instDecidableLePos} {docstring instDecidableLeUInt16} {docstring instDecidableLeUInt32} {docstring instDecidableLeUInt64} {docstring instDecidableLeUInt8} {docstring instDecidableLeUSize} {docstring instDecidableLtBitVec} {docstring instDecidableLtISize} {docstring instDecidableLtInt16} {docstring instDecidableLtInt32} {docstring instDecidableLtInt64} {docstring instDecidableLtInt8} {docstring instDecidableLtPos} {docstring instDecidableLtUInt16} {docstring instDecidableLtUInt32} {docstring instDecidableLtUInt64} {docstring instDecidableLtUInt8} {docstring instDecidableLtUSize} {docstring instDecidableNot} {docstring instDecidableOr} {docstring instDecidablePredComp} {docstring instDecidableRelLe} {docstring instDecidableRelLt} {docstring instDecidableTrue} {docstring instDivFloat} {docstring instDivFloat32} {docstring instDivISize} {docstring instDivInt16} {docstring instDivInt32} {docstring instDivInt64} {docstring instDivInt8} {docstring instDivUInt16} {docstring instDivUInt32} {docstring instDivUInt64} {docstring instDivUInt8} {docstring instDivUSize} {docstring instEquivBEqOfLawfulBEq} {docstring instForInOfForIn'} {docstring instForInOfStream} {docstring instFunctorOption} {docstring instGetElem?OfGetElemOfDecidable} {docstring instHAdd} {docstring instHAddPos} {docstring instHAddPosChar} {docstring instHAddPosString} {docstring instHAndOfAndOp} {docstring instHAndThenOfAndThen} {docstring instHAppendOfAppend} {docstring instHDiv} {docstring instHMod} {docstring instHModUInt16Nat} {docstring instHModUInt32Nat} {docstring instHModUInt64Nat} {docstring instHModUInt8Nat} {docstring instHModUSizeNat} {docstring instHMul} {docstring instHOrElseOfOrElse} {docstring instHOrOfOrOp} {docstring instHPow} {docstring instHShiftLeftOfShiftLeft} {docstring instHShiftRightOfShiftRight} {docstring instHSub} {docstring instHSubPos} {docstring instHXorOfXor} {docstring instHasEquivOfSetoid} {docstring instHashable} {docstring instHashableArray} {docstring instHashableBool} {docstring instHashableByteArray} {docstring instHashableChar} {docstring instHashableFin} {docstring instHashableInt} {docstring instHashableList} {docstring instHashableNat} {docstring instHashableOption} {docstring instHashablePos} {docstring instHashableProd} {docstring instHashableString} {docstring instHashableSubtype} {docstring instHashableUInt16} {docstring instHashableUInt32} {docstring instHashableUInt64} {docstring instHashableUInt8} {docstring instHashableUSize} {docstring instHomogeneousPowFloat} {docstring instHomogeneousPowFloat32} {docstring instIdempotentOpAnd} {docstring instIdempotentOpBoolAnd} {docstring instIdempotentOpBoolOr} {docstring instIdempotentOpOr} {docstring instInhabitedBool} {docstring instInhabitedEIO} {docstring instInhabitedEST} {docstring instInhabitedExcept} {docstring instInhabitedExceptTOfMonad} {docstring instInhabitedFloat} {docstring instInhabitedFloat32} {docstring instInhabitedForInStep} {docstring instInhabitedForInStep_1} {docstring instInhabitedForall} {docstring instInhabitedForallOfMonad} {docstring instInhabitedISize} {docstring instInhabitedInt16} {docstring instInhabitedInt32} {docstring instInhabitedInt64} {docstring instInhabitedInt8} {docstring instInhabitedList} {docstring instInhabitedMProd} {docstring instInhabitedNat} {docstring instInhabitedNonScalar} {docstring instInhabitedNonemptyType} {docstring instInhabitedOfMonad} {docstring instInhabitedOption} {docstring instInhabitedOrdering} {docstring instInhabitedPNonScalar} {docstring instInhabitedPProd} {docstring instInhabitedPUnit} {docstring instInhabitedPos} {docstring instInhabitedProd} {docstring instInhabitedProp} {docstring instInhabitedReaderT} {docstring instInhabitedSort} {docstring instInhabitedStdGen} {docstring instInhabitedSubstring} {docstring instInhabitedTask} {docstring instInhabitedTrue} {docstring instInhabitedUInt16} {docstring instInhabitedUInt32} {docstring instInhabitedUInt64} {docstring instInhabitedUInt8} {docstring instInhabitedUSize} {docstring instIntCastInt} {docstring instLEBitVec} {docstring instLEFin} {docstring instLEFloat} {docstring instLEFloat32} {docstring instLEISize} {docstring instLEInt16} {docstring instLEInt32} {docstring instLEInt64} {docstring instLEInt8} {docstring instLENat} {docstring instLEPos} {docstring instLEUInt16} {docstring instLEUInt32} {docstring instLEUInt64} {docstring instLEUInt8} {docstring instLEUSize} {docstring instLTBitVec} {docstring instLTFin} {docstring instLTFloat} {docstring instLTFloat32} {docstring instLTISize} {docstring instLTInt16} {docstring instLTInt32} {docstring instLTInt64} {docstring instLTInt8} {docstring instLTNat} {docstring instLTOption} {docstring instLTPos} {docstring instLTUInt16} {docstring instLTUInt32} {docstring instLTUInt64} {docstring instLTUInt8} {docstring instLTUSize} {docstring instLawfulApplicativeExcept} {docstring instLawfulApplicativeOption} {docstring instLawfulBEq} {docstring instLawfulBEqBool} {docstring instLawfulBEqChar} {docstring instLawfulBEqString} {docstring instLawfulFunctorExcept} {docstring instLawfulFunctorOption} {docstring instLawfulGetElem} {docstring instLawfulHashableOfLawfulBEq} {docstring instLawfulIdentityAndTrue} {docstring instLawfulIdentityBoolAndTrue} {docstring instLawfulIdentityBoolOrFalse} {docstring instLawfulIdentityOrFalse} {docstring instLawfulMonadEStateM} {docstring instLawfulMonadExcept} {docstring instLawfulMonadOption} {docstring instLawfulMonadStateRefT'} {docstring instMaxFloat} {docstring instMaxFloat32} {docstring instMaxISize} {docstring instMaxInt16} {docstring instMaxInt32} {docstring instMaxInt64} {docstring instMaxInt8} {docstring instMaxUInt16} {docstring instMaxUInt32} {docstring instMaxUInt64} {docstring instMaxUInt8} {docstring instMaxUSize} {docstring instMinFloat} {docstring instMinFloat32} {docstring instMinISize} {docstring instMinInt16} {docstring instMinInt32} {docstring instMinInt64} {docstring instMinInt8} {docstring instMinNat} {docstring instMinUInt16} {docstring instMinUInt32} {docstring instMinUInt64} {docstring instMinUInt8} {docstring instMinUSize} {docstring instModISize} {docstring instModInt16} {docstring instModInt32} {docstring instModInt64} {docstring instModInt8} {docstring instModUInt16} {docstring instModUInt32} {docstring instModUInt64} {docstring instModUInt8} {docstring instModUSize} {docstring instMonadBaseIO} {docstring instMonadControlExceptTOfMonad} {docstring instMonadControlOptionTOfMonad} {docstring instMonadControlReaderT} {docstring instMonadControlStateRefT'} {docstring instMonadControlTOfMonadControl} {docstring instMonadControlTOfPure} {docstring instMonadEIO} {docstring instMonadEST} {docstring instMonadEvalOfMonadLift} {docstring instMonadEvalT} {docstring instMonadEvalTOfMonadEval} {docstring instMonadExceptOfEIO} {docstring instMonadExceptOfEST} {docstring instMonadExceptOfExcept} {docstring instMonadExceptOfExceptT} {docstring instMonadExceptOfExceptTOfMonad} {docstring instMonadExceptOfMonadExceptOf} {docstring instMonadExceptOfUnitOption} {docstring instMonadFinallyBaseIO} {docstring instMonadFinallyEIO} {docstring instMonadFinallyStateRefT'} {docstring instMonadFunctorTOfMonadFunctor} {docstring instMonadLiftBaseIOEIO} {docstring instMonadLiftSTEST} {docstring instMonadLiftT} {docstring instMonadLiftTOfMonadLift} {docstring instMonadOption} {docstring instMonadReaderOfMonadReaderOf} {docstring instMonadReaderOfOfMonadLift} {docstring instMonadReaderOfReaderTOfMonad} {docstring instMonadST} {docstring instMonadStateOfMonadStateOf} {docstring instMonadStateOfOfMonadLift} {docstring instMonadStateOfStateTOfMonad} {docstring instMonadWithReaderOfMonadWithReaderOf} {docstring instMonadWithReaderOfOfMonadFunctor} {docstring instMonadWithReaderOfReaderT} {docstring instMulFloat} {docstring instMulFloat32} {docstring instMulISize} {docstring instMulInt16} {docstring instMulInt32} {docstring instMulInt64} {docstring instMulInt8} {docstring instMulNat} {docstring instMulUInt16} {docstring instMulUInt32} {docstring instMulUInt64} {docstring instMulUInt8} {docstring instMulUSize} {docstring instNatCastInt} {docstring instNatCastNat} {docstring instNatPowNat} {docstring instNeZeroNatIte} {docstring instNegFloat} {docstring instNegFloat32} {docstring instNegISize} {docstring instNegInt16} {docstring instNegInt32} {docstring instNegInt64} {docstring instNegInt8} {docstring instNonemptyDynamic} {docstring instNonemptyFloat} {docstring instNonemptyFloat32} {docstring instNonemptyForall} {docstring instNonemptyMProd} {docstring instNonemptyOfInhabited} {docstring instNonemptyOfMonad} {docstring instNonemptyPProd} {docstring instNonemptyProd} {docstring instNonemptyTask} {docstring instNonemptyTypeName} {docstring instOfNat} {docstring instOfNatFloat} {docstring instOfNatFloat32} {docstring instOfNatISize} {docstring instOfNatInt16} {docstring instOfNatInt32} {docstring instOfNatInt64} {docstring instOfNatInt8} {docstring instOfNatNat} {docstring instOfScientificFloat} {docstring instOfScientificFloat32} {docstring instOrElseEIO} {docstring instOrElseOfAlternative} {docstring instOrOpISize} {docstring instOrOpInt16} {docstring instOrOpInt32} {docstring instOrOpInt64} {docstring instOrOpInt8} {docstring instOrOpUInt16} {docstring instOrOpUInt32} {docstring instOrOpUInt64} {docstring instOrOpUInt8} {docstring instOrOpUSize} {docstring instOrdBool} {docstring instOrdChar} {docstring instOrdFin} {docstring instOrdInt} {docstring instOrdNat} {docstring instOrdOption} {docstring instOrdString} {docstring instOrdUInt16} {docstring instOrdUInt32} {docstring instOrdUInt64} {docstring instOrdUInt8} {docstring instOrdUSize} {docstring instPowNat} {docstring instPowOfHomogeneousPow} {docstring instRandomGenStdGen} {docstring instReprAtomBool} {docstring instReprAtomChar} {docstring instReprAtomFloat} {docstring instReprAtomFloat32} {docstring instReprAtomInt} {docstring instReprAtomNat} {docstring instReprAtomString} {docstring instReprAtomUInt16} {docstring instReprAtomUInt32} {docstring instReprAtomUInt64} {docstring instReprAtomUInt8} {docstring instReprAtomUSize} {docstring instReprBool} {docstring instReprChar} {docstring instReprDecidable} {docstring instReprEmpty} {docstring instReprExcept} {docstring instReprFin} {docstring instReprFloat} {docstring instReprFloat32} {docstring instReprId} {docstring instReprId_1} {docstring instReprInt} {docstring instReprIterator} {docstring instReprList} {docstring instReprListOfReprAtom} {docstring instReprNat} {docstring instReprOption} {docstring instReprPUnit} {docstring instReprPos} {docstring instReprProdOfReprTuple} {docstring instReprSSet} {docstring instReprSigma} {docstring instReprSourceInfo} {docstring instReprStdGen} {docstring instReprString} {docstring instReprSubarray} {docstring instReprSubstring} {docstring instReprSubtype} {docstring instReprSum} {docstring instReprTupleOfRepr} {docstring instReprTupleProdOfRepr} {docstring instReprUInt16} {docstring instReprUInt32} {docstring instReprUInt64} {docstring instReprUInt8} {docstring instReprULift} {docstring instReprUSize} {docstring instReprUnit} {docstring instReprVector} {docstring instSTWorldEST} {docstring instSTWorldOfMonadLift} {docstring instShiftLeftISize} {docstring instShiftLeftInt16} {docstring instShiftLeftInt32} {docstring instShiftLeftInt64} {docstring instShiftLeftInt8} {docstring instShiftLeftUInt16} {docstring instShiftLeftUInt32} {docstring instShiftLeftUInt64} {docstring instShiftLeftUInt8} {docstring instShiftLeftUSize} {docstring instShiftRightISize} {docstring instShiftRightInt16} {docstring instShiftRightInt32} {docstring instShiftRightInt64} {docstring instShiftRightInt8} {docstring instShiftRightUInt16} {docstring instShiftRightUInt32} {docstring instShiftRightUInt64} {docstring instShiftRightUInt8} {docstring instShiftRightUSize} {docstring instSizeOfDefault} {docstring instSizeOfForallUnit} {docstring instSizeOfNat} {docstring instStreamList} {docstring instStreamProd} {docstring instStreamRangeNat} {docstring instStreamSubarray} {docstring instStreamSubstringChar} {docstring instSubFloat} {docstring instSubFloat32} {docstring instSubISize} {docstring instSubInt16} {docstring instSubInt32} {docstring instSubInt64} {docstring instSubInt8} {docstring instSubNat} {docstring instSubUInt16} {docstring instSubUInt32} {docstring instSubUInt64} {docstring instSubUInt8} {docstring instSubUSize} {docstring instSubsingleton} {docstring instSubsingletonDecidable} {docstring instSubsingletonEmpty} {docstring instSubsingletonPEmpty} {docstring instSubsingletonPLift} {docstring instSubsingletonPUnit} {docstring instSubsingletonProd} {docstring instSubsingletonSquash} {docstring instSubsingletonStateM} {docstring instSubsingletonULift} {docstring instToBoolBool} {docstring instToBoolOption} {docstring instToFormatArray} {docstring instToFormatList} {docstring instToFormatOfToString} {docstring instToFormatOption} {docstring instToFormatPos} {docstring instToFormatProd} {docstring instToStreamArraySubarray} {docstring instToStreamList} {docstring instToStreamRange} {docstring instToStreamStringSubstring} {docstring instToStreamSubarray} {docstring instToStringBool} {docstring instToStringByteArray} {docstring instToStringChar} {docstring instToStringDecidable} {docstring instToStringExcept} {docstring instToStringFin} {docstring instToStringFloat} {docstring instToStringFloat32} {docstring instToStringFloatArray} {docstring instToStringFormat} {docstring instToStringISize} {docstring instToStringId} {docstring instToStringId_1} {docstring instToStringInt} {docstring instToStringInt16} {docstring instToStringInt32} {docstring instToStringInt64} {docstring instToStringInt8} {docstring instToStringIterator} {docstring instToStringList} {docstring instToStringNat} {docstring instToStringOption} {docstring instToStringPUnit} {docstring instToStringPos} {docstring instToStringProd} {docstring instToStringSigma} {docstring instToStringString} {docstring instToStringSubarray} {docstring instToStringSubstring} {docstring instToStringSubtype} {docstring instToStringSum} {docstring instToStringUInt16} {docstring instToStringUInt32} {docstring instToStringUInt64} {docstring instToStringUInt8} {docstring instToStringULift} {docstring instToStringUSize} {docstring instToStringUnit} {docstring instTransEq} {docstring instTransEq_1} {docstring instTransIff} {docstring instWellFoundedRelationOfSizeOf} {docstring instXorISize} {docstring instXorInt16} {docstring instXorInt32} {docstring instXorInt64} {docstring instXorInt8} {docstring instXorUInt16} {docstring instXorUInt32} {docstring instXorUInt64} {docstring instXorUInt8} {docstring instXorUSize} {docstring isExclusiveUnsafe} {docstring isSome_getElem?} {docstring isValidChar} {docstring ite} {docstring iteInduction} {docstring ite_cond_eq_false} {docstring ite_cond_eq_true} {docstring ite_congr} {docstring ite_else_decide_not_self} {docstring ite_else_decide_self} {docstring ite_else_not_self} {docstring ite_else_self} {docstring ite_eq_ite} {docstring ite_eq_left_iff} {docstring ite_eq_right_iff} {docstring ite_false} {docstring ite_id} {docstring ite_iff_ite} {docstring ite_iff_left_iff} {docstring ite_iff_right_iff} {docstring ite_not} {docstring ite_self} {docstring ite_then_decide_not_self} {docstring ite_then_decide_self} {docstring ite_then_not_self} {docstring ite_then_self} {docstring ite_true} {docstring lcCast} {docstring lcErased} {docstring lcProof} {docstring lcUnreachable} {docstring leOfOrd} {docstring le_of_eq_of_le} {docstring le_of_le_of_eq} {docstring le_usize_size} {docstring letFun} {docstring letFun_body_congr} {docstring letFun_congr} {docstring letFun_unused} {docstring letFun_val_congr} {docstring let_body_congr} {docstring let_congr} {docstring let_val_congr} {docstring lexOrd} {docstring liftExcept} {docstring liftM} {docstring liftOption} {docstring ltOfOrd} {docstring lt_of_eq_of_lt} {docstring lt_of_lt_of_eq} {docstring map_bind} {docstring map_congr} {docstring map_eq_pure_bind} {docstring maxOfLe} {docstring measure} {docstring minOfLe} {docstring mixHash} {docstring mkRecOn} {docstring monadFunctorRefl} {docstring monadLift_self} {docstring mt} {docstring namedPattern} {docstring neZero_iff} {docstring neZero_zero_iff_false} {docstring ne_comm} {docstring ne_eq} {docstring ne_false_of_eq_true} {docstring ne_false_of_self} {docstring ne_of_apply_ne} {docstring ne_of_beq_false} {docstring ne_of_mem_of_not_mem} {docstring ne_of_mem_of_not_mem'} {docstring ne_self_iff_false} {docstring ne_true_of_eq_false} {docstring ne_true_of_not} {docstring neq_of_not_iff} {docstring noConfusionEnum} {docstring noConfusionTypeEnum} {docstring nonempty_of_exists} {docstring nonempty_prop} {docstring not_and} {docstring not_and'} {docstring not_and_of_not_left} {docstring not_and_of_not_or_not} {docstring not_and_of_not_right} {docstring not_and_self} {docstring not_and_self_iff} {docstring not_congr} {docstring not_decide_eq_true} {docstring not_exists} {docstring not_exists_of_forall_not} {docstring not_false} {docstring not_false_eq_true} {docstring not_false_iff} {docstring not_forall_of_exists_not} {docstring not_iff_false_intro} {docstring not_iff_self} {docstring not_imp_of_and_not} {docstring not_not_em} {docstring not_not_intro} {docstring not_not_not} {docstring not_not_of_not_imp} {docstring not_of_iff_false} {docstring not_of_not_imp} {docstring not_or} {docstring not_or_intro} {docstring not_true} {docstring not_true_eq_false} {docstring observing} {docstring ofBoolUsing_eq_false} {docstring ofBoolUsing_eq_true} {docstring of_decide_eq_false} {docstring of_decide_eq_self_eq_true} {docstring of_decide_eq_true} {docstring of_eq_false} {docstring of_eq_true} {docstring of_iff_true} {docstring optParam_eq} {docstring optionCoe} {docstring or_and_left} {docstring or_and_right} {docstring or_assoc} {docstring or_comm} {docstring or_congr} {docstring or_congr_left} {docstring or_congr_right} {docstring or_false} {docstring or_iff_left} {docstring or_iff_left_iff_imp} {docstring or_iff_left_of_imp} {docstring or_iff_right} {docstring or_iff_right_iff_imp} {docstring or_iff_right_of_imp} {docstring or_imp} {docstring or_left_comm} {docstring or_or_distrib_left} {docstring or_or_distrib_right} {docstring or_or_or_comm} {docstring or_right_comm} {docstring or_rotate} {docstring or_self} {docstring or_self_iff} {docstring or_self_left} {docstring or_self_right} {docstring or_true} {docstring outOfBounds} {docstring outOfBounds_eq_default} {docstring panic} {docstring panicCore} {docstring panicWithPos} {docstring panicWithPosWithDecl} {docstring peirce'} {docstring pi_congr} {docstring precArg} {docstring precLead} {docstring precMax} {docstring precMin} {docstring precMin1} {docstring prioDefault} {docstring prioHigh} {docstring prioLow} {docstring prioMid} {docstring proof_irrel} {docstring proof_irrel_heq} {docstring propext_iff} {docstring ptrAddrUnsafe} {docstring ptrEq} {docstring ptrEqList} {docstring pure_id_seq} {docstring rawNatLit} {docstring recSubsingleton} {docstring reduceCtorEq} {docstring reduceDIte} {docstring reduceIte} {docstring repr} {docstring reprArg} {docstring reprStr} {docstring rfl} {docstring seqLeft_eq_bind} {docstring seqRight_eq_bind} {docstring seq_eq_bind} {docstring seq_eq_bind_map} {docstring shareCommonM} {docstring sizeOfWFRel} {docstring sizeOf_default} {docstring sizeOf_nat} {docstring sizeOf_thunk} {docstring sorryAx} {docstring strictAnd} {docstring strictOr} {docstring stx!_} {docstring stx_?} {docstring subtypeCoe} {docstring tacticClean_wf} {docstring tacticDecreasing_tactic} {docstring tacticDecreasing_trivial} {docstring tacticDecreasing_trivial_pre_omega} {docstring tacticDecreasing_with_} {docstring tacticFunext___} {docstring tacticGet_elem_tactic} {docstring tacticGet_elem_tactic_trivial} {docstring tacticSimp_wf} {docstring term!_} {docstring termDepIfThenElse} {docstring termIfLet} {docstring termIfThenElse} {docstring termMax_prec} {docstring termPrintln!__} {docstring termS!_} {docstring termWithout_expected_type_} {docstring thunkCoe} {docstring timeit} {docstring toBoolUsing} {docstring toBoolUsing_eq_true} {docstring toLBoolM} {docstring toLOptionM} {docstring trivial} {docstring true_and} {docstring true_eq_decide_iff} {docstring true_eq_false_of_false} {docstring true_iff} {docstring true_iff_false} {docstring true_imp_iff} {docstring true_implies} {docstring true_ne_false} {docstring true_or} {docstring tryFinally} {docstring type_eq_of_heq} {docstring unexpandArrayEmpty} {docstring unexpandEqNDRec} {docstring unexpandEqRec} {docstring unexpandExists} {docstring unexpandGetElem} {docstring unexpandGetElem!} {docstring unexpandGetElem?} {docstring unexpandIte} {docstring unexpandListCons} {docstring unexpandListNil} {docstring unexpandListToArray} {docstring unexpandMkArray0} {docstring unexpandMkArray1} {docstring unexpandMkArray2} {docstring unexpandMkArray3} {docstring unexpandMkArray4} {docstring unexpandMkArray5} {docstring unexpandMkArray6} {docstring unexpandMkArray7} {docstring unexpandMkArray8} {docstring unexpandPSigma} {docstring unexpandProdMk} {docstring unexpandSigma} {docstring unexpandSubtype} {docstring unexpandTSepArray} {docstring unexpandTSyntax} {docstring unexpandTSyntaxArray} {docstring unexpandUnit} {docstring unsafeBaseIO} {docstring unsafeCast} {docstring unsafeEIO} {docstring unsafeIO} {docstring usize_size_eq} {docstring usize_size_le} {docstring usize_size_pos} {docstring withPtrAddr} {docstring withPtrAddrUnsafe} {docstring withPtrEq} {docstring withPtrEqDecEq} {docstring withPtrEqUnsafe} {docstring withShareCommon} {docstring «prec(_)»} {docstring «prio(_)»} {docstring «stx_*»} {docstring «stx_+»} {docstring «stx_,*,?»} {docstring «stx_,*»} {docstring «stx_,+,?»} {docstring «stx_,+»} {docstring «stx_<|>_»} {docstring «tacticBy_cases_:_»} {docstring «term#[_,]»} {docstring «term%[_|_]»} {docstring «term-_»} {docstring «termExists_,_»} {docstring «term[_]»} {docstring «term_!=_»} {docstring «term_$__»} {docstring «term_%_»} {docstring «term_&&&_»} {docstring «term_&&_»} {docstring «term_*>_»} {docstring «term_*_»} {docstring «term_++_»} {docstring «term_+_»} {docstring «term_-_»} {docstring «term_/\_»} {docstring «term_/_»} {docstring «term_::_»} {docstring «term_<$>_»} {docstring «term_<&&>_»} {docstring «term_<&>_»} {docstring «term_<*>_»} {docstring «term_<*_»} {docstring «term_<->_»} {docstring «term_<<<_»} {docstring «term_<=<_»} {docstring «term_<=_»} {docstring «term_<_»} {docstring «term_<|>_»} {docstring «term_<|_»} {docstring «term_<||>_»} {docstring «term_=<<_»} {docstring «term_==_»} {docstring «term_=_»} {docstring «term_>=>_»} {docstring «term_>=_»} {docstring «term_>>=_»} {docstring «term_>>>_»} {docstring «term_>>_»} {docstring «term_>_»} {docstring «term_\/_»} {docstring «term_\_»} {docstring «term_^^^_»} {docstring «term_^_»} {docstring «term__[_]'_»} {docstring «term__[_]_!»} {docstring «term__[_]_?»} {docstring «term__[_]»} {docstring «term_|>_»} {docstring «term_||_»} {docstring «term_|||_»} {docstring «term_×'__1»} {docstring «term_×'_»} {docstring «term_×__1»} {docstring «term_×_»} {docstring «term_↔_»} {docstring «term_∈_»} {docstring «term_∉_»} {docstring «term_∘_»} {docstring «term_∣_»} {docstring «term_∧_»} {docstring «term_∨_»} {docstring «term_∩_»} {docstring «term_∪_»} {docstring «term_≈_»} {docstring «term_≠_»} {docstring «term_≤_»} {docstring «term_≥_»} {docstring «term_⊂_»} {docstring «term_⊃_»} {docstring «term_⊆_»} {docstring «term_⊇_»} {docstring «term_⊕'_»} {docstring «term_⊕_»} {docstring «term{_:_//_}»} {docstring «term{_}»} {docstring «term{}»} {docstring «term~~~_»} {docstring «term¬_»} {docstring «termΣ'_,_»} {docstring «termΣ_,_»} {docstring «term‹_›»} {docstring «term∃_,_»} {docstring «term∅»}
```exceptions And AndOp AndThen BitVec ByteArray Coe CoeDep CoeFun CoeHTC CoeHTCT CoeHead CoeOTC CoeOut CoeSort CoeT CoeTC CoeTail Complement DecidableLE DecidableLT DecidablePred DoResultBC DoResultPR DoResultPRBC DoResultSBC EmptyCollection Eq EquivBEq Equivalence Exists False Float Float32 FloatArray FloatSpec HAndThen HEq HOrElse HasEquiv HasSSubset HasSubset Iff Insert Inter InvImage LawfulHashable LawfulSingleton Max Membership Min MonadEval MonadEvalT MonadShareCommon Ne NonScalar NonemptyType Not Or OrElse OrOp PNonScalar PartialEquivBEq Quot Quotient ReflBEq ReprAtom ReprTuple SDiff SSuperset Sep Setoid ShareCommonM ShareCommonT Singleton Squash Stream Subrelation Subsingleton Substring Superset Thunk ToBool ToStream Trans True Union Vector Xor absurd acc_transGen_iff addParenHeuristic allocprof and_and_and_comm and_and_left and_and_right and_assoc and_comm and_congr and_congr_left and_congr_left' and_congr_left_eq and_congr_left_iff and_congr_right and_congr_right' and_congr_right_eq and_congr_right_iff and_exists_self and_false and_iff_left and_iff_left_iff_imp and_iff_left_of_imp and_iff_right and_iff_right_iff_imp and_iff_right_of_imp and_imp and_left_comm and_not_self and_not_self_iff and_or_left and_or_right and_right_comm and_rotate and_self and_self_iff and_self_left and_self_right and_true apply_dite apply_ite beq_eq_false_iff_ne beq_false beq_false_of_ne beq_iff_eq beq_of_eq beq_self_eq_true beq_self_eq_true' beq_true bind_congr bind_map_left bind_pure bind_pure_unit bne bne_comm bne_eq_false_iff_eq bne_iff_ne bne_self_eq_false bne_self_eq_false' bool boolIfThenElse boolPredToPred boolRelToRel boolToProp boolToPropSimps boolToSort cast cast_cast cast_eq cast_heq coeFunNotation coeNotation coeSortNotation commandDeclare_bitwise_uint_theorems__ commandDeclare_uint_simprocs_ commandDeclare_uint_theorems__ compareLex compareOfLessAndBEq compareOfLessAndEq compareOn cond_false cond_true congr congrArg congrFun dbgSleep dbgStackTrace dbgTrace dbgTraceIfShared dbgTraceVal decEq decPropToBool decidableGetElem? decidable_of_bool decidable_of_decidable_of_eq decidable_of_decidable_of_iff decidable_of_iff decidable_of_iff' decide_eq_decide decide_eq_false decide_eq_false_iff_not decide_eq_true decide_eq_true_eq decide_eq_true_iff decide_false decide_implies decide_ite decide_not decide_true dif_eq_if dif_neg dif_pos dite dite_cond_eq_false dite_cond_eq_true dite_congr dite_else_false dite_else_true dite_eq_ite dite_eq_left_iff dite_eq_right_iff dite_false dite_iff_left_iff dite_iff_right_iff dite_not dite_then_false dite_then_true dite_true dreduceDIte dreduceIte emptyRelation emptyWf eqRec_heq eq_comm eq_false eq_false' eq_false_of_decide eq_false_of_ne_true eq_iff_iff eq_iff_true_of_subsingleton eq_mp_eq_cast eq_mpr_eq_cast eq_of_heq eq_self eq_self_iff_true eq_true eq_true_eq_id eq_true_of_decide eq_true_of_ne_false exists_and_left exists_and_right exists_and_self exists_apply_eq_apply exists_comm exists_congr exists_const exists_eq exists_eq' exists_eq_left exists_eq_left' exists_eq_or_imp exists_eq_right exists_eq_right' exists_eq_right_right exists_eq_right_right' exists_false exists_idem exists_imp exists_or exists_or_eq_left exists_or_eq_left' exists_or_eq_right exists_or_eq_right' exists_prop exists_prop' exists_prop_congr exists_prop_decidable exists_prop_of_true exists_true_left exists₂_congr exists₂_imp exists₃_congr exists₄_congr exists₅_congr false_and false_eq_decide_iff false_iff false_iff_true false_imp_iff false_implies false_ne_true false_of_ne false_of_true_eq_false false_of_true_iff_false false_or flip float32DecLe float32DecLt float32Spec floatDecLe floatDecLt floatSpec forIn'_eq_forIn forall_and forall_apply_eq_imp_iff forall_apply_eq_imp_iff₂ forall_comm forall_congr forall_congr' forall_const forall_eq forall_eq' forall_eq_apply_imp_iff forall_eq_or_imp forall_exists_index forall_false forall_imp forall_not_of_not_exists forall_prop_congr_dom forall_prop_decidable forall_prop_domain_congr forall_prop_of_false forall_prop_of_true forall_self_imp forall₂_congr forall₃_congr forall₄_congr forall₅_congr funext_iff ge_iff_le getElem!_neg getElem!_pos getElem?_eq_none getElem?_neg getElem?_pos getElem_congr getElem_congr_coll getElem_congr_idx get_getElem? gt_iff_lt hash64 hash_eq heq_comm heq_eq_eq heq_of_eq heq_of_eqRec_eq heq_of_eq_of_heq heq_of_heq_of_eq heq_self_iff_true hexDigitRepr id id_def id_eq id_map' if_false if_false_left if_false_right if_neg if_pos if_true if_true_left if_true_right iff_and_self iff_comm iff_congr iff_def iff_def' iff_false iff_false_intro iff_false_left iff_false_right iff_iff_eq iff_iff_implies_and_implies iff_not_self iff_of_eq iff_of_false iff_of_true iff_or_self iff_self iff_self_and iff_self_or iff_true iff_true_intro iff_true_left iff_true_right imp_and imp_congr imp_congr_ctx imp_congr_left imp_congr_right imp_false imp_iff_not imp_iff_right imp_imp_imp imp_intro imp_not_comm imp_not_self imp_self imp_true_iff implies_congr implies_congr_ctx implies_dep_congr_ctx implies_true inline instAddFloat instAddFloat32 instAddISize instAddInt16 instAddInt32 instAddInt64 instAddInt8 instAddNat instAddUInt16 instAddUInt32 instAddUInt64 instAddUInt8 instAddUSize instAlternativeOption instAndOpISize instAndOpInt16 instAndOpInt32 instAndOpInt64 instAndOpInt8 instAndOpUInt16 instAndOpUInt32 instAndOpUInt64 instAndOpUInt8 instAndOpUSize instAppendSubarray instAssociativeAnd instAssociativeBoolAnd instAssociativeBoolOr instAssociativeOr instBEqFloat instBEqFloat32 instBEqOfDecidableEq instBEqOrdering instBEqProd instCoeHTC instCoeHTCOfCoeHeadOfCoeOTC instCoeHTCOfCoeOTC instCoeHTCT instCoeHTCTIntOfIntCast instCoeHTCTNatOfNatCast instCoeHTCTOfCoeHTC instCoeHTCTOfCoeTailOfCoeHTC instCoeOTC instCoeOTCOfCoeOut instCoeOTCOfCoeTC instCoeOutOfCoeFun instCoeOutOfCoeSort instCoeStringError instCoeT instCoeTC instCoeTCOfCoe instCoeTCOfCoe_1 instCoeTOfCoeDep instCoeTOfCoeHTCT instCoeTailIntOfIntCast instCoeTailNatOfNatCast instComplementISize instComplementInt16 instComplementInt32 instComplementInt64 instComplementInt8 instComplementUInt16 instComplementUInt32 instComplementUInt64 instComplementUInt8 instComplementUSize instDecidableAnd instDecidableDite instDecidableEqBitVec instDecidableEqBool instDecidableEqChar instDecidableEqEmpty instDecidableEqFin instDecidableEqISize instDecidableEqInt16 instDecidableEqInt32 instDecidableEqInt64 instDecidableEqInt8 instDecidableEqList instDecidableEqNat instDecidableEqOfIff instDecidableEqPEmpty instDecidableEqPLift instDecidableEqPUnit instDecidableEqPos instDecidableEqProd instDecidableEqString instDecidableEqSum instDecidableEqUInt16 instDecidableEqUInt32 instDecidableEqUInt64 instDecidableEqUInt8 instDecidableEqULift instDecidableEqUSize instDecidableEqVector instDecidableFalse instDecidableForall instDecidableIff instDecidableIte instDecidableLeBitVec instDecidableLeISize instDecidableLeInt16 instDecidableLeInt32 instDecidableLeInt64 instDecidableLeInt8 instDecidableLePos instDecidableLeUInt16 instDecidableLeUInt32 instDecidableLeUInt64 instDecidableLeUInt8 instDecidableLeUSize instDecidableLtBitVec instDecidableLtISize instDecidableLtInt16 instDecidableLtInt32 instDecidableLtInt64 instDecidableLtInt8 instDecidableLtPos instDecidableLtUInt16 instDecidableLtUInt32 instDecidableLtUInt64 instDecidableLtUInt8 instDecidableLtUSize instDecidableNot instDecidableOr instDecidablePredComp instDecidableRelLe instDecidableRelLt instDecidableTrue instDivFloat instDivFloat32 instDivISize instDivInt16 instDivInt32 instDivInt64 instDivInt8 instDivUInt16 instDivUInt32 instDivUInt64 instDivUInt8 instDivUSize instEquivBEqOfLawfulBEq instForInOfForIn' instForInOfStream instFunctorOption instGetElem?OfGetElemOfDecidable instHAdd instHAddPos instHAddPosChar instHAddPosString instHAndOfAndOp instHAndThenOfAndThen instHAppendOfAppend instHDiv instHMod instHModUInt16Nat instHModUInt32Nat instHModUInt64Nat instHModUInt8Nat instHModUSizeNat instHMul instHOrElseOfOrElse instHOrOfOrOp instHPow instHShiftLeftOfShiftLeft instHShiftRightOfShiftRight instHSub instHSubPos instHXorOfXor instHasEquivOfSetoid instHashable instHashableArray instHashableBool instHashableByteArray instHashableChar instHashableFin instHashableInt instHashableList instHashableNat instHashableOption instHashablePos instHashableProd instHashableString instHashableSubtype instHashableUInt16 instHashableUInt32 instHashableUInt64 instHashableUInt8 instHashableUSize instHomogeneousPowFloat instHomogeneousPowFloat32 instIdempotentOpAnd instIdempotentOpBoolAnd instIdempotentOpBoolOr instIdempotentOpOr instInhabitedBool instInhabitedEIO instInhabitedEST instInhabitedExcept instInhabitedExceptTOfMonad instInhabitedFloat instInhabitedFloat32 instInhabitedForInStep instInhabitedForInStep_1 instInhabitedForall instInhabitedForallOfMonad instInhabitedISize instInhabitedInt16 instInhabitedInt32 instInhabitedInt64 instInhabitedInt8 instInhabitedList instInhabitedMProd instInhabitedNat instInhabitedNonScalar instInhabitedNonemptyType instInhabitedOfMonad instInhabitedOption instInhabitedOrdering instInhabitedPNonScalar instInhabitedPProd instInhabitedPUnit instInhabitedPos instInhabitedProd instInhabitedProp instInhabitedReaderT instInhabitedSort instInhabitedStdGen instInhabitedSubstring instInhabitedTask instInhabitedTrue instInhabitedUInt16 instInhabitedUInt32 instInhabitedUInt64 instInhabitedUInt8 instInhabitedUSize instIntCastInt instLEBitVec instLEFin instLEFloat instLEFloat32 instLEISize instLEInt16 instLEInt32 instLEInt64 instLEInt8 instLENat instLEPos instLEUInt16 instLEUInt32 instLEUInt64 instLEUInt8 instLEUSize instLTBitVec instLTFin instLTFloat instLTFloat32 instLTISize instLTInt16 instLTInt32 instLTInt64 instLTInt8 instLTNat instLTOption instLTPos instLTUInt16 instLTUInt32 instLTUInt64 instLTUInt8 instLTUSize instLawfulApplicativeExcept instLawfulApplicativeOption instLawfulBEq instLawfulBEqBool instLawfulBEqChar instLawfulBEqString instLawfulFunctorExcept instLawfulFunctorOption instLawfulGetElem instLawfulHashableOfLawfulBEq instLawfulIdentityAndTrue instLawfulIdentityBoolAndTrue instLawfulIdentityBoolOrFalse instLawfulIdentityOrFalse instLawfulMonadEStateM instLawfulMonadExcept instLawfulMonadOption instLawfulMonadStateRefT' instMaxFloat instMaxFloat32 instMaxISize instMaxInt16 instMaxInt32 instMaxInt64 instMaxInt8 instMaxUInt16 instMaxUInt32 instMaxUInt64 instMaxUInt8 instMaxUSize instMinFloat instMinFloat32 instMinISize instMinInt16 instMinInt32 instMinInt64 instMinInt8 instMinNat instMinUInt16 instMinUInt32 instMinUInt64 instMinUInt8 instMinUSize instModISize instModInt16 instModInt32 instModInt64 instModInt8 instModUInt16 instModUInt32 instModUInt64 instModUInt8 instModUSize instMonadBaseIO instMonadControlExceptTOfMonad instMonadControlOptionTOfMonad instMonadControlReaderT instMonadControlStateRefT' instMonadControlTOfMonadControl instMonadControlTOfPure instMonadEIO instMonadEST instMonadEvalOfMonadLift instMonadEvalT instMonadEvalTOfMonadEval instMonadExceptOfEIO instMonadExceptOfEST instMonadExceptOfExcept instMonadExceptOfExceptT instMonadExceptOfExceptTOfMonad instMonadExceptOfMonadExceptOf instMonadExceptOfUnitOption instMonadFinallyBaseIO instMonadFinallyEIO instMonadFinallyStateRefT' instMonadFunctorTOfMonadFunctor instMonadLiftBaseIOEIO instMonadLiftSTEST instMonadLiftT instMonadLiftTOfMonadLift instMonadOption instMonadReaderOfMonadReaderOf instMonadReaderOfOfMonadLift instMonadReaderOfReaderTOfMonad instMonadST instMonadStateOfMonadStateOf instMonadStateOfOfMonadLift instMonadStateOfStateTOfMonad instMonadWithReaderOfMonadWithReaderOf instMonadWithReaderOfOfMonadFunctor instMonadWithReaderOfReaderT instMulFloat instMulFloat32 instMulISize instMulInt16 instMulInt32 instMulInt64 instMulInt8 instMulNat instMulUInt16 instMulUInt32 instMulUInt64 instMulUInt8 instMulUSize instNatCastInt instNatCastNat instNatPowNat instNeZeroNatIte instNegFloat instNegFloat32 instNegISize instNegInt16 instNegInt32 instNegInt64 instNegInt8 instNonemptyDynamic instNonemptyFloat instNonemptyFloat32 instNonemptyForall instNonemptyMProd instNonemptyOfInhabited instNonemptyOfMonad instNonemptyPProd instNonemptyProd instNonemptyTask instNonemptyTypeName instOfNat instOfNatFloat instOfNatFloat32 instOfNatISize instOfNatInt16 instOfNatInt32 instOfNatInt64 instOfNatInt8 instOfNatNat instOfScientificFloat instOfScientificFloat32 instOrElseEIO instOrElseOfAlternative instOrOpISize instOrOpInt16 instOrOpInt32 instOrOpInt64 instOrOpInt8 instOrOpUInt16 instOrOpUInt32 instOrOpUInt64 instOrOpUInt8 instOrOpUSize instOrdBool instOrdChar instOrdFin instOrdInt instOrdNat instOrdOption instOrdString instOrdUInt16 instOrdUInt32 instOrdUInt64 instOrdUInt8 instOrdUSize instPowNat instPowOfHomogeneousPow instRandomGenStdGen instReprAtomBool instReprAtomChar instReprAtomFloat instReprAtomFloat32 instReprAtomInt instReprAtomNat instReprAtomString instReprAtomUInt16 instReprAtomUInt32 instReprAtomUInt64 instReprAtomUInt8 instReprAtomUSize instReprBool instReprChar instReprDecidable instReprEmpty instReprExcept instReprFin instReprFloat instReprFloat32 instReprId instReprId_1 instReprInt instReprIterator instReprList instReprListOfReprAtom instReprNat instReprOption instReprPUnit instReprPos instReprProdOfReprTuple instReprSSet instReprSigma instReprSourceInfo instReprStdGen instReprString instReprSubarray instReprSubstring instReprSubtype instReprSum instReprTupleOfRepr instReprTupleProdOfRepr instReprUInt16 instReprUInt32 instReprUInt64 instReprUInt8 instReprULift instReprUSize instReprUnit instReprVector instSTWorldEST instSTWorldOfMonadLift instShiftLeftISize instShiftLeftInt16 instShiftLeftInt32 instShiftLeftInt64 instShiftLeftInt8 instShiftLeftUInt16 instShiftLeftUInt32 instShiftLeftUInt64 instShiftLeftUInt8 instShiftLeftUSize instShiftRightISize instShiftRightInt16 instShiftRightInt32 instShiftRightInt64 instShiftRightInt8 instShiftRightUInt16 instShiftRightUInt32 instShiftRightUInt64 instShiftRightUInt8 instShiftRightUSize instSizeOfDefault instSizeOfForallUnit instSizeOfNat instStreamList instStreamProd instStreamRangeNat instStreamSubarray instStreamSubstringChar instSubFloat instSubFloat32 instSubISize instSubInt16 instSubInt32 instSubInt64 instSubInt8 instSubNat instSubUInt16 instSubUInt32 instSubUInt64 instSubUInt8 instSubUSize instSubsingleton instSubsingletonDecidable instSubsingletonEmpty instSubsingletonPEmpty instSubsingletonPLift instSubsingletonPUnit instSubsingletonProd instSubsingletonSquash instSubsingletonStateM instSubsingletonULift instToBoolBool instToBoolOption instToFormatArray instToFormatList instToFormatOfToString instToFormatOption instToFormatPos instToFormatProd instToStreamArraySubarray instToStreamList instToStreamRange instToStreamStringSubstring instToStreamSubarray instToStringBool instToStringByteArray instToStringChar instToStringDecidable instToStringExcept instToStringFin instToStringFloat instToStringFloat32 instToStringFloatArray instToStringFormat instToStringISize instToStringId instToStringId_1 instToStringInt instToStringInt16 instToStringInt32 instToStringInt64 instToStringInt8 instToStringIterator instToStringList instToStringNat instToStringOption instToStringPUnit instToStringPos instToStringProd instToStringSigma instToStringString instToStringSubarray instToStringSubstring instToStringSubtype instToStringSum instToStringUInt16 instToStringUInt32 instToStringUInt64 instToStringUInt8 instToStringULift instToStringUSize instToStringUnit instTransEq instTransEq_1 instTransIff instWellFoundedRelationOfSizeOf instXorISize instXorInt16 instXorInt32 instXorInt64 instXorInt8 instXorUInt16 instXorUInt32 instXorUInt64 instXorUInt8 instXorUSize isExclusiveUnsafe isSome_getElem? isValidChar ite iteInduction ite_cond_eq_false ite_cond_eq_true ite_congr ite_else_decide_not_self ite_else_decide_self ite_else_not_self ite_else_self ite_eq_ite ite_eq_left_iff ite_eq_right_iff ite_false ite_id ite_iff_ite ite_iff_left_iff ite_iff_right_iff ite_not ite_self ite_then_decide_not_self ite_then_decide_self ite_then_not_self ite_then_self ite_true lcCast lcErased lcProof lcUnreachable leOfOrd le_of_eq_of_le le_of_le_of_eq le_usize_size letFun letFun_body_congr letFun_congr letFun_unused letFun_val_congr let_body_congr let_congr let_val_congr lexOrd liftExcept liftM liftOption ltOfOrd lt_of_eq_of_lt lt_of_lt_of_eq map_bind map_congr map_eq_pure_bind maxOfLe measure minOfLe mixHash mkRecOn monadFunctorRefl monadLift_self mt namedPattern neZero_iff neZero_zero_iff_false ne_comm ne_eq ne_false_of_eq_true ne_false_of_self ne_of_apply_ne ne_of_beq_false ne_of_mem_of_not_mem ne_of_mem_of_not_mem' ne_self_iff_false ne_true_of_eq_false ne_true_of_not neq_of_not_iff noConfusionEnum noConfusionTypeEnum nonempty_of_exists nonempty_prop not_and not_and' not_and_of_not_left not_and_of_not_or_not not_and_of_not_right not_and_self not_and_self_iff not_congr not_decide_eq_true not_exists not_exists_of_forall_not not_false not_false_eq_true not_false_iff not_forall_of_exists_not not_iff_false_intro not_iff_self not_imp_of_and_not not_not_em not_not_intro not_not_not not_not_of_not_imp not_of_iff_false not_of_not_imp not_or not_or_intro not_true not_true_eq_false observing ofBoolUsing_eq_false ofBoolUsing_eq_true of_decide_eq_false of_decide_eq_self_eq_true of_decide_eq_true of_eq_false of_eq_true of_iff_true optParam_eq optionCoe or_and_left or_and_right or_assoc or_comm or_congr or_congr_left or_congr_right or_false or_iff_left or_iff_left_iff_imp or_iff_left_of_imp or_iff_right or_iff_right_iff_imp or_iff_right_of_imp or_imp or_left_comm or_or_distrib_left or_or_distrib_right or_or_or_comm or_right_comm or_rotate or_self or_self_iff or_self_left or_self_right or_true outOfBounds outOfBounds_eq_default panic panicCore panicWithPos panicWithPosWithDecl peirce' pi_congr precArg precLead precMax precMin precMin1 prioDefault prioHigh prioLow prioMid proof_irrel proof_irrel_heq propext_iff ptrAddrUnsafe ptrEq ptrEqList pure_id_seq rawNatLit recSubsingleton reduceCtorEq reduceDIte reduceIte repr reprArg reprStr rfl seqLeft_eq_bind seqRight_eq_bind seq_eq_bind seq_eq_bind_map shareCommonM sizeOfWFRel sizeOf_default sizeOf_nat sizeOf_thunk sorryAx strictAnd strictOr stx!_ stx_? subtypeCoe tacticClean_wf tacticDecreasing_tactic tacticDecreasing_trivial tacticDecreasing_trivial_pre_omega tacticDecreasing_with_ tacticFunext___ tacticGet_elem_tactic tacticGet_elem_tactic_trivial tacticSimp_wf term!_ termDepIfThenElse termIfLet termIfThenElse termMax_prec termPrintln!__ termS!_ termWithout_expected_type_ thunkCoe timeit toBoolUsing toBoolUsing_eq_true toLBoolM toLOptionM trivial true_and true_eq_decide_iff true_eq_false_of_false true_iff true_iff_false true_imp_iff true_implies true_ne_false true_or tryFinally type_eq_of_heq unexpandArrayEmpty unexpandEqNDRec unexpandEqRec unexpandExists unexpandGetElem unexpandGetElem! unexpandGetElem? unexpandIte unexpandListCons unexpandListNil unexpandListToArray unexpandMkArray0 unexpandMkArray1 unexpandMkArray2 unexpandMkArray3 unexpandMkArray4 unexpandMkArray5 unexpandMkArray6 unexpandMkArray7 unexpandMkArray8 unexpandPSigma unexpandProdMk unexpandSigma unexpandSubtype unexpandTSepArray unexpandTSyntax unexpandTSyntaxArray unexpandUnit unsafeBaseIO unsafeCast unsafeEIO unsafeIO usize_size_eq usize_size_le usize_size_pos withPtrAddr withPtrAddrUnsafe withPtrEq withPtrEqDecEq withPtrEqUnsafe withShareCommon «prec(_)» «prio(_)» «stx_*» «stx_+» «stx_,*,?» «stx_,*» «stx_,+,?» «stx_,+» «stx_<|>_» «tacticBy_cases_:_» «term#[_,]» «term%[_|_]» «term-_» «termExists_,_» «term[_]» «term_!=_» «term_$__» «term_%_» «term_&&&_» «term_&&_» «term_*>_» «term_*_» «term_++_» «term_+_» «term_-_» «term_/\_» «term_/_» «term_::_» «term_<$>_» «term_<&&>_» «term_<&>_» «term_<*>_» «term_<*_» «term_<->_» «term_<<<_» «term_<=<_» «term_<=_» «term_<_» «term_<|>_» «term_<|_» «term_<||>_» «term_=<<_» «term_==_» «term_=_» «term_>=>_» «term_>=_» «term_>>=_» «term_>>>_» «term_>>_» «term_>_» «term_\/_» «term_\_» «term_^^^_» «term_^_» «term__[_]'_» «term__[_]_!» «term__[_]_?» «term__[_]» «term_|>_» «term_||_» «term_|||_» «term_×'__1» «term_×'_» «term_×__1» «term_×_» «term_↔_» «term_∈_» «term_∉_» «term_∘_» «term_∣_» «term_∧_» «term_∨_» «term_∩_» «term_∪_» «term_≈_» «term_≠_» «term_≤_» «term_≥_» «term_⊂_» «term_⊃_» «term_⊆_» «term_⊇_» «term_⊕'_» «term_⊕_» «term{_:_//_}» «term{_}» «term{}» «term~~~_» «term¬_» «termΣ'_,_» «termΣ_,_» «term‹_›» «term∃_,_» «term∅» ```
- Tactics
Lean.Parser.Tactic.acNf0, Lean.Parser.Tactic.grind, Lean.Parser.Tactic.tacticAc_nf_, Lean.Parser.Tactic.classical
{docstring Lean.Parser.Tactic.acNf0} {docstring Lean.Parser.Tactic.grind} {docstring Lean.Parser.Tactic.tacticAc_nf_} {docstring Lean.Parser.Tactic.classical}
```exceptions Lean.Parser.Tactic.acNf0 Lean.Parser.Tactic.grind Lean.Parser.Tactic.tacticAc_nf_ Lean.Parser.Tactic.classical ```