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. Fin.add
    3. ISize.add
    4. Int16.add
    5. Int32.add
    6. Int64.add
    7. Int8.add
    8. Nat.add
    9. UInt16.add
    10. UInt32.add
    11. UInt64.add
    12. UInt8.add
    13. USize.add
  140. add­Cases
    1. Fin.add­Cases
  141. add­Extension
    1. System.FilePath.add­Extension
  142. add­Heartbeats
    1. IO.add­Heartbeats
  143. add­Macro­Scope
    1. Lean.Macro.add­Macro­Scope
  144. add­Nat
    1. Fin.add­Nat
  145. admit
  146. all
    1. Array.all
    2. Nat.all
    3. Option.all
    4. String.all
    5. Subarray.all
  147. all­Diff
    1. Array.all­Diff
  148. all­M
    1. Array.all­M
    2. Nat.all­M
    3. Subarray.all­M
  149. all­TR
    1. Nat.all­TR
  150. all_goals (0) (1)
  151. and
    1. Bool.and
  152. and­M
  153. and_intros
  154. any
    1. Array.any
    2. Nat.any
    3. Option.any
    4. String.any
    5. Subarray.any
  155. any­M
    1. Array.any­M
    2. Nat.any­M
    3. Subarray.any­M
  156. any­TR
    1. Nat.any­TR
  157. any_goals (0) (1)
  158. app­Dir
    1. IO.app­Dir
  159. app­Path
    1. IO.app­Path
  160. append
    1. Append.append (class method)
    2. Array.append
    3. String.append
  161. append­Goals
    1. Lean.Elab.Tactic.append­Goals
  162. append­List
    1. Array.append­List
  163. apply (0) (1)
  164. apply?
  165. apply­Eq­Lemma
    1. Nat.apply­Eq­Lemma
  166. apply­Simproc­Const
    1. Nat.apply­Simproc­Const
  167. apply_assumption
  168. apply_ext_theorem
  169. apply_mod_cast
  170. apply_rfl
  171. apply_rules
  172. arg [@]i
  173. args
    1. [anonymous] (structure field)
  174. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  175. array
    1. Subarray.array (structure field)
  176. array_get_dec
  177. as­Task
    1. BaseIO.as­Task
    2. EIO.as­Task
    3. IO.as­Task
  178. assumption
    1. inaccessible
  179. assumption_mod_cast
  180. at­End
    1. String.Iterator.at­End
    2. String.at­End
  181. at­Least­Two
    1. Bool.at­Least­Two
  182. attach
    1. Array.attach
    2. Option.attach
  183. attach­With
    1. Array.attach­With
    2. Option.attach­With
  184. auto­Lift
  185. auto­Param
  186. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  187. 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. Option.bind
    6. OptionT.bind
    7. ReaderT.bind
    8. StateT.bind
  49. bind­Cont
    1. ExceptT.bind­Cont
  50. bind­Left
    1. Bind.bind­Left
  51. bind­M
    1. Option.bind­M
  52. bind­Task
    1. BaseIO.bind­Task
    2. EIO.bind­Task
    3. IO.bind­Task
  53. bind_assoc
    1. [anonymous] (class method)
  54. bind_map
    1. [anonymous] (class method)
  55. bind_pure_comp
    1. [anonymous] (class method)
  56. bitwise
    1. Nat.bitwise
  57. ble
    1. Nat.ble
  58. blt
    1. Nat.blt
  59. bootstrap.inductive­Check­Resulting­Universe
  60. bv_check
  61. bv_decide
  62. bv_decide?
  63. bv_normalize
  64. bv_omega
  65. by­Cases
    1. Decidable.by­Cases
  66. by_cases
  67. byte­Idx
    1. String.Pos.byte­Idx (structure field)
  68. 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
    1. Fin.cases
  23. cases­On
    1. Nat.cases­On
  24. cast
    1. Fin.cast
    2. Nat.cast
  25. cast­Add
    1. Fin.cast­Add
  26. cast­LE
    1. Fin.cast­LE
  27. cast­LT
    1. Fin.cast­LT
  28. cast­Succ
    1. Fin.cast­Succ
  29. catch­Exceptions
    1. EIO.catch­Exceptions
  30. change (0) (1)
  31. change ... with ...
  32. char­Lit­Kind
    1. Lean.char­Lit­Kind
  33. check­Canceled
    1. IO.check­Canceled
  34. checkpoint
  35. choice
    1. Option.choice
  36. choice­Kind
    1. Lean.choice­Kind
  37. clear
  38. close­Main­Goal
    1. Lean.Elab.Tactic.close­Main­Goal
  39. close­Main­Goal­Using
    1. Lean.Elab.Tactic.close­Main­Goal­Using
  40. cmd
    1. [anonymous] (structure field)
  41. codepoint­Pos­To­Utf16Pos
    1. String.codepoint­Pos­To­Utf16Pos
  42. codepoint­Pos­To­Utf16Pos­From
    1. String.codepoint­Pos­To­Utf16Pos­From
  43. codepoint­Pos­To­Utf8Pos­From
    1. String.codepoint­Pos­To­Utf8Pos­From
  44. col­Eq
  45. col­Ge
  46. col­Gt
  47. comment
    1. block
    2. line
  48. comp_map
    1. LawfulFunctor.comp_map (class method)
  49. compare
    1. Ord.compare (class method)
  50. complement
    1. ISize.complement
    2. Int16.complement
    3. Int32.complement
    4. Int64.complement
    5. Int8.complement
    6. UInt16.complement
    7. UInt32.complement
    8. UInt64.complement
    9. UInt8.complement
    10. USize.complement
  51. components
    1. System.FilePath.components
  52. concat­Map
    1. Array.concat­Map
  53. concat­Map­M
    1. Array.concat­Map­M
  54. cond
  55. configuration
    1. of tactics
  56. congr (0) (1)
  57. constructor (0) (1)
  58. contains
    1. Array.contains
    2. String.contains
  59. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  60. contradiction
  61. control
  62. control­At
  63. conv
  64. conv => ...
  65. conv' (0) (1)
  66. create­Dir
    1. IO.FS.create­Dir
  67. create­Dir­All
    1. IO.FS.create­Dir­All
  68. create­Temp­File
    1. IO.FS.create­Temp­File
  69. crlf­To­Lf
    1. String.crlf­To­Lf
  70. csize
    1. String.csize
  71. cumulativity
  72. curr
    1. String.Iterator.curr
  73. current­Dir
    1. IO.current­Dir
  74. custom­Eliminators
    1. tactic.custom­Eliminators
  75. 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. ISize.dec­Eq
    3. Int16.dec­Eq
    4. Int32.dec­Eq
    5. Int64.dec­Eq
    6. Int8.dec­Eq
    7. Nat.dec­Eq
    8. String.dec­Eq
    9. UInt16.dec­Eq
    10. UInt32.dec­Eq
    11. UInt64.dec­Eq
    12. UInt8.dec­Eq
    13. USize.dec­Eq
  20. dec­Le
    1. ISize.dec­Le
    2. Int16.dec­Le
    3. Int32.dec­Le
    4. Int64.dec­Le
    5. Int8.dec­Le
    6. Nat.dec­Le
    7. UInt16.dec­Le
    8. UInt32.dec­Le
    9. UInt64.dec­Le
    10. UInt8.dec­Le
    11. USize.dec­Le
  21. dec­Lt
    1. ISize.dec­Lt
    2. Int16.dec­Lt
    3. Int32.dec­Lt
    4. Int64.dec­Lt
    5. Int8.dec­Lt
    6. Nat.dec­Lt
    7. UInt16.dec­Lt
    8. UInt32.dec­Lt
    9. UInt64.dec­Lt
    10. UInt8.dec­Lt
    11. USize.dec­Lt
  22. decapitalize
    1. String.decapitalize
  23. decidable
  24. decidable_eq_none
    1. Option.decidable_eq_none
  25. decide
    1. Decidable.decide
    2. Lean.Meta.DSimp.Config.decide (structure field)
    3. Lean.Meta.Simp.Config.decide (structure field)
  26. decreasing_tactic
  27. decreasing_trivial
  28. decreasing_with
  29. dedicated
    1. Task.Priority.dedicated
  30. deep­Terms
    1. pp.deep­Terms
  31. default
    1. Inhabited.default (class method)
    2. Task.Priority.default
  32. delta (0) (1)
  33. digit­Char
    1. Nat.digit­Char
  34. discard
    1. Functor.discard
  35. discharge
    1. trace.Meta.Tactic.simp.discharge
  36. div
    1. Div.div (class method)
    2. Fin.div
    3. ISize.div
    4. Int16.div
    5. Int32.div
    6. Int64.div
    7. Int8.div
    8. Nat.div
    9. UInt16.div
    10. UInt32.div
    11. UInt64.div
    12. UInt8.div
    13. USize.div
  37. div2Induction
    1. Nat.div2Induction
  38. done (0) (1)
  39. down
    1. PLift.down (structure field)
    2. ULift.down (structure field)
  40. drop
    1. String.drop
    2. Subarray.drop
  41. drop­Right
    1. String.drop­Right
  42. drop­Right­While
    1. String.drop­Right­While
  43. drop­While
    1. String.drop­While
  44. dsimp (0) (1)
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  45. dsimp!
  46. dsimp?
  47. dsimp?!
  48. dsimp­Location'
    1. Lean.Elab.Tactic.dsimp­Location'
  49. 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
    1. Option.elim
  76. elim0
    1. Fin.elim0
  77. elim­M
    1. Option.elim­M
  78. elim­Offset
    1. Nat.elim­Offset
  79. empty
    1. Array.empty
    2. Subarray.empty
  80. end­Pos
    1. String.end­Pos
  81. ends­With
    1. String.ends­With
  82. ensure­Has­No­MVars
    1. Lean.Elab.Tactic.ensure­Has­No­MVars
  83. enter
  84. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  85. eprint
    1. IO.eprint
  86. eprintln
    1. IO.eprintln
  87. eq_of_beq
    1. LawfulBEq.eq_of_beq (class method)
  88. eq_refl
  89. erase
    1. Array.erase
  90. erase­Idx
    1. Array.erase­Idx
  91. erase­Reps
    1. Array.erase­Reps
  92. erw (0) (1)
  93. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.eta (structure field)
  94. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
    2. Lean.Meta.Simp.Config.eta­Struct (structure field)
  95. exact
  96. exact?
  97. exact_mod_cast
  98. exe­Extension
    1. System.FilePath.exe­Extension
  99. exfalso
  100. exists
  101. exit
    1. IO.Process.exit
  102. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  103. expand­Macro?
    1. Lean.Macro.expand­Macro?
  104. ext (0) (1)
  105. ext1
  106. ext­Separator
    1. System.FilePath.ext­Separator
  107. extension
    1. System.FilePath.extension
  108. extensionality
    1. of propositions
  109. 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.add
  5. Fin.add­Cases
  6. Fin.add­Nat
  7. Fin.cases
  8. Fin.cast
  9. Fin.cast­Add
  10. Fin.cast­LE
  11. Fin.cast­LT
  12. Fin.cast­Succ
  13. Fin.div
  14. Fin.elim0
  15. Fin.foldl
  16. Fin.foldl­M
  17. Fin.foldr
  18. Fin.foldr­M
  19. Fin.from­Expr?
  20. Fin.h­Iterate
  21. Fin.h­Iterate­From
  22. Fin.induction
  23. Fin.induction­On
  24. Fin.is­Value
  25. Fin.land
  26. Fin.last
  27. Fin.last­Cases
  28. Fin.log2
  29. Fin.lor
  30. Fin.mk
    1. Constructor of Fin
  31. Fin.mod
  32. Fin.modn
  33. Fin.mul
  34. Fin.nat­Add
  35. Fin.of­Nat'
  36. Fin.pred
  37. Fin.reduce­Add
  38. Fin.reduce­Add­Nat
  39. Fin.reduce­And
  40. Fin.reduce­BEq
  41. Fin.reduce­BNe
  42. Fin.reduce­Bin
  43. Fin.reduce­Bin­Pred
  44. Fin.reduce­Bool­Pred
  45. Fin.reduce­Cast­Add
  46. Fin.reduce­Cast­LE
  47. Fin.reduce­Cast­LT
  48. Fin.reduce­Cast­Succ
  49. Fin.reduce­Div
  50. Fin.reduce­Eq
  51. Fin.reduce­Fin­Mk
  52. Fin.reduce­GE
  53. Fin.reduce­GT
  54. Fin.reduce­LE
  55. Fin.reduce­LT
  56. Fin.reduce­Last
  57. Fin.reduce­Mod
  58. Fin.reduce­Mul
  59. Fin.reduce­Nat­Add
  60. Fin.reduce­Nat­Op
  61. Fin.reduce­Ne
  62. Fin.reduce­Of­Nat'
  63. Fin.reduce­Op
  64. Fin.reduce­Or
  65. Fin.reduce­Pred
  66. Fin.reduce­Rev
  67. Fin.reduce­Shift­Left
  68. Fin.reduce­Shift­Right
  69. Fin.reduce­Sub
  70. Fin.reduce­Sub­Nat
  71. Fin.reduce­Succ
  72. Fin.reduce­Xor
  73. Fin.rev
  74. Fin.reverse­Induction
  75. Fin.shift­Left
  76. Fin.shift­Right
  77. Fin.sub
  78. Fin.sub­Nat
  79. Fin.succ
  80. Fin.succ­Rec
  81. Fin.succ­Rec­On
  82. Fin.xor
  83. For­In
  84. For­In'
  85. ForIn'.mk
    1. Instance constructor of For­In'
  86. ForIn.mk
    1. Instance constructor of For­In
  87. For­In­Step
  88. For­InStep.done
    1. Constructor of For­In­Step
  89. For­InStep.yield
    1. Constructor of For­In­Step
  90. For­M
  91. ForM.for­In
  92. ForM.mk
    1. Instance constructor of For­M
  93. Functor
  94. Functor.discard
  95. Functor.map­Rev
  96. Functor.mk
    1. Instance constructor of Functor
  97. fail
    1. OptionT.fail
  98. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
    2. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  99. fail_if_success (0) (1)
  100. failure
    1. ReaderT.failure
    2. StateT.failure
    3. [anonymous] (class method)
  101. false_or_by_contra
  102. field­Idx­Kind
    1. Lean.field­Idx­Kind
  103. field­Notation
    1. pp.field­Notation
  104. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
    2. System.FilePath.file­Name
  105. file­Stem
    1. System.FilePath.file­Stem
  106. filter
    1. Array.filter
    2. Option.filter
  107. filter­M
    1. Array.filter­M
  108. filter­Map
    1. Array.filter­Map
  109. filter­Map­M
    1. Array.filter­Map­M
  110. filter­Pairs­M
    1. Array.filter­Pairs­M
  111. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  112. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  113. find
    1. String.find
  114. find?
    1. Array.find?
  115. find­Idx?
    1. Array.find­Idx?
  116. find­Idx­M?
    1. Array.find­Idx­M?
  117. find­Line­Start
    1. String.find­Line­Start
  118. find­M?
    1. Array.find­M?
  119. find­Rev?
    1. Array.find­Rev?
    2. Subarray.find­Rev?
  120. find­Rev­M?
    1. Array.find­Rev­M?
    2. Subarray.find­Rev­M?
  121. find­Some!
    1. Array.find­Some!
  122. find­Some?
    1. Array.find­Some?
  123. find­Some­M?
    1. Array.find­Some­M?
  124. find­Some­Rev?
    1. Array.find­Some­Rev?
  125. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
    2. Subarray.find­Some­Rev­M?
  126. first (0) (1)
  127. first­Diff­Pos
    1. String.first­Diff­Pos
  128. flags
    1. IO.FileRight.flags
  129. flat­Map
    1. Array.flat­Map
  130. flat­Map­M
    1. Array.flat­Map­M
  131. flatten
    1. Array.flatten
  132. flush
    1. IO.FS.Handle.flush
    2. IO.FS.Stream.flush (structure field)
  133. focus (0) (1)
    1. Lean.Elab.Tactic.focus
  134. fold
    1. Nat.fold
  135. fold­M
    1. Nat.fold­M
  136. fold­Rev
    1. Nat.fold­Rev
  137. fold­Rev­M
    1. Nat.fold­Rev­M
  138. fold­TR
    1. Nat.fold­TR
  139. foldl
    1. Array.foldl
    2. Fin.foldl
    3. String.foldl
    4. Subarray.foldl
  140. foldl­M
    1. Array.foldl­M
    2. Fin.foldl­M
    3. Subarray.foldl­M
  141. foldr
    1. Array.foldr
    2. Fin.foldr
    3. String.foldr
    4. Subarray.foldr
  142. foldr­M
    1. Array.foldr­M
    2. Fin.foldr­M
    3. Subarray.foldr­M
  143. fopen­Error­To­String
    1. IO.Error.fopen­Error­To­String
  144. for­In
    1. ForIn.for­In (class method)
    2. ForM.for­In
    3. Subarray.for­In
  145. for­In'
    1. Array.for­In'
    2. ForIn'.for­In' (class method)
  146. for­M
    1. Array.for­M
    2. ForM.for­M (class method)
    3. Nat.for­M
    4. Option.for­M
    5. Subarray.for­M
  147. for­Rev­M
    1. Array.for­Rev­M
    2. Nat.for­Rev­M
    3. Subarray.for­Rev­M
  148. format
    1. Option.format
  149. forward
    1. String.Iterator.forward
  150. from­Expr
    1. UInt16.from­Expr
    2. UInt32.from­Expr
    3. UInt64.from­Expr
    4. UInt8.from­Expr
    5. USize.from­Expr
  151. from­Expr?
    1. Fin.from­Expr?
    2. Nat.from­Expr?
    3. String.from­Expr?
  152. from­State­M
    1. EStateM.from­State­M
  153. from­UTF8
    1. String.from­UTF8
  154. from­UTF8!
    1. String.from­UTF8!
  155. from­UTF8?
    1. String.from­UTF8?
  156. front
    1. String.front
  157. 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)
  158. fun
  159. 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. Option.get
    7. ST.Ref.get
    8. State­RefT'.get
    9. StateT.get
    10. String.get
    11. Subarray.get
    12. Task.get
    13. Task.get (structure field)
  8. get!
    1. Array.get!
    2. Option.get!
    3. String.get!
    4. 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. Option.get­D
    3. Subarray.get­D
  16. get­DM
    1. Option.get­DM
  17. get­Elem
    1. GetElem.get­Elem (class method)
  18. get­Elem!
    1. GetElem?.get­Elem? (class method)
  19. get­Elem!_def
    1. Lawful­GetElem.get­Elem!_def (class method)
  20. get­Elem?
    1. [anonymous] (class method)
  21. get­Elem?_def
    1. Lawful­GetElem.get­Elem?_def (class method)
  22. get­Env
    1. IO.get­Env
  23. get­Even­Elems
    1. Array.get­Even­Elems
  24. get­FVar­Id
    1. Lean.Elab.Tactic.get­FVar­Id
  25. get­FVar­Ids
    1. Lean.Elab.Tactic.get­FVar­Ids
  26. get­Goals
    1. Lean.Elab.Tactic.get­Goals
  27. get­Hygiene­Info
    1. Lean.TSyntax.get­Hygiene­Info
  28. get­Id
    1. Lean.TSyntax.get­Id
  29. get­Idx?
    1. Array.get­Idx?
  30. get­Kind
    1. Lean.Syntax.get­Kind
  31. get­Line
    1. IO.FS.Handle.get­Line
    2. IO.FS.Stream.get­Line (structure field)
  32. get­M
    1. Option.get­M
  33. get­Main­Goal
    1. Lean.Elab.Tactic.get­Main­Goal
  34. get­Main­Module
    1. Lean.Elab.Tactic.get­Main­Module
  35. get­Main­Tag
    1. Lean.Elab.Tactic.get­Main­Tag
  36. get­Max?
    1. Array.get­Max?
  37. get­Modify
  38. get­Name
    1. Lean.TSyntax.get­Name
  39. get­Nat
    1. Lean.TSyntax.get­Nat
  40. get­Num­Heartbeats
    1. IO.get­Num­Heartbeats
  41. get­PID
    1. IO.Process.get­PID
  42. get­Random­Bytes
    1. IO.get­Random­Bytes
  43. get­Scientific
    1. Lean.TSyntax.get­Scientific
  44. get­Stderr
    1. IO.get­Stderr
  45. get­Stdin
    1. IO.get­Stdin
  46. get­Stdout
    1. IO.get­Stdout
  47. get­String
    1. Lean.TSyntax.get­String
  48. get­Task­State
    1. IO.get­Task­State
  49. get­The
  50. get­Unsolved­Goals
    1. Lean.Elab.Tactic.get­Unsolved­Goals
  51. get­Utf8Byte
    1. String.get­Utf8Byte
  52. get_elem_tactic
  53. get_elem_tactic_trivial
  54. goal
    1. main
  55. ground
    1. Lean.Meta.Simp.Config.ground (structure field)
  56. group
    1. IO.FileRight.group (structure field)
  57. group­By­Key
    1. Array.group­By­Key
  58. group­Kind
    1. Lean.group­Kind
  59. guard
    1. Option.guard
  60. guard_expr
  61. guard_hyp
  62. 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­Iterate
    1. Fin.h­Iterate
  37. h­Iterate­From
    1. Fin.h­Iterate­From
  38. h­Mod
    1. HMod.h­Mod (class method)
  39. h­Mul
    1. HMul.h­Mul (class method)
  40. h­Or
    1. HOr.h­Or (class method)
  41. h­Pow
    1. HPow.h­Pow (class method)
  42. h­Shift­Left
    1. HShiftLeft.h­Shift­Left (class method)
  43. h­Shift­Right
    1. HShiftRight.h­Shift­Right (class method)
  44. h­Sub
    1. HSub.h­Sub (class method)
  45. h­Xor
    1. HXor.h­Xor (class method)
  46. has­Bind
    1. Id.has­Bind
  47. has­Decl
    1. Lean.Macro.has­Decl
  48. has­Finished
    1. IO.has­Finished
  49. has­Next
    1. String.Iterator.has­Next
  50. has­Prev
    1. String.Iterator.has­Prev
  51. hash
    1. Hashable.hash (class method)
    2. String.hash
  52. have
  53. have'
  54. have­I
  55. hygiene
    1. in tactics
  56. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  57. 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. ISize
  173. ISize.add
  174. ISize.complement
  175. ISize.dec­Eq
  176. ISize.dec­Le
  177. ISize.dec­Lt
  178. ISize.div
  179. ISize.land
  180. ISize.le
  181. ISize.lor
  182. ISize.lt
  183. ISize.mk
    1. Constructor of ISize
  184. ISize.mod
  185. ISize.mul
  186. ISize.neg
  187. ISize.of­Int
  188. ISize.of­Nat
  189. ISize.shift­Left
  190. ISize.shift­Right
  191. ISize.size
  192. ISize.sub
  193. ISize.to­Bit­Vec
  194. ISize.to­Int
  195. ISize.to­Int32
  196. ISize.to­Int64
  197. ISize.to­Nat
  198. ISize.xor
  199. Id
  200. Id.has­Bind
  201. Id.run
  202. Ident
    1. Lean.Syntax.Ident
  203. Inhabited
  204. Inhabited.mk
    1. Instance constructor of Inhabited
  205. Int
  206. Int.neg­Succ
    1. Constructor of Int
  207. Int.of­Nat
    1. Constructor of Int
  208. Int16
  209. Int16.add
  210. Int16.complement
  211. Int16.dec­Eq
  212. Int16.dec­Le
  213. Int16.dec­Lt
  214. Int16.div
  215. Int16.land
  216. Int16.le
  217. Int16.lor
  218. Int16.lt
  219. Int16.mk
    1. Constructor of Int16
  220. Int16.mod
  221. Int16.mul
  222. Int16.neg
  223. Int16.of­Int
  224. Int16.of­Nat
  225. Int16.shift­Left
  226. Int16.shift­Right
  227. Int16.size
  228. Int16.sub
  229. Int16.to­Bit­Vec
  230. Int16.to­Int
  231. Int16.to­Int32 (0) (1)
  232. Int16.to­Int64
  233. Int16.to­Int8
  234. Int16.to­Nat
  235. Int16.xor
  236. Int32
  237. Int32.add
  238. Int32.complement
  239. Int32.dec­Eq
  240. Int32.dec­Le
  241. Int32.dec­Lt
  242. Int32.div
  243. Int32.land
  244. Int32.le
  245. Int32.lor
  246. Int32.lt
  247. Int32.mk
    1. Constructor of Int32
  248. Int32.mod
  249. Int32.mul
  250. Int32.neg
  251. Int32.of­Int
  252. Int32.of­Nat
  253. Int32.shift­Left
  254. Int32.shift­Right
  255. Int32.size
  256. Int32.sub
  257. Int32.to­Bit­Vec
  258. Int32.to­ISize
  259. Int32.to­Int
  260. Int32.to­Int16
  261. Int32.to­Int64
  262. Int32.to­Int8
  263. Int32.to­Nat
  264. Int32.xor
  265. Int64
  266. Int64.add
  267. Int64.complement
  268. Int64.dec­Eq
  269. Int64.dec­Le
  270. Int64.dec­Lt
  271. Int64.div
  272. Int64.land
  273. Int64.le
  274. Int64.lor
  275. Int64.lt
  276. Int64.mk
    1. Constructor of Int64
  277. Int64.mod
  278. Int64.mul
  279. Int64.neg
  280. Int64.of­Int
  281. Int64.of­Nat
  282. Int64.shift­Left
  283. Int64.shift­Right
  284. Int64.size
  285. Int64.sub
  286. Int64.to­Bit­Vec
  287. Int64.to­ISize
  288. Int64.to­Int
  289. Int64.to­Int16
  290. Int64.to­Int32
  291. Int64.to­Int8
  292. Int64.to­Nat
  293. Int64.xor
  294. Int8
  295. Int8.add
  296. Int8.complement
  297. Int8.dec­Eq
  298. Int8.dec­Le
  299. Int8.dec­Lt
  300. Int8.div
  301. Int8.land
  302. Int8.le
  303. Int8.lor
  304. Int8.lt
  305. Int8.mk
    1. Constructor of Int8
  306. Int8.mod
  307. Int8.mul
  308. Int8.neg
  309. Int8.of­Int
  310. Int8.of­Nat
  311. Int8.shift­Left
  312. Int8.shift­Right
  313. Int8.size
  314. Int8.sub
  315. Int8.to­Bit­Vec
  316. Int8.to­Int
  317. Int8.to­Int16
  318. Int8.to­Int32 (0) (1)
  319. Int8.to­Int64
  320. Int8.to­Nat
  321. Int8.xor
  322. Iterator
    1. String.Iterator
  323. i
    1. String.Iterator.i (structure field)
  324. ibelow
    1. Nat.ibelow
  325. id_map
    1. LawfulFunctor.id_map (class method)
  326. ident­Kind
    1. Lean.ident­Kind
  327. identifier
    1. raw
  328. if ... then ... else ...
  329. if h : ... then ... else ...
  330. imax
    1. Nat.imax
  331. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  332. impredicative
  333. inaccessible
  334. index
    1. Lean.Meta.DSimp.Config.index (structure field)
    2. Lean.Meta.Simp.Config.index (structure field)
    3. of inductive type
  335. index­Of?
    1. Array.index­Of?
  336. indexed family
    1. of types
  337. induction
    1. Fin.induction
  338. induction­On
    1. Fin.induction­On
    2. Nat.div.induction­On
    3. Nat.mod.induction­On
  339. inductive.auto­Promote­Indices
  340. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  341. infer­Instance
  342. infer­Instance­As
  343. infer_instance
  344. injection
  345. injections
  346. insert­At
    1. Array.insert­At
  347. insert­At!
    1. Array.insert­At!
  348. insertion­Sort
    1. Array.insertion­Sort
  349. instance synthesis
  350. intercalate
    1. String.intercalate
  351. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  352. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  353. intro (0) (1)
  354. intro | ... => ... | ... => ...
  355. intros
  356. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  357. is­Absolute
    1. System.FilePath.is­Absolute
  358. is­Alpha
    1. Char.is­Alpha
  359. is­Alphanum
    1. Char.is­Alphanum
  360. is­Digit
    1. Char.is­Digit
  361. is­Dir
    1. System.FilePath.is­Dir
  362. is­Empty
    1. Array.is­Empty
    2. String.is­Empty
  363. is­Eq­Some
    1. Option.is­Eq­Some
  364. is­Eqv
    1. Array.is­Eqv
  365. is­Int
    1. String.is­Int
  366. is­Lower
    1. Char.is­Lower
  367. is­Lt
    1. Fin.is­Lt (structure field)
  368. is­Nat
    1. String.is­Nat
  369. is­None
    1. Option.is­None
  370. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  371. is­Ok
    1. Except.is­Ok
  372. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  373. is­Prefix­Of
    1. Array.is­Prefix­Of
    2. String.is­Prefix­Of
  374. is­Relative
    1. System.FilePath.is­Relative
  375. is­Some
    1. Option.is­Some
  376. is­Tty
    1. IO.FS.Handle.is­Tty
    2. IO.FS.Stream.is­Tty (structure field)
  377. is­Upper
    1. Char.is­Upper
  378. is­Valid
    1. String.Pos.is­Valid
  379. is­Valid­Char
    1. Nat.is­Valid­Char
    2. UInt32.is­Valid­Char
  380. is­Value
    1. Fin.is­Value
    2. Nat.is­Value
  381. is­Whitespace
    1. Char.is­Whitespace
  382. iter
    1. String.iter
  383. iterate
    1. IO.iterate

