Index

Symbols

  1. ( ... )
  2. . ...
  3. <;> (0) (1)
  4. _private.Init.Dynamic.0.TypeName.mk'
    1. Instance constructor of Type­Name
  5. { ... }
  6. ·
  7. · ...
  8. ι-reduction

A

  1. Add
  2. Add.mk
    1. Instance constructor of Add
  3. Alternative
  4. Alternative.mk
    1. Instance constructor of Alternative
  5. Append
  6. Append.mk
    1. Instance constructor of Append
  7. Applicative
  8. Applicative.mk
    1. Instance constructor of Applicative
  9. Array
  10. Array.all
  11. Array.all­Diff
  12. Array.all­M
  13. Array.any
  14. Array.any­M
  15. Array.append
  16. Array.append­List
  17. Array.attach
  18. Array.attach­With
  19. Array.back
  20. Array.back!
  21. Array.back?
  22. Array.bin­Insert
  23. Array.bin­Insert­M
  24. Array.bin­Search
  25. Array.bin­Search­Contains
  26. Array.concat­Map
  27. Array.concat­Map­M
  28. Array.contains
  29. Array.elem
  30. Array.empty
  31. Array.erase
  32. Array.erase­Idx
  33. Array.erase­Reps
  34. Array.extract
  35. Array.filter
  36. Array.filter­M
  37. Array.filter­Map
  38. Array.filter­Map­M
  39. Array.filter­Pairs­M
  40. Array.filter­Sep­Elems
  41. Array.filter­Sep­Elems­M
  42. Array.find?
  43. Array.find­Idx?
  44. Array.find­Idx­M?
  45. Array.find­M?
  46. Array.find­Rev?
  47. Array.find­Rev­M?
  48. Array.find­Some!
  49. Array.find­Some?
  50. Array.find­Some­M?
  51. Array.find­Some­Rev?
  52. Array.find­Some­Rev­M?
  53. Array.flat­Map
  54. Array.flat­Map­M
  55. Array.flatten
  56. Array.foldl
  57. Array.foldl­M
  58. Array.foldr
  59. Array.foldr­M
  60. Array.for­In'
  61. Array.for­M
  62. Array.for­Rev­M
  63. Array.get
  64. Array.get!
  65. Array.get?
  66. Array.get­D
  67. Array.get­Even­Elems
  68. Array.get­Idx?
  69. Array.get­Max?
  70. Array.group­By­Key
  71. Array.index­Of?
  72. Array.insert­At
  73. Array.insert­At!
  74. Array.insertion­Sort
  75. Array.is­Empty
  76. Array.is­Eqv
  77. Array.is­Prefix­Of
  78. Array.map
  79. Array.map­Fin­Idx
  80. Array.map­Fin­Idx­M
  81. Array.map­Idx
  82. Array.map­Idx­M
  83. Array.map­Indexed
  84. Array.map­Indexed­M
  85. Array.map­M
  86. Array.map­M'
  87. Array.map­Mono
  88. Array.map­Mono­M
  89. Array.mk
    1. Constructor of Array
  90. Array.mk­Array
  91. Array.modify
  92. Array.modify­M
  93. Array.modify­Op
  94. Array.of­Fn
  95. Array.of­Subarray
  96. Array.partition
  97. Array.pop
  98. Array.pop­While
  99. Array.push
  100. Array.qsort
  101. Array.qsort­Ord
  102. Array.range
  103. Array.reduce­Get­Elem
  104. Array.reduce­Get­Elem!
  105. Array.reduce­Get­Elem?
  106. Array.reduce­Option
  107. Array.reverse
  108. Array.sequence­Map
  109. Array.set
  110. Array.set!
  111. Array.set­D
  112. Array.singleton
  113. Array.size
  114. Array.split
  115. Array.swap
  116. Array.swap!
  117. Array.swap­At
  118. Array.swap­At!
  119. Array.take
  120. Array.take­While
  121. Array.to­List
  122. Array.to­List­Append
  123. Array.to­List­Rev
  124. Array.to­PArray'
  125. Array.to­Subarray
  126. Array.uget
  127. Array.unattach
  128. Array.unzip
  129. Array.uset
  130. Array.usize
  131. Array.zip
  132. Array.zip­With
  133. Array.zip­With­Index
  134. ac_rfl
  135. accessed
    1. IO.FS.Metadata.accessed (structure field)
  136. adapt
    1. ExceptT.adapt
    2. ReaderT.adapt
  137. adapt­Except
    1. EStateM.adapt­Except
  138. adapt­Expander
    1. Lean.Elab.Tactic.adapt­Expander
  139. add
    1. Add.add (class method)
    2. Nat.add
  140. add­Extension
    1. System.FilePath.add­Extension
  141. add­Heartbeats
    1. IO.add­Heartbeats
  142. add­Macro­Scope
    1. Lean.Macro.add­Macro­Scope
  143. admit
  144. all
    1. Array.all
    2. Nat.all
    3. String.all
    4. Subarray.all
  145. all­Diff
    1. Array.all­Diff
  146. all­M
    1. Array.all­M
    2. Nat.all­M
    3. Subarray.all­M
  147. all­TR
    1. Nat.all­TR
  148. all_goals (0) (1)
  149. and
    1. Bool.and
  150. and­M
  151. and_intros
  152. any
    1. Array.any
    2. Nat.any
    3. String.any
    4. Subarray.any
  153. any­M
    1. Array.any­M
    2. Nat.any­M
    3. Subarray.any­M
  154. any­TR
    1. Nat.any­TR
  155. any_goals (0) (1)
  156. app­Dir
    1. IO.app­Dir
  157. app­Path
    1. IO.app­Path
  158. append
    1. Append.append (class method)
    2. Array.append
    3. String.append
  159. append­Goals
    1. Lean.Elab.Tactic.append­Goals
  160. append­List
    1. Array.append­List
  161. apply (0) (1)
  162. apply?
  163. apply­Eq­Lemma
    1. Nat.apply­Eq­Lemma
  164. apply­Simproc­Const
    1. Nat.apply­Simproc­Const
  165. apply_assumption
  166. apply_ext_theorem
  167. apply_mod_cast
  168. apply_rfl
  169. apply_rules
  170. arg [@]i
  171. args
    1. [anonymous] (structure field)
  172. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  173. array
    1. Subarray.array (structure field)
  174. array_get_dec
  175. as­Task
    1. BaseIO.as­Task
    2. EIO.as­Task
    3. IO.as­Task
  176. assumption
    1. inaccessible
  177. assumption_mod_cast
  178. at­End
    1. String.Iterator.at­End
    2. String.at­End
  179. at­Least­Two
    1. Bool.at­Least­Two
  180. attach
    1. Array.attach
  181. attach­With
    1. Array.attach­With
  182. auto­Lift
  183. auto­Param
  184. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  185. auto­Unfold
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
    2. Lean.Meta.Simp.Config.auto­Unfold (structure field)

B

  1. BEq
  2. BEq.mk
    1. Instance constructor of BEq
  3. Backtrackable
    1. EStateM.Backtrackable
  4. Base­IO
  5. BaseIO.as­Task
  6. BaseIO.bind­Task
  7. BaseIO.map­Task
  8. BaseIO.map­Tasks
  9. BaseIO.to­EIO
  10. BaseIO.to­IO
  11. Bind
  12. Bind.bind­Left
  13. Bind.kleisli­Left
  14. Bind.kleisli­Right
  15. Bind.mk
    1. Instance constructor of Bind
  16. Bool
  17. Bool.and
  18. Bool.at­Least­Two
  19. Bool.dec­Eq
  20. Bool.false
    1. Constructor of Bool
  21. Bool.not
  22. Bool.or
  23. Bool.to­ISize
  24. Bool.to­Int16
  25. Bool.to­Int32
  26. Bool.to­Int64
  27. Bool.to­Int8
  28. Bool.to­Nat
  29. Bool.to­UInt16
  30. Bool.to­UInt32
  31. Bool.to­UInt64
  32. Bool.to­UInt8
  33. Bool.to­USize
  34. Bool.true
    1. Constructor of Bool
  35. Bool.xor
  36. Buffer
    1. IO.FS.Stream.Buffer
  37. back
    1. Array.back
    2. String.back
  38. back!
    1. Array.back!
  39. back?
    1. Array.back?
  40. backward.synthInstance.canon­Instances
  41. below
    1. Nat.below
  42. beq
    1. BEq.beq (class method)
    2. Nat.beq
  43. beta
    1. Lean.Meta.DSimp.Config.beta (structure field)
    2. Lean.Meta.Simp.Config.beta (structure field)
  44. bin­Insert
    1. Array.bin­Insert
  45. bin­Insert­M
    1. Array.bin­Insert­M
  46. bin­Search
    1. Array.bin­Search
  47. bin­Search­Contains
    1. Array.bin­Search­Contains
  48. bind
    1. Bind.bind (class method)
    2. EStateM.bind
    3. Except.bind
    4. ExceptT.bind
    5. OptionT.bind
    6. ReaderT.bind
    7. StateT.bind
  49. bind­Cont
    1. ExceptT.bind­Cont
  50. bind­Left
    1. Bind.bind­Left
  51. bind­Task
    1. BaseIO.bind­Task
    2. EIO.bind­Task
    3. IO.bind­Task
  52. bind_assoc
    1. [anonymous] (class method)
  53. bind_map
    1. [anonymous] (class method)
  54. bind_pure_comp
    1. [anonymous] (class method)
  55. bitwise
    1. Nat.bitwise
  56. ble
    1. Nat.ble
  57. blt
    1. Nat.blt
  58. bootstrap.inductive­Check­Resulting­Universe
  59. bv_check
  60. bv_decide
  61. bv_decide?
  62. bv_normalize
  63. bv_omega
  64. by­Cases
    1. Decidable.by­Cases
  65. by_cases
  66. byte­Idx
    1. String.Pos.byte­Idx (structure field)
  67. byte­Size
    1. IO.FS.Metadata.byte­Size (structure field)

C

  1. Char
  2. Char.is­Alpha
  3. Char.is­Alphanum
  4. Char.is­Digit
  5. Char.is­Lower
  6. Char.is­Upper
  7. Char.is­Whitespace
  8. Char.mk
    1. Constructor of Char
  9. Char­Lit
    1. Lean.Syntax.Char­Lit
  10. Child
    1. IO.Process.Child
  11. Command
    1. Lean.Syntax.Command
  12. Config
    1. Lean.Meta.DSimp.Config
    2. Lean.Meta.Rewrite.Config
    3. Lean.Meta.Simp.Config
  13. calc
  14. cancel
    1. IO.cancel
  15. canon­Instances
    1. backward.synthInstance.canon­Instances
  16. capitalize
    1. String.capitalize
  17. case
  18. case ... => ...
  19. case'
  20. case' ... => ...
  21. case­Strong­Induction­On
    1. Nat.case­Strong­Induction­On
  22. cases
  23. cases­On
    1. Nat.cases­On
  24. cast
    1. Nat.cast
  25. catch­Exceptions
    1. EIO.catch­Exceptions
  26. change (0) (1)
  27. change ... with ...
  28. char­Lit­Kind
    1. Lean.char­Lit­Kind
  29. check­Canceled
    1. IO.check­Canceled
  30. checkpoint
  31. choice­Kind
    1. Lean.choice­Kind
  32. clear
  33. close­Main­Goal
    1. Lean.Elab.Tactic.close­Main­Goal
  34. close­Main­Goal­Using
    1. Lean.Elab.Tactic.close­Main­Goal­Using
  35. cmd
    1. [anonymous] (structure field)
  36. codepoint­Pos­To­Utf16Pos
    1. String.codepoint­Pos­To­Utf16Pos
  37. codepoint­Pos­To­Utf16Pos­From
    1. String.codepoint­Pos­To­Utf16Pos­From
  38. codepoint­Pos­To­Utf8Pos­From
    1. String.codepoint­Pos­To­Utf8Pos­From
  39. col­Eq
  40. col­Ge
  41. col­Gt
  42. comment
    1. block
    2. line
  43. comp_map
    1. LawfulFunctor.comp_map (class method)
  44. compare
    1. Ord.compare (class method)
  45. components
    1. System.FilePath.components
  46. concat­Map
    1. Array.concat­Map
  47. concat­Map­M
    1. Array.concat­Map­M
  48. cond
  49. configuration
    1. of tactics
  50. congr (0) (1)
  51. constructor (0) (1)
  52. contains
    1. Array.contains
    2. String.contains
  53. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  54. contradiction
  55. control
  56. control­At
  57. conv
  58. conv => ...
  59. conv' (0) (1)
  60. create­Dir
    1. IO.FS.create­Dir
  61. create­Dir­All
    1. IO.FS.create­Dir­All
  62. create­Temp­File
    1. IO.FS.create­Temp­File
  63. crlf­To­Lf
    1. String.crlf­To­Lf
  64. csize
    1. String.csize
  65. cumulativity
  66. curr
    1. String.Iterator.curr
  67. current­Dir
    1. IO.current­Dir
  68. custom­Eliminators
    1. tactic.custom­Eliminators
  69. cwd
    1. [anonymous] (structure field)

D

  1. Decidable
  2. Decidable.by­Cases
  3. Decidable.decide
  4. Decidable.is­False
    1. Constructor of Decidable
  5. Decidable.is­True
    1. Constructor of Decidable
  6. Decidable­Eq
  7. Decidable­Rel
  8. Dir­Entry
    1. IO.FS.Dir­Entry
  9. Div
  10. Div.mk
    1. Instance constructor of Div
  11. Dvd
  12. Dvd.mk
    1. Instance constructor of Dvd
  13. Dynamic
  14. Dynamic.get?
  15. Dynamic.mk
  16. data
    1. IO.FS.Stream.Buffer.data
    2. IO.FS.Stream.Buffer.data (structure field)
    3. String.data (structure field)
    4. _private.Init.Dynamic.0.TypeName.data (class method)
  17. dbg_cache
    1. tactic.dbg_cache
  18. dbg_trace
  19. dec­Eq
    1. Bool.dec­Eq
    2. Nat.dec­Eq
    3. String.dec­Eq
  20. dec­Le
    1. Nat.dec­Le
  21. dec­Lt
    1. Nat.dec­Lt
  22. decapitalize
    1. String.decapitalize
  23. decidable
  24. decide
    1. Decidable.decide
    2. Lean.Meta.DSimp.Config.decide (structure field)
    3. Lean.Meta.Simp.Config.decide (structure field)
  25. decreasing_tactic
  26. decreasing_trivial
  27. decreasing_with
  28. dedicated
    1. Task.Priority.dedicated
  29. deep­Terms
    1. pp.deep­Terms
  30. default
    1. Inhabited.default (class method)
    2. Task.Priority.default
  31. delta (0) (1)
  32. digit­Char
    1. Nat.digit­Char
  33. discard
    1. Functor.discard
  34. discharge
    1. trace.Meta.Tactic.simp.discharge
  35. div
    1. Div.div (class method)
    2. Nat.div
  36. div2Induction
    1. Nat.div2Induction
  37. done (0) (1)
  38. down
    1. PLift.down (structure field)
    2. ULift.down (structure field)
  39. drop
    1. String.drop
    2. Subarray.drop
  40. drop­Right
    1. String.drop­Right
  41. drop­Right­While
    1. String.drop­Right­While
  42. drop­While
    1. String.drop­While
  43. dsimp (0) (1)
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  44. dsimp!
  45. dsimp?
  46. dsimp?!
  47. dsimp­Location'
    1. Lean.Elab.Tactic.dsimp­Location'
  48. dvd
    1. Dvd.dvd (class method)

E

  1. EIO
  2. EIO.as­Task
  3. EIO.bind­Task
  4. EIO.catch­Exceptions
  5. EIO.map­Task
  6. EIO.map­Tasks
  7. EIO.to­Base­IO
  8. EIO.to­IO
  9. EIO.to­IO'
  10. EST
  11. EState­M
  12. EStateM.Backtrackable
  13. EStateM.Backtrackable.mk
    1. Instance constructor of EStateM.Backtrackable
  14. EStateM.Result
  15. EStateM.Result.error
    1. Constructor of EStateM.Result
  16. EStateM.Result.ok
    1. Constructor of EStateM.Result
  17. EStateM.adapt­Except
  18. EStateM.bind
  19. EStateM.from­State­M
  20. EStateM.get
  21. EStateM.map
  22. EStateM.modify­Get
  23. EStateM.non­Backtrackable
  24. EStateM.or­Else
  25. EStateM.or­Else'
  26. EStateM.pure
  27. EStateM.run
  28. EStateM.run'
  29. EStateM.seq­Right
  30. EStateM.set
  31. EStateM.throw
  32. EStateM.try­Catch
  33. Empty
  34. Error
    1. IO.Error
  35. Even
  36. Even.plus­Two
    1. Constructor of Even
  37. Even.zero
    1. Constructor of Even
  38. Except
  39. Except.bind
  40. Except.error
    1. Constructor of Except
  41. Except.is­Ok
  42. Except.map
  43. Except.map­Error
  44. Except.ok
    1. Constructor of Except
  45. Except.or­Else­Lazy
  46. Except.pure
  47. Except.to­Bool
  48. Except.to­Option
  49. Except.try­Catch
  50. Except­Cps­T
  51. Except­CpsT.lift
  52. Except­CpsT.run
  53. Except­CpsT.run­Catch
  54. Except­CpsT.run­K
  55. Except­T
  56. ExceptT.adapt
  57. ExceptT.bind
  58. ExceptT.bind­Cont
  59. ExceptT.lift
  60. ExceptT.map
  61. ExceptT.mk
  62. ExceptT.pure
  63. ExceptT.run
  64. ExceptT.try­Catch
  65. elab­Cases­Targets
    1. Lean.Elab.Tactic.elab­Cases­Targets
  66. elab­DSimp­Config­Core
    1. Lean.Elab.Tactic.elab­DSimp­Config­Core
  67. elab­Simp­Args
    1. Lean.Elab.Tactic.elab­Simp­Args
  68. elab­Simp­Config
    1. Lean.Elab.Tactic.elab­Simp­Config
  69. elab­Simp­Config­Ctx­Core
    1. Lean.Elab.Tactic.elab­Simp­Config­Ctx­Core
  70. elab­Term
    1. Lean.Elab.Tactic.elab­Term
  71. elab­Term­Ensuring­Type
    1. Lean.Elab.Tactic.elab­Term­Ensuring­Type
  72. elab­Term­With­Holes
    1. Lean.Elab.Tactic.elab­Term­With­Holes
  73. elem
    1. Array.elem
  74. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  75. elim­Offset
    1. Nat.elim­Offset
  76. empty
    1. Array.empty
    2. Subarray.empty
  77. end­Pos
    1. String.end­Pos
  78. ends­With
    1. String.ends­With
  79. ensure­Has­No­MVars
    1. Lean.Elab.Tactic.ensure­Has­No­MVars
  80. enter
  81. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  82. eprint
    1. IO.eprint
  83. eprintln
    1. IO.eprintln
  84. eq_of_beq
    1. LawfulBEq.eq_of_beq (class method)
  85. eq_refl
  86. erase
    1. Array.erase
  87. erase­Idx
    1. Array.erase­Idx
  88. erase­Reps
    1. Array.erase­Reps
  89. erw (0) (1)
  90. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.eta (structure field)
  91. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
    2. Lean.Meta.Simp.Config.eta­Struct (structure field)
  92. exact
  93. exact?
  94. exact_mod_cast
  95. exe­Extension
    1. System.FilePath.exe­Extension
  96. exfalso
  97. exists
  98. exit
    1. IO.Process.exit
  99. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  100. expand­Macro?
    1. Lean.Macro.expand­Macro?
  101. ext (0) (1)
  102. ext1
  103. ext­Separator
    1. System.FilePath.ext­Separator
  104. extension
    1. System.FilePath.extension
  105. extensionality
    1. of propositions
  106. extract
    1. Array.extract
    2. String.Iterator.extract
    3. String.extract