J

  1. join
    1. Option.join
    2. String.join
    3. 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. Fin.land
    2. ISize.land
    3. Int16.land
    4. Int32.land
    5. Int64.land
    6. Int8.land
    7. Nat.land
    8. UInt16.land
    9. UInt32.land
    10. UInt64.land
    11. UInt8.land
    12. USize.land
  153. last
    1. Fin.last
  154. last­Cases
    1. Fin.last­Cases
  155. lazy­Pure
    1. IO.lazy­Pure
  156. lcm
    1. Nat.lcm
  157. le
    1. ISize.le
    2. Int16.le
    3. Int32.le
    4. Int64.le
    5. Int8.le
    6. LE.le (class method)
    7. Nat.le
    8. String.le
    9. UInt16.le
    10. UInt64.le
    11. UInt8.le
    12. USize.le
  158. lean_is_array
  159. lean_is_string
  160. lean_string_object (0) (1)
  161. lean_to_array
  162. lean_to_string
  163. left (0) (1)
  164. length
    1. String.length
  165. let
  166. let rec
  167. let'
  168. let­I
  169. level
    1. of universe
  170. lhs
  171. lift
    1. Except­CpsT.lift
    2. ExceptT.lift
    3. OptionT.lift
    4. State­CpsT.lift
    5. State­RefT'.lift
    6. StateT.lift
  172. lift­Meta­MAt­Main
    1. Lean.Elab.Tactic.lift­Meta­MAt­Main
  173. lift­Or­Get
    1. Option.lift­Or­Get
  174. lift­With
    1. MonadControl.lift­With (class method)
    2. Monad­ControlT.lift­With (class method)
  175. line­Eq
  176. lines
    1. IO.FS.lines
  177. linter.unnecessary­Simpa
  178. literal
    1. raw string
    2. string
  179. lock
    1. IO.FS.Handle.lock
  180. log2
    1. Fin.log2
    2. Nat.log2
    3. UInt16.log2
    4. UInt32.log2
    5. UInt64.log2
    6. UInt8.log2
    7. USize.log2
  181. lor
    1. Fin.lor
    2. ISize.lor
    3. Int16.lor
    4. Int32.lor
    5. Int64.lor
    6. Int8.lor
    7. Nat.lor
    8. UInt16.lor
    9. UInt32.lor
    10. UInt64.lor
    11. UInt8.lor
    12. USize.lor
  182. lt
    1. ISize.lt
    2. Int16.lt
    3. Int32.lt
    4. Int64.lt
    5. Int8.lt
    6. LT.lt (class method)
    7. Nat.lt
    8. Option.lt
    9. UInt16.lt
    10. UInt64.lt
    11. UInt8.lt
    12. USize.lt
  183. 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. Option.map
    7. StateT.map
    8. String.map
  49. map­A
    1. Option.map­A
  50. map­Const
    1. Functor.map­Const (class method)
  51. map­Error
    1. Except.map­Error
  52. map­Fin­Idx
    1. Array.map­Fin­Idx
  53. map­Fin­Idx­M
    1. Array.map­Fin­Idx­M
  54. map­Idx
    1. Array.map­Idx
  55. map­Idx­M
    1. Array.map­Idx­M
  56. map­Indexed
    1. Array.map­Indexed
  57. map­Indexed­M
    1. Array.map­Indexed­M
  58. map­M
    1. Array.map­M
    2. Option.map­M
  59. map­M'
    1. Array.map­M'
  60. map­Mono
    1. Array.map­Mono
  61. map­Mono­M
    1. Array.map­Mono­M
  62. map­Rev
    1. Functor.map­Rev
  63. map­Task
    1. BaseIO.map­Task
    2. EIO.map­Task
    3. IO.map­Task
  64. map­Tasks
    1. BaseIO.map­Tasks
    2. EIO.map­Tasks
    3. IO.map­Tasks
  65. map_const
    1. LawfulFunctor.map_const (class method)
  66. map_pure
    1. LawfulApplicative.seq­Left_eq (class method)
  67. match
    1. pp.match
  68. max
    1. Nat.max
    2. Option.max
    3. Task.Priority.max
  69. max­Discharge­Depth
    1. Lean.Meta.Simp.Config.max­Discharge­Depth (structure field)
  70. max­Heartbeats
    1. synthInstance.max­Heartbeats
  71. max­Size
    1. synthInstance.max­Size
  72. max­Steps
    1. Lean.Meta.Simp.Config.max­Steps (structure field)
    2. pp.max­Steps
  73. memoize
    1. Lean.Meta.Simp.Config.memoize (structure field)
  74. merge
    1. Option.merge
  75. metadata
    1. System.FilePath.metadata
  76. min
    1. Nat.min
    2. Option.min
    3. String.Pos.min
  77. mk
    1. Dynamic.mk
    2. ExceptT.mk
    3. IO.FS.Handle.mk
    4. OptionT.mk
  78. mk'
    1. LawfulMonad.mk'
  79. mk­Already­Exists
    1. IO.Error.mk­Already­Exists
  80. mk­Already­Exists­File
    1. IO.Error.mk­Already­Exists­File
  81. mk­Array
    1. Array.mk­Array
  82. mk­Eof­Error
    1. IO.Error.mk­Eof­Error
  83. mk­File­Path
    1. System.mk­File­Path
  84. mk­Hardware­Fault
    1. IO.Error.mk­Hardware­Fault
  85. mk­Illegal­Operation
    1. IO.Error.mk­Illegal­Operation
  86. mk­Inappropriate­Type
    1. IO.Error.mk­Inappropriate­Type
  87. mk­Inappropriate­Type­File
    1. IO.Error.mk­Inappropriate­Type­File
  88. mk­Interrupted
    1. IO.Error.mk­Interrupted
  89. mk­Invalid­Argument
    1. IO.Error.mk­Invalid­Argument
  90. mk­Invalid­Argument­File
    1. IO.Error.mk­Invalid­Argument­File
  91. mk­Iterator
    1. String.mk­Iterator
  92. mk­No­File­Or­Directory
    1. IO.Error.mk­No­File­Or­Directory
  93. mk­No­Such­Thing
    1. IO.Error.mk­No­Such­Thing
  94. mk­No­Such­Thing­File
    1. IO.Error.mk­No­Such­Thing­File
  95. mk­Other­Error
    1. IO.Error.mk­Other­Error
  96. mk­Permission­Denied
    1. IO.Error.mk­Permission­Denied
  97. mk­Permission­Denied­File
    1. IO.Error.mk­Permission­Denied­File
  98. mk­Protocol­Error
    1. IO.Error.mk­Protocol­Error
  99. mk­Ref
    1. IO.mk­Ref
    2. ST.mk­Ref
  100. mk­Resource­Busy
    1. IO.Error.mk­Resource­Busy
  101. mk­Resource­Exhausted
    1. IO.Error.mk­Resource­Exhausted
  102. mk­Resource­Exhausted­File
    1. IO.Error.mk­Resource­Exhausted­File
  103. mk­Resource­Vanished
    1. IO.Error.mk­Resource­Vanished
  104. mk­Std­Gen
  105. mk­Tactic­Attribute
    1. Lean.Elab.Tactic.mk­Tactic­Attribute
  106. mk­Time­Expired
    1. IO.Error.mk­Time­Expired
  107. mk­Unsatisfied­Constraints
    1. IO.Error.mk­Unsatisfied­Constraints
  108. mk­Unsupported­Operation
    1. IO.Error.mk­Unsupported­Operation
  109. mod
    1. Fin.mod
    2. ISize.mod
    3. Int16.mod
    4. Int32.mod
    5. Int64.mod
    6. Int8.mod
    7. Mod.mod (class method)
    8. Nat.mod
    9. UInt16.mod
    10. UInt32.mod
    11. UInt64.mod
    12. UInt8.mod
    13. USize.mod
  110. mod­Core
    1. Nat.mod­Core
  111. modified
    1. IO.FS.Metadata.modified (structure field)
  112. modify
    1. Array.modify
    2. ST.Ref.modify
    3. String.modify
  113. 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
  114. modify­Get­The
  115. modify­M
    1. Array.modify­M
  116. modify­Op
    1. Array.modify­Op
  117. modify­The
  118. modn
    1. Fin.modn
  119. monad­Lift
    1. MonadLift.monad­Lift (class method)
    2. Monad­LiftT.monad­Lift (class method)
  120. monad­Map
    1. MonadFunctor.monad­Map (class method)
    2. Monad­FunctorT.monad­Map (class method)
  121. mono­Ms­Now
    1. IO.mono­Ms­Now
  122. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  123. mul
    1. Fin.mul
    2. ISize.mul
    3. Int16.mul
    4. Int32.mul
    5. Int64.mul
    6. Int8.mul
    7. Mul.mul (class method)
    8. Nat.mul
    9. UInt16.mul
    10. UInt32.mul
    11. UInt64.mul
    12. UInt8.mul
    13. USize.mul
  124. 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­Add
    1. Fin.nat­Add
  128. nat­Cast
    1. NatCast.nat­Cast (class method)
  129. native_decide
  130. neg
    1. ISize.neg
    2. Int16.neg
    3. Int32.neg
    4. Int64.neg
    5. Int8.neg
    6. Neg.neg (class method)
  131. neutral­Config
    1. Lean.Meta.Simp.neutral­Config
  132. new­Goals
    1. Lean.Meta.Rewrite.Config.new­Goals (structure field)
  133. next
    1. RandomGen.next (class method)
    2. String.Iterator.next
    3. String.next
  134. next ... => ...
  135. next'
    1. String.next'
  136. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  137. next­Until
    1. String.next­Until
  138. next­While
    1. String.next­While
  139. nextn
    1. String.Iterator.nextn
  140. no­Confusion
    1. Nat.no­Confusion
  141. no­Confusion­Type
    1. Nat.no­Confusion­Type
  142. nofun
  143. nomatch
  144. non­Backtrackable
    1. EStateM.non­Backtrackable
  145. norm_cast (0) (1)
  146. normalize
    1. System.FilePath.normalize
  147. not
    1. Bool.not
  148. not­M
  149. null­Kind
    1. Lean.null­Kind
  150. 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.all
  8. Option.any
  9. Option.attach
  10. Option.attach­With
  11. Option.bind
  12. Option.bind­M
  13. Option.choice
  14. Option.decidable_eq_none
  15. Option.elim
  16. Option.elim­M
  17. Option.filter
  18. Option.for­M
  19. Option.format
  20. Option.get
  21. Option.get!
  22. Option.get­D
  23. Option.get­DM
  24. Option.get­M
  25. Option.guard
  26. Option.is­Eq­Some
  27. Option.is­None
  28. Option.is­Some
  29. Option.join
  30. Option.lift­Or­Get
  31. Option.lt
  32. Option.map
  33. Option.map­A
  34. Option.map­M
  35. Option.max
  36. Option.merge
  37. Option.min
  38. Option.none
    1. Constructor of Option
  39. Option.or
  40. Option.or­Else
  41. Option.pbind
  42. Option.pelim
  43. Option.pmap
  44. Option.repr
  45. Option.sequence
  46. Option.some
    1. Constructor of Option
  47. Option.to­Array
  48. Option.to­List
  49. Option.try­Catch
  50. Option.unattach
  51. Option­T
  52. OptionT.bind
  53. OptionT.fail
  54. OptionT.lift
  55. OptionT.mk
  56. OptionT.or­Else
  57. OptionT.pure
  58. OptionT.run
  59. OptionT.try­Catch
  60. Ord
  61. Ord.mk
    1. Instance constructor of Ord
  62. Output
    1. IO.Process.Output
  63. obtain
  64. occs
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  65. of­Buffer
    1. IO.FS.Stream.of­Buffer
  66. of­Except
    1. IO.of­Except
    2. MonadExcept.of­Except
  67. of­Fn
    1. Array.of­Fn
  68. of­Handle
    1. IO.FS.Stream.of­Handle
  69. of­Int
    1. ISize.of­Int
    2. Int16.of­Int
    3. Int32.of­Int
    4. Int64.of­Int
    5. Int8.of­Int
  70. of­Nat
    1. ISize.of­Nat
    2. Int16.of­Nat
    3. Int32.of­Nat
    4. Int64.of­Nat
    5. Int8.of­Nat
    6. OfNat.of­Nat (class method)
    7. UInt16.of­Nat
    8. UInt32.of­Nat
    9. UInt64.of­Nat
    10. UInt8.of­Nat
    11. USize.of­Nat
  71. of­Nat'
    1. Fin.of­Nat'
    2. UInt32.of­Nat'
  72. of­Nat32
    1. USize.of­Nat32
  73. of­Nat­Core
    1. UInt16.of­Nat­Core
    2. UInt32.of­Nat­Core
    3. UInt64.of­Nat­Core
    4. UInt8.of­Nat­Core
    5. USize.of­Nat­Core
  74. of­Nat­Truncate
    1. UInt32.of­Nat­Truncate
  75. of­Scientific
    1. OfScientific.of­Scientific (class method)
  76. of­Subarray
    1. Array.of­Subarray
  77. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  78. offset­Of­Pos
    1. String.offset­Of­Pos
  79. omega
  80. open
  81. opt­Param
  82. optional
  83. or
    1. Bool.or
    2. Option.or
  84. or­Else
    1. EStateM.or­Else
    2. Lean.Elab.Tactic.or­Else
    3. MonadExcept.or­Else
    4. Option.or­Else
    5. OptionT.or­Else
    6. ReaderT.or­Else
    7. StateT.or­Else
    8. [anonymous] (class method)
  85. or­Else'
    1. EStateM.or­Else'
  86. or­Else­Lazy
    1. Except.or­Else­Lazy
  87. or­M
  88. orelse'
    1. MonadExcept.orelse'
  89. other
    1. IO.FileRight.other (structure field)
  90. other­Error­To­String
    1. IO.Error.other­Error­To­String
  91. out
    1. NeZero.out (class method)
  92. out­Param
  93. 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. pbind
    1. Option.pbind
  35. pelim
    1. Option.pelim
  36. placeholder term
  37. pmap
    1. Option.pmap
  38. polymorphism
    1. universe
  39. pop
    1. Array.pop
  40. pop­Front
    1. Subarray.pop­Front
  41. pop­While
    1. Array.pop­While
  42. pos
    1. IO.FS.Stream.Buffer.pos
    2. IO.FS.Stream.Buffer.pos (structure field)
    3. String.Iterator.pos
  43. pos­Of
    1. String.pos­Of
  44. pow
    1. HomogeneousPow.pow (class method)
    2. Nat.pow
    3. NatPow.pow (class method)
    4. Pow.pow (class method)
  45. pp.deep­Terms
  46. pp.deepTerms.threshold
  47. pp.field­Notation
  48. pp.match
  49. pp.max­Steps
  50. pp.mvars
  51. pp.proofs
  52. pp.proofs.threshold
  53. pred
    1. Fin.pred
    2. Nat.pred
  54. predicative
  55. prev
    1. String.Iterator.prev
    2. String.prev
  56. prevn
    1. String.Iterator.prevn
  57. print
    1. IO.print
  58. println
    1. IO.println
  59. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
    2. Lean.Meta.Simp.Config.proj (structure field)
  60. proof state
  61. proofs
    1. pp.proofs
  62. property
    1. Subtype.property (structure field)
  63. propext
  64. proposition
    1. decidable
  65. prune­Solved­Goals
    1. Lean.Elab.Tactic.prune­Solved­Goals
  66. ptr­Eq
    1. ST.Ref.ptr­Eq
  67. pure
    1. EStateM.pure
    2. Except.pure
    3. ExceptT.pure
    4. OptionT.pure
    5. Pure.pure (class method)
    6. ReaderT.pure
    7. StateT.pure
  68. pure_bind
    1. [anonymous] (class method)
  69. pure_seq
    1. [anonymous] (class method)
  70. push
    1. Array.push
    2. String.push
  71. push_cast
  72. pushn
    1. String.pushn
  73. put­Str
    1. IO.FS.Handle.put­Str
    2. IO.FS.Stream.put­Str (structure field)
  74. 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. Fin.reduce­Add
    2. Nat.reduce­Add
    3. UInt16.reduce­Add
    4. UInt32.reduce­Add
    5. UInt64.reduce­Add
    6. UInt8.reduce­Add
  36. reduce­Add­Nat
    1. Fin.reduce­Add­Nat
  37. reduce­And
    1. Fin.reduce­And
  38. reduce­Append
    1. String.reduce­Append
  39. reduce­BEq
    1. Fin.reduce­BEq
    2. Nat.reduce­BEq
    3. String.reduce­BEq
  40. reduce­BNe
    1. Fin.reduce­BNe
    2. Nat.reduce­BNe
    3. String.reduce­BNe
  41. reduce­Beq­Diff
    1. Nat.reduce­Beq­Diff
  42. reduce­Bin
    1. Fin.reduce­Bin
    2. Nat.reduce­Bin
  43. reduce­Bin­Pred
    1. Fin.reduce­Bin­Pred
    2. Nat.reduce­Bin­Pred
    3. String.reduce­Bin­Pred
  44. reduce­Bne­Diff
    1. Nat.reduce­Bne­Diff
  45. reduce­Bool­Pred
    1. Fin.reduce­Bool­Pred
    2. Nat.reduce­Bool­Pred
    3. String.reduce­Bool­Pred
  46. reduce­Cast­Add
    1. Fin.reduce­Cast­Add
  47. reduce­Cast­LE
    1. Fin.reduce­Cast­LE
  48. reduce­Cast­LT
    1. Fin.reduce­Cast­LT
  49. reduce­Cast­Succ
    1. Fin.reduce­Cast­Succ
  50. reduce­Div
    1. Fin.reduce­Div
    2. Nat.reduce­Div
    3. UInt16.reduce­Div
    4. UInt32.reduce­Div
    5. UInt64.reduce­Div
    6. UInt8.reduce­Div
  51. reduce­Eq
    1. Fin.reduce­Eq
    2. String.reduce­Eq
  52. reduce­Eq­Diff
    1. Nat.reduce­Eq­Diff
  53. reduce­Fin­Mk
    1. Fin.reduce­Fin­Mk
  54. reduce­GE
    1. Fin.reduce­GE
    2. String.reduce­GE
    3. UInt16.reduce­GE
    4. UInt32.reduce­GE
    5. UInt64.reduce­GE
    6. UInt8.reduce­GE
  55. reduce­GT
    1. Fin.reduce­GT
    2. Nat.reduce­GT
    3. String.reduce­GT
    4. UInt16.reduce­GT
    5. UInt32.reduce­GT
    6. UInt64.reduce­GT
    7. UInt8.reduce­GT
  56. reduce­Gcd
    1. Nat.reduce­Gcd
  57. reduce­Get­Elem
    1. Array.reduce­Get­Elem
  58. reduce­Get­Elem!
    1. Array.reduce­Get­Elem!
  59. reduce­Get­Elem?
    1. Array.reduce­Get­Elem?
  60. reduce­LE
    1. Fin.reduce­LE
    2. String.reduce­LE
    3. UInt16.reduce­LE
    4. UInt32.reduce­LE
    5. UInt64.reduce­LE
    6. UInt8.reduce­LE
  61. reduce­LT
    1. Fin.reduce­LT
    2. Nat.reduce­LT
    3. String.reduce­LT
    4. UInt16.reduce­LT
    5. UInt32.reduce­LT
    6. UInt64.reduce­LT
    7. UInt8.reduce­LT
  62. reduce­LTLE
    1. Nat.reduce­LTLE
  63. reduce­Last
    1. Fin.reduce­Last
  64. reduce­Le­Diff
    1. Nat.reduce­Le­Diff
  65. reduce­Mk
    1. String.reduce­Mk
  66. reduce­Mod
    1. Fin.reduce­Mod
    2. Nat.reduce­Mod
    3. UInt16.reduce­Mod
    4. UInt32.reduce­Mod
    5. UInt64.reduce­Mod
    6. UInt8.reduce­Mod
  67. reduce­Mul
    1. Fin.reduce­Mul
    2. Nat.reduce­Mul
    3. UInt16.reduce­Mul
    4. UInt32.reduce­Mul
    5. UInt64.reduce­Mul
    6. UInt8.reduce­Mul
  68. reduce­Nat­Add
    1. Fin.reduce­Nat­Add
  69. reduce­Nat­Eq­Expr
    1. Nat.reduce­Nat­Eq­Expr
  70. reduce­Nat­Op
    1. Fin.reduce­Nat­Op
  71. reduce­Ne
    1. Fin.reduce­Ne
    2. String.reduce­Ne
  72. reduce­Of­Nat
    1. UInt16.reduce­Of­Nat
    2. UInt32.reduce­Of­Nat
    3. UInt64.reduce­Of­Nat
    4. UInt8.reduce­Of­Nat
  73. reduce­Of­Nat'
    1. Fin.reduce­Of­Nat'
  74. reduce­Of­Nat­Core
    1. UInt16.reduce­Of­Nat­Core
    2. UInt32.reduce­Of­Nat­Core
    3. UInt64.reduce­Of­Nat­Core
    4. UInt8.reduce­Of­Nat­Core
  75. reduce­Op
    1. Fin.reduce­Op
  76. reduce­Option
    1. Array.reduce­Option
  77. reduce­Or
    1. Fin.reduce­Or
  78. reduce­Pow
    1. Nat.reduce­Pow
  79. reduce­Pred
    1. Fin.reduce­Pred
  80. reduce­Rev
    1. Fin.reduce­Rev
  81. reduce­Shift­Left
    1. Fin.reduce­Shift­Left
  82. reduce­Shift­Right
    1. Fin.reduce­Shift­Right
  83. reduce­Sub
    1. Fin.reduce­Sub
    2. Nat.reduce­Sub
    3. UInt16.reduce­Sub
    4. UInt32.reduce­Sub
    5. UInt64.reduce­Sub
    6. UInt8.reduce­Sub
  84. reduce­Sub­Diff
    1. Nat.reduce­Sub­Diff
  85. reduce­Sub­Nat
    1. Fin.reduce­Sub­Nat
  86. reduce­Succ
    1. Fin.reduce­Succ
    2. Nat.reduce­Succ
  87. reduce­To­Nat
    1. UInt16.reduce­To­Nat
    2. UInt32.reduce­To­Nat
    3. UInt64.reduce­To­Nat
    4. UInt8.reduce­To­Nat
    5. USize.reduce­To­Nat
  88. reduce­Unary
    1. Nat.reduce­Unary
  89. reduce­Xor
    1. Fin.reduce­Xor
  90. reduction
    1. ι (iota)
  91. ref
    1. ST.Ref.ref (structure field)
  92. refine
  93. refine'
  94. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  95. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  96. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  97. remaining­To­String
    1. String.Iterator.remaining­To­String
  98. remove­Dir
    1. IO.FS.remove­Dir
  99. remove­Dir­All
    1. IO.FS.remove­Dir­All
  100. remove­File
    1. IO.FS.remove­File
  101. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  102. rename
    1. IO.FS.rename
  103. rename_i
  104. repeat (0) (1)
    1. Nat.repeat
  105. repeat'
  106. repeat1'
  107. repeat­TR
    1. Nat.repeat­TR
  108. replace
    1. String.replace
  109. repr
    1. Nat.repr
    2. Option.repr
    3. USize.repr
  110. repr­Prec
    1. Repr.repr­Prec (class method)
  111. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  112. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  113. restore
    1. EStateM.Backtrackable.restore (class method)
  114. restore­M
    1. MonadControl.restore­M (class method)
    2. Monad­ControlT.restore­M (class method)
  115. rev
    1. Fin.rev
  116. rev­Find
    1. String.rev­Find
  117. rev­Pos­Of
    1. String.rev­Pos­Of
  118. reverse
    1. Array.reverse
  119. reverse­Induction
    1. Fin.reverse­Induction
  120. revert
  121. rewind
    1. IO.FS.Handle.rewind
  122. rewrite (0) (1)
    1. trace.Meta.Tactic.simp.rewrite
  123. rfl (0) (1)
    1. LawfulBEq.rfl (class method)
  124. rfl'
  125. rhs
  126. right (0) (1)
  127. rintro
  128. root
    1. IO.FS.DirEntry.root (structure field)
  129. rotate_left
  130. rotate_right
  131. 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
  132. run'
    1. EStateM.run'
    2. State­CpsT.run'
    3. State­RefT'.run'
    4. StateT.run'
  133. run­Catch
    1. Except­CpsT.run­Catch
  134. run­EST
  135. run­K
    1. Except­CpsT.run­K
    2. State­CpsT.run­K
  136. run­ST
  137. run­Term­Elab
    1. Lean.Elab.Tactic.run­Term­Elab
  138. run_tac
  139. rw (0) (1)
  140. rw?
  141. rw_mod_cast
  142. 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
    1. Option.sequence
  269. sequence­Map
    1. Array.sequence­Map
  270. 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
  271. set!
    1. Array.set!
  272. set­Access­Rights
    1. IO.set­Access­Rights
  273. set­Curr
    1. String.Iterator.set­Curr
  274. set­Current­Dir
    1. IO.Process.set­Current­Dir
  275. set­D
    1. Array.set­D
  276. set­Goals
    1. Lean.Elab.Tactic.set­Goals
  277. set­Kind
    1. Lean.Syntax.set­Kind
  278. set­Rand­Seed
    1. IO.set­Rand­Seed
  279. set­Stderr
    1. IO.set­Stderr
  280. set­Stdin
    1. IO.set­Stdin
  281. set­Stdout
    1. IO.set­Stdout
  282. set_option
  283. setsid
    1. IO.Process.SpawnArgs.args (structure field)
  284. shift­Left
    1. Fin.shift­Left
    2. ISize.shift­Left
    3. Int16.shift­Left
    4. Int32.shift­Left
    5. Int64.shift­Left
    6. Int8.shift­Left
    7. Nat.shift­Left
    8. ShiftLeft.shift­Left (class method)
    9. UInt16.shift­Left
    10. UInt32.shift­Left
    11. UInt64.shift­Left
    12. UInt8.shift­Left
    13. USize.shift­Left
  285. shift­Right
    1. Fin.shift­Right
    2. ISize.shift­Right
    3. Int16.shift­Right
    4. Int32.shift­Right
    5. Int64.shift­Right
    6. Int8.shift­Right
    7. Nat.shift­Right
    8. ShiftRight.shift­Right (class method)
    9. UInt16.shift­Right
    10. UInt32.shift­Right
    11. UInt64.shift­Right
    12. UInt8.shift­Right
    13. USize.shift­Right
  286. show
  287. show_term
  288. simp (0) (1)
  289. simp!
  290. simp?
  291. simp?!
  292. simp_all
  293. simp_all!
  294. simp_all?
  295. simp_all?!
  296. simp_all_arith
  297. simp_all_arith!
  298. simp_arith
  299. simp_arith!
  300. simp_match
  301. simp_wf
  302. simpa
  303. simpa!
  304. simpa?
  305. simpa?!
  306. simprocs
  307. single­Pass
    1. Lean.Meta.Simp.Config.single­Pass (structure field)
  308. singleton
    1. Array.singleton
    2. String.singleton
  309. size
    1. Array.size
    2. ISize.size
    3. Int16.size
    4. Int32.size
    5. Int64.size
    6. Int8.size
    7. Subarray.size
    8. UInt16.size
    9. UInt32.size
    10. UInt64.size
    11. UInt8.size
    12. USize.size
  310. size­Of
    1. SizeOf.size­Of (class method)
  311. skip (0) (1)
  312. skip­Assigned­Instances
    1. tactic.skip­Assigned­Instances
  313. sleep
    1. IO.sleep
  314. 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)
  315. solve
  316. solve_by_elim
  317. sorry
  318. sort­MVar­Id­Array­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  319. sort­MVar­Ids­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  320. spawn
    1. IO.Process.spawn
    2. Task.spawn
  321. specialize
  322. split
    1. Array.split
    2. RandomGen.split (class method)
    3. String.split
    4. Subarray.split
  323. split­On
    1. String.split­On
  324. st­M
    1. MonadControl.st­M (class method)
    2. Monad­ControlT.st­M (class method)
  325. start
    1. Subarray.start (structure field)
  326. start_le_stop
    1. Subarray.start_le_stop (structure field)
  327. starts­With
    1. String.starts­With
  328. std­Next
  329. std­Range
  330. std­Split
  331. stderr
    1. IO.Process.Child.stderr (structure field)
    2. IO.Process.Output.stderr (structure field)
    3. IO.Process.StdioConfig.stderr (structure field)
  332. stdin
    1. IO.Process.Child.stdin (structure field)
    2. IO.Process.StdioConfig.stdin (structure field)
  333. stdout
    1. IO.Process.Child.stdout (structure field)
    2. IO.Process.Output.stdout (structure field)
    3. IO.Process.StdioConfig.stdout (structure field)
  334. stop
    1. Subarray.stop (structure field)
  335. stop_le_array_size
    1. Subarray.stop_le_array_size (structure field)
  336. str­Lit­Kind
    1. Lean.str­Lit­Kind
  337. strong­Induction­On
    1. Nat.strong­Induction­On
  338. sub
    1. Fin.sub
    2. ISize.sub
    3. Int16.sub
    4. Int32.sub
    5. Int64.sub
    6. Int8.sub
    7. Nat.sub
    8. Sub.sub (class method)
    9. UInt16.sub
    10. UInt32.sub
    11. UInt64.sub
    12. UInt8.sub
    13. USize.sub
  339. sub­Digit­Char
    1. Nat.sub­Digit­Char
  340. sub­Nat
    1. Fin.sub­Nat
  341. subst
  342. subst_eqs
  343. subst_vars
  344. substr­Eq
    1. String.substr­Eq
  345. succ
    1. Fin.succ
  346. succ­Rec
    1. Fin.succ­Rec
  347. succ­Rec­On
    1. Fin.succ­Rec­On
  348. suffices
  349. super­Digit­Char
    1. Nat.super­Digit­Char
  350. swap
    1. Array.swap
    2. ST.Ref.swap
  351. swap!
    1. Array.swap!
  352. swap­At
    1. Array.swap­At
  353. swap­At!
    1. Array.swap­At!
  354. symm
  355. symm_saturate
  356. synthInstance.max­Heartbeats
  357. synthInstance.max­Size
  358. 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. Option.to­Array
    2. Subarray.to­Array
  44. to­Base­IO
    1. EIO.to­Base­IO
  45. to­Bind
    1. [anonymous] (class method)
  46. to­Bit­Vec
    1. ISize.to­Bit­Vec
    2. Int16.to­Bit­Vec
    3. Int32.to­Bit­Vec
    4. Int64.to­Bit­Vec
    5. Int8.to­Bit­Vec
    6. UInt16.to­Bit­Vec (structure field)
    7. UInt32.to­Bit­Vec (structure field)
    8. UInt64.to­Bit­Vec (structure field)
    9. UInt8.to­Bit­Vec (structure field)
    10. 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
    2. UInt64.to­Float
  54. to­Float32
    1. UInt64.to­Float32
  55. to­Format
    1. String.to­Format
  56. to­Functor
    1. Applicative.to­Functor (class method)
  57. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  58. to­Handle­Type
    1. IO.Process.Stdio.to­Handle­Type
  59. to­IO
    1. BaseIO.to­IO
    2. EIO.to­IO
  60. to­IO'
    1. EIO.to­IO'
  61. to­ISize
    1. Bool.to­ISize
    2. Int32.to­ISize
    3. Int64.to­ISize
  62. to­Int
    1. ISize.to­Int
    2. Int16.to­Int
    3. Int32.to­Int
    4. Int64.to­Int
    5. Int8.to­Int
  63. to­Int!
    1. String.to­Int!
  64. to­Int16
    1. Bool.to­Int16
    2. Int32.to­Int16
    3. Int64.to­Int16
    4. Int8.to­Int16
  65. to­Int32
    1. Bool.to­Int32
    2. ISize.to­Int32
    3. Int16.to­Int32 (0) (1)
    4. Int64.to­Int32
    5. Int8.to­Int32 (0) (1)
  66. to­Int64
    1. Bool.to­Int64
    2. ISize.to­Int64
    3. Int16.to­Int64
    4. Int32.to­Int64
    5. Int8.to­Int64
  67. to­Int8
    1. Bool.to­Int8
    2. Int16.to­Int8
    3. Int32.to­Int8
    4. Int64.to­Int8
  68. to­Int?
    1. String.to­Int?
  69. to­Lawful­Applicative
    1. LawfulMonad.to­Lawful­Applicative (class method)
  70. to­Lawful­Functor
    1. LawfulApplicative.to­Lawful­Functor (class method)
  71. to­Level
    1. Nat.to­Level
  72. to­List
    1. Array.to­List
    2. Array.to­List (structure field)
    3. Option.to­List
    4. String.to­List
  73. to­List­Append
    1. Array.to­List­Append
  74. to­List­Rev
    1. Array.to­List­Rev
  75. to­Lower
    1. String.to­Lower
  76. to­Monad­State­Of
    1. ST.Ref.to­Monad­State­Of
  77. to­Name
    1. String.to­Name
  78. to­Nat
    1. Bool.to­Nat
    2. ISize.to­Nat
    3. Int16.to­Nat
    4. Int32.to­Nat
    5. Int64.to­Nat
    6. Int8.to­Nat
    7. UInt16.to­Nat
    8. UInt32.to­Nat
    9. UInt64.to­Nat
    10. UInt8.to­Nat
    11. USize.to­Nat
  79. to­Nat!
    1. String.to­Nat!
  80. to­Nat?
    1. String.to­Nat?
  81. to­Option
    1. Except.to­Option
  82. to­PArray'
    1. Array.to­PArray'
  83. to­Pure
    1. [anonymous] (class method)
  84. to­Seq
    1. [anonymous] (class method)
  85. to­Seq­Left
    1. Applicative.to­Pure (class method)
  86. to­Seq­Right
    1. [anonymous] (class method)
  87. to­Stdio­Config
    1. IO.Process.SpawnArgs.to­Stdio­Config (structure field)
  88. to­String
    1. IO.Error.to­String
    2. System.FilePath.to­String (structure field)
    3. ToString.to­String (class method)
  89. to­Sub­Digits
    1. Nat.to­Sub­Digits
  90. to­Subarray
    1. Array.to­Subarray
  91. to­Subscript­String
    1. Nat.to­Subscript­String
  92. to­Substring
    1. String.to­Substring
  93. to­Substring'
    1. String.to­Substring'
  94. to­Super­Digits
    1. Nat.to­Super­Digits
  95. to­Superscript­String
    1. Nat.to­Superscript­String
  96. to­UInt16
    1. Bool.to­UInt16
    2. Int16.to­UInt16 (structure field)
    3. Nat.to­UInt16
    4. UInt32.to­UInt16
    5. UInt64.to­UInt16
    6. UInt8.to­UInt16
    7. USize.to­UInt16
  97. to­UInt32
    1. Bool.to­UInt32
    2. Int32.to­UInt32 (structure field)
    3. Nat.to­UInt32
    4. UInt16.to­UInt32
    5. UInt64.to­UInt32
    6. UInt8.to­UInt32
    7. USize.to­UInt32
  98. to­UInt64
    1. Bool.to­UInt64
    2. Int64.to­UInt64 (structure field)
    3. Nat.to­UInt64
    4. UInt16.to­UInt64
    5. UInt32.to­UInt64
    6. UInt8.to­UInt64
    7. USize.to­UInt64
  99. to­UInt8
    1. Bool.to­UInt8
    2. Int8.to­UInt8 (structure field)
    3. Nat.to­UInt8
    4. UInt16.to­UInt8
    5. UInt32.to­UInt8
    6. UInt64.to­UInt8
    7. USize.to­UInt8
  100. to­USize
    1. Bool.to­USize
    2. ISize.to­USize (structure field)
    3. Nat.to­USize
    4. UInt16.to­USize
    5. UInt32.to­USize
    6. UInt64.to­USize
    7. UInt8.to­USize
  101. to­UTF8
    1. String.to­UTF8
  102. to­Upper
    1. String.to­Upper
  103. trace
    1. Lean.Macro.trace
    2. tactic.simp.trace (0) (1)
  104. trace.Meta.Tactic.simp.discharge
  105. trace.Meta.Tactic.simp.rewrite
  106. trace_state (0) (1)
  107. transparency
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  108. trim
    1. String.trim
  109. trim­Left
    1. String.trim­Left
  110. trim­Right
    1. String.trim­Right
  111. trivial
  112. truncate
    1. IO.FS.Handle.truncate
  113. try (0) (1)
  114. 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. Option.try­Catch
    8. OptionT.try­Catch
  115. try­Catch­The
  116. try­Finally'
    1. MonadFinally.try­Finally' (class method)
  117. try­Lock
    1. IO.FS.Handle.try­Lock
  118. try­Tactic
    1. Lean.Elab.Tactic.try­Tactic
  119. try­Tactic?
    1. Lean.Elab.Tactic.try­Tactic?
  120. try­Wait
    1. IO.Process.Child.try­Wait
  121. type
    1. IO.FS.Metadata.type (structure field)
  122. type constructor