F

  1. File­Path
    1. System.File­Path
  2. File­Right
    1. IO.File­Right
  3. Fin
  4. Fin.mk
    1. Constructor of Fin
  5. For­In
  6. For­In'
  7. ForIn'.mk
    1. Instance constructor of For­In'
  8. ForIn.mk
    1. Instance constructor of For­In
  9. For­In­Step
  10. For­InStep.done
    1. Constructor of For­In­Step
  11. For­InStep.yield
    1. Constructor of For­In­Step
  12. For­M
  13. ForM.for­In
  14. ForM.mk
    1. Instance constructor of For­M
  15. Functor
  16. Functor.discard
  17. Functor.map­Rev
  18. Functor.mk
    1. Instance constructor of Functor
  19. fail
    1. OptionT.fail
  20. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
    2. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  21. fail_if_success (0) (1)
  22. failure
    1. ReaderT.failure
    2. StateT.failure
    3. [anonymous] (class method)
  23. false_or_by_contra
  24. field­Idx­Kind
    1. Lean.field­Idx­Kind
  25. field­Notation
    1. pp.field­Notation
  26. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
    2. System.FilePath.file­Name
  27. file­Stem
    1. System.FilePath.file­Stem
  28. filter
    1. Array.filter
  29. filter­M
    1. Array.filter­M
  30. filter­Map
    1. Array.filter­Map
  31. filter­Map­M
    1. Array.filter­Map­M
  32. filter­Pairs­M
    1. Array.filter­Pairs­M
  33. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  34. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  35. find
    1. String.find
  36. find?
    1. Array.find?
  37. find­Idx?
    1. Array.find­Idx?
  38. find­Idx­M?
    1. Array.find­Idx­M?
  39. find­Line­Start
    1. String.find­Line­Start
  40. find­M?
    1. Array.find­M?
  41. find­Rev?
    1. Array.find­Rev?
    2. Subarray.find­Rev?
  42. find­Rev­M?
    1. Array.find­Rev­M?
    2. Subarray.find­Rev­M?
  43. find­Some!
    1. Array.find­Some!
  44. find­Some?
    1. Array.find­Some?
  45. find­Some­M?
    1. Array.find­Some­M?
  46. find­Some­Rev?
    1. Array.find­Some­Rev?
  47. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
    2. Subarray.find­Some­Rev­M?
  48. first (0) (1)
  49. first­Diff­Pos
    1. String.first­Diff­Pos
  50. flags
    1. IO.FileRight.flags
  51. flat­Map
    1. Array.flat­Map
  52. flat­Map­M
    1. Array.flat­Map­M
  53. flatten
    1. Array.flatten
  54. flush
    1. IO.FS.Handle.flush
    2. IO.FS.Stream.flush (structure field)
  55. focus (0) (1)
    1. Lean.Elab.Tactic.focus
  56. fold
    1. Nat.fold
  57. fold­M
    1. Nat.fold­M
  58. fold­Rev
    1. Nat.fold­Rev
  59. fold­Rev­M
    1. Nat.fold­Rev­M
  60. fold­TR
    1. Nat.fold­TR
  61. foldl
    1. Array.foldl
    2. String.foldl
    3. Subarray.foldl
  62. foldl­M
    1. Array.foldl­M
    2. Subarray.foldl­M
  63. foldr
    1. Array.foldr
    2. String.foldr
    3. Subarray.foldr
  64. foldr­M
    1. Array.foldr­M
    2. Subarray.foldr­M
  65. fopen­Error­To­String
    1. IO.Error.fopen­Error­To­String
  66. for­In
    1. ForIn.for­In (class method)
    2. ForM.for­In
    3. Subarray.for­In
  67. for­In'
    1. Array.for­In'
    2. ForIn'.for­In' (class method)
  68. for­M
    1. Array.for­M
    2. ForM.for­M (class method)
    3. Nat.for­M
    4. Subarray.for­M
  69. for­Rev­M
    1. Array.for­Rev­M
    2. Nat.for­Rev­M
    3. Subarray.for­Rev­M
  70. forward
    1. String.Iterator.forward
  71. from­Expr?
    1. Nat.from­Expr?
    2. String.from­Expr?
  72. from­State­M
    1. EStateM.from­State­M
  73. from­UTF8
    1. String.from­UTF8
  74. from­UTF8!
    1. String.from­UTF8!
  75. from­UTF8?
    1. String.from­UTF8?
  76. front
    1. String.front
  77. fst
    1. MProd.fst (structure field)
    2. PProd.fst (structure field)
    3. PSigma.fst (structure field)
    4. Prod.fst (structure field)
    5. Sigma.fst (structure field)
  78. fun
  79. funext (0) (1)

G

  1. Get­Elem
  2. GetElem.mk
    1. Instance constructor of Get­Elem
  3. Get­Elem?
  4. GetElem?.mk
    1. Instance constructor of Get­Elem?
  5. gcd
    1. Nat.gcd
  6. generalize
  7. get
    1. Array.get
    2. EStateM.get
    3. MonadState.get
    4. MonadState.get (class method)
    5. Monad­StateOf.get (class method)
    6. ST.Ref.get
    7. State­RefT'.get
    8. StateT.get
    9. String.get
    10. Subarray.get
    11. Task.get
    12. Task.get (structure field)
  8. get!
    1. Array.get!
    2. String.get!
    3. Subarray.get!
  9. get'
    1. String.get'
  10. get?
    1. Array.get?
    2. Dynamic.get?
    3. String.get?
  11. get­Char
    1. Lean.TSyntax.get­Char
  12. get­Curr­Macro­Scope
    1. Lean.Elab.Tactic.get­Curr­Macro­Scope
  13. get­Curr­Namespace
    1. Lean.Macro.get­Curr­Namespace
  14. get­Current­Dir
    1. IO.Process.get­Current­Dir
  15. get­D
    1. Array.get­D
    2. Subarray.get­D
  16. get­Elem
    1. GetElem.get­Elem (class method)
  17. get­Elem!
    1. GetElem?.get­Elem? (class method)
  18. get­Elem!_def
    1. Lawful­GetElem.get­Elem!_def (class method)
  19. get­Elem?
    1. [anonymous] (class method)
  20. get­Elem?_def
    1. Lawful­GetElem.get­Elem?_def (class method)
  21. get­Env
    1. IO.get­Env
  22. get­Even­Elems
    1. Array.get­Even­Elems
  23. get­FVar­Id
    1. Lean.Elab.Tactic.get­FVar­Id
  24. get­FVar­Ids
    1. Lean.Elab.Tactic.get­FVar­Ids
  25. get­Goals
    1. Lean.Elab.Tactic.get­Goals
  26. get­Hygiene­Info
    1. Lean.TSyntax.get­Hygiene­Info
  27. get­Id
    1. Lean.TSyntax.get­Id
  28. get­Idx?
    1. Array.get­Idx?
  29. get­Kind
    1. Lean.Syntax.get­Kind
  30. get­Line
    1. IO.FS.Handle.get­Line
    2. IO.FS.Stream.get­Line (structure field)
  31. get­Main­Goal
    1. Lean.Elab.Tactic.get­Main­Goal
  32. get­Main­Module
    1. Lean.Elab.Tactic.get­Main­Module
  33. get­Main­Tag
    1. Lean.Elab.Tactic.get­Main­Tag
  34. get­Max?
    1. Array.get­Max?
  35. get­Modify
  36. get­Name
    1. Lean.TSyntax.get­Name
  37. get­Nat
    1. Lean.TSyntax.get­Nat
  38. get­Num­Heartbeats
    1. IO.get­Num­Heartbeats
  39. get­PID
    1. IO.Process.get­PID
  40. get­Random­Bytes
    1. IO.get­Random­Bytes
  41. get­Scientific
    1. Lean.TSyntax.get­Scientific
  42. get­Stderr
    1. IO.get­Stderr
  43. get­Stdin
    1. IO.get­Stdin
  44. get­Stdout
    1. IO.get­Stdout
  45. get­String
    1. Lean.TSyntax.get­String
  46. get­Task­State
    1. IO.get­Task­State
  47. get­The
  48. get­Unsolved­Goals
    1. Lean.Elab.Tactic.get­Unsolved­Goals
  49. get­Utf8Byte
    1. String.get­Utf8Byte
  50. get_elem_tactic
  51. get_elem_tactic_trivial
  52. goal
    1. main
  53. ground
    1. Lean.Meta.Simp.Config.ground (structure field)
  54. group
    1. IO.FileRight.group (structure field)
  55. group­By­Key
    1. Array.group­By­Key
  56. group­Kind
    1. Lean.group­Kind
  57. guard
  58. guard_expr
  59. guard_hyp
  60. guard_target

H

  1. HAdd
  2. HAdd.mk
    1. Instance constructor of HAdd
  3. HAnd
  4. HAnd.mk
    1. Instance constructor of HAnd
  5. HAppend
  6. HAppend.mk
    1. Instance constructor of HAppend
  7. HDiv
  8. HDiv.mk
    1. Instance constructor of HDiv
  9. HMod
  10. HMod.mk
    1. Instance constructor of HMod
  11. HMul
  12. HMul.mk
    1. Instance constructor of HMul
  13. HOr
  14. HOr.mk
    1. Instance constructor of HOr
  15. HPow
  16. HPow.mk
    1. Instance constructor of HPow
  17. HShift­Left
  18. HShiftLeft.mk
    1. Instance constructor of HShift­Left
  19. HShift­Right
  20. HShiftRight.mk
    1. Instance constructor of HShift­Right
  21. HSub
  22. HSub.mk
    1. Instance constructor of HSub
  23. HXor
  24. HXor.mk
    1. Instance constructor of HXor
  25. Handle
    1. IO.FS.Handle
  26. Hashable
  27. Hashable.mk
    1. Instance constructor of Hashable
  28. Homogeneous­Pow
  29. HomogeneousPow.mk
    1. Instance constructor of Homogeneous­Pow
  30. Hygiene­Info
    1. Lean.Syntax.Hygiene­Info
  31. h
    1. ST.Ref.h (structure field)
  32. h­Add
    1. HAdd.h­Add (class method)
  33. h­And
    1. HAnd.h­And (class method)
  34. h­Append
    1. HAppend.h­Append (class method)
  35. h­Div
    1. HDiv.h­Div (class method)
  36. h­Mod
    1. HMod.h­Mod (class method)
  37. h­Mul
    1. HMul.h­Mul (class method)
  38. h­Or
    1. HOr.h­Or (class method)
  39. h­Pow
    1. HPow.h­Pow (class method)
  40. h­Shift­Left
    1. HShiftLeft.h­Shift­Left (class method)
  41. h­Shift­Right
    1. HShiftRight.h­Shift­Right (class method)
  42. h­Sub
    1. HSub.h­Sub (class method)
  43. h­Xor
    1. HXor.h­Xor (class method)
  44. has­Bind
    1. Id.has­Bind
  45. has­Decl
    1. Lean.Macro.has­Decl
  46. has­Finished
    1. IO.has­Finished
  47. has­Next
    1. String.Iterator.has­Next
  48. has­Prev
    1. String.Iterator.has­Prev
  49. hash
    1. Hashable.hash (class method)
    2. String.hash
  50. have
  51. have'
  52. have­I
  53. hygiene
    1. in tactics
  54. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  55. hygienic
    1. tactic.hygienic

I

  1. IO
  2. IO.Error
  3. IO.Error.already­Exists
    1. Constructor of IO.Error
  4. IO.Error.fopen­Error­To­String
  5. IO.Error.hardware­Fault
    1. Constructor of IO.Error
  6. IO.Error.illegal­Operation
    1. Constructor of IO.Error
  7. IO.Error.inappropriate­Type
    1. Constructor of IO.Error
  8. IO.Error.interrupted
    1. Constructor of IO.Error
  9. IO.Error.invalid­Argument
    1. Constructor of IO.Error
  10. IO.Error.mk­Already­Exists
  11. IO.Error.mk­Already­Exists­File
  12. IO.Error.mk­Eof­Error
  13. IO.Error.mk­Hardware­Fault
  14. IO.Error.mk­Illegal­Operation
  15. IO.Error.mk­Inappropriate­Type
  16. IO.Error.mk­Inappropriate­Type­File
  17. IO.Error.mk­Interrupted
  18. IO.Error.mk­Invalid­Argument
  19. IO.Error.mk­Invalid­Argument­File
  20. IO.Error.mk­No­File­Or­Directory
  21. IO.Error.mk­No­Such­Thing
  22. IO.Error.mk­No­Such­Thing­File
  23. IO.Error.mk­Other­Error
  24. IO.Error.mk­Permission­Denied
  25. IO.Error.mk­Permission­Denied­File
  26. IO.Error.mk­Protocol­Error
  27. IO.Error.mk­Resource­Busy
  28. IO.Error.mk­Resource­Exhausted
  29. IO.Error.mk­Resource­Exhausted­File
  30. IO.Error.mk­Resource­Vanished
  31. IO.Error.mk­Time­Expired
  32. IO.Error.mk­Unsatisfied­Constraints
  33. IO.Error.mk­Unsupported­Operation
  34. IO.Error.no­File­Or­Directory
    1. Constructor of IO.Error
  35. IO.Error.no­Such­Thing
    1. Constructor of IO.Error
  36. IO.Error.other­Error
    1. Constructor of IO.Error
  37. IO.Error.other­Error­To­String
  38. IO.Error.permission­Denied
    1. Constructor of IO.Error
  39. IO.Error.protocol­Error
    1. Constructor of IO.Error
  40. IO.Error.resource­Busy
    1. Constructor of IO.Error
  41. IO.Error.resource­Exhausted
    1. Constructor of IO.Error
  42. IO.Error.resource­Vanished
    1. Constructor of IO.Error
  43. IO.Error.time­Expired
    1. Constructor of IO.Error
  44. IO.Error.to­String
  45. IO.Error.unexpected­Eof
    1. Constructor of IO.Error
  46. IO.Error.unsatisfied­Constraints
    1. Constructor of IO.Error
  47. IO.Error.unsupported­Operation
    1. Constructor of IO.Error
  48. IO.Error.user­Error
    1. Constructor of IO.Error
  49. IO.FS.Dir­Entry
  50. IO.FS.DirEntry.mk
    1. Constructor of IO.FS.Dir­Entry
  51. IO.FS.DirEntry.path
  52. IO.FS.Handle
  53. IO.FS.Handle.flush
  54. IO.FS.Handle.get­Line
  55. IO.FS.Handle.is­Tty
  56. IO.FS.Handle.lock
  57. IO.FS.Handle.mk
  58. IO.FS.Handle.put­Str
  59. IO.FS.Handle.put­Str­Ln
  60. IO.FS.Handle.read
  61. IO.FS.Handle.read­Bin­To­End
  62. IO.FS.Handle.read­Bin­To­End­Into
  63. IO.FS.Handle.read­To­End
  64. IO.FS.Handle.rewind
  65. IO.FS.Handle.truncate
  66. IO.FS.Handle.try­Lock
  67. IO.FS.Handle.unlock
  68. IO.FS.Handle.write
  69. IO.FS.Metadata
  70. IO.FS.Metadata.mk
    1. Constructor of IO.FS.Metadata
  71. IO.FS.Mode
  72. IO.FS.Mode.append
    1. Constructor of IO.FS.Mode
  73. IO.FS.Mode.read
    1. Constructor of IO.FS.Mode
  74. IO.FS.Mode.read­Write
    1. Constructor of IO.FS.Mode
  75. IO.FS.Mode.write
    1. Constructor of IO.FS.Mode
  76. IO.FS.Mode.write­New
    1. Constructor of IO.FS.Mode
  77. IO.FS.Stream
  78. IO.FS.Stream.Buffer
  79. IO.FS.Stream.Buffer.data
  80. IO.FS.Stream.Buffer.mk
    1. Constructor of IO.FS.Stream.Buffer
  81. IO.FS.Stream.Buffer.pos
  82. IO.FS.Stream.mk
    1. Constructor of IO.FS.Stream
  83. IO.FS.Stream.of­Buffer
  84. IO.FS.Stream.of­Handle
  85. IO.FS.Stream.put­Str­Ln
  86. IO.FS.create­Dir
  87. IO.FS.create­Dir­All
  88. IO.FS.create­Temp­File
  89. IO.FS.lines
  90. IO.FS.read­Bin­File
  91. IO.FS.read­File
  92. IO.FS.real­Path
  93. IO.FS.remove­Dir
  94. IO.FS.remove­Dir­All
  95. IO.FS.remove­File
  96. IO.FS.rename
  97. IO.FS.with­File
  98. IO.FS.with­Isolated­Streams (0) (1)
  99. IO.FS.with­Temp­File
  100. IO.FS.write­Bin­File
  101. IO.FS.write­File
  102. IO.File­Right
  103. IO.FileRight.flags
  104. IO.FileRight.mk
    1. Constructor of IO.File­Right
  105. IO.Process.Child
  106. IO.Process.Child.kill
  107. IO.Process.Child.mk
    1. Constructor of IO.Process.Child
  108. IO.Process.Child.take­Stdin
  109. IO.Process.Child.try­Wait
  110. IO.Process.Child.wait
  111. IO.Process.Output
  112. IO.Process.Output.mk
    1. Constructor of IO.Process.Output
  113. IO.Process.Spawn­Args
  114. IO.Process.SpawnArgs.mk
    1. Constructor of IO.Process.Spawn­Args
  115. IO.Process.Stdio
  116. IO.Process.Stdio.inherit
    1. Constructor of IO.Process.Stdio
  117. IO.Process.Stdio.null
    1. Constructor of IO.Process.Stdio
  118. IO.Process.Stdio.piped
    1. Constructor of IO.Process.Stdio
  119. IO.Process.Stdio.to­Handle­Type
  120. IO.Process.Stdio­Config
  121. IO.Process.StdioConfig.mk
    1. Constructor of IO.Process.Stdio­Config
  122. IO.Process.exit
  123. IO.Process.get­Current­Dir
  124. IO.Process.get­PID
  125. IO.Process.output
  126. IO.Process.run
  127. IO.Process.set­Current­Dir
  128. IO.Process.spawn
  129. IO.Ref
  130. IO.add­Heartbeats
  131. IO.app­Dir
  132. IO.app­Path
  133. IO.as­Task
  134. IO.bind­Task
  135. IO.cancel
  136. IO.check­Canceled
  137. IO.current­Dir
  138. IO.eprint
  139. IO.eprintln
  140. IO.get­Env
  141. IO.get­Num­Heartbeats
  142. IO.get­Random­Bytes
  143. IO.get­Stderr
  144. IO.get­Stdin
  145. IO.get­Stdout
  146. IO.get­Task­State
  147. IO.has­Finished
  148. IO.iterate
  149. IO.lazy­Pure
  150. IO.map­Task
  151. IO.map­Tasks
  152. IO.mk­Ref
  153. IO.mono­Ms­Now
  154. IO.mono­Nanos­Now
  155. IO.of­Except
  156. IO.print
  157. IO.println
  158. IO.rand
  159. IO.set­Access­Rights
  160. IO.set­Rand­Seed
  161. IO.set­Stderr
  162. IO.set­Stdin
  163. IO.set­Stdout
  164. IO.sleep
  165. IO.to­EIO
  166. IO.user­Error
  167. IO.wait
  168. IO.wait­Any
  169. IO.with­Stderr
  170. IO.with­Stdin
  171. IO.with­Stdout
  172. Id
  173. Id.has­Bind
  174. Id.run
  175. Ident
    1. Lean.Syntax.Ident
  176. Inhabited
  177. Inhabited.mk
    1. Instance constructor of Inhabited
  178. Int
  179. Int.neg­Succ
    1. Constructor of Int
  180. Int.of­Nat
    1. Constructor of Int
  181. Int16
  182. Int16.mk
    1. Constructor of Int16
  183. Int32
  184. Int32.mk
    1. Constructor of Int32
  185. Int64
  186. Int64.mk
    1. Constructor of Int64
  187. Int8
  188. Int8.mk
    1. Constructor of Int8
  189. Iterator
    1. String.Iterator
  190. i
    1. String.Iterator.i (structure field)
  191. ibelow
    1. Nat.ibelow
  192. id_map
    1. LawfulFunctor.id_map (class method)
  193. ident­Kind
    1. Lean.ident­Kind
  194. identifier
    1. raw
  195. if ... then ... else ...
  196. if h : ... then ... else ...
  197. imax
    1. Nat.imax
  198. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  199. impredicative
  200. inaccessible
  201. index
    1. Lean.Meta.DSimp.Config.index (structure field)
    2. Lean.Meta.Simp.Config.index (structure field)
    3. of inductive type
  202. index­Of?
    1. Array.index­Of?
  203. indexed family
    1. of types
  204. induction
  205. induction­On
    1. Nat.div.induction­On
    2. Nat.mod.induction­On
  206. inductive.auto­Promote­Indices
  207. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  208. infer­Instance
  209. infer­Instance­As
  210. infer_instance
  211. injection
  212. injections
  213. insert­At
    1. Array.insert­At
  214. insert­At!
    1. Array.insert­At!
  215. insertion­Sort
    1. Array.insertion­Sort
  216. instance synthesis
  217. intercalate
    1. String.intercalate
  218. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  219. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  220. intro (0) (1)
  221. intro | ... => ... | ... => ...
  222. intros
  223. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  224. is­Absolute
    1. System.FilePath.is­Absolute
  225. is­Alpha
    1. Char.is­Alpha
  226. is­Alphanum
    1. Char.is­Alphanum
  227. is­Digit
    1. Char.is­Digit
  228. is­Dir
    1. System.FilePath.is­Dir
  229. is­Empty
    1. Array.is­Empty
    2. String.is­Empty
  230. is­Eqv
    1. Array.is­Eqv
  231. is­Int
    1. String.is­Int
  232. is­Lower
    1. Char.is­Lower
  233. is­Lt
    1. Fin.is­Lt (structure field)
  234. is­Nat
    1. String.is­Nat
  235. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  236. is­Ok
    1. Except.is­Ok
  237. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  238. is­Prefix­Of
    1. Array.is­Prefix­Of
    2. String.is­Prefix­Of
  239. is­Relative
    1. System.FilePath.is­Relative
  240. is­Tty
    1. IO.FS.Handle.is­Tty
    2. IO.FS.Stream.is­Tty (structure field)
  241. is­Upper
    1. Char.is­Upper
  242. is­Valid
    1. String.Pos.is­Valid
  243. is­Valid­Char
    1. Nat.is­Valid­Char
  244. is­Value
    1. Nat.is­Value
  245. is­Whitespace
    1. Char.is­Whitespace
  246. iter
    1. String.iter
  247. iterate
    1. IO.iterate