U

  1. UInt16
  2. UInt16.add
  3. UInt16.complement
  4. UInt16.dec­Eq
  5. UInt16.dec­Le
  6. UInt16.dec­Lt
  7. UInt16.div
  8. UInt16.from­Expr
  9. UInt16.land
  10. UInt16.le
  11. UInt16.log2
  12. UInt16.lor
  13. UInt16.lt
  14. UInt16.mk
    1. Constructor of UInt16
  15. UInt16.mod
  16. UInt16.mul
  17. UInt16.of­Nat
  18. UInt16.of­Nat­Core
  19. UInt16.reduce­Add
  20. UInt16.reduce­Div
  21. UInt16.reduce­GE
  22. UInt16.reduce­GT
  23. UInt16.reduce­LE
  24. UInt16.reduce­LT
  25. UInt16.reduce­Mod
  26. UInt16.reduce­Mul
  27. UInt16.reduce­Of­Nat
  28. UInt16.reduce­Of­Nat­Core
  29. UInt16.reduce­Sub
  30. UInt16.reduce­To­Nat
  31. UInt16.shift­Left
  32. UInt16.shift­Right
  33. UInt16.size
  34. UInt16.sub
  35. UInt16.to­Nat
  36. UInt16.to­UInt32
  37. UInt16.to­UInt64
  38. UInt16.to­UInt8
  39. UInt16.to­USize
  40. UInt16.val
  41. UInt16.xor
  42. UInt32
  43. UInt32.add
  44. UInt32.complement
  45. UInt32.dec­Eq
  46. UInt32.dec­Le
  47. UInt32.dec­Lt
  48. UInt32.div
  49. UInt32.from­Expr
  50. UInt32.is­Valid­Char
  51. UInt32.land
  52. UInt32.log2
  53. UInt32.lor
  54. UInt32.mk
    1. Constructor of UInt32
  55. UInt32.mod
  56. UInt32.mul
  57. UInt32.of­Nat
  58. UInt32.of­Nat'
  59. UInt32.of­Nat­Core
  60. UInt32.of­Nat­Truncate
  61. UInt32.reduce­Add
  62. UInt32.reduce­Div
  63. UInt32.reduce­GE
  64. UInt32.reduce­GT
  65. UInt32.reduce­LE
  66. UInt32.reduce­LT
  67. UInt32.reduce­Mod
  68. UInt32.reduce­Mul
  69. UInt32.reduce­Of­Nat
  70. UInt32.reduce­Of­Nat­Core
  71. UInt32.reduce­Sub
  72. UInt32.reduce­To­Nat
  73. UInt32.shift­Left
  74. UInt32.shift­Right
  75. UInt32.size
  76. UInt32.sub
  77. UInt32.to­Nat
  78. UInt32.to­UInt16
  79. UInt32.to­UInt64
  80. UInt32.to­UInt8
  81. UInt32.to­USize
  82. UInt32.val
  83. UInt32.xor
  84. UInt64
  85. UInt64.add
  86. UInt64.complement
  87. UInt64.dec­Eq
  88. UInt64.dec­Le
  89. UInt64.dec­Lt
  90. UInt64.div
  91. UInt64.from­Expr
  92. UInt64.land
  93. UInt64.le
  94. UInt64.log2
  95. UInt64.lor
  96. UInt64.lt
  97. UInt64.mk
    1. Constructor of UInt64
  98. UInt64.mod
  99. UInt64.mul
  100. UInt64.of­Nat
  101. UInt64.of­Nat­Core
  102. UInt64.reduce­Add
  103. UInt64.reduce­Div
  104. UInt64.reduce­GE
  105. UInt64.reduce­GT
  106. UInt64.reduce­LE
  107. UInt64.reduce­LT
  108. UInt64.reduce­Mod
  109. UInt64.reduce­Mul
  110. UInt64.reduce­Of­Nat
  111. UInt64.reduce­Of­Nat­Core
  112. UInt64.reduce­Sub
  113. UInt64.reduce­To­Nat
  114. UInt64.shift­Left
  115. UInt64.shift­Right
  116. UInt64.size
  117. UInt64.sub
  118. UInt64.to­Float
  119. UInt64.to­Float32
  120. UInt64.to­Nat
  121. UInt64.to­UInt16
  122. UInt64.to­UInt32
  123. UInt64.to­UInt8
  124. UInt64.to­USize
  125. UInt64.val
  126. UInt64.xor
  127. UInt8
  128. UInt8.add
  129. UInt8.complement
  130. UInt8.dec­Eq
  131. UInt8.dec­Le
  132. UInt8.dec­Lt
  133. UInt8.div
  134. UInt8.from­Expr
  135. UInt8.land
  136. UInt8.le
  137. UInt8.log2
  138. UInt8.lor
  139. UInt8.lt
  140. UInt8.mk
    1. Constructor of UInt8
  141. UInt8.mod
  142. UInt8.mul
  143. UInt8.of­Nat
  144. UInt8.of­Nat­Core
  145. UInt8.reduce­Add
  146. UInt8.reduce­Div
  147. UInt8.reduce­GE
  148. UInt8.reduce­GT
  149. UInt8.reduce­LE
  150. UInt8.reduce­LT
  151. UInt8.reduce­Mod
  152. UInt8.reduce­Mul
  153. UInt8.reduce­Of­Nat
  154. UInt8.reduce­Of­Nat­Core
  155. UInt8.reduce­Sub
  156. UInt8.reduce­To­Nat
  157. UInt8.shift­Left
  158. UInt8.shift­Right
  159. UInt8.size
  160. UInt8.sub
  161. UInt8.to­Nat
  162. UInt8.to­UInt16
  163. UInt8.to­UInt32
  164. UInt8.to­UInt64
  165. UInt8.to­USize
  166. UInt8.val
  167. UInt8.xor
  168. ULift
  169. ULift.up
    1. Constructor of ULift
  170. USize
  171. USize.add
  172. USize.complement
  173. USize.dec­Eq
  174. USize.dec­Le
  175. USize.dec­Lt
  176. USize.div
  177. USize.from­Expr
  178. USize.land
  179. USize.le
  180. USize.log2
  181. USize.lor
  182. USize.lt
  183. USize.mk
    1. Constructor of USize
  184. USize.mod
  185. USize.mul
  186. USize.of­Nat
  187. USize.of­Nat32
  188. USize.of­Nat­Core
  189. USize.reduce­To­Nat
  190. USize.repr
  191. USize.shift­Left
  192. USize.shift­Right
  193. USize.size
  194. USize.sub
  195. USize.to­Nat
  196. USize.to­UInt16
  197. USize.to­UInt32
  198. USize.to­UInt64
  199. USize.to­UInt8
  200. USize.val
  201. USize.xor
  202. Unit
  203. Unit.unit
  204. uget
    1. Array.uget
  205. unattach
    1. Array.unattach
    2. Option.unattach
  206. unfold (0) (1)
  207. unfold­Partial­App
    1. Lean.Meta.DSimp.Config.unfold­Partial­App (structure field)
    2. Lean.Meta.Simp.Config.unfold­Partial­App (structure field)
  208. unhygienic
  209. unit
    1. Unit.unit
  210. universe
  211. universe polymorphism
  212. unlock
    1. IO.FS.Handle.unlock
  213. unnecessary­Simpa
    1. linter.unnecessary­Simpa
  214. unsupported­Syntax
    1. Lean.Macro.Exception.unsupported­Syntax
  215. unzip
    1. Array.unzip
  216. user
    1. IO.FileRight.user (structure field)
  217. user­Error
    1. IO.user­Error
  218. uset
    1. Array.uset
  219. usize
    1. Array.usize
  220. utf16Length
    1. String.utf16Length
  221. utf16Pos­To­Codepoint­Pos
    1. String.utf16Pos­To­Codepoint­Pos
  222. utf16Pos­To­Codepoint­Pos­From
    1. String.utf16Pos­To­Codepoint­Pos­From
  223. utf8Byte­Size
    1. String.utf8Byte­Size
  224. utf8Decode­Char?
    1. String.utf8Decode­Char?
  225. utf8Encode­Char
    1. String.utf8Encode­Char