J

  1. join
    1. String.join
    2. System.FilePath.join

K

  1. kill
    1. IO.Process.Child.kill
  2. kleisli­Left
    1. Bind.kleisli­Left
  3. kleisli­Right
    1. Bind.kleisli­Right

L

  1. LE
  2. LE.mk
    1. Instance constructor of LE
  3. LT
  4. LT.mk
    1. Instance constructor of LT
  5. Lawful­Applicative
  6. LawfulApplicative.mk
    1. Instance constructor of Lawful­Applicative
  7. Lawful­BEq
  8. LawfulBEq.mk
    1. Instance constructor of Lawful­BEq
  9. Lawful­Functor
  10. LawfulFunctor.mk
    1. Instance constructor of Lawful­Functor
  11. Lawful­Get­Elem
  12. Lawful­GetElem.mk
    1. Instance constructor of Lawful­Get­Elem
  13. Lawful­Monad
  14. LawfulMonad.mk
    1. Instance constructor of Lawful­Monad
  15. LawfulMonad.mk'
  16. Leading­Ident­Behavior
    1. Lean.Parser.Leading­Ident­Behavior
  17. Lean.Elab.Tactic.Tactic
  18. Lean.Elab.Tactic.Tactic­M
  19. Lean.Elab.Tactic.adapt­Expander
  20. Lean.Elab.Tactic.append­Goals
  21. Lean.Elab.Tactic.close­Main­Goal
  22. Lean.Elab.Tactic.close­Main­Goal­Using
  23. Lean.Elab.Tactic.dsimp­Location'
  24. Lean.Elab.Tactic.elab­Cases­Targets
  25. Lean.Elab.Tactic.elab­DSimp­Config­Core
  26. Lean.Elab.Tactic.elab­Simp­Args
  27. Lean.Elab.Tactic.elab­Simp­Config
  28. Lean.Elab.Tactic.elab­Simp­Config­Ctx­Core
  29. Lean.Elab.Tactic.elab­Term
  30. Lean.Elab.Tactic.elab­Term­Ensuring­Type
  31. Lean.Elab.Tactic.elab­Term­With­Holes
  32. Lean.Elab.Tactic.ensure­Has­No­MVars
  33. Lean.Elab.Tactic.focus
  34. Lean.Elab.Tactic.get­Curr­Macro­Scope
  35. Lean.Elab.Tactic.get­FVar­Id
  36. Lean.Elab.Tactic.get­FVar­Ids
  37. Lean.Elab.Tactic.get­Goals
  38. Lean.Elab.Tactic.get­Main­Goal
  39. Lean.Elab.Tactic.get­Main­Module
  40. Lean.Elab.Tactic.get­Main­Tag
  41. Lean.Elab.Tactic.get­Unsolved­Goals
  42. Lean.Elab.Tactic.lift­Meta­MAt­Main
  43. Lean.Elab.Tactic.mk­Tactic­Attribute
  44. Lean.Elab.Tactic.or­Else
  45. Lean.Elab.Tactic.prune­Solved­Goals
  46. Lean.Elab.Tactic.run
  47. Lean.Elab.Tactic.run­Term­Elab
  48. Lean.Elab.Tactic.set­Goals
  49. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  50. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  51. Lean.Elab.Tactic.tactic­Elab­Attribute
  52. Lean.Elab.Tactic.tag­Untagged­Goals
  53. Lean.Elab.Tactic.try­Catch
  54. Lean.Elab.Tactic.try­Tactic
  55. Lean.Elab.Tactic.try­Tactic?
  56. Lean.Elab.Tactic.with­Location
  57. Lean.Elab.register­Deriving­Handler
  58. Lean.Macro.Exception.unsupported­Syntax
  59. Lean.Macro.add­Macro­Scope
  60. Lean.Macro.expand­Macro?
  61. Lean.Macro.get­Curr­Namespace
  62. Lean.Macro.has­Decl
  63. Lean.Macro.resolve­Global­Name
  64. Lean.Macro.resolve­Namespace
  65. Lean.Macro.throw­Error
  66. Lean.Macro.throw­Error­At
  67. Lean.Macro.throw­Unsupported
  68. Lean.Macro.trace
  69. Lean.Macro.with­Fresh­Macro­Scope
  70. Lean.Macro­M
  71. Lean.Meta.DSimp.Config
  72. Lean.Meta.DSimp.Config.mk
    1. Constructor of Lean.Meta.DSimp.Config
  73. Lean.Meta.Occurrences
  74. Lean.Meta.Occurrences.all
    1. Constructor of Lean.Meta.Occurrences
  75. Lean.Meta.Occurrences.neg
    1. Constructor of Lean.Meta.Occurrences
  76. Lean.Meta.Occurrences.pos
    1. Constructor of Lean.Meta.Occurrences
  77. Lean.Meta.Rewrite.Config
  78. Lean.Meta.Rewrite.Config.mk
    1. Constructor of Lean.Meta.Rewrite.Config
  79. Lean.Meta.Rewrite.New­Goals
  80. Lean.Meta.Simp.Config
  81. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  82. Lean.Meta.Simp.neutral­Config
  83. Lean.Meta.Simp­Extension
  84. Lean.Meta.Transparency­Mode
  85. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.Transparency­Mode
  86. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.Transparency­Mode
  87. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.Transparency­Mode
  88. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.Transparency­Mode
  89. Lean.Meta.register­Simp­Attr
  90. Lean.Parser.Leading­Ident­Behavior
  91. Lean.Parser.Leading­IdentBehavior.both
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  92. Lean.Parser.Leading­IdentBehavior.default
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  93. Lean.Parser.Leading­IdentBehavior.symbol
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  94. Lean.Source­Info
  95. Lean.SourceInfo.none
    1. Constructor of Lean.Source­Info
  96. Lean.SourceInfo.original
    1. Constructor of Lean.Source­Info
  97. Lean.SourceInfo.synthetic
    1. Constructor of Lean.Source­Info
  98. Lean.Syntax
  99. Lean.Syntax.Char­Lit
  100. Lean.Syntax.Command
  101. Lean.Syntax.Hygiene­Info
  102. Lean.Syntax.Ident
  103. Lean.Syntax.Level
  104. Lean.Syntax.Name­Lit
  105. Lean.Syntax.Num­Lit
  106. Lean.Syntax.Prec
  107. Lean.Syntax.Preresolved
  108. Lean.Syntax.Preresolved.decl
    1. Constructor of Lean.Syntax.Preresolved
  109. Lean.Syntax.Preresolved.namespace
    1. Constructor of Lean.Syntax.Preresolved
  110. Lean.Syntax.Prio
  111. Lean.Syntax.Scientific­Lit
  112. Lean.Syntax.Str­Lit
  113. Lean.Syntax.TSep­Array
  114. Lean.Syntax.TSepArray.mk
    1. Constructor of Lean.Syntax.TSep­Array
  115. Lean.Syntax.Tactic
  116. Lean.Syntax.Term
  117. Lean.Syntax.atom
    1. Constructor of Lean.Syntax
  118. Lean.Syntax.get­Kind
  119. Lean.Syntax.ident
    1. Constructor of Lean.Syntax
  120. Lean.Syntax.is­Of­Kind
  121. Lean.Syntax.missing
    1. Constructor of Lean.Syntax
  122. Lean.Syntax.node
    1. Constructor of Lean.Syntax
  123. Lean.Syntax.set­Kind
  124. Lean.Syntax­Node­Kind
  125. Lean.TSyntax
  126. Lean.TSyntax.get­Char
  127. Lean.TSyntax.get­Hygiene­Info
  128. Lean.TSyntax.get­Id
  129. Lean.TSyntax.get­Name
  130. Lean.TSyntax.get­Nat
  131. Lean.TSyntax.get­Scientific
  132. Lean.TSyntax.get­String
  133. Lean.TSyntax.mk
    1. Constructor of Lean.TSyntax
  134. Lean.TSyntax­Array
  135. Lean.char­Lit­Kind
  136. Lean.choice­Kind
  137. Lean.field­Idx­Kind
  138. Lean.group­Kind
  139. Lean.hygiene­Info­Kind
  140. Lean.ident­Kind
  141. Lean.interpolated­Str­Kind
  142. Lean.interpolated­Str­Lit­Kind
  143. Lean.name­Lit­Kind
  144. Lean.null­Kind
  145. Lean.num­Lit­Kind
  146. Lean.scientific­Lit­Kind
  147. Lean.str­Lit­Kind
  148. Level
    1. Lean.Syntax.Level
  149. List
  150. List.cons
    1. Constructor of List
  151. List.nil
    1. Constructor of List
  152. land
    1. Nat.land
  153. lazy­Pure
    1. IO.lazy­Pure
  154. lcm
    1. Nat.lcm
  155. le
    1. LE.le (class method)
    2. Nat.le
    3. String.le
  156. lean_is_array
  157. lean_is_string
  158. lean_string_object (0) (1)
  159. lean_to_array
  160. lean_to_string
  161. left (0) (1)
  162. length
    1. String.length
  163. let
  164. let rec
  165. let'
  166. let­I
  167. level
    1. of universe
  168. lhs
  169. lift
    1. Except­CpsT.lift
    2. ExceptT.lift
    3. OptionT.lift
    4. State­CpsT.lift
    5. State­RefT'.lift
    6. StateT.lift
  170. lift­Meta­MAt­Main
    1. Lean.Elab.Tactic.lift­Meta­MAt­Main
  171. lift­With
    1. MonadControl.lift­With (class method)
    2. Monad­ControlT.lift­With (class method)
  172. line­Eq
  173. lines
    1. IO.FS.lines
  174. linter.unnecessary­Simpa
  175. literal
    1. raw string
    2. string
  176. lock
    1. IO.FS.Handle.lock
  177. log2
    1. Nat.log2
  178. lor
    1. Nat.lor
  179. lt
    1. LT.lt (class method)
    2. Nat.lt
  180. lt_wf­Rel
    1. Nat.lt_wf­Rel

M

  1. MProd
  2. MProd.mk
    1. Constructor of MProd
  3. Macro­M
    1. Lean.Macro­M
  4. Metadata
    1. IO.FS.Metadata
  5. Mod
  6. Mod.mk
    1. Instance constructor of Mod
  7. Mode
    1. IO.FS.Mode
  8. Monad
  9. Monad.mk
    1. Instance constructor of Monad
  10. Monad­Control
  11. MonadControl.mk
    1. Instance constructor of Monad­Control
  12. Monad­Control­T
  13. Monad­ControlT.mk
    1. Instance constructor of Monad­Control­T
  14. Monad­Except
  15. MonadExcept.mk
    1. Instance constructor of Monad­Except
  16. MonadExcept.of­Except
  17. MonadExcept.or­Else
  18. MonadExcept.orelse'
  19. Monad­Except­Of
  20. Monad­ExceptOf.mk
    1. Instance constructor of Monad­Except­Of
  21. Monad­Finally
  22. MonadFinally.mk
    1. Instance constructor of Monad­Finally
  23. Monad­Functor
  24. MonadFunctor.mk
    1. Instance constructor of Monad­Functor
  25. Monad­Functor­T
  26. Monad­FunctorT.mk
    1. Instance constructor of Monad­Functor­T
  27. Monad­Lift
  28. MonadLift.mk
    1. Instance constructor of Monad­Lift
  29. Monad­Lift­T
  30. Monad­LiftT.mk
    1. Instance constructor of Monad­Lift­T
  31. Monad­Reader
  32. MonadReader.mk
    1. Instance constructor of Monad­Reader
  33. Monad­Reader­Of
  34. Monad­ReaderOf.mk
    1. Instance constructor of Monad­Reader­Of
  35. Monad­State
  36. MonadState.get
  37. MonadState.mk
    1. Instance constructor of Monad­State
  38. MonadState.modify­Get
  39. Monad­State­Of
  40. Monad­StateOf.mk
    1. Instance constructor of Monad­State­Of
  41. Monad­With­Reader
  42. Monad­WithReader.mk
    1. Instance constructor of Monad­With­Reader
  43. Monad­With­Reader­Of
  44. Monad­With­ReaderOf.mk
    1. Instance constructor of Monad­With­Reader­Of
  45. Mul
  46. Mul.mk
    1. Instance constructor of Mul
  47. main goal
  48. map
    1. Array.map
    2. EStateM.map
    3. Except.map
    4. ExceptT.map
    5. Functor.map (class method)
    6. StateT.map
    7. String.map
  49. map­Const
    1. Functor.map­Const (class method)
  50. map­Error
    1. Except.map­Error
  51. map­Fin­Idx
    1. Array.map­Fin­Idx
  52. map­Fin­Idx­M
    1. Array.map­Fin­Idx­M
  53. map­Idx
    1. Array.map­Idx
  54. map­Idx­M
    1. Array.map­Idx­M
  55. map­Indexed
    1. Array.map­Indexed
  56. map­Indexed­M
    1. Array.map­Indexed­M
  57. map­M
    1. Array.map­M
  58. map­M'
    1. Array.map­M'
  59. map­Mono
    1. Array.map­Mono
  60. map­Mono­M
    1. Array.map­Mono­M
  61. map­Rev
    1. Functor.map­Rev
  62. map­Task
    1. BaseIO.map­Task
    2. EIO.map­Task
    3. IO.map­Task
  63. map­Tasks
    1. BaseIO.map­Tasks
    2. EIO.map­Tasks
    3. IO.map­Tasks
  64. map_const
    1. LawfulFunctor.map_const (class method)
  65. map_pure
    1. LawfulApplicative.seq­Left_eq (class method)
  66. match
    1. pp.match
  67. max
    1. Nat.max
    2. Task.Priority.max
  68. max­Discharge­Depth
    1. Lean.Meta.Simp.Config.max­Discharge­Depth (structure field)
  69. max­Heartbeats
    1. synthInstance.max­Heartbeats
  70. max­Size
    1. synthInstance.max­Size
  71. max­Steps
    1. Lean.Meta.Simp.Config.max­Steps (structure field)
    2. pp.max­Steps
  72. memoize
    1. Lean.Meta.Simp.Config.memoize (structure field)
  73. metadata
    1. System.FilePath.metadata
  74. min
    1. Nat.min
    2. String.Pos.min
  75. mk
    1. Dynamic.mk
    2. ExceptT.mk
    3. IO.FS.Handle.mk
    4. OptionT.mk
  76. mk'
    1. LawfulMonad.mk'
  77. mk­Already­Exists
    1. IO.Error.mk­Already­Exists
  78. mk­Already­Exists­File
    1. IO.Error.mk­Already­Exists­File
  79. mk­Array
    1. Array.mk­Array
  80. mk­Eof­Error
    1. IO.Error.mk­Eof­Error
  81. mk­File­Path
    1. System.mk­File­Path
  82. mk­Hardware­Fault
    1. IO.Error.mk­Hardware­Fault
  83. mk­Illegal­Operation
    1. IO.Error.mk­Illegal­Operation
  84. mk­Inappropriate­Type
    1. IO.Error.mk­Inappropriate­Type
  85. mk­Inappropriate­Type­File
    1. IO.Error.mk­Inappropriate­Type­File
  86. mk­Interrupted
    1. IO.Error.mk­Interrupted
  87. mk­Invalid­Argument
    1. IO.Error.mk­Invalid­Argument
  88. mk­Invalid­Argument­File
    1. IO.Error.mk­Invalid­Argument­File
  89. mk­Iterator
    1. String.mk­Iterator
  90. mk­No­File­Or­Directory
    1. IO.Error.mk­No­File­Or­Directory
  91. mk­No­Such­Thing
    1. IO.Error.mk­No­Such­Thing
  92. mk­No­Such­Thing­File
    1. IO.Error.mk­No­Such­Thing­File
  93. mk­Other­Error
    1. IO.Error.mk­Other­Error
  94. mk­Permission­Denied
    1. IO.Error.mk­Permission­Denied
  95. mk­Permission­Denied­File
    1. IO.Error.mk­Permission­Denied­File
  96. mk­Protocol­Error
    1. IO.Error.mk­Protocol­Error
  97. mk­Ref
    1. IO.mk­Ref
    2. ST.mk­Ref
  98. mk­Resource­Busy
    1. IO.Error.mk­Resource­Busy
  99. mk­Resource­Exhausted
    1. IO.Error.mk­Resource­Exhausted
  100. mk­Resource­Exhausted­File
    1. IO.Error.mk­Resource­Exhausted­File
  101. mk­Resource­Vanished
    1. IO.Error.mk­Resource­Vanished
  102. mk­Std­Gen
  103. mk­Tactic­Attribute
    1. Lean.Elab.Tactic.mk­Tactic­Attribute
  104. mk­Time­Expired
    1. IO.Error.mk­Time­Expired
  105. mk­Unsatisfied­Constraints
    1. IO.Error.mk­Unsatisfied­Constraints
  106. mk­Unsupported­Operation
    1. IO.Error.mk­Unsupported­Operation
  107. mod
    1. Mod.mod (class method)
    2. Nat.mod
  108. mod­Core
    1. Nat.mod­Core
  109. modified
    1. IO.FS.Metadata.modified (structure field)
  110. modify
    1. Array.modify
    2. ST.Ref.modify
    3. String.modify
  111. modify­Get
    1. EStateM.modify­Get
    2. MonadState.modify­Get
    3. MonadState.modify­Get (class method)
    4. Monad­StateOf.modify­Get (class method)
    5. ST.Ref.modify­Get
    6. State­RefT'.modify­Get
    7. StateT.modify­Get
  112. modify­Get­The
  113. modify­M
    1. Array.modify­M
  114. modify­Op
    1. Array.modify­Op
  115. modify­The
  116. monad­Lift
    1. MonadLift.monad­Lift (class method)
    2. Monad­LiftT.monad­Lift (class method)
  117. monad­Map
    1. MonadFunctor.monad­Map (class method)
    2. Monad­FunctorT.monad­Map (class method)
  118. mono­Ms­Now
    1. IO.mono­Ms­Now
  119. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  120. mul
    1. Mul.mul (class method)
    2. Nat.mul
  121. mvars
    1. pp.mvars