V

  1. val
    1. Char.val (structure field)
    2. Fin.val (structure field)
    3. Subtype.val (structure field)
    4. UInt16.val
    5. UInt32.val
    6. UInt64.val
    7. UInt8.val
    8. USize.val
  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. Fin.xor
    3. ISize.xor
    4. Int16.xor
    5. Int32.xor
    6. Int64.xor
    7. Int8.xor
    8. Nat.xor
    9. UInt16.xor
    10. UInt32.xor
    11. UInt64.xor
    12. UInt8.xor
    13. USize.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
Applicative
```exceptions
```

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

{docstring Array.eraseIdxIfInBounds}

{docstring Array.eraseP}

{docstring Array.finRange}

{docstring Array.findFinIdx?}

{docstring Array.findFinIdx?.loop}

{docstring Array.insertIdx}

{docstring Array.insertIdx!}

{docstring Array.insertIdx.loop}

{docstring Array.insertIdxIfInBounds}

{docstring Array.lex}

{docstring Array.pmap}

{docstring Array.setIfInBounds}

{docstring Array.swapIfInBounds}

{docstring Array.toVector}

{docstring Array.zipWithAll}

{docstring Array.zipWithAll.go}

{docstring Array.«term__[:_]»}

{docstring Array.«term__[_:]»}