N

  1. Name­Lit
    1. Lean.Syntax.Name­Lit
  2. Nat
  3. Nat.add
  4. Nat.all
  5. Nat.all­M
  6. Nat.all­TR
  7. Nat.any
  8. Nat.any­M
  9. Nat.any­TR
  10. Nat.apply­Eq­Lemma
  11. Nat.apply­Simproc­Const
  12. Nat.below
  13. Nat.beq
  14. Nat.bitwise
  15. Nat.ble
  16. Nat.blt
  17. Nat.case­Strong­Induction­On
  18. Nat.cases­On
  19. Nat.cast
  20. Nat.dec­Eq
  21. Nat.dec­Le
  22. Nat.dec­Lt
  23. Nat.digit­Char
  24. Nat.div
  25. Nat.div.induction­On
  26. Nat.div2Induction
  27. Nat.elim­Offset
  28. Nat.fold
  29. Nat.fold­M
  30. Nat.fold­Rev
  31. Nat.fold­Rev­M
  32. Nat.fold­TR
  33. Nat.for­M
  34. Nat.for­Rev­M
  35. Nat.from­Expr?
  36. Nat.gcd
  37. Nat.ibelow
  38. Nat.imax
  39. Nat.is­Power­Of­Two
  40. Nat.is­Valid­Char
  41. Nat.is­Value
  42. Nat.land
  43. Nat.lcm
  44. Nat.le
  45. Nat.le.refl
    1. Constructor of Nat.le
  46. Nat.le.step
    1. Constructor of Nat.le
  47. Nat.log2
  48. Nat.lor
  49. Nat.lt
  50. Nat.lt_wf­Rel
  51. Nat.max
  52. Nat.min
  53. Nat.mod
  54. Nat.mod.induction­On
  55. Nat.mod­Core
  56. Nat.mul
  57. Nat.next­Power­Of­Two
  58. Nat.no­Confusion
  59. Nat.no­Confusion­Type
  60. Nat.pow
  61. Nat.pred
  62. Nat.rec
  63. Nat.rec­On
  64. Nat.reduce­Add
  65. Nat.reduce­BEq
  66. Nat.reduce­BNe
  67. Nat.reduce­Beq­Diff
  68. Nat.reduce­Bin
  69. Nat.reduce­Bin­Pred
  70. Nat.reduce­Bne­Diff
  71. Nat.reduce­Bool­Pred
  72. Nat.reduce­Div
  73. Nat.reduce­Eq­Diff
  74. Nat.reduce­GT
  75. Nat.reduce­Gcd
  76. Nat.reduce­LT
  77. Nat.reduce­LTLE
  78. Nat.reduce­Le­Diff
  79. Nat.reduce­Mod
  80. Nat.reduce­Mul
  81. Nat.reduce­Nat­Eq­Expr
  82. Nat.reduce­Pow
  83. Nat.reduce­Sub
  84. Nat.reduce­Sub­Diff
  85. Nat.reduce­Succ
  86. Nat.reduce­Unary
  87. Nat.repeat
  88. Nat.repeat­TR
  89. Nat.repr
  90. Nat.shift­Left
  91. Nat.shift­Right
  92. Nat.strong­Induction­On
  93. Nat.sub
  94. Nat.sub­Digit­Char
  95. Nat.succ
    1. Constructor of Nat
  96. Nat.super­Digit­Char
  97. Nat.test­Bit
  98. Nat.to­Digits
  99. Nat.to­Digits­Core
  100. Nat.to­Float
  101. Nat.to­Level
  102. Nat.to­Sub­Digits
  103. Nat.to­Subscript­String
  104. Nat.to­Super­Digits
  105. Nat.to­Superscript­String
  106. Nat.to­UInt16
  107. Nat.to­UInt32
  108. Nat.to­UInt64
  109. Nat.to­UInt8
  110. Nat.to­USize
  111. Nat.xor
  112. Nat.zero
    1. Constructor of Nat
  113. Nat­Cast
  114. NatCast.mk
    1. Instance constructor of Nat­Cast
  115. Nat­Pow
  116. NatPow.mk
    1. Instance constructor of Nat­Pow
  117. Ne­Zero
  118. NeZero.mk
    1. Instance constructor of Ne­Zero
  119. Neg
  120. Neg.mk
    1. Instance constructor of Neg
  121. New­Goals
    1. Lean.Meta.Rewrite.New­Goals
  122. Nonempty
  123. Nonempty.intro
    1. Constructor of Nonempty
  124. Num­Lit
    1. Lean.Syntax.Num­Lit
  125. name­Lit­Kind
    1. Lean.name­Lit­Kind
  126. namespace
    1. of inductive type
  127. nat­Cast
    1. NatCast.nat­Cast (class method)
  128. native_decide
  129. neg
    1. Neg.neg (class method)
  130. neutral­Config
    1. Lean.Meta.Simp.neutral­Config
  131. new­Goals
    1. Lean.Meta.Rewrite.Config.new­Goals (structure field)
  132. next
    1. RandomGen.next (class method)
    2. String.Iterator.next
    3. String.next
  133. next ... => ...
  134. next'
    1. String.next'
  135. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  136. next­Until
    1. String.next­Until
  137. next­While
    1. String.next­While
  138. nextn
    1. String.Iterator.nextn
  139. no­Confusion
    1. Nat.no­Confusion
  140. no­Confusion­Type
    1. Nat.no­Confusion­Type
  141. nofun
  142. nomatch
  143. non­Backtrackable
    1. EStateM.non­Backtrackable
  144. norm_cast (0) (1)
  145. normalize
    1. System.FilePath.normalize
  146. not
    1. Bool.not
  147. not­M
  148. null­Kind
    1. Lean.null­Kind
  149. num­Lit­Kind
    1. Lean.num­Lit­Kind

O

  1. Occurrences
    1. Lean.Meta.Occurrences
  2. Of­Nat
  3. OfNat.mk
    1. Instance constructor of Of­Nat
  4. Of­Scientific
  5. OfScientific.mk
    1. Instance constructor of Of­Scientific
  6. Option
  7. Option.none
    1. Constructor of Option
  8. Option.some
    1. Constructor of Option
  9. Option­T
  10. OptionT.bind
  11. OptionT.fail
  12. OptionT.lift
  13. OptionT.mk
  14. OptionT.or­Else
  15. OptionT.pure
  16. OptionT.run
  17. OptionT.try­Catch
  18. Ord
  19. Ord.mk
    1. Instance constructor of Ord
  20. Output
    1. IO.Process.Output
  21. obtain
  22. occs
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  23. of­Buffer
    1. IO.FS.Stream.of­Buffer
  24. of­Except
    1. IO.of­Except
    2. MonadExcept.of­Except
  25. of­Fn
    1. Array.of­Fn
  26. of­Handle
    1. IO.FS.Stream.of­Handle
  27. of­Nat
    1. OfNat.of­Nat (class method)
  28. of­Scientific
    1. OfScientific.of­Scientific (class method)
  29. of­Subarray
    1. Array.of­Subarray
  30. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  31. offset­Of­Pos
    1. String.offset­Of­Pos
  32. omega
  33. open
  34. opt­Param
  35. optional
  36. or
    1. Bool.or
  37. or­Else
    1. EStateM.or­Else
    2. Lean.Elab.Tactic.or­Else
    3. MonadExcept.or­Else
    4. OptionT.or­Else
    5. ReaderT.or­Else
    6. StateT.or­Else
    7. [anonymous] (class method)
  38. or­Else'
    1. EStateM.or­Else'
  39. or­Else­Lazy
    1. Except.or­Else­Lazy
  40. or­M
  41. orelse'
    1. MonadExcept.orelse'
  42. other
    1. IO.FileRight.other (structure field)
  43. other­Error­To­String
    1. IO.Error.other­Error­To­String
  44. out
    1. NeZero.out (class method)
  45. out­Param
  46. output
    1. IO.Process.output

P

  1. PEmpty
  2. PLift
  3. PLift.up
    1. Constructor of PLift
  4. PProd
  5. PProd.mk
    1. Constructor of PProd
  6. PSigma
  7. PSigma.mk
    1. Constructor of PSigma
  8. PSum
  9. PSum.inl
    1. Constructor of PSum
  10. PSum.inr
    1. Constructor of PSum
  11. PUnit
  12. PUnit.unit
    1. Constructor of PUnit
  13. Pos
    1. String.Pos
  14. Pow
  15. Pow.mk
    1. Instance constructor of Pow
  16. Prec
    1. Lean.Syntax.Prec
  17. Preresolved
    1. Lean.Syntax.Preresolved
  18. Prio
    1. Lean.Syntax.Prio
  19. Priority
    1. Task.Priority
  20. Prod
  21. Prod.mk
    1. Constructor of Prod
  22. Prop
  23. Pure
  24. Pure.mk
    1. Instance constructor of Pure
  25. parameter
    1. of inductive type
  26. parent
    1. System.FilePath.parent
  27. parser
  28. partition
    1. Array.partition
  29. path
    1. IO.FS.DirEntry.path
  30. path­Exists
    1. System.FilePath.path­Exists
  31. path­Separator
    1. System.FilePath.path­Separator
  32. path­Separators
    1. System.FilePath.path­Separators
  33. pattern
  34. placeholder term
  35. polymorphism
    1. universe
  36. pop
    1. Array.pop
  37. pop­Front
    1. Subarray.pop­Front
  38. pop­While
    1. Array.pop­While
  39. pos
    1. IO.FS.Stream.Buffer.pos
    2. IO.FS.Stream.Buffer.pos (structure field)
    3. String.Iterator.pos
  40. pos­Of
    1. String.pos­Of
  41. pow
    1. HomogeneousPow.pow (class method)
    2. Nat.pow
    3. NatPow.pow (class method)
    4. Pow.pow (class method)
  42. pp.deep­Terms
  43. pp.deepTerms.threshold
  44. pp.field­Notation
  45. pp.match
  46. pp.max­Steps
  47. pp.mvars
  48. pp.proofs
  49. pp.proofs.threshold
  50. pred
    1. Nat.pred
  51. predicative
  52. prev
    1. String.Iterator.prev
    2. String.prev
  53. prevn
    1. String.Iterator.prevn
  54. print
    1. IO.print
  55. println
    1. IO.println
  56. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
    2. Lean.Meta.Simp.Config.proj (structure field)
  57. proof state
  58. proofs
    1. pp.proofs
  59. property
    1. Subtype.property (structure field)
  60. propext
  61. proposition
    1. decidable
  62. prune­Solved­Goals
    1. Lean.Elab.Tactic.prune­Solved­Goals
  63. ptr­Eq
    1. ST.Ref.ptr­Eq
  64. pure
    1. EStateM.pure
    2. Except.pure
    3. ExceptT.pure
    4. OptionT.pure
    5. Pure.pure (class method)
    6. ReaderT.pure
    7. StateT.pure
  65. pure_bind
    1. [anonymous] (class method)
  66. pure_seq
    1. [anonymous] (class method)
  67. push
    1. Array.push
    2. String.push
  68. push_cast
  69. pushn
    1. String.pushn
  70. put­Str
    1. IO.FS.Handle.put­Str
    2. IO.FS.Stream.put­Str (structure field)
  71. put­Str­Ln
    1. IO.FS.Handle.put­Str­Ln
    2. IO.FS.Stream.put­Str­Ln

Q

  1. qsort
    1. Array.qsort
  2. qsort­Ord
    1. Array.qsort­Ord
  3. quantification
    1. impredicative
    2. predicative
  4. quote
    1. String.quote

R

  1. Random­Gen
  2. RandomGen.mk
    1. Instance constructor of Random­Gen
  3. Reader­M
  4. Reader­T
  5. ReaderT.adapt
  6. ReaderT.bind
  7. ReaderT.failure
  8. ReaderT.or­Else
  9. ReaderT.pure
  10. ReaderT.read
  11. ReaderT.run
  12. Ref
    1. IO.Ref
    2. ST.Ref
  13. Repr
  14. Repr.mk
    1. Instance constructor of Repr
  15. Result
    1. EStateM.Result
  16. rand
    1. IO.rand
  17. rand­Bool
  18. rand­Nat
  19. range
    1. Array.range
    2. RandomGen.range (class method)
  20. raw
    1. Lean.TSyntax.raw (structure field)
  21. rcases
  22. read
    1. IO.FS.Handle.read
    2. IO.FS.Stream.read (structure field)
    3. MonadReader.read (class method)
    4. Monad­ReaderOf.read (class method)
    5. ReaderT.read
  23. read­Bin­File
    1. IO.FS.read­Bin­File
  24. read­Bin­To­End
    1. IO.FS.Handle.read­Bin­To­End
  25. read­Bin­To­End­Into
    1. IO.FS.Handle.read­Bin­To­End­Into
  26. read­Dir
    1. System.FilePath.read­Dir
  27. read­File
    1. IO.FS.read­File
  28. read­The
  29. read­To­End
    1. IO.FS.Handle.read­To­End
  30. real­Path
    1. IO.FS.real­Path
  31. rec
    1. Nat.rec
  32. rec­On
    1. Nat.rec­On
  33. recursor
  34. reduce
  35. reduce­Add
    1. Nat.reduce­Add
  36. reduce­Append
    1. String.reduce­Append
  37. reduce­BEq
    1. Nat.reduce­BEq
    2. String.reduce­BEq
  38. reduce­BNe
    1. Nat.reduce­BNe
    2. String.reduce­BNe
  39. reduce­Beq­Diff
    1. Nat.reduce­Beq­Diff
  40. reduce­Bin
    1. Nat.reduce­Bin
  41. reduce­Bin­Pred
    1. Nat.reduce­Bin­Pred
    2. String.reduce­Bin­Pred
  42. reduce­Bne­Diff
    1. Nat.reduce­Bne­Diff
  43. reduce­Bool­Pred
    1. Nat.reduce­Bool­Pred
    2. String.reduce­Bool­Pred
  44. reduce­Div
    1. Nat.reduce­Div
  45. reduce­Eq
    1. String.reduce­Eq
  46. reduce­Eq­Diff
    1. Nat.reduce­Eq­Diff
  47. reduce­GE
    1. String.reduce­GE
  48. reduce­GT
    1. Nat.reduce­GT
    2. String.reduce­GT
  49. reduce­Gcd
    1. Nat.reduce­Gcd
  50. reduce­Get­Elem
    1. Array.reduce­Get­Elem
  51. reduce­Get­Elem!
    1. Array.reduce­Get­Elem!
  52. reduce­Get­Elem?
    1. Array.reduce­Get­Elem?
  53. reduce­LE
    1. String.reduce­LE
  54. reduce­LT
    1. Nat.reduce­LT
    2. String.reduce­LT
  55. reduce­LTLE
    1. Nat.reduce­LTLE
  56. reduce­Le­Diff
    1. Nat.reduce­Le­Diff
  57. reduce­Mk
    1. String.reduce­Mk
  58. reduce­Mod
    1. Nat.reduce­Mod
  59. reduce­Mul
    1. Nat.reduce­Mul
  60. reduce­Nat­Eq­Expr
    1. Nat.reduce­Nat­Eq­Expr
  61. reduce­Ne
    1. String.reduce­Ne
  62. reduce­Option
    1. Array.reduce­Option
  63. reduce­Pow
    1. Nat.reduce­Pow
  64. reduce­Sub
    1. Nat.reduce­Sub
  65. reduce­Sub­Diff
    1. Nat.reduce­Sub­Diff
  66. reduce­Succ
    1. Nat.reduce­Succ
  67. reduce­Unary
    1. Nat.reduce­Unary
  68. reduction
    1. ι (iota)
  69. ref
    1. ST.Ref.ref (structure field)
  70. refine
  71. refine'
  72. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  73. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  74. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  75. remaining­To­String
    1. String.Iterator.remaining­To­String
  76. remove­Dir
    1. IO.FS.remove­Dir
  77. remove­Dir­All
    1. IO.FS.remove­Dir­All
  78. remove­File
    1. IO.FS.remove­File
  79. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  80. rename
    1. IO.FS.rename
  81. rename_i
  82. repeat (0) (1)
    1. Nat.repeat
  83. repeat'
  84. repeat1'
  85. repeat­TR
    1. Nat.repeat­TR
  86. replace
    1. String.replace
  87. repr
    1. Nat.repr
  88. repr­Prec
    1. Repr.repr­Prec (class method)
  89. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  90. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  91. restore
    1. EStateM.Backtrackable.restore (class method)
  92. restore­M
    1. MonadControl.restore­M (class method)
    2. Monad­ControlT.restore­M (class method)
  93. rev­Find
    1. String.rev­Find
  94. rev­Pos­Of
    1. String.rev­Pos­Of
  95. reverse
    1. Array.reverse
  96. revert
  97. rewind
    1. IO.FS.Handle.rewind
  98. rewrite (0) (1)
    1. trace.Meta.Tactic.simp.rewrite
  99. rfl (0) (1)
    1. LawfulBEq.rfl (class method)
  100. rfl'
  101. rhs
  102. right (0) (1)
  103. rintro
  104. root
    1. IO.FS.DirEntry.root (structure field)
  105. rotate_left
  106. rotate_right
  107. run
    1. EStateM.run
    2. Except­CpsT.run
    3. ExceptT.run
    4. IO.Process.run
    5. Id.run
    6. Lean.Elab.Tactic.run
    7. OptionT.run
    8. ReaderT.run
    9. State­CpsT.run
    10. State­RefT'.run
    11. StateT.run
  108. run'
    1. EStateM.run'
    2. State­CpsT.run'
    3. State­RefT'.run'
    4. StateT.run'
  109. run­Catch
    1. Except­CpsT.run­Catch
  110. run­EST
  111. run­K
    1. Except­CpsT.run­K
    2. State­CpsT.run­K
  112. run­ST
  113. run­Term­Elab
    1. Lean.Elab.Tactic.run­Term­Elab
  114. run_tac
  115. rw (0) (1)
  116. rw?
  117. rw_mod_cast
  118. rwa