{docstring Array.«term__[_:_]»}

{docstring Array.«term_~_»}


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

BaseIO
```exceptions
```

Bind
```exceptions
```

Bool
Bool.toInt
{docstring Bool.toInt}


```exceptions
Bool.toInt
```

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

{docstring Char.isValidCharNat}

{docstring Char.isValue}

{docstring Char.le}

{docstring Char.lt}

{docstring Char.notLTAntisymm}

{docstring Char.notLTTotal}

{docstring Char.notLTTrans}

{docstring Char.ofNat}

{docstring Char.ofNatAux}

{docstring Char.ofUInt8}

{docstring Char.quote}

{docstring Char.quoteCore}

{docstring Char.quoteCore.smallCharToHex}

{docstring Char.reduceBEq}

{docstring Char.reduceBNe}

{docstring Char.reduceBinPred}

{docstring Char.reduceBoolPred}

{docstring Char.reduceDefault}

{docstring Char.reduceEq}

{docstring Char.reduceGE}

{docstring Char.reduceGT}

{docstring Char.reduceIsAlpha}

{docstring Char.reduceIsAlphaNum}

{docstring Char.reduceIsDigit}

{docstring Char.reduceIsLower}

{docstring Char.reduceIsUpper}

{docstring Char.reduceIsWhitespace}

{docstring Char.reduceLE}

{docstring Char.reduceLT}

{docstring Char.reduceNe}

{docstring Char.reduceOfNatAux}

{docstring Char.reduceToLower}

{docstring Char.reduceToNat}

{docstring Char.reduceToString}

{docstring Char.reduceToUpper}

{docstring Char.reduceUnary}

{docstring Char.reduceVal}

{docstring Char.repr}

{docstring Char.toLower}

{docstring Char.toNat}

{docstring Char.toString}

{docstring Char.toUInt8}

{docstring Char.toUpper}

{docstring Char.utf16Size}

{docstring Char.utf8Size}


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

Decidable
```exceptions
```

EIO
```exceptions
```

EStateM
```exceptions
```

EStateM.Backtrackable
```exceptions
```

EStateM.Result
```exceptions
```

Except
```exceptions
```

ExceptCpsT
```exceptions
```

ExceptT
```exceptions
```

Fin
```exceptions
```

ForIn
```exceptions
```

ForIn'
```exceptions
```

ForInStep
ForInStep.value
{docstring ForInStep.value}


```exceptions
ForInStep.value
```

ForM
```exceptions
```

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

{docstring Function.const}

{docstring Function.curry}

{docstring Function.uncurry}


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

Functor
```exceptions
```