S

  1. ST
  2. ST.Ref
  3. ST.Ref.get
  4. ST.Ref.mk
    1. Constructor of ST.Ref
  5. ST.Ref.modify
  6. ST.Ref.modify­Get
  7. ST.Ref.ptr­Eq
  8. ST.Ref.set
  9. ST.Ref.swap
  10. ST.Ref.take
  11. ST.Ref.to­Monad­State­Of
  12. ST.mk­Ref
  13. STWorld
  14. STWorld.mk
    1. Instance constructor of STWorld
  15. Scientific­Lit
    1. Lean.Syntax.Scientific­Lit
  16. Seq
  17. Seq.mk
    1. Instance constructor of Seq
  18. Seq­Left
  19. SeqLeft.mk
    1. Instance constructor of Seq­Left
  20. Seq­Right
  21. SeqRight.mk
    1. Instance constructor of Seq­Right
  22. Shift­Left
  23. ShiftLeft.mk
    1. Instance constructor of Shift­Left
  24. Shift­Right
  25. ShiftRight.mk
    1. Instance constructor of Shift­Right
  26. Sigma
  27. Sigma.mk
    1. Constructor of Sigma
  28. Simp­Extension
    1. Lean.Meta.Simp­Extension
  29. Size­Of
  30. SizeOf.mk
    1. Instance constructor of Size­Of
  31. Sort
  32. Source­Info
    1. Lean.Source­Info
  33. Spawn­Args
    1. IO.Process.Spawn­Args
  34. State­Cps­T
  35. State­CpsT.lift
  36. State­CpsT.run
  37. State­CpsT.run'
  38. State­CpsT.run­K
  39. State­M
  40. State­Ref­T'
  41. State­RefT'.get
  42. State­RefT'.lift
  43. State­RefT'.modify­Get
  44. State­RefT'.run
  45. State­RefT'.run'
  46. State­RefT'.set
  47. State­T
  48. StateT.bind
  49. StateT.failure
  50. StateT.get
  51. StateT.lift
  52. StateT.map
  53. StateT.modify­Get
  54. StateT.or­Else
  55. StateT.pure
  56. StateT.run
  57. StateT.run'
  58. StateT.set
  59. Std­Gen
  60. StdGen.mk
    1. Constructor of Std­Gen
  61. Stdio
    1. IO.Process.Stdio
  62. Stdio­Config
    1. IO.Process.Stdio­Config
  63. Str­Lit
    1. Lean.Syntax.Str­Lit
  64. Stream
    1. IO.FS.Stream
  65. String
  66. String.Iterator
  67. String.Iterator.at­End
  68. String.Iterator.curr
  69. String.Iterator.extract
  70. String.Iterator.forward
  71. String.Iterator.has­Next
  72. String.Iterator.has­Prev
  73. String.Iterator.mk
    1. Constructor of String.Iterator
  74. String.Iterator.next
  75. String.Iterator.nextn
  76. String.Iterator.pos
  77. String.Iterator.prev
  78. String.Iterator.prevn
  79. String.Iterator.remaining­Bytes
  80. String.Iterator.remaining­To­String
  81. String.Iterator.set­Curr
  82. String.Iterator.to­End
  83. String.Pos
  84. String.Pos.is­Valid
  85. String.Pos.min
  86. String.Pos.mk
    1. Constructor of String.Pos
  87. String.all
  88. String.any
  89. String.append
  90. String.at­End
  91. String.back
  92. String.capitalize
  93. String.codepoint­Pos­To­Utf16Pos
  94. String.codepoint­Pos­To­Utf16Pos­From
  95. String.codepoint­Pos­To­Utf8Pos­From
  96. String.contains
  97. String.crlf­To­Lf
  98. String.csize
  99. String.dec­Eq
  100. String.decapitalize
  101. String.drop
  102. String.drop­Right
  103. String.drop­Right­While
  104. String.drop­While
  105. String.end­Pos
  106. String.ends­With
  107. String.extract
  108. String.find
  109. String.find­Line­Start
  110. String.first­Diff­Pos
  111. String.foldl
  112. String.foldr
  113. String.from­Expr?
  114. String.from­UTF8
  115. String.from­UTF8!
  116. String.from­UTF8?
  117. String.front
  118. String.get
  119. String.get!
  120. String.get'
  121. String.get?
  122. String.get­Utf8Byte
  123. String.hash
  124. String.intercalate
  125. String.is­Empty
  126. String.is­Int
  127. String.is­Nat
  128. String.is­Prefix­Of
  129. String.iter
  130. String.join
  131. String.le
  132. String.length
  133. String.map
  134. String.mk
    1. Constructor of String
  135. String.mk­Iterator
  136. String.modify
  137. String.next
  138. String.next'
  139. String.next­Until
  140. String.next­While
  141. String.offset­Of­Pos
  142. String.pos­Of
  143. String.prev
  144. String.push
  145. String.pushn
  146. String.quote
  147. String.reduce­Append
  148. String.reduce­BEq
  149. String.reduce­BNe
  150. String.reduce­Bin­Pred
  151. String.reduce­Bool­Pred
  152. String.reduce­Eq
  153. String.reduce­GE
  154. String.reduce­GT
  155. String.reduce­LE
  156. String.reduce­LT
  157. String.reduce­Mk
  158. String.reduce­Ne
  159. String.remove­Leading­Spaces
  160. String.replace
  161. String.rev­Find
  162. String.rev­Pos­Of
  163. String.set
  164. String.singleton
  165. String.split
  166. String.split­On
  167. String.starts­With
  168. String.substr­Eq
  169. String.take
  170. String.take­Right
  171. String.take­Right­While
  172. String.take­While
  173. String.to­File­Map
  174. String.to­Format
  175. String.to­Int!
  176. String.to­Int?
  177. String.to­List
  178. String.to­Lower
  179. String.to­Name
  180. String.to­Nat!
  181. String.to­Nat?
  182. String.to­Substring
  183. String.to­Substring'
  184. String.to­UTF8
  185. String.to­Upper
  186. String.trim
  187. String.trim­Left
  188. String.trim­Right
  189. String.utf16Length
  190. String.utf16Pos­To­Codepoint­Pos
  191. String.utf16Pos­To­Codepoint­Pos­From
  192. String.utf8Byte­Size
  193. String.utf8Decode­Char?
  194. String.utf8Encode­Char
  195. String.validate­UTF8
  196. Sub
  197. Sub.mk
    1. Instance constructor of Sub
  198. Subarray
  199. Subarray.all
  200. Subarray.all­M
  201. Subarray.any
  202. Subarray.any­M
  203. Subarray.drop
  204. Subarray.empty
  205. Subarray.find­Rev?
  206. Subarray.find­Rev­M?
  207. Subarray.find­Some­Rev­M?
  208. Subarray.foldl
  209. Subarray.foldl­M
  210. Subarray.foldr
  211. Subarray.foldr­M
  212. Subarray.for­In
  213. Subarray.for­M
  214. Subarray.for­Rev­M
  215. Subarray.get
  216. Subarray.get!
  217. Subarray.get­D
  218. Subarray.mk
    1. Constructor of Subarray
  219. Subarray.pop­Front
  220. Subarray.size
  221. Subarray.split
  222. Subarray.take
  223. Subarray.to­Array
  224. Subtype
  225. Subtype.mk
    1. Constructor of Subtype
  226. Sum
  227. Sum.inl
    1. Constructor of Sum
  228. Sum.inr
    1. Constructor of Sum
  229. Syntax
    1. Lean.Syntax
  230. Syntax­Node­Kind
    1. Lean.Syntax­Node­Kind
  231. System.File­Path
  232. System.FilePath.add­Extension
  233. System.FilePath.components
  234. System.FilePath.exe­Extension
  235. System.FilePath.ext­Separator
  236. System.FilePath.extension
  237. System.FilePath.file­Name
  238. System.FilePath.file­Stem
  239. System.FilePath.is­Absolute
  240. System.FilePath.is­Dir
  241. System.FilePath.is­Relative
  242. System.FilePath.join
  243. System.FilePath.metadata
  244. System.FilePath.mk
    1. Constructor of System.File­Path
  245. System.FilePath.normalize
  246. System.FilePath.parent
  247. System.FilePath.path­Exists
  248. System.FilePath.path­Separator
  249. System.FilePath.path­Separators
  250. System.FilePath.read­Dir
  251. System.FilePath.walk­Dir
  252. System.FilePath.with­Extension
  253. System.FilePath.with­File­Name
  254. System.mk­File­Path
  255. s
    1. String.Iterator.s (structure field)
  256. s1
    1. StdGen.s1 (structure field)
  257. s2
    1. StdGen.s2 (structure field)
  258. save
    1. EStateM.Backtrackable.save (class method)
  259. scientific­Lit­Kind
    1. Lean.scientific­Lit­Kind
  260. semi­Out­Param
  261. seq
    1. Seq.seq (class method)
  262. seq­Left
    1. SeqLeft.seq­Left (class method)
  263. seq­Left_eq
    1. [anonymous] (class method)
  264. seq­Right
    1. EStateM.seq­Right
    2. SeqRight.seq­Right (class method)
  265. seq­Right_eq
    1. [anonymous] (class method)
  266. seq_assoc
    1. LawfulApplicative.pure_seq (class method)
  267. seq_pure
    1. LawfulApplicative.seq­Right_eq (class method)
  268. sequence­Map
    1. Array.sequence­Map
  269. set
    1. Array.set
    2. EStateM.set
    3. MonadState.set (class method)
    4. Monad­StateOf.set (class method)
    5. ST.Ref.set
    6. State­RefT'.set
    7. StateT.set
    8. String.set
  270. set!
    1. Array.set!
  271. set­Access­Rights
    1. IO.set­Access­Rights
  272. set­Curr
    1. String.Iterator.set­Curr
  273. set­Current­Dir
    1. IO.Process.set­Current­Dir
  274. set­D
    1. Array.set­D
  275. set­Goals
    1. Lean.Elab.Tactic.set­Goals
  276. set­Kind
    1. Lean.Syntax.set­Kind
  277. set­Rand­Seed
    1. IO.set­Rand­Seed
  278. set­Stderr
    1. IO.set­Stderr
  279. set­Stdin
    1. IO.set­Stdin
  280. set­Stdout
    1. IO.set­Stdout
  281. set_option
  282. setsid
    1. IO.Process.SpawnArgs.args (structure field)
  283. shift­Left
    1. Nat.shift­Left
    2. ShiftLeft.shift­Left (class method)
  284. shift­Right
    1. Nat.shift­Right
    2. ShiftRight.shift­Right (class method)
  285. show
  286. show_term
  287. simp (0) (1)
  288. simp!
  289. simp?
  290. simp?!
  291. simp_all
  292. simp_all!
  293. simp_all?
  294. simp_all?!
  295. simp_all_arith
  296. simp_all_arith!
  297. simp_arith
  298. simp_arith!
  299. simp_match
  300. simp_wf
  301. simpa
  302. simpa!
  303. simpa?
  304. simpa?!
  305. simprocs
  306. single­Pass
    1. Lean.Meta.Simp.Config.single­Pass (structure field)
  307. singleton
    1. Array.singleton
    2. String.singleton
  308. size
    1. Array.size
    2. Subarray.size
  309. size­Of
    1. SizeOf.size­Of (class method)
  310. skip (0) (1)
  311. skip­Assigned­Instances
    1. tactic.skip­Assigned­Instances
  312. sleep
    1. IO.sleep
  313. snd
    1. MProd.snd (structure field)
    2. PProd.snd (structure field)
    3. PSigma.snd (structure field)
    4. Prod.snd (structure field)
    5. Sigma.snd (structure field)
  314. solve
  315. solve_by_elim
  316. sorry
  317. sort­MVar­Id­Array­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  318. sort­MVar­Ids­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  319. spawn
    1. IO.Process.spawn
    2. Task.spawn
  320. specialize
  321. split
    1. Array.split
    2. RandomGen.split (class method)
    3. String.split
    4. Subarray.split
  322. split­On
    1. String.split­On
  323. st­M
    1. MonadControl.st­M (class method)
    2. Monad­ControlT.st­M (class method)
  324. start
    1. Subarray.start (structure field)
  325. start_le_stop
    1. Subarray.start_le_stop (structure field)
  326. starts­With
    1. String.starts­With
  327. std­Next
  328. std­Range
  329. std­Split
  330. stderr
    1. IO.Process.Child.stderr (structure field)
    2. IO.Process.Output.stderr (structure field)
    3. IO.Process.StdioConfig.stderr (structure field)
  331. stdin
    1. IO.Process.Child.stdin (structure field)
    2. IO.Process.StdioConfig.stdin (structure field)
  332. stdout
    1. IO.Process.Child.stdout (structure field)
    2. IO.Process.Output.stdout (structure field)
    3. IO.Process.StdioConfig.stdout (structure field)
  333. stop
    1. Subarray.stop (structure field)
  334. stop_le_array_size
    1. Subarray.stop_le_array_size (structure field)
  335. str­Lit­Kind
    1. Lean.str­Lit­Kind
  336. strong­Induction­On
    1. Nat.strong­Induction­On
  337. sub
    1. Nat.sub
    2. Sub.sub (class method)
  338. sub­Digit­Char
    1. Nat.sub­Digit­Char
  339. subst
  340. subst_eqs
  341. subst_vars
  342. substr­Eq
    1. String.substr­Eq
  343. suffices
  344. super­Digit­Char
    1. Nat.super­Digit­Char
  345. swap
    1. Array.swap
    2. ST.Ref.swap
  346. swap!
    1. Array.swap!
  347. swap­At
    1. Array.swap­At
  348. swap­At!
    1. Array.swap­At!
  349. symm
  350. symm_saturate
  351. synthInstance.max­Heartbeats
  352. synthInstance.max­Size
  353. synthesis
    1. of type class instances

T

  1. TSep­Array
    1. Lean.Syntax.TSep­Array
  2. TSyntax
    1. Lean.TSyntax
  3. TSyntax­Array
    1. Lean.TSyntax­Array
  4. Tactic
    1. Lean.Elab.Tactic.Tactic
    2. Lean.Syntax.Tactic
  5. Tactic­M
    1. Lean.Elab.Tactic.Tactic­M
  6. Task
  7. Task.Priority
  8. Task.Priority.dedicated
  9. Task.Priority.default
  10. Task.Priority.max
  11. Task.get
  12. Task.pure
    1. Constructor of Task
  13. Task.spawn
  14. Term
    1. Lean.Syntax.Term
  15. To­String
  16. ToString.mk
    1. Instance constructor of To­String
  17. Transparency­Mode
    1. Lean.Meta.Transparency­Mode
  18. Type
  19. Type­Name
  20. tactic
  21. tactic'
  22. tactic.custom­Eliminators
  23. tactic.dbg_cache
  24. tactic.hygienic
  25. tactic.simp.trace (0) (1)
  26. tactic.skip­Assigned­Instances
  27. tactic­Elab­Attribute
    1. Lean.Elab.Tactic.tactic­Elab­Attribute
  28. tag­Untagged­Goals
    1. Lean.Elab.Tactic.tag­Untagged­Goals
  29. take
    1. Array.take
    2. ST.Ref.take
    3. String.take
    4. Subarray.take
  30. take­Right
    1. String.take­Right
  31. take­Right­While
    1. String.take­Right­While
  32. take­Stdin
    1. IO.Process.Child.take­Stdin
  33. take­While
    1. Array.take­While
    2. String.take­While
  34. term
    1. placeholder
  35. test­Bit
    1. Nat.test­Bit
  36. threshold
    1. pp.deepTerms.threshold
    2. pp.proofs.threshold
  37. throw
    1. EStateM.throw
    2. MonadExcept.throw (class method)
    3. Monad­ExceptOf.throw (class method)
  38. throw­Error
    1. Lean.Macro.throw­Error
  39. throw­Error­At
    1. Lean.Macro.throw­Error­At
  40. throw­The
  41. throw­Unsupported
    1. Lean.Macro.throw­Unsupported
  42. to­Applicative
    1. Alternative.to­Applicative (class method)
    2. Monad.to­Applicative (class method)
  43. to­Array
    1. Subarray.to­Array
  44. to­Base­IO
    1. EIO.to­Base­IO
  45. to­Bind
    1. [anonymous] (class method)
  46. to­Bit­Vec
    1. UInt16.to­Bit­Vec (structure field)
    2. UInt32.to­Bit­Vec (structure field)
    3. UInt64.to­Bit­Vec (structure field)
    4. UInt8.to­Bit­Vec (structure field)
    5. USize.to­Bit­Vec (structure field)
  47. to­Bool
    1. Except.to­Bool
  48. to­Digits
    1. Nat.to­Digits
  49. to­Digits­Core
    1. Nat.to­Digits­Core
  50. to­EIO
    1. BaseIO.to­EIO
    2. IO.to­EIO
  51. to­End
    1. String.Iterator.to­End
  52. to­File­Map
    1. String.to­File­Map
  53. to­Float
    1. Nat.to­Float
  54. to­Format
    1. String.to­Format
  55. to­Functor
    1. Applicative.to­Functor (class method)
  56. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  57. to­Handle­Type
    1. IO.Process.Stdio.to­Handle­Type
  58. to­IO
    1. BaseIO.to­IO
    2. EIO.to­IO
  59. to­IO'
    1. EIO.to­IO'
  60. to­ISize
    1. Bool.to­ISize
  61. to­Int!
    1. String.to­Int!
  62. to­Int16
    1. Bool.to­Int16
  63. to­Int32
    1. Bool.to­Int32
  64. to­Int64
    1. Bool.to­Int64
  65. to­Int8
    1. Bool.to­Int8
  66. to­Int?
    1. String.to­Int?
  67. to­Lawful­Applicative
    1. LawfulMonad.to­Lawful­Applicative (class method)
  68. to­Lawful­Functor
    1. LawfulApplicative.to­Lawful­Functor (class method)
  69. to­Level
    1. Nat.to­Level
  70. to­List
    1. Array.to­List
    2. Array.to­List (structure field)
    3. String.to­List
  71. to­List­Append
    1. Array.to­List­Append
  72. to­List­Rev
    1. Array.to­List­Rev
  73. to­Lower
    1. String.to­Lower
  74. to­Monad­State­Of
    1. ST.Ref.to­Monad­State­Of
  75. to­Name
    1. String.to­Name
  76. to­Nat
    1. Bool.to­Nat
  77. to­Nat!
    1. String.to­Nat!
  78. to­Nat?
    1. String.to­Nat?
  79. to­Option
    1. Except.to­Option
  80. to­PArray'
    1. Array.to­PArray'
  81. to­Pure
    1. [anonymous] (class method)
  82. to­Seq
    1. [anonymous] (class method)
  83. to­Seq­Left
    1. Applicative.to­Pure (class method)
  84. to­Seq­Right
    1. [anonymous] (class method)
  85. to­Stdio­Config
    1. IO.Process.SpawnArgs.to­Stdio­Config (structure field)
  86. to­String
    1. IO.Error.to­String
    2. System.FilePath.to­String (structure field)
    3. ToString.to­String (class method)
  87. to­Sub­Digits
    1. Nat.to­Sub­Digits
  88. to­Subarray
    1. Array.to­Subarray
  89. to­Subscript­String
    1. Nat.to­Subscript­String
  90. to­Substring
    1. String.to­Substring
  91. to­Substring'
    1. String.to­Substring'
  92. to­Super­Digits
    1. Nat.to­Super­Digits
  93. to­Superscript­String
    1. Nat.to­Superscript­String
  94. to­UInt16
    1. Bool.to­UInt16
    2. Int16.to­UInt16 (structure field)
    3. Nat.to­UInt16
  95. to­UInt32
    1. Bool.to­UInt32
    2. Int32.to­UInt32 (structure field)
    3. Nat.to­UInt32
  96. to­UInt64
    1. Bool.to­UInt64
    2. Int64.to­UInt64 (structure field)
    3. Nat.to­UInt64
  97. to­UInt8
    1. Bool.to­UInt8
    2. Int8.to­UInt8 (structure field)
    3. Nat.to­UInt8
  98. to­USize
    1. Bool.to­USize
    2. Nat.to­USize
  99. to­UTF8
    1. String.to­UTF8
  100. to­Upper
    1. String.to­Upper
  101. trace
    1. Lean.Macro.trace
    2. tactic.simp.trace (0) (1)
  102. trace.Meta.Tactic.simp.discharge
  103. trace.Meta.Tactic.simp.rewrite
  104. trace_state (0) (1)
  105. transparency
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  106. trim
    1. String.trim
  107. trim­Left
    1. String.trim­Left
  108. trim­Right
    1. String.trim­Right
  109. trivial
  110. truncate
    1. IO.FS.Handle.truncate
  111. try (0) (1)
  112. try­Catch
    1. EStateM.try­Catch
    2. Except.try­Catch
    3. ExceptT.try­Catch
    4. Lean.Elab.Tactic.try­Catch
    5. MonadExcept.try­Catch (class method)
    6. Monad­ExceptOf.try­Catch (class method)
    7. OptionT.try­Catch
  113. try­Catch­The
  114. try­Finally'
    1. MonadFinally.try­Finally' (class method)
  115. try­Lock
    1. IO.FS.Handle.try­Lock
  116. try­Tactic
    1. Lean.Elab.Tactic.try­Tactic
  117. try­Tactic?
    1. Lean.Elab.Tactic.try­Tactic?
  118. try­Wait
    1. IO.Process.Child.try­Wait
  119. type
    1. IO.FS.Metadata.type (structure field)
  120. type constructor

U

  1. UInt16
  2. UInt16.mk
    1. Constructor of UInt16
  3. UInt32
  4. UInt32.mk
    1. Constructor of UInt32
  5. UInt64
  6. UInt64.mk
    1. Constructor of UInt64
  7. UInt8
  8. UInt8.mk
    1. Constructor of UInt8
  9. ULift
  10. ULift.up
    1. Constructor of ULift
  11. USize
  12. USize.mk
    1. Constructor of USize
  13. Unit
  14. Unit.unit
  15. uget
    1. Array.uget
  16. unattach
    1. Array.unattach
  17. unfold (0) (1)
  18. unfold­Partial­App
    1. Lean.Meta.DSimp.Config.unfold­Partial­App (structure field)
    2. Lean.Meta.Simp.Config.unfold­Partial­App (structure field)
  19. unhygienic
  20. unit
    1. Unit.unit
  21. universe
  22. universe polymorphism
  23. unlock
    1. IO.FS.Handle.unlock
  24. unnecessary­Simpa
    1. linter.unnecessary­Simpa
  25. unsupported­Syntax
    1. Lean.Macro.Exception.unsupported­Syntax
  26. unzip
    1. Array.unzip
  27. user
    1. IO.FileRight.user (structure field)
  28. user­Error
    1. IO.user­Error
  29. uset
    1. Array.uset
  30. usize
    1. Array.usize
  31. utf16Length
    1. String.utf16Length
  32. utf16Pos­To­Codepoint­Pos
    1. String.utf16Pos­To­Codepoint­Pos
  33. utf16Pos­To­Codepoint­Pos­From
    1. String.utf16Pos­To­Codepoint­Pos­From
  34. utf8Byte­Size
    1. String.utf8Byte­Size
  35. utf8Decode­Char?
    1. String.utf8Decode­Char?
  36. utf8Encode­Char
    1. String.utf8Encode­Char

V

  1. val
    1. Char.val (structure field)
    2. Fin.val (structure field)
    3. Subtype.val (structure field)
  2. valid
    1. Char.valid (structure field)
  3. validate­UTF8
    1. String.validate­UTF8

W

  1. wait
    1. IO.Process.Child.wait
    2. IO.wait
  2. wait­Any
    1. IO.wait­Any
  3. walk­Dir
    1. System.FilePath.walk­Dir
  4. whnf
  5. with­Extension
    1. System.FilePath.with­Extension
  6. with­File
    1. IO.FS.with­File
  7. with­File­Name
    1. System.FilePath.with­File­Name
  8. with­Fresh­Macro­Scope
    1. Lean.Macro.with­Fresh­Macro­Scope
  9. with­Isolated­Streams
    1. IO.FS.with­Isolated­Streams (0) (1)
  10. with­Location
    1. Lean.Elab.Tactic.with­Location
  11. with­Position
  12. with­Position­After­Linebreak
  13. with­Reader
    1. Monad­WithReader.with­Reader (class method)
    2. Monad­With­ReaderOf.with­Reader (class method)
  14. with­Stderr
    1. IO.with­Stderr
  15. with­Stdin
    1. IO.with­Stdin
  16. with­Stdout
    1. IO.with­Stdout
  17. with­Temp­File
    1. IO.FS.with­Temp­File
  18. with­The­Reader
  19. with_reducible
  20. with_reducible_and_instances
  21. with_unfolding_all
  22. without­Position
  23. write
    1. IO.FS.Handle.write
    2. IO.FS.Stream.write (structure field)
  24. write­Bin­File
    1. IO.FS.write­Bin­File
  25. write­File
    1. IO.FS.write­File

X

  1. xor
    1. Bool.xor
    2. Nat.xor

Z

  1. Zero
  2. Zero.mk
    1. Instance constructor of Zero
  3. zero
    1. Zero.zero (class method)
  4. zeta
    1. Lean.Meta.DSimp.Config.zeta (structure field)
    2. Lean.Meta.Simp.Config.zeta (structure field)
  5. zeta­Delta
    1. Lean.Meta.DSimp.Config.zeta­Delta (structure field)
    2. Lean.Meta.Simp.Config.zeta­Delta (structure field)
  6. zip
    1. Array.zip
  7. zip­With
    1. Array.zip­With
  8. zip­With­Index
    1. Array.zip­With­Index
OptionT
```exceptions
```

LawfulFunctor
```exceptions
```

Function
Function.comp, Function.curry, Function.const, Function.uncurry
{docstring Function.comp}
{docstring Function.curry}
{docstring Function.const}
{docstring Function.uncurry}

```exceptions
Function.comp
Function.curry
Function.const
Function.uncurry
```

Subarray
```exceptions
```

Task
Task.bind, Task.map
{docstring Task.bind}
{docstring Task.map}

```exceptions
Task.bind
Task.map
```

MonadFunctorT
```exceptions
```

Int16
Int16.shiftLeft, Int16.decLe, Int16.le, Int16.toInt8, Int16.div, Int16.lor, Int16.ofInt, Int16.land, Int16.mod, Int16.add, Int16.complement, Int16.xor, Int16.ofNat, Int16.lt, Int16.toBitVec, Int16.toInt, Int16.decEq, Int16.shiftRight, Int16.toInt64, Int16.decLt, Int16.size, Int16.sub, Int16.toNat, Int16.mul, Int16.neg, Int16.toInt32
{docstring Int16.shiftLeft}
{docstring Int16.decLe}
{docstring Int16.le}
{docstring Int16.toInt8}
{docstring Int16.div}
{docstring Int16.lor}
{docstring Int16.ofInt}
{docstring Int16.land}
{docstring Int16.mod}
{docstring Int16.add}
{docstring Int16.complement}
{docstring Int16.xor}
{docstring Int16.ofNat}
{docstring Int16.lt}
{docstring Int16.toBitVec}
{docstring Int16.toInt}
{docstring Int16.decEq}
{docstring Int16.shiftRight}
{docstring Int16.toInt64}
{docstring Int16.decLt}
{docstring Int16.size}
{docstring Int16.sub}
{docstring Int16.toNat}
{docstring Int16.mul}
{docstring Int16.neg}
{docstring Int16.toInt32}