IO
IO.getTID
{docstring IO.getTID}


```exceptions
IO.getTID
```

IO.Error
```exceptions
```

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

{docstring IO.FS.withTempDir}


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

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

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

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

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

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

IO.FileRight
```exceptions
```

IO.Process
```exceptions
```

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

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

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

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

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

IO.Ref
```exceptions
```

ISize
```exceptions
```

Id
```exceptions
```

Int16
```exceptions
```

Int32
```exceptions
```

Int64
```exceptions
```

Int8
```exceptions
```

LawfulApplicative
```exceptions
```

LawfulFunctor
```exceptions
```

LawfulMonad
```exceptions
```

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

{docstring Lean.Elab.Tactic.checkCommandConfigElab}

{docstring Lean.Elab.Tactic.checkConfigElab}

{docstring Lean.Elab.Tactic.classical}

{docstring Lean.Elab.Tactic.closeUsingOrAdmit}

{docstring Lean.Elab.Tactic.commandConfigElab}

{docstring Lean.Elab.Tactic.configElab}

{docstring Lean.Elab.Tactic.deltaLocalDecl}

{docstring Lean.Elab.Tactic.deltaTarget}

{docstring Lean.Elab.Tactic.done}

{docstring Lean.Elab.Tactic.dsimpLocation}

{docstring Lean.Elab.Tactic.elabAsFVar}

{docstring Lean.Elab.Tactic.elabChange}

{docstring Lean.Elab.Tactic.elabDecideConfig}

{docstring Lean.Elab.Tactic.elabGrindConfig}

{docstring Lean.Elab.Tactic.elabGrindPattern}

{docstring Lean.Elab.Tactic.elabRewriteConfig}

{docstring Lean.Elab.Tactic.elabSimpArgs.toZetaDeltaSet}

{docstring Lean.Elab.Tactic.elabSimpConfigCore}

{docstring Lean.Elab.Tactic.elabTermForApply}

{docstring Lean.Elab.Tactic.evalApplyRfl}

{docstring Lean.Elab.Tactic.evalClassical}

{docstring Lean.Elab.Tactic.evalDecideCore}

{docstring Lean.Elab.Tactic.evalDecideCore.diagnose}

{docstring Lean.Elab.Tactic.evalDecideCore.doElab}

{docstring Lean.Elab.Tactic.evalDecideCore.doKernel}

{docstring Lean.Elab.Tactic.expandLocation}

{docstring Lean.Elab.Tactic.expandOptLocation}

{docstring Lean.Elab.Tactic.filterOldMVars}

{docstring Lean.Elab.Tactic.focusAndDone}

{docstring Lean.Elab.Tactic.forEachVar}

{docstring Lean.Elab.Tactic.getInductiveValFromMajor}

{docstring Lean.Elab.Tactic.getMainDecl}

{docstring Lean.Elab.Tactic.getMainTarget}

{docstring Lean.Elab.Tactic.getNameOfIdent'}

{docstring Lean.Elab.Tactic.grind}

{docstring Lean.Elab.Tactic.isCheckpointableTactic}

{docstring Lean.Elab.Tactic.isHoleRHS}

{docstring Lean.Elab.Tactic.liftMetaFinishingTactic}

{docstring Lean.Elab.Tactic.liftMetaTactic}

{docstring Lean.Elab.Tactic.liftMetaTactic1}

{docstring Lean.Elab.Tactic.logUnassignedAndAbort}

{docstring Lean.Elab.Tactic.mkInitialTacticInfo}

{docstring Lean.Elab.Tactic.mkSimpCallStx}

{docstring Lean.Elab.Tactic.mkSimpContext}

{docstring Lean.Elab.Tactic.mkSimpOnly}

{docstring Lean.Elab.Tactic.mkTacticInfo}

{docstring Lean.Elab.Tactic.popMainGoal}

{docstring Lean.Elab.Tactic.pushGoal}

{docstring Lean.Elab.Tactic.pushGoals}

{docstring Lean.Elab.Tactic.refineCore}

{docstring Lean.Elab.Tactic.renameInaccessibles}

{docstring Lean.Elab.Tactic.replaceMainGoal}

{docstring Lean.Elab.Tactic.rewriteLocalDecl}

{docstring Lean.Elab.Tactic.rewriteTarget}

{docstring Lean.Elab.Tactic.saveState}

{docstring Lean.Elab.Tactic.saveTacticInfoForToken}

{docstring Lean.Elab.Tactic.simpLocation}

{docstring Lean.Elab.Tactic.simpOnlyBuiltins}

{docstring Lean.Elab.Tactic.tactic.customEliminators}

{docstring Lean.Elab.Tactic.tacticToDischarge}

{docstring Lean.Elab.Tactic.throwNoGoalsToBeSolved}

{docstring Lean.Elab.Tactic.traceSimpCall}

{docstring Lean.Elab.Tactic.tryCatchRestore}

{docstring Lean.Elab.Tactic.unfoldLocalDecl}

{docstring Lean.Elab.Tactic.unfoldTarget}

{docstring Lean.Elab.Tactic.withCaseRef}

{docstring Lean.Elab.Tactic.withCollectingNewGoalsFrom}

{docstring Lean.Elab.Tactic.withMacroExpansion}

{docstring Lean.Elab.Tactic.withMainContext}

{docstring Lean.Elab.Tactic.withRWRulesSeq}

{docstring Lean.Elab.Tactic.withRestoreOrSaveFull}

{docstring Lean.Elab.Tactic.withSimpDiagnostics}

{docstring Lean.Elab.Tactic.withTacticInfoContext}

{docstring Lean.Elab.Tactic.withoutRecover}

{docstring Lean.Elab.Tactic.zetaDeltaLocalDecl}

{docstring Lean.Elab.Tactic.zetaDeltaTarget}


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

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

{docstring List.allM}

{docstring List.and}

{docstring List.any}

{docstring List.anyM}

{docstring List.append}

{docstring List.appendTR}

{docstring List.asString}

{docstring List.attach}

{docstring List.attachWith}

{docstring List.beq}

{docstring List.concat}

{docstring List.contains}

{docstring List.count}

{docstring List.countP}

{docstring List.countP.go}

{docstring List.drop}

{docstring List.dropLast}

{docstring List.dropLastTR}

{docstring List.dropWhile}

{docstring List.elem}

{docstring List.enum}

{docstring List.enumFrom}

{docstring List.enumFromTR}

{docstring List.enumLE}

{docstring List.erase}

{docstring List.eraseDups}

{docstring List.eraseDups.loop}

{docstring List.eraseIdx}

{docstring List.eraseIdxTR}

{docstring List.eraseIdxTR.go}

{docstring List.eraseP}

{docstring List.erasePTR}

{docstring List.erasePTR.go}

{docstring List.eraseReps}

{docstring List.eraseReps.loop}

{docstring List.eraseTR}

{docstring List.eraseTR.go}

{docstring List.filter}

{docstring List.filterAuxM}

{docstring List.filterM}

{docstring List.filterMap}

{docstring List.filterMapM}

{docstring List.filterMapM.loop}

{docstring List.filterMapTR}

{docstring List.filterMapTR.go}

{docstring List.filterRevM}

{docstring List.filterTR}

{docstring List.filterTR.loop}

{docstring List.finRange}

{docstring List.find?}

{docstring List.findIdx}

{docstring List.findIdx.go}

{docstring List.findIdx?}

{docstring List.findM?}

{docstring List.findSome?}

{docstring List.findSomeM?}

{docstring List.firstM}

{docstring List.flatMap}

{docstring List.flatMapTR}

{docstring List.flatMapTR.go}

{docstring List.flatten}

{docstring List.flattenTR}

{docstring List.foldl}

{docstring List.foldlM}

{docstring List.foldlRecOn}

{docstring List.foldr}

{docstring List.foldrM}

{docstring List.foldrRecOn}

{docstring List.foldrTR}

{docstring List.forA}

{docstring List.forIn'}

{docstring List.forIn'.loop}

{docstring List.forM}

{docstring List.format}

{docstring List.get}

{docstring List.get!}

{docstring List.get?}

{docstring List.getD}

{docstring List.getLast}

{docstring List.getLast!}

{docstring List.getLast?}

{docstring List.getLastD}

{docstring List.groupByKey}

{docstring List.hasDecEq}

{docstring List.head}

{docstring List.head!}

{docstring List.head?}

{docstring List.headD}

{docstring List.indexOf}

{docstring List.indexOf?}

{docstring List.insert}

{docstring List.insertIdx}

{docstring List.insertIdxTR}

{docstring List.insertIdxTR.go}

{docstring List.intercalate}

{docstring List.intercalateTR}

{docstring List.intercalateTR.go}

{docstring List.intersperse}

{docstring List.intersperseTR}

{docstring List.iota}

{docstring List.iotaTR}

{docstring List.iotaTR.go}

{docstring List.isEmpty}

{docstring List.isEqv}

{docstring List.isPerm}

{docstring List.isPrefixOf}

{docstring List.isPrefixOf?}

{docstring List.isSublist}

{docstring List.isSuffixOf}

{docstring List.isSuffixOf?}

{docstring List.le}

{docstring List.leftpad}

{docstring List.leftpadTR}

{docstring List.length}

{docstring List.lengthTR}

{docstring List.lengthTRAux}

{docstring List.lex}

{docstring List.lookup}

{docstring List.lt}

{docstring List.map}

{docstring List.mapA}

{docstring List.mapFinIdx}

{docstring List.mapFinIdx.go}

{docstring List.mapIdx}

{docstring List.mapIdx.go}

{docstring List.mapM}

{docstring List.mapM'}

{docstring List.mapM.loop}

{docstring List.mapMono}

{docstring List.mapMonoM}

{docstring List.mapTR}

{docstring List.mapTR.loop}

{docstring List.max?}

{docstring List.maxNatAbs}

{docstring List.merge}

{docstring List.mergeSort}

{docstring List.min?}

{docstring List.minNatAbs}

{docstring List.modify}

{docstring List.modifyHead}

{docstring List.modifyTR}

{docstring List.modifyTR.go}

{docstring List.modifyTailIdx}

{docstring List.nonzeroMinimum}

{docstring List.ofFn}

{docstring List.or}

{docstring List.partition}

{docstring List.partition.loop}

{docstring List.partitionM}

{docstring List.partitionM.go}

{docstring List.partitionMap}

{docstring List.partitionMap.go}

{docstring List.pmap}

{docstring List.range}

{docstring List.range'}

{docstring List.range'TR}

{docstring List.range'TR.go}

{docstring List.range.loop}

{docstring List.reduceOption}

{docstring List.reduceReplicate}

{docstring List.removeAll}

{docstring List.replace}

{docstring List.replaceTR}

{docstring List.replaceTR.go}

{docstring List.replicate}

{docstring List.replicateTR}

{docstring List.replicateTR.loop}

{docstring List.repr}

{docstring List.repr'}

{docstring List.reverse}

{docstring List.reverseAux}

{docstring List.rightpad}

{docstring List.rotateLeft}

{docstring List.rotateRight}

{docstring List.set}

{docstring List.setTR}

{docstring List.setTR.go}

{docstring List.singleton}

{docstring List.span}

{docstring List.span.loop}

{docstring List.splitAt}

{docstring List.splitAt.go}

{docstring List.splitBy}

{docstring List.splitBy.loop}

{docstring List.sum}

{docstring List.tail}

{docstring List.tail!}

{docstring List.tail?}

{docstring List.tailD}

{docstring List.take}

{docstring List.takeTR}

{docstring List.takeTR.go}

{docstring List.takeWhile}

{docstring List.takeWhileTR}

{docstring List.takeWhileTR.go}

{docstring List.toArray}

{docstring List.toArrayAux}

{docstring List.toArrayImpl}

{docstring List.toAssocList'}

{docstring List.toByteArray}

{docstring List.toByteArray.loop}

{docstring List.toFloatArray}

{docstring List.toFloatArray.loop}

{docstring List.toPArray'}

{docstring List.toPArray'.loop}

{docstring List.toSMap}

{docstring List.toSSet}

{docstring List.toString}

{docstring List.unattach}

{docstring List.unzip}

{docstring List.unzipTR}

{docstring List.zip}

{docstring List.zipWith}

{docstring List.zipWithAll}

{docstring List.zipWithTR}

{docstring List.zipWithTR.go}

{docstring List.«term_<+:_»}

{docstring List.«term_<+_»}

{docstring List.«term_<:+:_»}

{docstring List.«term_<:+_»}

{docstring List.«term_~_»}


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

Monad
```exceptions
```

MonadControl
```exceptions
```

MonadControlT
```exceptions
```

MonadExcept
```exceptions
```

MonadExceptOf
```exceptions
```

MonadFunctor
```exceptions
```

MonadFunctorT
```exceptions
```

MonadLift
```exceptions
```

MonadLiftT
```exceptions
```

MonadReader
```exceptions
```

MonadReaderOf
```exceptions
```

MonadState
```exceptions
```

MonadStateOf
```exceptions
```

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

{docstring Nat.reduceAnd}

{docstring Nat.reduceOr}

{docstring Nat.reduceShiftLeft}

{docstring Nat.reduceShiftRight}

{docstring Nat.reduceXor}

{docstring Nat.strongRecOn}

{docstring Nat.toFloat32}

{docstring Nat.toISize}

{docstring Nat.toInt16}

{docstring Nat.toInt32}

{docstring Nat.toInt64}

{docstring Nat.toInt8}


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

Option
```exceptions
```

OptionT
```exceptions
```

PLift
```exceptions
```

PUnit
```exceptions
```

Pure
```exceptions
```

ReaderM
```exceptions
```

ReaderT
```exceptions
```

ST
```exceptions
```

ST.Ref
```exceptions
```

Seq
```exceptions
```

SeqLeft
```exceptions
```

SeqRight
```exceptions
```

StateCpsT
```exceptions
```

StateM
```exceptions
```

StateRefT'
```exceptions
```

StateT
```exceptions
```

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

{docstring String.dropSuffix?}

{docstring String.stripPrefix}

{docstring String.stripSuffix}


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

Subarray
```exceptions
```

Subtype
```exceptions
```

System
```exceptions
```

System.FilePath
```exceptions
```

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

{docstring System.Platform.getIsOSX}

{docstring System.Platform.getIsWindows}

{docstring System.Platform.getNumBits}

{docstring System.Platform.getTarget}

{docstring System.Platform.isEmscripten}

{docstring System.Platform.isOSX}

{docstring System.Platform.isWindows}

{docstring System.Platform.numBits}

{docstring System.Platform.target}


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

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

{docstring Task.map}


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

Task.Priority
```exceptions
```

UInt16
```exceptions
```

UInt32
```exceptions
```

UInt64
```exceptions
```

UInt8
```exceptions
```

ULift
```exceptions
```

USize
```exceptions
```

Unit
```exceptions
```

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

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