```exceptions
Int16.shiftLeft
Int16.decLe
Int16.le
Int16.toInt8
Int16.div
Int16.lor
Int16.ofInt
Int16.land
Int16.mod
Int16.add
Int16.complement
Int16.xor
Int16.ofNat
Int16.lt
Int16.toBitVec
Int16.toInt
Int16.decEq
Int16.shiftRight
Int16.toInt64
Int16.decLt
Int16.size
Int16.sub
Int16.toNat
Int16.mul
Int16.neg
Int16.toInt32
```

IO.Process
```exceptions
```

Functor
```exceptions
```

MonadStateOf
```exceptions
```

ReaderT
```exceptions
```

UInt64
UInt64.reduceToNat, UInt64.size, UInt64.toUInt16, UInt64.mod, UInt64.ofNat, UInt64.toUSize, UInt64.lor, UInt64.decLt, UInt64.reduceMul, UInt64.reduceGT, UInt64.land, UInt64.reduceLE, UInt64.shiftRight, UInt64.ofNatCore, UInt64.complement, UInt64.val, UInt64.toFloat, UInt64.reduceMod, UInt64.toNat, UInt64.add, UInt64.reduceAdd, UInt64.div, UInt64.reduceDiv, UInt64.toUInt8, UInt64.le, UInt64.toUInt32, UInt64.reduceGE, UInt64.mul, UInt64.reduceSub, UInt64.reduceOfNatCore, UInt64.sub, UInt64.fromExpr, UInt64.lt, UInt64.log2, UInt64.xor, UInt64.decLe, UInt64.shiftLeft, UInt64.decEq, UInt64.reduceOfNat, UInt64.reduceLT
{docstring UInt64.reduceToNat}
{docstring UInt64.size}
{docstring UInt64.toUInt16}
{docstring UInt64.mod}
{docstring UInt64.ofNat}
{docstring UInt64.toUSize}
{docstring UInt64.lor}
{docstring UInt64.decLt}
{docstring UInt64.reduceMul}
{docstring UInt64.reduceGT}
{docstring UInt64.land}
{docstring UInt64.reduceLE}
{docstring UInt64.shiftRight}
{docstring UInt64.ofNatCore}
{docstring UInt64.complement}
{docstring UInt64.val}
{docstring UInt64.toFloat}
{docstring UInt64.reduceMod}
{docstring UInt64.toNat}
{docstring UInt64.add}
{docstring UInt64.reduceAdd}
{docstring UInt64.div}
{docstring UInt64.reduceDiv}
{docstring UInt64.toUInt8}
{docstring UInt64.le}
{docstring UInt64.toUInt32}
{docstring UInt64.reduceGE}
{docstring UInt64.mul}
{docstring UInt64.reduceSub}
{docstring UInt64.reduceOfNatCore}
{docstring UInt64.sub}
{docstring UInt64.fromExpr}
{docstring UInt64.lt}
{docstring UInt64.log2}
{docstring UInt64.xor}
{docstring UInt64.decLe}
{docstring UInt64.shiftLeft}
{docstring UInt64.decEq}
{docstring UInt64.reduceOfNat}
{docstring UInt64.reduceLT}

```exceptions
UInt64.reduceToNat
UInt64.size
UInt64.toUInt16
UInt64.mod
UInt64.ofNat
UInt64.toUSize
UInt64.lor
UInt64.decLt
UInt64.reduceMul
UInt64.reduceGT
UInt64.land
UInt64.reduceLE
UInt64.shiftRight
UInt64.ofNatCore
UInt64.complement
UInt64.val
UInt64.toFloat
UInt64.reduceMod
UInt64.toNat
UInt64.add
UInt64.reduceAdd
UInt64.div
UInt64.reduceDiv
UInt64.toUInt8
UInt64.le
UInt64.toUInt32
UInt64.reduceGE
UInt64.mul
UInt64.reduceSub
UInt64.reduceOfNatCore
UInt64.sub
UInt64.fromExpr
UInt64.lt
UInt64.log2
UInt64.xor
UInt64.decLe
UInt64.shiftLeft
UInt64.decEq
UInt64.reduceOfNat
UInt64.reduceLT
```

IO.Process.StdioConfig
```exceptions
```

System.Platform
System.Platform.getNumBits, System.Platform.isOSX, System.Platform.getIsWindows, System.Platform.numBits, System.Platform.getIsEmscripten, System.Platform.isEmscripten, System.Platform.getIsOSX, System.Platform.target, System.Platform.isWindows, System.Platform.getTarget
{docstring System.Platform.getNumBits}
{docstring System.Platform.isOSX}
{docstring System.Platform.getIsWindows}
{docstring System.Platform.numBits}
{docstring System.Platform.getIsEmscripten}
{docstring System.Platform.isEmscripten}
{docstring System.Platform.getIsOSX}
{docstring System.Platform.target}
{docstring System.Platform.isWindows}
{docstring System.Platform.getTarget}

```exceptions
System.Platform.getNumBits
System.Platform.isOSX
System.Platform.getIsWindows
System.Platform.numBits
System.Platform.getIsEmscripten
System.Platform.isEmscripten
System.Platform.getIsOSX
System.Platform.target
System.Platform.isWindows
System.Platform.getTarget
```

String
String.dropSuffix?, String.stripSuffix, String.stripPrefix, String.dropPrefix?
{docstring String.dropSuffix?}
{docstring String.stripSuffix}
{docstring String.stripPrefix}
{docstring String.dropPrefix?}

```exceptions
String.dropSuffix?
String.stripSuffix
String.stripPrefix
String.dropPrefix?
```

EStateM.Result
```exceptions
```

ForM
```exceptions
```

System
```exceptions
```

ULift
```exceptions
```

Decidable
```exceptions
```

IO
IO.getTID
{docstring IO.getTID}

```exceptions
IO.getTID
```

Int8
Int8.decEq, Int8.toInt16, Int8.shiftLeft, Int8.toInt64, Int8.toInt, Int8.mul, Int8.complement, Int8.div, Int8.mod, Int8.lor, Int8.neg, Int8.le, Int8.shiftRight, Int8.size, Int8.sub, Int8.toInt32, Int8.add, Int8.lt, Int8.decLt, Int8.toBitVec, Int8.ofNat, Int8.decLe, Int8.ofInt, Int8.xor, Int8.toNat, Int8.land
{docstring Int8.decEq}
{docstring Int8.toInt16}
{docstring Int8.shiftLeft}
{docstring Int8.toInt64}
{docstring Int8.toInt}
{docstring Int8.mul}
{docstring Int8.complement}
{docstring Int8.div}
{docstring Int8.mod}
{docstring Int8.lor}
{docstring Int8.neg}
{docstring Int8.le}
{docstring Int8.shiftRight}
{docstring Int8.size}
{docstring Int8.sub}
{docstring Int8.toInt32}
{docstring Int8.add}
{docstring Int8.lt}
{docstring Int8.decLt}
{docstring Int8.toBitVec}
{docstring Int8.ofNat}
{docstring Int8.decLe}
{docstring Int8.ofInt}
{docstring Int8.xor}
{docstring Int8.toNat}
{docstring Int8.land}

```exceptions
Int8.decEq
Int8.toInt16
Int8.shiftLeft
Int8.toInt64
Int8.toInt
Int8.mul
Int8.complement
Int8.div
Int8.mod
Int8.lor
Int8.neg
Int8.le
Int8.shiftRight
Int8.size
Int8.sub
Int8.toInt32
Int8.add
Int8.lt
Int8.decLt
Int8.toBitVec
Int8.ofNat
Int8.decLe
Int8.ofInt
Int8.xor
Int8.toNat
Int8.land
```

MonadState
```exceptions
```

MonadFunctor
```exceptions
```

ReaderM
```exceptions
```

Subtype
```exceptions
```

PLift
```exceptions
```

Pure
```exceptions
```

EIO
```exceptions
```

Task.Priority
```exceptions
```

Int64
Int64.complement, Int64.toInt, Int64.div, Int64.mod, Int64.toInt8, Int64.decLt, Int64.land, Int64.toInt32, Int64.neg, Int64.le, Int64.shiftLeft, Int64.decLe, Int64.mul, Int64.add, Int64.decEq, Int64.sub, Int64.toBitVec, Int64.lor, Int64.lt, Int64.ofNat, Int64.size, Int64.ofInt, Int64.shiftRight, Int64.xor, Int64.toISize, Int64.toNat, Int64.toInt16
{docstring Int64.complement}
{docstring Int64.toInt}
{docstring Int64.div}
{docstring Int64.mod}
{docstring Int64.toInt8}
{docstring Int64.decLt}
{docstring Int64.land}
{docstring Int64.toInt32}
{docstring Int64.neg}
{docstring Int64.le}
{docstring Int64.shiftLeft}
{docstring Int64.decLe}
{docstring Int64.mul}
{docstring Int64.add}
{docstring Int64.decEq}
{docstring Int64.sub}
{docstring Int64.toBitVec}
{docstring Int64.lor}
{docstring Int64.lt}
{docstring Int64.ofNat}
{docstring Int64.size}
{docstring Int64.ofInt}
{docstring Int64.shiftRight}
{docstring Int64.xor}
{docstring Int64.toISize}
{docstring Int64.toNat}
{docstring Int64.toInt16}

```exceptions
Int64.complement
Int64.toInt
Int64.div
Int64.mod
Int64.toInt8
Int64.decLt
Int64.land
Int64.toInt32
Int64.neg
Int64.le
Int64.shiftLeft
Int64.decLe
Int64.mul
Int64.add
Int64.decEq
Int64.sub
Int64.toBitVec
Int64.lor
Int64.lt
Int64.ofNat
Int64.size
Int64.ofInt
Int64.shiftRight
Int64.xor
Int64.toISize
Int64.toNat
Int64.toInt16
```

LawfulMonad
```exceptions
```

IO.Process.Output
```exceptions
```

IO.FileRight
```exceptions
```

MonadLiftT
```exceptions
```

Id
```exceptions
```

IO.Process.Child
```exceptions
```

ForInStep
ForInStep.value
{docstring ForInStep.value}

```exceptions
ForInStep.value
```

MonadExcept
```exceptions
```

ExceptT
```exceptions
```

Applicative
```exceptions
```

StateCpsT
```exceptions
```

ForIn'
```exceptions
```

Array
Array.insertIdxIfInBounds, Array.insertIdx.loop, Array.insertIdx, Array.findFinIdx?.loop, Array.eraseP, Array.pmap, Array.swapIfInBounds, Array.zipWithAll.go, Array.finRange, Array.eraseIdxIfInBounds, Array.«term__[:_]», Array.findFinIdx?, Array.insertIdx!, Array.eraseIdx!, Array.«term__[_:]», Array.setIfInBounds, Array.zipWithAll, Array.«term__[_:_]»
{docstring Array.insertIdxIfInBounds}
{docstring Array.insertIdx.loop}
{docstring Array.insertIdx}
{docstring Array.findFinIdx?.loop}
{docstring Array.eraseP}
{docstring Array.pmap}
{docstring Array.swapIfInBounds}
{docstring Array.zipWithAll.go}
{docstring Array.finRange}
{docstring Array.eraseIdxIfInBounds}
{docstring Array.«term__[:_]»}
{docstring Array.findFinIdx?}
{docstring Array.insertIdx!}
{docstring Array.eraseIdx!}
{docstring Array.«term__[_:]»}
{docstring Array.setIfInBounds}
{docstring Array.zipWithAll}
{docstring Array.«term__[_:_]»}

```exceptions
Array.insertIdxIfInBounds
Array.insertIdx.loop
Array.insertIdx
Array.findFinIdx?.loop
Array.eraseP
Array.pmap
Array.swapIfInBounds
Array.zipWithAll.go
Array.finRange
Array.eraseIdxIfInBounds
Array.«term__[:_]»
Array.findFinIdx?
Array.insertIdx!
Array.eraseIdx!
Array.«term__[_:]»
Array.setIfInBounds
Array.zipWithAll
Array.«term__[_:_]»
```

IO.Process.Stdio
```exceptions
```

IO.FS.Stream.Buffer
```exceptions
```

MonadLift
```exceptions
```

SeqLeft
```exceptions
```

IO.FS.Metadata
```exceptions
```

SeqRight
```exceptions
```

List
List.head?, List.unattach, List.zipWithTR, List.head, List.splitInTwo, List.eraseReps, List.iota, List.getLast, List.mapIdx, List.asString, List.all, List.rotateRight, List.replicate, List.countP, List.mapMonoM, List.min?, List.zipWith, List.toArrayImpl, List.mapTR.loop, List.eraseTR, List.eraseIdx, List.partitionMap, List.nonzeroMinimum, List.partitionM.go, List.findSomeM?, List.eraseDups.loop, List.getLast?, List.toAssocList', List.foldlM, List.allM, List.range'TR.go, List.mapM.loop, List.attachWith, List.elem, List.flatMapTR.go, List.filterTR.loop, List.concat, List.get, List.map, List.enumFromTR, List.filterMapTR.go, List.range'TR, List.«term_<:+_», List.isEqv, List.contains, List.tail?, List.removeAll, List.insertIdx, List.iotaTR.go, List.sum, List.merge, List.setTR.go, List.range', List.mapIdx.go, List.head!, List.find?, List.reverseAux, List.ofFn, List.format, List.reduceReplicate, List.forA, List.intersperseTR, List.takeTR, List.modify, List.«term_<+_», List.eraseTR.go, List.getD, List.span.loop, List.foldrM, List.replaceTR, List.«term_<:+:_», List.mapM', List.toByteArray.loop, List.intercalateTR, List.repr, List.or, List.mapFinIdx, List.set, List.findIdx?, List.toFloatArray.loop, List.indexOf, List.insertIdxTR, List.filterMapTR, List.toSSet, List.zipWithAll, List.zip, List.dropLast, List.modifyTR.go, List.countP.go, List.range, List.foldl, List.replicateTR, List.mapM, List.toByteArray, List.eraseDups, List.replace, List.isSuffixOf?, List.max?, List.toPArray', List.tail, List.filterRevM, List.findM?, List.splitBy, List.foldrTR, List.isSublist, List.foldlRecOn, List.and, List.toArray, List.isPrefixOf, List.eraseIdxTR.go, List.enumFrom, List.flattenTR, List.append, List.headD, List.eraseIdxTR, List.isPerm, List.erasePTR, List.pmap, List.toPArray'.loop, List.singleton, List.flatMapTR, List.unzip, List.count, List.filterAuxM, List.erase, List.maxNatAbs, List.span, List.leftpad, List.drop, List.repr', List.intercalateTR.go, List.splitBy.loop, List.modifyTR, List.takeWhileTR, List.lengthTRAux, List.findSome?, List.indexOf?, List.isEmpty, List.enumLE, List.lookup, List.«term_<+:_», List.erasePTR.go, List.partitionM, List.takeTR.go, List.filter, List.getLastD, List.isSuffixOf, List.le, List.mapMono, List.foldrRecOn, List.findIdx, List.intercalate, List.reverse, List.filterTR, List.lt.below, List.eraseReps.loop, List.get!, List.rotateLeft, List.leftpadTR, List.forIn'.loop, List.any, List.zipWithTR.go, List.splitAt, List.splitAt.go, List.get?, List.beq, List.modifyHead, List.toArrayAux, List.firstM, List.modifyTailIdx, List.filterMapM.loop, List.toFloatArray, List.tailD, List.iotaTR, List.reduceOption, List.hasDecEq, List.replaceTR.go, List.tail!, List.toString, List.filterMap, List.toSMap, List.mapTR, List.getLast!, List.eraseP, List.partition.loop, List.forM, List.findIdx.go, List.intersperse, List.dropWhile, List.finRange, List.isPrefixOf?, List.foldr, List.appendTR, List.takeWhile, List.takeWhileTR.go, List.rightpad, List.take, List.length, List.filterMapM, List.attach, List.mapFinIdx.go, List.replicateTR.loop, List.mergeSort, List.insert, List.partition, List.anyM, List.flatMap, List.unzipTR, List.filterM, List.lengthTR, List.lt, List.mapA, List.minNatAbs, List.partitionMap.go, List.setTR, List.flatten, List.«term_~_», List.enum, List.insertIdxTR.go, List.range.loop, List.forIn', List.dropLastTR, List.groupByKey
{docstring List.head?}
{docstring List.unattach}
{docstring List.zipWithTR}
{docstring List.head}
{docstring List.splitInTwo}
{docstring List.eraseReps}
{docstring List.iota}
{docstring List.getLast}
{docstring List.mapIdx}
{docstring List.asString}
{docstring List.all}
{docstring List.rotateRight}
{docstring List.replicate}
{docstring List.countP}
{docstring List.mapMonoM}
{docstring List.min?}
{docstring List.zipWith}
{docstring List.toArrayImpl}
{docstring List.mapTR.loop}
{docstring List.eraseTR}
{docstring List.eraseIdx}
{docstring List.partitionMap}
{docstring List.nonzeroMinimum}
{docstring List.partitionM.go}
{docstring List.findSomeM?}
{docstring List.eraseDups.loop}
{docstring List.getLast?}
{docstring List.toAssocList'}
{docstring List.foldlM}
{docstring List.allM}
{docstring List.range'TR.go}
{docstring List.mapM.loop}
{docstring List.attachWith}
{docstring List.elem}
{docstring List.flatMapTR.go}
{docstring List.filterTR.loop}
{docstring List.concat}
{docstring List.get}
{docstring List.map}
{docstring List.enumFromTR}
{docstring List.filterMapTR.go}
{docstring List.range'TR}
{docstring List.«term_<:+_»}
{docstring List.isEqv}
{docstring List.contains}
{docstring List.tail?}
{docstring List.removeAll}
{docstring List.insertIdx}
{docstring List.iotaTR.go}
{docstring List.sum}
{docstring List.merge}
{docstring List.setTR.go}
{docstring List.range'}
{docstring List.mapIdx.go}
{docstring List.head!}
{docstring List.find?}
{docstring List.reverseAux}
{docstring List.ofFn}
{docstring List.format}
{docstring List.reduceReplicate}
{docstring List.forA}
{docstring List.intersperseTR}
{docstring List.takeTR}
{docstring List.modify}
{docstring List.«term_<+_»}
{docstring List.eraseTR.go}
{docstring List.getD}
{docstring List.span.loop}
{docstring List.foldrM}
{docstring List.replaceTR}
{docstring List.«term_<:+:_»}
{docstring List.mapM'}
{docstring List.toByteArray.loop}
{docstring List.intercalateTR}
{docstring List.repr}
{docstring List.or}
{docstring List.mapFinIdx}
{docstring List.set}
{docstring List.findIdx?}
{docstring List.toFloatArray.loop}
{docstring List.indexOf}
{docstring List.insertIdxTR}
{docstring List.filterMapTR}
{docstring List.toSSet}
{docstring List.zipWithAll}
{docstring List.zip}
{docstring List.dropLast}
{docstring List.modifyTR.go}
{docstring List.countP.go}
{docstring List.range}
{docstring List.foldl}
{docstring List.replicateTR}
{docstring List.mapM}
{docstring List.toByteArray}
{docstring List.eraseDups}
{docstring List.replace}
{docstring List.isSuffixOf?}
{docstring List.max?}
{docstring List.toPArray'}
{docstring List.tail}
{docstring List.filterRevM}
{docstring List.findM?}
{docstring List.splitBy}
{docstring List.foldrTR}
{docstring List.isSublist}
{docstring List.foldlRecOn}
{docstring List.and}
{docstring List.toArray}
{docstring List.isPrefixOf}
{docstring List.eraseIdxTR.go}
{docstring List.enumFrom}
{docstring List.flattenTR}
{docstring List.append}
{docstring List.headD}
{docstring List.eraseIdxTR}
{docstring List.isPerm}
{docstring List.erasePTR}
{docstring List.pmap}
{docstring List.toPArray'.loop}
{docstring List.singleton}
{docstring List.flatMapTR}
{docstring List.unzip}
{docstring List.count}
{docstring List.filterAuxM}
{docstring List.erase}
{docstring List.maxNatAbs}
{docstring List.span}
{docstring List.leftpad}
{docstring List.drop}
{docstring List.repr'}
{docstring List.intercalateTR.go}
{docstring List.splitBy.loop}
{docstring List.modifyTR}
{docstring List.takeWhileTR}
{docstring List.lengthTRAux}
{docstring List.findSome?}
{docstring List.indexOf?}
{docstring List.isEmpty}
{docstring List.enumLE}
{docstring List.lookup}
{docstring List.«term_<+:_»}
{docstring List.erasePTR.go}
{docstring List.partitionM}
{docstring List.takeTR.go}
{docstring List.filter}
{docstring List.getLastD}
{docstring List.isSuffixOf}
{docstring List.le}
{docstring List.mapMono}
{docstring List.foldrRecOn}
{docstring List.findIdx}
{docstring List.intercalate}
{docstring List.reverse}
{docstring List.filterTR}
{docstring List.lt.below}
{docstring List.eraseReps.loop}
{docstring List.get!}
{docstring List.rotateLeft}
{docstring List.leftpadTR}
{docstring List.forIn'.loop}
{docstring List.any}
{docstring List.zipWithTR.go}
{docstring List.splitAt}
{docstring List.splitAt.go}
{docstring List.get?}
{docstring List.beq}
{docstring List.modifyHead}
{docstring List.toArrayAux}
{docstring List.firstM}
{docstring List.modifyTailIdx}
{docstring List.filterMapM.loop}
{docstring List.toFloatArray}
{docstring List.tailD}
{docstring List.iotaTR}
{docstring List.reduceOption}
{docstring List.hasDecEq}
{docstring List.replaceTR.go}
{docstring List.tail!}
{docstring List.toString}
{docstring List.filterMap}
{docstring List.toSMap}
{docstring List.mapTR}
{docstring List.getLast!}
{docstring List.eraseP}
{docstring List.partition.loop}
{docstring List.forM}
{docstring List.findIdx.go}
{docstring List.intersperse}
{docstring List.dropWhile}
{docstring List.finRange}
{docstring List.isPrefixOf?}
{docstring List.foldr}
{docstring List.appendTR}
{docstring List.takeWhile}
{docstring List.takeWhileTR.go}
{docstring List.rightpad}
{docstring List.take}
{docstring List.length}
{docstring List.filterMapM}
{docstring List.attach}
{docstring List.mapFinIdx.go}
{docstring List.replicateTR.loop}
{docstring List.mergeSort}
{docstring List.insert}
{docstring List.partition}
{docstring List.anyM}
{docstring List.flatMap}
{docstring List.unzipTR}
{docstring List.filterM}
{docstring List.lengthTR}
{docstring List.lt}
{docstring List.mapA}
{docstring List.minNatAbs}
{docstring List.partitionMap.go}
{docstring List.setTR}
{docstring List.flatten}
{docstring List.«term_~_»}
{docstring List.enum}
{docstring List.insertIdxTR.go}
{docstring List.range.loop}
{docstring List.forIn'}
{docstring List.dropLastTR}
{docstring List.groupByKey}

```exceptions
List.head?
List.unattach
List.zipWithTR
List.head
List.splitInTwo
List.eraseReps
List.iota
List.getLast
List.mapIdx
List.asString
List.all
List.rotateRight
List.replicate
List.countP
List.mapMonoM
List.min?
List.zipWith
List.toArrayImpl
List.mapTR.loop
List.eraseTR
List.eraseIdx
List.partitionMap
List.nonzeroMinimum
List.partitionM.go
List.findSomeM?
List.eraseDups.loop
List.getLast?
List.toAssocList'
List.foldlM
List.allM
List.range'TR.go
List.mapM.loop
List.attachWith
List.elem
List.flatMapTR.go
List.filterTR.loop
List.concat
List.get
List.map
List.enumFromTR
List.filterMapTR.go
List.range'TR
List.«term_<:+_»
List.isEqv
List.contains
List.tail?
List.removeAll
List.insertIdx
List.iotaTR.go
List.sum
List.merge
List.setTR.go
List.range'
List.mapIdx.go
List.head!
List.find?
List.reverseAux
List.ofFn
List.format
List.reduceReplicate
List.forA
List.intersperseTR
List.takeTR
List.modify
List.«term_<+_»
List.eraseTR.go
List.getD
List.span.loop
List.foldrM
List.replaceTR
List.«term_<:+:_»
List.mapM'
List.toByteArray.loop
List.intercalateTR
List.repr
List.or
List.mapFinIdx
List.set
List.findIdx?
List.toFloatArray.loop
List.indexOf
List.insertIdxTR
List.filterMapTR
List.toSSet
List.zipWithAll
List.zip
List.dropLast
List.modifyTR.go
List.countP.go
List.range
List.foldl
List.replicateTR
List.mapM
List.toByteArray
List.eraseDups
List.replace
List.isSuffixOf?
List.max?
List.toPArray'
List.tail
List.filterRevM
List.findM?
List.splitBy
List.foldrTR
List.isSublist
List.foldlRecOn
List.and
List.toArray
List.isPrefixOf
List.eraseIdxTR.go
List.enumFrom
List.flattenTR
List.append
List.headD
List.eraseIdxTR
List.isPerm
List.erasePTR
List.pmap
List.toPArray'.loop
List.singleton
List.flatMapTR
List.unzip
List.count
List.filterAuxM
List.erase
List.maxNatAbs
List.span
List.leftpad
List.drop
List.repr'
List.intercalateTR.go
List.splitBy.loop
List.modifyTR
List.takeWhileTR
List.lengthTRAux
List.findSome?
List.indexOf?
List.isEmpty
List.enumLE
List.lookup
List.«term_<+:_»
List.erasePTR.go
List.partitionM
List.takeTR.go
List.filter
List.getLastD
List.isSuffixOf
List.le
List.mapMono
List.foldrRecOn
List.findIdx
List.intercalate
List.reverse
List.filterTR
List.lt.below
List.eraseReps.loop
List.get!
List.rotateLeft
List.leftpadTR
List.forIn'.loop
List.any
List.zipWithTR.go
List.splitAt
List.splitAt.go
List.get?
List.beq
List.modifyHead
List.toArrayAux
List.firstM
List.modifyTailIdx
List.filterMapM.loop
List.toFloatArray
List.tailD
List.iotaTR
List.reduceOption
List.hasDecEq
List.replaceTR.go
List.tail!
List.toString
List.filterMap
List.toSMap
List.mapTR
List.getLast!
List.eraseP
List.partition.loop
List.forM
List.findIdx.go
List.intersperse
List.dropWhile
List.finRange
List.isPrefixOf?
List.foldr
List.appendTR
List.takeWhile
List.takeWhileTR.go
List.rightpad
List.take
List.length
List.filterMapM
List.attach
List.mapFinIdx.go
List.replicateTR.loop
List.mergeSort
List.insert
List.partition
List.anyM
List.flatMap
List.unzipTR
List.filterM
List.lengthTR
List.lt
List.mapA
List.minNatAbs
List.partitionMap.go
List.setTR
List.flatten
List.«term_~_»
List.enum
List.insertIdxTR.go
List.range.loop
List.forIn'
List.dropLastTR
List.groupByKey
```

UInt16
UInt16.log2, UInt16.mod, UInt16.decLt, UInt16.reduceLE, UInt16.reduceGE, UInt16.size, UInt16.reduceOfNat, UInt16.reduceMul, UInt16.complement, UInt16.reduceOfNatCore, UInt16.le, UInt16.ofNatCore, UInt16.reduceMod, UInt16.reduceDiv, UInt16.lt, UInt16.val, UInt16.xor, UInt16.div, UInt16.shiftRight, UInt16.toUSize, UInt16.ofNat, UInt16.reduceGT, UInt16.toUInt8, UInt16.decEq, UInt16.sub, UInt16.land, UInt16.lor, UInt16.toUInt64, UInt16.add, UInt16.decLe, UInt16.toNat, UInt16.reduceAdd, UInt16.reduceToNat, UInt16.reduceSub, UInt16.reduceLT, UInt16.mul, UInt16.shiftLeft, UInt16.toUInt32, UInt16.fromExpr
{docstring UInt16.log2}
{docstring UInt16.mod}
{docstring UInt16.decLt}
{docstring UInt16.reduceLE}
{docstring UInt16.reduceGE}
{docstring UInt16.size}
{docstring UInt16.reduceOfNat}
{docstring UInt16.reduceMul}
{docstring UInt16.complement}
{docstring UInt16.reduceOfNatCore}
{docstring UInt16.le}
{docstring UInt16.ofNatCore}
{docstring UInt16.reduceMod}
{docstring UInt16.reduceDiv}
{docstring UInt16.lt}
{docstring UInt16.val}
{docstring UInt16.xor}
{docstring UInt16.div}
{docstring UInt16.shiftRight}
{docstring UInt16.toUSize}
{docstring UInt16.ofNat}
{docstring UInt16.reduceGT}
{docstring UInt16.toUInt8}
{docstring UInt16.decEq}
{docstring UInt16.sub}
{docstring UInt16.land}
{docstring UInt16.lor}
{docstring UInt16.toUInt64}
{docstring UInt16.add}
{docstring UInt16.decLe}
{docstring UInt16.toNat}
{docstring UInt16.reduceAdd}
{docstring UInt16.reduceToNat}
{docstring UInt16.reduceSub}
{docstring UInt16.reduceLT}
{docstring UInt16.mul}
{docstring UInt16.shiftLeft}
{docstring UInt16.toUInt32}
{docstring UInt16.fromExpr}

```exceptions
UInt16.log2
UInt16.mod
UInt16.decLt
UInt16.reduceLE
UInt16.reduceGE
UInt16.size
UInt16.reduceOfNat
UInt16.reduceMul
UInt16.complement
UInt16.reduceOfNatCore
UInt16.le
UInt16.ofNatCore
UInt16.reduceMod
UInt16.reduceDiv
UInt16.lt
UInt16.val
UInt16.xor
UInt16.div
UInt16.shiftRight
UInt16.toUSize
UInt16.ofNat
UInt16.reduceGT
UInt16.toUInt8
UInt16.decEq
UInt16.sub
UInt16.land
UInt16.lor
UInt16.toUInt64
UInt16.add
UInt16.decLe
UInt16.toNat
UInt16.reduceAdd
UInt16.reduceToNat
UInt16.reduceSub
UInt16.reduceLT
UInt16.mul
UInt16.shiftLeft
UInt16.toUInt32
UInt16.fromExpr
```

Unit
```exceptions
```

Seq
```exceptions
```

MonadControlT
```exceptions
```

ST
```exceptions
```

StateRefT'
```exceptions
```

IO.FS
IO.FS.createTempDir, IO.FS.withTempDir
{docstring IO.FS.createTempDir}
{docstring IO.FS.withTempDir}

```exceptions
IO.FS.createTempDir
IO.FS.withTempDir
```

PUnit
```exceptions
```

IO.Process.SpawnArgs
```exceptions
```

ForIn
```exceptions
```

Nat
Nat.caseStrongRecOn, Nat.reduceXor, Nat.reduceShiftRight, Nat.reduceOr, Nat.toInt16, Nat.toInt32, Nat.toISize, Nat.toInt8, Nat.reduceAnd, Nat.toInt64, Nat.strongRecOn, Nat.reduceShiftLeft
{docstring Nat.caseStrongRecOn}
{docstring Nat.reduceXor}
{docstring Nat.reduceShiftRight}
{docstring Nat.reduceOr}
{docstring Nat.toInt16}
{docstring Nat.toInt32}
{docstring Nat.toISize}
{docstring Nat.toInt8}
{docstring Nat.reduceAnd}
{docstring Nat.toInt64}
{docstring Nat.strongRecOn}
{docstring Nat.reduceShiftLeft}

```exceptions
Nat.caseStrongRecOn
Nat.reduceXor
Nat.reduceShiftRight
Nat.reduceOr
Nat.toInt16
Nat.toInt32
Nat.toISize
Nat.toInt8
Nat.reduceAnd
Nat.toInt64
Nat.strongRecOn
Nat.reduceShiftLeft
```

IO.FS.DirEntry
```exceptions
```

StateM
```exceptions
```

MonadReader
```exceptions
```

IO.FS.Handle
```exceptions
```

Lean.Elab.Tactic
Lean.Elab.Tactic.tryCatchRestore, Lean.Elab.Tactic.withRWRulesSeq, Lean.Elab.Tactic.unfoldLocalDecl, Lean.Elab.Tactic.expandOptLocation, Lean.Elab.Tactic.expandLocation, Lean.Elab.Tactic.elabChange, Lean.Elab.Tactic.deltaLocalDecl, Lean.Elab.Tactic.addCheckpoints, Lean.Elab.Tactic.mkTacticInfo, Lean.Elab.Tactic.evalClassical, Lean.Elab.Tactic.withCaseRef, Lean.Elab.Tactic.isHoleRHS, Lean.Elab.Tactic.elabDecideConfig, Lean.Elab.Tactic.deltaTarget, Lean.Elab.Tactic.pushGoals, Lean.Elab.Tactic.renameInaccessibles, Lean.Elab.Tactic.commandConfigElab, Lean.Elab.Tactic.getNameOfIdent', Lean.Elab.Tactic.pushGoal, Lean.Elab.Tactic.elabAsFVar, Lean.Elab.Tactic.tactic.customEliminators, Lean.Elab.Tactic.popMainGoal, Lean.Elab.Tactic.getInductiveValFromMajor, Lean.Elab.Tactic.tacticToDischarge, Lean.Elab.Tactic.rewriteLocalDecl, Lean.Elab.Tactic.elabSimpConfigCore, Lean.Elab.Tactic.saveTacticInfoForToken, Lean.Elab.Tactic.focusAndDone, Lean.Elab.Tactic.unfoldTarget, Lean.Elab.Tactic.getMainTarget, Lean.Elab.Tactic.withSimpDiagnostics, Lean.Elab.Tactic.evalDecideCore.doElab, Lean.Elab.Tactic.checkCommandConfigElab, Lean.Elab.Tactic.dsimpLocation, Lean.Elab.Tactic.getMainDecl, Lean.Elab.Tactic.zetaDeltaLocalDecl, Lean.Elab.Tactic.elabTermForApply, Lean.Elab.Tactic.rewriteTarget, Lean.Elab.Tactic.evalDecideCore.doKernel, Lean.Elab.Tactic.configElab, Lean.Elab.Tactic.simpLocation, Lean.Elab.Tactic.refineCore, Lean.Elab.Tactic.evalDecideCore.diagnose, Lean.Elab.Tactic.throwNoGoalsToBeSolved, Lean.Elab.Tactic.closeUsingOrAdmit, Lean.Elab.Tactic.forEachVar, Lean.Elab.Tactic.checkConfigElab, Lean.Elab.Tactic.withTacticInfoContext, Lean.Elab.Tactic.withRestoreOrSaveFull, Lean.Elab.Tactic.logUnassignedAndAbort, Lean.Elab.Tactic.traceSimpCall, Lean.Elab.Tactic.zetaDeltaTarget, Lean.Elab.Tactic.mkSimpContext, Lean.Elab.Tactic.withMacroExpansion, Lean.Elab.Tactic.evalDecideCore, Lean.Elab.Tactic.withCollectingNewGoalsFrom, Lean.Elab.Tactic.withMainContext, Lean.Elab.Tactic.elabRewriteConfig, Lean.Elab.Tactic.mkInitialTacticInfo, Lean.Elab.Tactic.liftMetaFinishingTactic, Lean.Elab.Tactic.mkSimpOnly, Lean.Elab.Tactic.classical, Lean.Elab.Tactic.liftMetaTactic1, Lean.Elab.Tactic.isCheckpointableTactic, Lean.Elab.Tactic.saveState, Lean.Elab.Tactic.mkSimpCallStx, Lean.Elab.Tactic.filterOldMVars, Lean.Elab.Tactic.replaceMainGoal, Lean.Elab.Tactic.liftMetaTactic, Lean.Elab.Tactic.done, Lean.Elab.Tactic.simpOnlyBuiltins, Lean.Elab.Tactic.withoutRecover
{docstring Lean.Elab.Tactic.tryCatchRestore}
{docstring Lean.Elab.Tactic.withRWRulesSeq}
{docstring Lean.Elab.Tactic.unfoldLocalDecl}
{docstring Lean.Elab.Tactic.expandOptLocation}
{docstring Lean.Elab.Tactic.expandLocation}
{docstring Lean.Elab.Tactic.elabChange}
{docstring Lean.Elab.Tactic.deltaLocalDecl}
{docstring Lean.Elab.Tactic.addCheckpoints}
{docstring Lean.Elab.Tactic.mkTacticInfo}
{docstring Lean.Elab.Tactic.evalClassical}
{docstring Lean.Elab.Tactic.withCaseRef}
{docstring Lean.Elab.Tactic.isHoleRHS}
{docstring Lean.Elab.Tactic.elabDecideConfig}
{docstring Lean.Elab.Tactic.deltaTarget}
{docstring Lean.Elab.Tactic.pushGoals}
{docstring Lean.Elab.Tactic.renameInaccessibles}
{docstring Lean.Elab.Tactic.commandConfigElab}
{docstring Lean.Elab.Tactic.getNameOfIdent'}
{docstring Lean.Elab.Tactic.pushGoal}
{docstring Lean.Elab.Tactic.elabAsFVar}
{docstring Lean.Elab.Tactic.tactic.customEliminators}
{docstring Lean.Elab.Tactic.popMainGoal}
{docstring Lean.Elab.Tactic.getInductiveValFromMajor}
{docstring Lean.Elab.Tactic.tacticToDischarge}
{docstring Lean.Elab.Tactic.rewriteLocalDecl}
{docstring Lean.Elab.Tactic.elabSimpConfigCore}
{docstring Lean.Elab.Tactic.saveTacticInfoForToken}
{docstring Lean.Elab.Tactic.focusAndDone}
{docstring Lean.Elab.Tactic.unfoldTarget}
{docstring Lean.Elab.Tactic.getMainTarget}
{docstring Lean.Elab.Tactic.withSimpDiagnostics}
{docstring Lean.Elab.Tactic.evalDecideCore.doElab}
{docstring Lean.Elab.Tactic.checkCommandConfigElab}
{docstring Lean.Elab.Tactic.dsimpLocation}
{docstring Lean.Elab.Tactic.getMainDecl}
{docstring Lean.Elab.Tactic.zetaDeltaLocalDecl}
{docstring Lean.Elab.Tactic.elabTermForApply}
{docstring Lean.Elab.Tactic.rewriteTarget}
{docstring Lean.Elab.Tactic.evalDecideCore.doKernel}
{docstring Lean.Elab.Tactic.configElab}
{docstring Lean.Elab.Tactic.simpLocation}
{docstring Lean.Elab.Tactic.refineCore}
{docstring Lean.Elab.Tactic.evalDecideCore.diagnose}
{docstring Lean.Elab.Tactic.throwNoGoalsToBeSolved}
{docstring Lean.Elab.Tactic.closeUsingOrAdmit}
{docstring Lean.Elab.Tactic.forEachVar}
{docstring Lean.Elab.Tactic.checkConfigElab}
{docstring Lean.Elab.Tactic.withTacticInfoContext}
{docstring Lean.Elab.Tactic.withRestoreOrSaveFull}
{docstring Lean.Elab.Tactic.logUnassignedAndAbort}
{docstring Lean.Elab.Tactic.traceSimpCall}
{docstring Lean.Elab.Tactic.zetaDeltaTarget}
{docstring Lean.Elab.Tactic.mkSimpContext}
{docstring Lean.Elab.Tactic.withMacroExpansion}
{docstring Lean.Elab.Tactic.evalDecideCore}
{docstring Lean.Elab.Tactic.withCollectingNewGoalsFrom}
{docstring Lean.Elab.Tactic.withMainContext}
{docstring Lean.Elab.Tactic.elabRewriteConfig}
{docstring Lean.Elab.Tactic.mkInitialTacticInfo}
{docstring Lean.Elab.Tactic.liftMetaFinishingTactic}
{docstring Lean.Elab.Tactic.mkSimpOnly}
{docstring Lean.Elab.Tactic.classical}
{docstring Lean.Elab.Tactic.liftMetaTactic1}
{docstring Lean.Elab.Tactic.isCheckpointableTactic}
{docstring Lean.Elab.Tactic.saveState}
{docstring Lean.Elab.Tactic.mkSimpCallStx}
{docstring Lean.Elab.Tactic.filterOldMVars}
{docstring Lean.Elab.Tactic.replaceMainGoal}
{docstring Lean.Elab.Tactic.liftMetaTactic}
{docstring Lean.Elab.Tactic.done}
{docstring Lean.Elab.Tactic.simpOnlyBuiltins}
{docstring Lean.Elab.Tactic.withoutRecover}

```exceptions
Lean.Elab.Tactic.tryCatchRestore
Lean.Elab.Tactic.withRWRulesSeq
Lean.Elab.Tactic.unfoldLocalDecl
Lean.Elab.Tactic.expandOptLocation
Lean.Elab.Tactic.expandLocation
Lean.Elab.Tactic.elabChange
Lean.Elab.Tactic.deltaLocalDecl
Lean.Elab.Tactic.addCheckpoints
Lean.Elab.Tactic.mkTacticInfo
Lean.Elab.Tactic.evalClassical
Lean.Elab.Tactic.withCaseRef
Lean.Elab.Tactic.isHoleRHS
Lean.Elab.Tactic.elabDecideConfig
Lean.Elab.Tactic.deltaTarget
Lean.Elab.Tactic.pushGoals
Lean.Elab.Tactic.renameInaccessibles
Lean.Elab.Tactic.commandConfigElab
Lean.Elab.Tactic.getNameOfIdent'
Lean.Elab.Tactic.pushGoal
Lean.Elab.Tactic.elabAsFVar
Lean.Elab.Tactic.tactic.customEliminators
Lean.Elab.Tactic.popMainGoal
Lean.Elab.Tactic.getInductiveValFromMajor
Lean.Elab.Tactic.tacticToDischarge
Lean.Elab.Tactic.rewriteLocalDecl
Lean.Elab.Tactic.elabSimpConfigCore
Lean.Elab.Tactic.saveTacticInfoForToken
Lean.Elab.Tactic.focusAndDone
Lean.Elab.Tactic.unfoldTarget
Lean.Elab.Tactic.getMainTarget
Lean.Elab.Tactic.withSimpDiagnostics
Lean.Elab.Tactic.evalDecideCore.doElab
Lean.Elab.Tactic.checkCommandConfigElab
Lean.Elab.Tactic.dsimpLocation
Lean.Elab.Tactic.getMainDecl
Lean.Elab.Tactic.zetaDeltaLocalDecl
Lean.Elab.Tactic.elabTermForApply
Lean.Elab.Tactic.rewriteTarget
Lean.Elab.Tactic.evalDecideCore.doKernel
Lean.Elab.Tactic.configElab
Lean.Elab.Tactic.simpLocation
Lean.Elab.Tactic.refineCore
Lean.Elab.Tactic.evalDecideCore.diagnose
Lean.Elab.Tactic.throwNoGoalsToBeSolved
Lean.Elab.Tactic.closeUsingOrAdmit
Lean.Elab.Tactic.forEachVar
Lean.Elab.Tactic.checkConfigElab
Lean.Elab.Tactic.withTacticInfoContext
Lean.Elab.Tactic.withRestoreOrSaveFull
Lean.Elab.Tactic.logUnassignedAndAbort
Lean.Elab.Tactic.traceSimpCall
Lean.Elab.Tactic.zetaDeltaTarget
Lean.Elab.Tactic.mkSimpContext
Lean.Elab.Tactic.withMacroExpansion
Lean.Elab.Tactic.evalDecideCore
Lean.Elab.Tactic.withCollectingNewGoalsFrom
Lean.Elab.Tactic.withMainContext
Lean.Elab.Tactic.elabRewriteConfig
Lean.Elab.Tactic.mkInitialTacticInfo
Lean.Elab.Tactic.liftMetaFinishingTactic
Lean.Elab.Tactic.mkSimpOnly
Lean.Elab.Tactic.classical
Lean.Elab.Tactic.liftMetaTactic1
Lean.Elab.Tactic.isCheckpointableTactic
Lean.Elab.Tactic.saveState
Lean.Elab.Tactic.mkSimpCallStx
Lean.Elab.Tactic.filterOldMVars
Lean.Elab.Tactic.replaceMainGoal
Lean.Elab.Tactic.liftMetaTactic
Lean.Elab.Tactic.done
Lean.Elab.Tactic.simpOnlyBuiltins
Lean.Elab.Tactic.withoutRecover
```

Bool
```exceptions
```

UInt32
UInt32.toUInt8, UInt32.size, UInt32.mod, UInt32.toNat, UInt32.reduceSub, UInt32.ofNatTruncate, UInt32.complement, UInt32.shiftRight, UInt32.log2, UInt32.fromExpr, UInt32.mul, UInt32.decLe, UInt32.ofNat, UInt32.reduceLE, UInt32.div, UInt32.toUInt16, UInt32.reduceOfNat, UInt32.toUSize, UInt32.toUInt64, UInt32.xor, UInt32.reduceLT, UInt32.reduceAdd, UInt32.sub, UInt32.ofNat', UInt32.decEq, UInt32.reduceGE, UInt32.reduceDiv, UInt32.reduceOfNatCore, UInt32.lor, UInt32.shiftLeft, UInt32.ofNatCore, UInt32.reduceMod, UInt32.reduceGT, UInt32.decLt, UInt32.land, UInt32.reduceMul, UInt32.add, UInt32.reduceToNat, UInt32.isValidChar, UInt32.val
{docstring UInt32.toUInt8}
{docstring UInt32.size}
{docstring UInt32.mod}
{docstring UInt32.toNat}
{docstring UInt32.reduceSub}
{docstring UInt32.ofNatTruncate}
{docstring UInt32.complement}
{docstring UInt32.shiftRight}
{docstring UInt32.log2}
{docstring UInt32.fromExpr}
{docstring UInt32.mul}
{docstring UInt32.decLe}
{docstring UInt32.ofNat}
{docstring UInt32.reduceLE}
{docstring UInt32.div}
{docstring UInt32.toUInt16}
{docstring UInt32.reduceOfNat}
{docstring UInt32.toUSize}
{docstring UInt32.toUInt64}
{docstring UInt32.xor}
{docstring UInt32.reduceLT}
{docstring UInt32.reduceAdd}
{docstring UInt32.sub}
{docstring UInt32.ofNat'}
{docstring UInt32.decEq}
{docstring UInt32.reduceGE}
{docstring UInt32.reduceDiv}
{docstring UInt32.reduceOfNatCore}
{docstring UInt32.lor}
{docstring UInt32.shiftLeft}
{docstring UInt32.ofNatCore}
{docstring UInt32.reduceMod}
{docstring UInt32.reduceGT}
{docstring UInt32.decLt}
{docstring UInt32.land}
{docstring UInt32.reduceMul}
{docstring UInt32.add}
{docstring UInt32.reduceToNat}
{docstring UInt32.isValidChar}
{docstring UInt32.val}

```exceptions
UInt32.toUInt8
UInt32.size
UInt32.mod
UInt32.toNat
UInt32.reduceSub
UInt32.ofNatTruncate
UInt32.complement
UInt32.shiftRight
UInt32.log2
UInt32.fromExpr
UInt32.mul
UInt32.decLe
UInt32.ofNat
UInt32.reduceLE
UInt32.div
UInt32.toUInt16
UInt32.reduceOfNat
UInt32.toUSize
UInt32.toUInt64
UInt32.xor
UInt32.reduceLT
UInt32.reduceAdd
UInt32.sub
UInt32.ofNat'
UInt32.decEq
UInt32.reduceGE
UInt32.reduceDiv
UInt32.reduceOfNatCore
UInt32.lor
UInt32.shiftLeft
UInt32.ofNatCore
UInt32.reduceMod
UInt32.reduceGT
UInt32.decLt
UInt32.land
UInt32.reduceMul
UInt32.add
UInt32.reduceToNat
UInt32.isValidChar
UInt32.val
```

EStateM
```exceptions
```

ExceptCpsT
```exceptions
```

IO.Error
```exceptions
```

Char
Char.reduceVal, Char.ofUInt8, Char.reduceOfNatAux, Char.reduceIsDigit, Char.reduceUnary, Char.reduceBEq, Char.reduceEq, Char.fromExpr?, Char.reduceIsWhitespace, Char.toNat, Char.toLower, Char.toUpper, Char.toUInt8, Char.reduceNe, Char.reduceIsUpper, Char.quoteCore.smallCharToHex, Char.quote, Char.le, Char.reduceIsAlpha, Char.reduceToNat, Char.reduceIsLower, Char.lt, Char.utf16Size, Char.reduceBNe, Char.isValidCharNat, Char.toString, Char.repr, Char.reduceToString, Char.reduceDefault, Char.reduceGT, Char.reduceLE, Char.ofNatAux, Char.reduceBinPred, Char.reduceToLower, Char.reduceLT, Char.isValue, Char.reduceGE, Char.utf8Size, Char.reduceIsAlphaNum, Char.reduceBoolPred, Char.quoteCore, Char.reduceToUpper, Char.ofNat
{docstring Char.reduceVal}
{docstring Char.ofUInt8}
{docstring Char.reduceOfNatAux}
{docstring Char.reduceIsDigit}
{docstring Char.reduceUnary}
{docstring Char.reduceBEq}
{docstring Char.reduceEq}
{docstring Char.fromExpr?}
{docstring Char.reduceIsWhitespace}
{docstring Char.toNat}
{docstring Char.toLower}
{docstring Char.toUpper}
{docstring Char.toUInt8}
{docstring Char.reduceNe}
{docstring Char.reduceIsUpper}
{docstring Char.quoteCore.smallCharToHex}
{docstring Char.quote}
{docstring Char.le}
{docstring Char.reduceIsAlpha}
{docstring Char.reduceToNat}
{docstring Char.reduceIsLower}
{docstring Char.lt}
{docstring Char.utf16Size}
{docstring Char.reduceBNe}
{docstring Char.isValidCharNat}
{docstring Char.toString}
{docstring Char.repr}
{docstring Char.reduceToString}
{docstring Char.reduceDefault}
{docstring Char.reduceGT}
{docstring Char.reduceLE}
{docstring Char.ofNatAux}
{docstring Char.reduceBinPred}
{docstring Char.reduceToLower}
{docstring Char.reduceLT}
{docstring Char.isValue}
{docstring Char.reduceGE}
{docstring Char.utf8Size}
{docstring Char.reduceIsAlphaNum}
{docstring Char.reduceBoolPred}
{docstring Char.quoteCore}
{docstring Char.reduceToUpper}
{docstring Char.ofNat}

```exceptions
Char.reduceVal
Char.ofUInt8
Char.reduceOfNatAux
Char.reduceIsDigit
Char.reduceUnary
Char.reduceBEq
Char.reduceEq
Char.fromExpr?
Char.reduceIsWhitespace
Char.toNat
Char.toLower
Char.toUpper
Char.toUInt8
Char.reduceNe
Char.reduceIsUpper
Char.quoteCore.smallCharToHex
Char.quote
Char.le
Char.reduceIsAlpha
Char.reduceToNat
Char.reduceIsLower
Char.lt
Char.utf16Size
Char.reduceBNe
Char.isValidCharNat
Char.toString
Char.repr
Char.reduceToString
Char.reduceDefault
Char.reduceGT
Char.reduceLE
Char.ofNatAux
Char.reduceBinPred
Char.reduceToLower
Char.reduceLT
Char.isValue
Char.reduceGE
Char.utf8Size
Char.reduceIsAlphaNum
Char.reduceBoolPred
Char.quoteCore
Char.reduceToUpper
Char.ofNat
```

IO.Ref
```exceptions
```

StateT
```exceptions
```

IO.FS.Stream
```exceptions
```

Except
```exceptions
```

ST.Ref
```exceptions
```

Monad
```exceptions
```

UInt8
UInt8.sub, UInt8.ofNatCore, UInt8.decLt, UInt8.lor, UInt8.reduceGT, UInt8.toUInt32, UInt8.size, UInt8.toUSize, UInt8.land, UInt8.le, UInt8.add, UInt8.shiftLeft, UInt8.reduceOfNat, UInt8.fromExpr, UInt8.reduceLT, UInt8.toUInt64, UInt8.mod, UInt8.reduceAdd, UInt8.toUInt16, UInt8.log2, UInt8.mul, UInt8.reduceDiv, UInt8.reduceSub, UInt8.div, UInt8.complement, UInt8.reduceGE, UInt8.xor, UInt8.reduceToNat, UInt8.reduceMod, UInt8.decLe, UInt8.reduceOfNatCore, UInt8.shiftRight, UInt8.reduceMul, UInt8.ofNat, UInt8.toNat, UInt8.decEq, UInt8.reduceLE, UInt8.lt, UInt8.val
{docstring UInt8.sub}
{docstring UInt8.ofNatCore}
{docstring UInt8.decLt}
{docstring UInt8.lor}
{docstring UInt8.reduceGT}
{docstring UInt8.toUInt32}
{docstring UInt8.size}
{docstring UInt8.toUSize}
{docstring UInt8.land}
{docstring UInt8.le}
{docstring UInt8.add}
{docstring UInt8.shiftLeft}
{docstring UInt8.reduceOfNat}
{docstring UInt8.fromExpr}
{docstring UInt8.reduceLT}
{docstring UInt8.toUInt64}
{docstring UInt8.mod}
{docstring UInt8.reduceAdd}
{docstring UInt8.toUInt16}
{docstring UInt8.log2}
{docstring UInt8.mul}
{docstring UInt8.reduceDiv}
{docstring UInt8.reduceSub}
{docstring UInt8.div}
{docstring UInt8.complement}
{docstring UInt8.reduceGE}
{docstring UInt8.xor}
{docstring UInt8.reduceToNat}
{docstring UInt8.reduceMod}
{docstring UInt8.decLe}
{docstring UInt8.reduceOfNatCore}
{docstring UInt8.shiftRight}
{docstring UInt8.reduceMul}
{docstring UInt8.ofNat}
{docstring UInt8.toNat}
{docstring UInt8.decEq}
{docstring UInt8.reduceLE}
{docstring UInt8.lt}
{docstring UInt8.val}

```exceptions
UInt8.sub
UInt8.ofNatCore
UInt8.decLt
UInt8.lor
UInt8.reduceGT
UInt8.toUInt32
UInt8.size
UInt8.toUSize
UInt8.land
UInt8.le
UInt8.add
UInt8.shiftLeft
UInt8.reduceOfNat
UInt8.fromExpr
UInt8.reduceLT
UInt8.toUInt64
UInt8.mod
UInt8.reduceAdd
UInt8.toUInt16
UInt8.log2
UInt8.mul
UInt8.reduceDiv
UInt8.reduceSub
UInt8.div
UInt8.complement
UInt8.reduceGE
UInt8.xor
UInt8.reduceToNat
UInt8.reduceMod
UInt8.decLe
UInt8.reduceOfNatCore
UInt8.shiftRight
UInt8.reduceMul
UInt8.ofNat
UInt8.toNat
UInt8.decEq
UInt8.reduceLE
UInt8.lt
UInt8.val
```

BaseIO
```exceptions
```

Bind
```exceptions
```

MonadReaderOf
```exceptions
```

LawfulApplicative
```exceptions
```

System.FilePath
```exceptions
```

Int32
Int32.land, Int32.ofNat, Int32.toBitVec, Int32.lt, Int32.toInt8, Int32.xor, Int32.decLt, Int32.toInt, Int32.shiftLeft, Int32.le, Int32.decLe, Int32.shiftRight, Int32.mod, Int32.add, Int32.toInt16, Int32.toISize, Int32.size, Int32.mul, Int32.lor, Int32.neg, Int32.sub, Int32.toInt64, Int32.div, Int32.toNat, Int32.decEq, Int32.complement, Int32.ofInt
{docstring Int32.land}
{docstring Int32.ofNat}
{docstring Int32.toBitVec}
{docstring Int32.lt}
{docstring Int32.toInt8}
{docstring Int32.xor}
{docstring Int32.decLt}
{docstring Int32.toInt}
{docstring Int32.shiftLeft}
{docstring Int32.le}
{docstring Int32.decLe}
{docstring Int32.shiftRight}
{docstring Int32.mod}
{docstring Int32.add}
{docstring Int32.toInt16}
{docstring Int32.toISize}
{docstring Int32.size}
{docstring Int32.mul}
{docstring Int32.lor}
{docstring Int32.neg}
{docstring Int32.sub}
{docstring Int32.toInt64}
{docstring Int32.div}
{docstring Int32.toNat}
{docstring Int32.decEq}
{docstring Int32.complement}
{docstring Int32.ofInt}

```exceptions
Int32.land
Int32.ofNat
Int32.toBitVec
Int32.lt
Int32.toInt8
Int32.xor
Int32.decLt
Int32.toInt
Int32.shiftLeft
Int32.le
Int32.decLe
Int32.shiftRight
Int32.mod
Int32.add
Int32.toInt16
Int32.toISize
Int32.size
Int32.mul
Int32.lor
Int32.neg
Int32.sub
Int32.toInt64
Int32.div
Int32.toNat
Int32.decEq
Int32.complement
Int32.ofInt
```

EStateM.Backtrackable
```exceptions
```

USize
USize.shiftRight, USize.decLe, USize.toUInt8, USize.mul, USize.decEq, USize.ofNatCore, USize.complement, USize.toUInt16, USize.ofNat, USize.lor, USize.toUInt64, USize.lt, USize.val, USize.toUInt32, USize.mod, USize.toNat, USize.ofNat32, USize.le, USize.size, USize.reduceToNat, USize.sub, USize.add, USize.xor, USize.shiftLeft, USize.repr, USize.decLt, USize.fromExpr, USize.log2, USize.land, USize.div
{docstring USize.shiftRight}
{docstring USize.decLe}
{docstring USize.toUInt8}
{docstring USize.mul}
{docstring USize.decEq}
{docstring USize.ofNatCore}
{docstring USize.complement}
{docstring USize.toUInt16}
{docstring USize.ofNat}
{docstring USize.lor}
{docstring USize.toUInt64}
{docstring USize.lt}
{docstring USize.val}
{docstring USize.toUInt32}
{docstring USize.mod}
{docstring USize.toNat}
{docstring USize.ofNat32}
{docstring USize.le}
{docstring USize.size}
{docstring USize.reduceToNat}
{docstring USize.sub}
{docstring USize.add}
{docstring USize.xor}
{docstring USize.shiftLeft}
{docstring USize.repr}
{docstring USize.decLt}
{docstring USize.fromExpr}
{docstring USize.log2}
{docstring USize.land}
{docstring USize.div}

```exceptions
USize.shiftRight
USize.decLe
USize.toUInt8
USize.mul
USize.decEq
USize.ofNatCore
USize.complement
USize.toUInt16
USize.ofNat
USize.lor
USize.toUInt64
USize.lt
USize.val
USize.toUInt32
USize.mod
USize.toNat
USize.ofNat32
USize.le
USize.size
USize.reduceToNat
USize.sub
USize.add
USize.xor
USize.shiftLeft
USize.repr
USize.decLt
USize.fromExpr
USize.log2
USize.land
USize.div
```

MonadControl
```exceptions
```

Option
Option.isNone, Option.guard, Option.max, Option.mapM, Option.forM, Option.toList, Option.mapA, Option.any, Option.orElse, Option.getM, Option.repr, Option.toArray, Option.getD, Option.isEqSome, Option.bind, Option.get!, Option.merge, Option.attach, Option.or, Option.choice, Option.join, Option.all, Option.format, Option.elimM, Option.bindM, Option.map, Option.sequence, Option.filter, Option.get, Option.unattach, Option.lt, Option.decidable_eq_none, Option.tryCatch, Option.getDM, Option.pbind, Option.attachWith, Option.isSome, Option.min, Option.elim, Option.pmap, Option.liftOrGet, Option.toLOption
{docstring Option.isNone}
{docstring Option.guard}
{docstring Option.max}
{docstring Option.mapM}
{docstring Option.forM}
{docstring Option.toList}
{docstring Option.mapA}
{docstring Option.any}
{docstring Option.orElse}
{docstring Option.getM}
{docstring Option.repr}
{docstring Option.toArray}
{docstring Option.getD}
{docstring Option.isEqSome}
{docstring Option.bind}
{docstring Option.get!}
{docstring Option.merge}
{docstring Option.attach}
{docstring Option.or}
{docstring Option.choice}
{docstring Option.join}
{docstring Option.all}
{docstring Option.format}
{docstring Option.elimM}
{docstring Option.bindM}
{docstring Option.map}
{docstring Option.sequence}
{docstring Option.filter}
{docstring Option.get}
{docstring Option.unattach}
{docstring Option.lt}
{docstring Option.decidable_eq_none}
{docstring Option.tryCatch}
{docstring Option.getDM}
{docstring Option.pbind}
{docstring Option.attachWith}
{docstring Option.isSome}
{docstring Option.min}
{docstring Option.elim}
{docstring Option.pmap}
{docstring Option.liftOrGet}
{docstring Option.toLOption}

```exceptions
Option.isNone
Option.guard
Option.max
Option.mapM
Option.forM
Option.toList
Option.mapA
Option.any
Option.orElse
Option.getM
Option.repr
Option.toArray
Option.getD
Option.isEqSome
Option.bind
Option.get!
Option.merge
Option.attach
Option.or
Option.choice
Option.join
Option.all
Option.format
Option.elimM
Option.bindM
Option.map
Option.sequence
Option.filter
Option.get
Option.unattach
Option.lt
Option.decidable_eq_none
Option.tryCatch
Option.getDM
Option.pbind
Option.attachWith
Option.isSome
Option.min
Option.elim
Option.pmap
Option.liftOrGet
Option.toLOption
```

MonadExceptOf
```exceptions
```

Tactics
Lean.Parser.Tactic.acNf0, Lean.Parser.Tactic.tacticAc_nf_, Lean.Parser.Tactic.classical
{docstring Lean.Parser.Tactic.acNf0}
{docstring Lean.Parser.Tactic.tacticAc_nf_}
{docstring Lean.Parser.Tactic.classical}

```exceptions
Lean.Parser.Tactic.acNf0
Lean.Parser.Tactic.tacticAc_nf_
Lean.Parser.Tactic.classical
```