Index

Symbols

  1. ( ... )
  2. . ...
  3. <;> (0) (1)
  4. _private.Init.Dynamic.0.TypeName.data
  5. { ... }
  6. ·
  7. · ...
  8. ι-reduction

A

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

B

  1. BEq
  2. BEq.beq
  3. Base­IO
  4. BaseIO.as­Task
  5. BaseIO.bind­Task
  6. BaseIO.map­Task
  7. BaseIO.map­Tasks
  8. BaseIO.to­EIO
  9. BaseIO.to­IO
  10. Bool
  11. Bool.false
    1. Constructor of Bool
  12. Bool.true
    1. Constructor of Bool
  13. Buffer
    1. IO.FS.Stream.Buffer
  14. back
    1. Array.back
    2. String.back
  15. back!
    1. Array.back!
  16. back?
    1. Array.back?
  17. backward.synthInstance.canon­Instances
  18. below
    1. Nat.below
  19. beq
    1. BEq.beq (class method)
    2. Nat.beq
  20. beta
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
    2. Lean.Meta.Simp.Config.arith (structure field)
  21. bin­Insert
    1. Array.bin­Insert
  22. bin­Insert­M
    1. Array.bin­Insert­M
  23. bin­Search
    1. Array.bin­Search
  24. bin­Search­Contains
    1. Array.bin­Search­Contains
  25. bind­Task
    1. BaseIO.bind­Task
    2. EIO.bind­Task
    3. IO.bind­Task
  26. bitwise
    1. Nat.bitwise
  27. ble
    1. Nat.ble
  28. blt
    1. Nat.blt
  29. bootstrap.inductive­Check­Resulting­Universe
  30. bv_check
  31. bv_decide
  32. bv_decide?
  33. bv_normalize
  34. bv_omega
  35. by_cases
  36. byte­Idx
    1. String.Pos.byte­Idx (structure field)
  37. byte­Size
    1. IO.FS.Metadata.byte­Size (structure field)

C

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

D

  1. Decidable
  2. Decidable.is­False
    1. Constructor of Decidable
  3. Decidable.is­True
    1. Constructor of Decidable
  4. Decidable­Eq
  5. Decidable­Rel
  6. Dir­Entry
    1. IO.FS.Dir­Entry
  7. Div
  8. Div.div
  9. Dvd
  10. Dvd.dvd
  11. Dynamic
  12. Dynamic.get?
  13. Dynamic.mk
  14. data
    1. IO.FS.Stream.Buffer.data
    2. IO.FS.Stream.Buffer.pos (structure field)
    3. String.data (structure field)
    4. _private.Init.Dynamic.0.TypeName.data (class method)
  15. dbg_cache
    1. tactic.dbg_cache
  16. dbg_trace
  17. dec­Eq
    1. Nat.dec­Eq
    2. String.dec­Eq
  18. dec­Le
    1. Nat.dec­Le
  19. dec­Lt
    1. Nat.dec­Lt
  20. decapitalize
    1. String.decapitalize
  21. decide
    1. Lean.Meta.DSimp.Config.zeta (structure field)
    2. Lean.Meta.Simp.Config.zeta (structure field)
  22. decreasing_tactic
  23. decreasing_trivial
  24. decreasing_with
  25. dedicated
    1. Task.Priority.dedicated
  26. deep­Terms
    1. pp.deep­Terms
  27. default
    1. Inhabited.default (class method)
    2. Task.Priority.default
  28. delta (0) (1)
  29. digit­Char
    1. Nat.digit­Char
  30. discharge
    1. trace.Meta.Tactic.simp.discharge
  31. div
    1. Div.div (class method)
    2. Nat.div
  32. div2Induction
    1. Nat.div2Induction
  33. done (0) (1)
  34. drop
    1. String.drop
    2. Subarray.drop
  35. drop­Right
    1. String.drop­Right
  36. drop­Right­While
    1. String.drop­Right­While
  37. drop­While
    1. String.drop­While
  38. dsimp (0) (1)
    1. Lean.Meta.Simp.Config.max­Discharge­Depth (structure field)
  39. dsimp!
  40. dsimp?
  41. dsimp?!
  42. dsimp­Location'
    1. Lean.Elab.Tactic.dsimp­Location'
  43. 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. Error
    1. IO.Error
  12. Even
  13. Even.plus­Two
    1. Constructor of Even
  14. Even.zero
    1. Constructor of Even
  15. elab­Cases­Targets
    1. Lean.Elab.Tactic.elab­Cases­Targets
  16. elab­DSimp­Config­Core
    1. Lean.Elab.Tactic.elab­DSimp­Config­Core
  17. elab­Simp­Args
    1. Lean.Elab.Tactic.elab­Simp­Args
  18. elab­Simp­Config
    1. Lean.Elab.Tactic.elab­Simp­Config
  19. elab­Simp­Config­Ctx­Core
    1. Lean.Elab.Tactic.elab­Simp­Config­Ctx­Core
  20. elab­Term
    1. Lean.Elab.Tactic.elab­Term
  21. elab­Term­Ensuring­Type
    1. Lean.Elab.Tactic.elab­Term­Ensuring­Type
  22. elab­Term­With­Holes
    1. Lean.Elab.Tactic.elab­Term­With­Holes
  23. elem
    1. Array.elem
  24. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  25. elim­Offset
    1. Nat.elim­Offset
  26. empty
    1. Array.empty
    2. Subarray.empty
  27. end­Pos
    1. String.end­Pos
  28. ends­With
    1. String.ends­With
  29. ensure­Has­No­MVars
    1. Lean.Elab.Tactic.ensure­Has­No­MVars
  30. enter
  31. env
    1. IO.Process.SpawnArgs.args (structure field)
  32. eprint
    1. IO.eprint
  33. eprintln
    1. IO.eprintln
  34. eq_of_beq
    1. LawfulBEq.eq_of_beq (class method)
  35. eq_refl
  36. erase
    1. Array.erase
  37. erase­Idx
    1. Array.erase­Idx
  38. erase­Reps
    1. Array.erase­Reps
  39. erw (0) (1)
  40. eta
    1. Lean.Meta.DSimp.Config.index (structure field)
    2. Lean.Meta.Simp.Config.max­Steps (structure field)
  41. eta­Struct
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  42. exact
  43. exact?
  44. exact_mod_cast
  45. exe­Extension
    1. System.FilePath.exe­Extension
  46. exfalso
  47. exists
  48. exit
    1. IO.Process.exit
  49. exit­Code
    1. IO.Process.Output.stderr (structure field)
  50. expand­Macro?
    1. Lean.Macro.expand­Macro?
  51. ext (0) (1)
  52. ext1
  53. ext­Separator
    1. System.FilePath.ext­Separator
  54. extension
    1. System.FilePath.extension
  55. extensionality
    1. of propositions
  56. 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. fail
  4. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
    2. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  5. fail_if_success (0) (1)
  6. false_or_by_contra
  7. field­Idx­Kind
    1. Lean.field­Idx­Kind
  8. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
    2. System.FilePath.file­Name
  9. file­Stem
    1. System.FilePath.file­Stem
  10. filter
    1. Array.filter
  11. filter­M
    1. Array.filter­M
  12. filter­Map
    1. Array.filter­Map
  13. filter­Map­M
    1. Array.filter­Map­M
  14. filter­Pairs­M
    1. Array.filter­Pairs­M
  15. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  16. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  17. find
    1. String.find
  18. find?
    1. Array.find?
  19. find­Idx?
    1. Array.find­Idx?
  20. find­Idx­M?
    1. Array.find­Idx­M?
  21. find­Line­Start
    1. String.find­Line­Start
  22. find­M?
    1. Array.find­M?
  23. find­Rev?
    1. Array.find­Rev?
    2. Subarray.find­Rev?
  24. find­Rev­M?
    1. Array.find­Rev­M?
    2. Subarray.find­Rev­M?
  25. find­Some!
    1. Array.find­Some!
  26. find­Some?
    1. Array.find­Some?
  27. find­Some­M?
    1. Array.find­Some­M?
  28. find­Some­Rev?
    1. Array.find­Some­Rev?
  29. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
    2. Subarray.find­Some­Rev­M?
  30. first (0) (1)
  31. first­Diff­Pos
    1. String.first­Diff­Pos
  32. flags
    1. IO.FileRight.flags
  33. flat­Map
    1. Array.flat­Map
  34. flat­Map­M
    1. Array.flat­Map­M
  35. flatten
    1. Array.flatten
  36. flush
    1. IO.FS.Handle.flush
    2. IO.FS.Stream.flush (structure field)
  37. focus (0) (1)
    1. Lean.Elab.Tactic.focus
  38. fold
    1. Nat.fold
  39. fold­M
    1. Nat.fold­M
  40. fold­Rev
    1. Nat.fold­Rev
  41. fold­Rev­M
    1. Nat.fold­Rev­M
  42. fold­TR
    1. Nat.fold­TR
  43. foldl
    1. Array.foldl
    2. String.foldl
    3. Subarray.foldl
  44. foldl­M
    1. Array.foldl­M
    2. Subarray.foldl­M
  45. foldr
    1. Array.foldr
    2. String.foldr
    3. Subarray.foldr
  46. foldr­M
    1. Array.foldr­M
    2. Subarray.foldr­M
  47. fopen­Error­To­String
    1. IO.Error.fopen­Error­To­String
  48. for­In
    1. Subarray.for­In
  49. for­In'
    1. Array.for­In'
  50. for­M
    1. Array.for­M
    2. Nat.for­M
    3. Subarray.for­M
  51. for­Rev­M
    1. Array.for­Rev­M
    2. Nat.for­Rev­M
    3. Subarray.for­Rev­M
  52. forward
    1. String.Iterator.forward
  53. from­Expr?
    1. Nat.from­Expr?
    2. String.from­Expr?
  54. from­UTF8
    1. String.from­UTF8
  55. from­UTF8!
    1. String.from­UTF8!
  56. from­UTF8?
    1. String.from­UTF8?
  57. front
    1. String.front
  58. fun
  59. funext (0) (1)

G

  1. Get­Elem
  2. GetElem.get­Elem
  3. Get­Elem?
  4. GetElem?.get­Elem!
  5. GetElem?.get­Elem?
  6. GetElem?.to­Get­Elem
  7. gcd
    1. Nat.gcd
  8. generalize
  9. get
    1. Array.get
    2. ST.Ref.get
    3. String.get
    4. Subarray.get
    5. Task.get
    6. Task.get (structure field)
  10. get!
    1. Array.get!
    2. String.get!
    3. Subarray.get!
  11. get'
    1. String.get'
  12. get?
    1. Array.get?
    2. Dynamic.get?
    3. String.get?
  13. get­Char
    1. Lean.TSyntax.get­Char
  14. get­Curr­Macro­Scope
    1. Lean.Elab.Tactic.get­Curr­Macro­Scope
  15. get­Curr­Namespace
    1. Lean.Macro.get­Curr­Namespace
  16. get­Current­Dir
    1. IO.Process.get­Current­Dir
  17. get­D
    1. Array.get­D
    2. Subarray.get­D
  18. get­Elem
    1. GetElem.get­Elem (class method)
  19. get­Elem!
    1. GetElem?.get­Elem! (class method)
  20. get­Elem!_def
    1. Lawful­GetElem.get­Elem?_def (class method)
  21. get­Elem?
    1. GetElem?.get­Elem? (class method)
  22. get­Elem?_def
    1. Lawful­GetElem.get­Elem!_def (class method)
  23. get­Env
    1. IO.get­Env
  24. get­Even­Elems
    1. Array.get­Even­Elems
  25. get­FVar­Id
    1. Lean.Elab.Tactic.get­FVar­Id
  26. get­FVar­Ids
    1. Lean.Elab.Tactic.get­FVar­Ids
  27. get­Goals
    1. Lean.Elab.Tactic.get­Goals
  28. get­Hygiene­Info
    1. Lean.TSyntax.get­Hygiene­Info
  29. get­Id
    1. Lean.TSyntax.get­Id
  30. get­Idx?
    1. Array.get­Idx?
  31. get­Kind
    1. Lean.Syntax.get­Kind
  32. get­Line
    1. IO.FS.Handle.get­Line
    2. IO.FS.Stream.write (structure field)
  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­Name
    1. Lean.TSyntax.get­Name
  38. get­Nat
    1. Lean.TSyntax.get­Nat
  39. get­Num­Heartbeats
    1. IO.get­Num­Heartbeats
  40. get­PID
    1. IO.Process.get­PID
  41. get­Random­Bytes
    1. IO.get­Random­Bytes
  42. get­Scientific
    1. Lean.TSyntax.get­Scientific
  43. get­Stderr
    1. IO.get­Stderr
  44. get­Stdin
    1. IO.get­Stdin
  45. get­Stdout
    1. IO.get­Stdout
  46. get­String
    1. Lean.TSyntax.get­String
  47. get­Task­State
    1. IO.get­Task­State
  48. get­Unsolved­Goals
    1. Lean.Elab.Tactic.get­Unsolved­Goals
  49. get­Utf8Byte
    1. String.get­Utf8Byte
  50. get_elem_tactic
  51. get_elem_tactic_trivial
  52. goal
    1. main
  53. ground
    1. Lean.Meta.Simp.Config.auto­Unfold (structure field)
  54. group
    1. IO.FileRight.other (structure field)
  55. group­By­Key
    1. Array.group­By­Key
  56. group­Kind
    1. Lean.group­Kind
  57. guard_expr
  58. guard_hyp
  59. guard_target

H

  1. HAdd
  2. HAdd.h­Add
  3. HAnd
  4. HAnd.h­And
  5. HAppend
  6. HAppend.h­Append
  7. HDiv
  8. HDiv.h­Div
  9. HMod
  10. HMod.h­Mod
  11. HMul
  12. HMul.h­Mul
  13. HOr
  14. HOr.h­Or
  15. HPow
  16. HPow.h­Pow
  17. HShift­Left
  18. HShiftLeft.h­Shift­Left
  19. HShift­Right
  20. HShiftRight.h­Shift­Right
  21. HSub
  22. HSub.h­Sub
  23. HXor
  24. HXor.h­Xor
  25. Handle
    1. IO.FS.Handle
  26. Hashable
  27. Hashable.hash
  28. Homogeneous­Pow
  29. HomogeneousPow.pow
  30. Hygiene­Info
    1. Lean.Syntax.Hygiene­Info
  31. h
    1. ST.Ref.ref (structure field)
  32. h­Add
    1. HAdd.h­Add (class method)
  33. h­And
    1. HAnd.h­And (class method)
  34. h­Append
    1. HAppend.h­Append (class method)
  35. h­Div
    1. HDiv.h­Div (class method)
  36. h­Mod
    1. HMod.h­Mod (class method)
  37. h­Mul
    1. HMul.h­Mul (class method)
  38. h­Or
    1. HOr.h­Or (class method)
  39. h­Pow
    1. HPow.h­Pow (class method)
  40. h­Shift­Left
    1. HShiftLeft.h­Shift­Left (class method)
  41. h­Shift­Right
    1. HShiftRight.h­Shift­Right (class method)
  42. h­Sub
    1. HSub.h­Sub (class method)
  43. h­Xor
    1. HXor.h­Xor (class method)
  44. has­Decl
    1. Lean.Macro.has­Decl
  45. has­Finished
    1. IO.has­Finished
  46. has­Next
    1. String.Iterator.has­Next
  47. has­Prev
    1. String.Iterator.has­Prev
  48. hash
    1. Hashable.hash (class method)
    2. String.hash
  49. have
  50. have'
  51. have­I
  52. hygiene
    1. in tactics
  53. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  54. 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. Ident
    1. Lean.Syntax.Ident
  173. Inhabited
  174. Inhabited.default
  175. Iterator
    1. String.Iterator
  176. i
    1. String.Iterator.s (structure field)
  177. ibelow
    1. Nat.ibelow
  178. ident­Kind
    1. Lean.ident­Kind
  179. identifier
    1. raw
  180. if ... then ... else ...
  181. if h : ... then ... else ...
  182. imax
    1. Nat.imax
  183. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  184. impredicative
  185. inaccessible
  186. index
    1. Lean.Meta.DSimp.Config.unfold­Partial­App (structure field)
    2. Lean.Meta.Simp.Config.unfold­Partial­App (structure field)
    3. of inductive type
  187. index­Of?
    1. Array.index­Of?
  188. indexed family
    1. of types
  189. induction
  190. induction­On
    1. Nat.div.induction­On
    2. Nat.mod.induction­On
  191. inductive.auto­Promote­Indices
  192. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  193. infer­Instance
  194. infer­Instance­As
  195. infer_instance
  196. injection
  197. injections
  198. insert­At
    1. Array.insert­At
  199. insert­At!
    1. Array.insert­At!
  200. insertion­Sort
    1. Array.insertion­Sort
  201. instance synthesis
  202. intercalate
    1. String.intercalate
  203. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  204. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  205. intro (0) (1)
  206. intro | ... => ... | ... => ...
  207. intros
  208. iota
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  209. is­Absolute
    1. System.FilePath.is­Absolute
  210. is­Alpha
    1. Char.is­Alpha
  211. is­Alphanum
    1. Char.is­Alphanum
  212. is­Digit
    1. Char.is­Digit
  213. is­Dir
    1. System.FilePath.is­Dir
  214. is­Empty
    1. Array.is­Empty
    2. String.is­Empty
  215. is­Eqv
    1. Array.is­Eqv
  216. is­Int
    1. String.is­Int
  217. is­Lower
    1. Char.is­Lower
  218. is­Nat
    1. String.is­Nat
  219. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  220. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  221. is­Prefix­Of
    1. Array.is­Prefix­Of
    2. String.is­Prefix­Of
  222. is­Relative
    1. System.FilePath.is­Relative
  223. is­Tty
    1. IO.FS.Handle.is­Tty
    2. IO.FS.Stream.get­Line (structure field)
  224. is­Upper
    1. Char.is­Upper
  225. is­Valid
    1. String.Pos.is­Valid
  226. is­Valid­Char
    1. Nat.is­Valid­Char
  227. is­Value
    1. Nat.is­Value
  228. is­Whitespace
    1. Char.is­Whitespace
  229. iter
    1. String.iter
  230. iterate
    1. IO.iterate

J

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

K

  1. kill
    1. IO.Process.Child.kill

L

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

M

  1. Macro­M
    1. Lean.Macro­M
  2. Metadata
    1. IO.FS.Metadata
  3. Mod
  4. Mod.mod
  5. Mode
    1. IO.FS.Mode
  6. Mul
  7. Mul.mul
  8. main goal
  9. map
    1. Array.map
    2. String.map
  10. map­Fin­Idx
    1. Array.map­Fin­Idx
  11. map­Fin­Idx­M
    1. Array.map­Fin­Idx­M
  12. map­Idx
    1. Array.map­Idx
  13. map­Idx­M
    1. Array.map­Idx­M
  14. map­Indexed
    1. Array.map­Indexed
  15. map­Indexed­M
    1. Array.map­Indexed­M
  16. map­M
    1. Array.map­M
  17. map­M'
    1. Array.map­M'
  18. map­Mono
    1. Array.map­Mono
  19. map­Mono­M
    1. Array.map­Mono­M
  20. map­Task
    1. BaseIO.map­Task
    2. EIO.map­Task
    3. IO.map­Task
  21. map­Tasks
    1. BaseIO.map­Tasks
    2. EIO.map­Tasks
    3. IO.map­Tasks
  22. match
    1. pp.match
  23. max
    1. Nat.max
    2. Task.Priority.max
  24. max­Discharge­Depth
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  25. max­Heartbeats
    1. synthInstance.max­Heartbeats
  26. max­Size
    1. synthInstance.max­Size
  27. max­Steps
    1. Lean.Meta.Simp.Config.zeta­Delta (structure field)
    2. pp.max­Steps
  28. memoize
    1. Lean.Meta.Simp.Config.index (structure field)
  29. metadata
    1. System.FilePath.metadata
  30. min
    1. Nat.min
    2. String.Pos.min
  31. mk
    1. Dynamic.mk
    2. IO.FS.Handle.mk
  32. mk­Already­Exists
    1. IO.Error.mk­Already­Exists
  33. mk­Already­Exists­File
    1. IO.Error.mk­Already­Exists­File
  34. mk­Array
    1. Array.mk­Array
  35. mk­Eof­Error
    1. IO.Error.mk­Eof­Error
  36. mk­File­Path
    1. System.mk­File­Path
  37. mk­Hardware­Fault
    1. IO.Error.mk­Hardware­Fault
  38. mk­Illegal­Operation
    1. IO.Error.mk­Illegal­Operation
  39. mk­Inappropriate­Type
    1. IO.Error.mk­Inappropriate­Type
  40. mk­Inappropriate­Type­File
    1. IO.Error.mk­Inappropriate­Type­File
  41. mk­Interrupted
    1. IO.Error.mk­Interrupted
  42. mk­Invalid­Argument
    1. IO.Error.mk­Invalid­Argument
  43. mk­Invalid­Argument­File
    1. IO.Error.mk­Invalid­Argument­File
  44. mk­Iterator
    1. String.mk­Iterator
  45. mk­No­File­Or­Directory
    1. IO.Error.mk­No­File­Or­Directory
  46. mk­No­Such­Thing
    1. IO.Error.mk­No­Such­Thing
  47. mk­No­Such­Thing­File
    1. IO.Error.mk­No­Such­Thing­File
  48. mk­Other­Error
    1. IO.Error.mk­Other­Error
  49. mk­Permission­Denied
    1. IO.Error.mk­Permission­Denied
  50. mk­Permission­Denied­File
    1. IO.Error.mk­Permission­Denied­File
  51. mk­Protocol­Error
    1. IO.Error.mk­Protocol­Error
  52. mk­Ref
    1. IO.mk­Ref
    2. ST.mk­Ref
  53. mk­Resource­Busy
    1. IO.Error.mk­Resource­Busy
  54. mk­Resource­Exhausted
    1. IO.Error.mk­Resource­Exhausted
  55. mk­Resource­Exhausted­File
    1. IO.Error.mk­Resource­Exhausted­File
  56. mk­Resource­Vanished
    1. IO.Error.mk­Resource­Vanished
  57. mk­Std­Gen
  58. mk­Tactic­Attribute
    1. Lean.Elab.Tactic.mk­Tactic­Attribute
  59. mk­Time­Expired
    1. IO.Error.mk­Time­Expired
  60. mk­Unsatisfied­Constraints
    1. IO.Error.mk­Unsatisfied­Constraints
  61. mk­Unsupported­Operation
    1. IO.Error.mk­Unsupported­Operation
  62. mod
    1. Mod.mod (class method)
    2. Nat.mod
  63. mod­Core
    1. Nat.mod­Core
  64. modified
    1. IO.FS.Metadata.type (structure field)
  65. modify
    1. Array.modify
    2. ST.Ref.modify
    3. String.modify
  66. modify­Get
    1. ST.Ref.modify­Get
  67. modify­M
    1. Array.modify­M
  68. modify­Op
    1. Array.modify­Op
  69. mono­Ms­Now
    1. IO.mono­Ms­Now
  70. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  71. mul
    1. Mul.mul (class method)
    2. Nat.mul
  72. 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.nat­Cast
  115. Nat­Pow
  116. NatPow.pow
  117. Ne­Zero
  118. NeZero.out
  119. Neg
  120. Neg.neg
  121. New­Goals
    1. Lean.Meta.Rewrite.New­Goals
  122. Nonempty
  123. Nonempty.intro
    1. Constructor of Nonempty
  124. Num­Lit
    1. Lean.Syntax.Num­Lit
  125. name­Lit­Kind
    1. Lean.name­Lit­Kind
  126. namespace
    1. of inductive type
  127. nat­Cast
    1. NatCast.nat­Cast (class method)
  128. native_decide
  129. neg
    1. Neg.neg (class method)
  130. neutral­Config
    1. Lean.Meta.Simp.neutral­Config
  131. new­Goals
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  132. next
    1. RandomGen.range (class method)
    2. String.Iterator.next
    3. String.next
  133. next ... => ...
  134. next'
    1. String.next'
  135. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  136. next­Until
    1. String.next­Until
  137. next­While
    1. String.next­While
  138. nextn
    1. String.Iterator.nextn
  139. no­Confusion
    1. Nat.no­Confusion
  140. no­Confusion­Type
    1. Nat.no­Confusion­Type
  141. nofun
  142. nomatch
  143. norm_cast (0) (1)
  144. normalize
    1. System.FilePath.normalize
  145. null­Kind
    1. Lean.null­Kind
  146. num­Lit­Kind
    1. Lean.num­Lit­Kind

O

  1. Occurrences
    1. Lean.Meta.Occurrences
  2. Option
  3. Option.none
    1. Constructor of Option
  4. Option.some
    1. Constructor of Option
  5. Ord
  6. Ord.compare
  7. Output
    1. IO.Process.Output
  8. obtain
  9. occs
    1. Lean.Meta.Rewrite.Config.new­Goals (structure field)
  10. of­Buffer
    1. IO.FS.Stream.of­Buffer
  11. of­Except
    1. IO.of­Except
  12. of­Fn
    1. Array.of­Fn
  13. of­Handle
    1. IO.FS.Stream.of­Handle
  14. of­Subarray
    1. Array.of­Subarray
  15. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  16. offset­Of­Pos
    1. String.offset­Of­Pos
  17. omega
  18. open
  19. or­Else
    1. Lean.Elab.Tactic.or­Else
  20. other
    1. IO.FileRight.user (structure field)
  21. other­Error­To­String
    1. IO.Error.other­Error­To­String
  22. out
    1. NeZero.out (class method)
  23. out­Param
  24. output
    1. IO.Process.output

P

  1. PUnit
  2. PUnit.unit
    1. Constructor of PUnit
  3. Pos
    1. String.Pos
  4. Pow
  5. Pow.pow
  6. Prec
    1. Lean.Syntax.Prec
  7. Preresolved
    1. Lean.Syntax.Preresolved
  8. Prio
    1. Lean.Syntax.Prio
  9. Priority
    1. Task.Priority
  10. Prop
  11. parameter
    1. of inductive type
  12. parent
    1. System.FilePath.parent
  13. parser
  14. partition
    1. Array.partition
  15. path
    1. IO.FS.DirEntry.path
  16. path­Exists
    1. System.FilePath.path­Exists
  17. path­Separator
    1. System.FilePath.path­Separator
  18. path­Separators
    1. System.FilePath.path­Separators
  19. pattern
  20. polymorphism
    1. universe
  21. pop
    1. Array.pop
  22. pop­Front
    1. Subarray.pop­Front
  23. pop­While
    1. Array.pop­While
  24. pos
    1. IO.FS.Stream.Buffer.data (structure field)
    2. IO.FS.Stream.Buffer.pos
    3. String.Iterator.pos
  25. pos­Of
    1. String.pos­Of
  26. pow
    1. HomogeneousPow.pow (class method)
    2. Nat.pow
    3. NatPow.pow (class method)
    4. Pow.pow (class method)
  27. pp.deep­Terms
  28. pp.deepTerms.threshold
  29. pp.match
  30. pp.max­Steps
  31. pp.mvars
  32. pp.proofs
  33. pp.proofs.threshold
  34. pred
    1. Nat.pred
  35. predicative
  36. prev
    1. String.Iterator.prev
    2. String.prev
  37. prevn
    1. String.Iterator.prevn
  38. print
    1. IO.print
  39. println
    1. IO.println
  40. proj
    1. Lean.Meta.DSimp.Config.iota (structure field)
    2. Lean.Meta.Simp.Config.memoize (structure field)
  41. proof state
  42. proofs
    1. pp.proofs
  43. propext
  44. proposition
  45. prune­Solved­Goals
    1. Lean.Elab.Tactic.prune­Solved­Goals
  46. ptr­Eq
    1. ST.Ref.ptr­Eq
  47. push
    1. Array.push
    2. String.push
  48. push_cast
  49. pushn
    1. String.pushn
  50. put­Str
    1. IO.FS.Handle.put­Str
    2. IO.FS.Stream.read (structure field)
  51. 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.next
  3. RandomGen.range
  4. RandomGen.split
  5. Ref
    1. IO.Ref
    2. ST.Ref
  6. Repr
  7. Repr.repr­Prec
  8. rand
    1. IO.rand
  9. rand­Bool
  10. rand­Nat
  11. range
    1. Array.range
    2. RandomGen.next (class method)
  12. raw
    1. Lean.TSyntax.raw (structure field)
  13. rcases
  14. read
    1. IO.FS.Handle.read
    2. IO.FS.Stream.is­Tty (structure field)
  15. read­Bin­File
    1. IO.FS.read­Bin­File
  16. read­Bin­To­End
    1. IO.FS.Handle.read­Bin­To­End
  17. read­Bin­To­End­Into
    1. IO.FS.Handle.read­Bin­To­End­Into
  18. read­Dir
    1. System.FilePath.read­Dir
  19. read­File
    1. IO.FS.read­File
  20. read­To­End
    1. IO.FS.Handle.read­To­End
  21. real­Path
    1. IO.FS.real­Path
  22. rec
    1. Nat.rec
  23. rec­On
    1. Nat.rec­On
  24. recursor
  25. reduce
  26. reduce­Add
    1. Nat.reduce­Add
  27. reduce­Append
    1. String.reduce­Append
  28. reduce­BEq
    1. Nat.reduce­BEq
    2. String.reduce­BEq
  29. reduce­BNe
    1. Nat.reduce­BNe
    2. String.reduce­BNe
  30. reduce­Beq­Diff
    1. Nat.reduce­Beq­Diff
  31. reduce­Bin
    1. Nat.reduce­Bin
  32. reduce­Bin­Pred
    1. Nat.reduce­Bin­Pred
    2. String.reduce­Bin­Pred
  33. reduce­Bne­Diff
    1. Nat.reduce­Bne­Diff
  34. reduce­Bool­Pred
    1. Nat.reduce­Bool­Pred
    2. String.reduce­Bool­Pred
  35. reduce­Div
    1. Nat.reduce­Div
  36. reduce­Eq
    1. String.reduce­Eq
  37. reduce­Eq­Diff
    1. Nat.reduce­Eq­Diff
  38. reduce­GE
    1. String.reduce­GE
  39. reduce­GT
    1. Nat.reduce­GT
    2. String.reduce­GT
  40. reduce­Gcd
    1. Nat.reduce­Gcd
  41. reduce­Get­Elem
    1. Array.reduce­Get­Elem
  42. reduce­Get­Elem!
    1. Array.reduce­Get­Elem!
  43. reduce­Get­Elem?
    1. Array.reduce­Get­Elem?
  44. reduce­LE
    1. String.reduce­LE
  45. reduce­LT
    1. Nat.reduce­LT
    2. String.reduce­LT
  46. reduce­LTLE
    1. Nat.reduce­LTLE
  47. reduce­Le­Diff
    1. Nat.reduce­Le­Diff
  48. reduce­Mk
    1. String.reduce­Mk
  49. reduce­Mod
    1. Nat.reduce­Mod
  50. reduce­Mul
    1. Nat.reduce­Mul
  51. reduce­Nat­Eq­Expr
    1. Nat.reduce­Nat­Eq­Expr
  52. reduce­Ne
    1. String.reduce­Ne
  53. reduce­Option
    1. Array.reduce­Option
  54. reduce­Pow
    1. Nat.reduce­Pow
  55. reduce­Sub
    1. Nat.reduce­Sub
  56. reduce­Sub­Diff
    1. Nat.reduce­Sub­Diff
  57. reduce­Succ
    1. Nat.reduce­Succ
  58. reduce­Unary
    1. Nat.reduce­Unary
  59. reduction
    1. ι (iota)
  60. ref
    1. ST.Ref.h (structure field)
  61. refine
  62. refine'
  63. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  64. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  65. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  66. remaining­To­String
    1. String.Iterator.remaining­To­String
  67. remove­Dir
    1. IO.FS.remove­Dir
  68. remove­Dir­All
    1. IO.FS.remove­Dir­All
  69. remove­File
    1. IO.FS.remove­File
  70. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  71. rename
    1. IO.FS.rename
  72. rename_i
  73. repeat (0) (1)
    1. Nat.repeat
  74. repeat'
  75. repeat1'
  76. repeat­TR
    1. Nat.repeat­TR
  77. replace
    1. String.replace
  78. repr
    1. Nat.repr
  79. repr­Prec
    1. Repr.repr­Prec (class method)
  80. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  81. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  82. rev­Find
    1. String.rev­Find
  83. rev­Pos­Of
    1. String.rev­Pos­Of
  84. reverse
    1. Array.reverse
  85. revert
  86. rewind
    1. IO.FS.Handle.rewind
  87. rewrite (0) (1)
    1. trace.Meta.Tactic.simp.rewrite
  88. rfl (0) (1)
    1. LawfulBEq.rfl (class method)
  89. rfl'
  90. rhs
  91. right (0) (1)
  92. rintro
  93. root
    1. IO.FS.DirEntry.root (structure field)
  94. rotate_left
  95. rotate_right
  96. run
    1. IO.Process.run
    2. Lean.Elab.Tactic.run
  97. run­EST
  98. run­ST
  99. run­Term­Elab
    1. Lean.Elab.Tactic.run­Term­Elab
  100. run_tac
  101. rw (0) (1)
  102. rw?
  103. rw_mod_cast
  104. 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. Scientific­Lit
    1. Lean.Syntax.Scientific­Lit
  14. Shift­Left
  15. ShiftLeft.shift­Left
  16. Shift­Right
  17. ShiftRight.shift­Right
  18. Simp­Extension
    1. Lean.Meta.Simp­Extension
  19. Size­Of
  20. SizeOf.size­Of
  21. Sort
  22. Source­Info
    1. Lean.Source­Info
  23. Spawn­Args
    1. IO.Process.Spawn­Args
  24. Std­Gen
  25. StdGen.mk
    1. Constructor of Std­Gen
  26. Stdio
    1. IO.Process.Stdio
  27. Stdio­Config
    1. IO.Process.Stdio­Config
  28. Str­Lit
    1. Lean.Syntax.Str­Lit
  29. Stream
    1. IO.FS.Stream
  30. String
  31. String.Iterator
  32. String.Iterator.at­End
  33. String.Iterator.curr
  34. String.Iterator.extract
  35. String.Iterator.forward
  36. String.Iterator.has­Next
  37. String.Iterator.has­Prev
  38. String.Iterator.mk
    1. Constructor of String.Iterator
  39. String.Iterator.next
  40. String.Iterator.nextn
  41. String.Iterator.pos
  42. String.Iterator.prev
  43. String.Iterator.prevn
  44. String.Iterator.remaining­Bytes
  45. String.Iterator.remaining­To­String
  46. String.Iterator.set­Curr
  47. String.Iterator.to­End
  48. String.Pos
  49. String.Pos.is­Valid
  50. String.Pos.min
  51. String.Pos.mk
    1. Constructor of String.Pos
  52. String.all
  53. String.any
  54. String.append
  55. String.at­End
  56. String.back
  57. String.capitalize
  58. String.codepoint­Pos­To­Utf16Pos
  59. String.codepoint­Pos­To­Utf16Pos­From
  60. String.codepoint­Pos­To­Utf8Pos­From
  61. String.contains
  62. String.crlf­To­Lf
  63. String.csize
  64. String.dec­Eq
  65. String.decapitalize
  66. String.drop
  67. String.drop­Right
  68. String.drop­Right­While
  69. String.drop­While
  70. String.end­Pos
  71. String.ends­With
  72. String.extract
  73. String.find
  74. String.find­Line­Start
  75. String.first­Diff­Pos
  76. String.foldl
  77. String.foldr
  78. String.from­Expr?
  79. String.from­UTF8
  80. String.from­UTF8!
  81. String.from­UTF8?
  82. String.front
  83. String.get
  84. String.get!
  85. String.get'
  86. String.get?
  87. String.get­Utf8Byte
  88. String.hash
  89. String.intercalate
  90. String.is­Empty
  91. String.is­Int
  92. String.is­Nat
  93. String.is­Prefix­Of
  94. String.iter
  95. String.join
  96. String.le
  97. String.length
  98. String.map
  99. String.mk
    1. Constructor of String
  100. String.mk­Iterator
  101. String.modify
  102. String.next
  103. String.next'
  104. String.next­Until
  105. String.next­While
  106. String.offset­Of­Pos
  107. String.pos­Of
  108. String.prev
  109. String.push
  110. String.pushn
  111. String.quote
  112. String.reduce­Append
  113. String.reduce­BEq
  114. String.reduce­BNe
  115. String.reduce­Bin­Pred
  116. String.reduce­Bool­Pred
  117. String.reduce­Eq
  118. String.reduce­GE
  119. String.reduce­GT
  120. String.reduce­LE
  121. String.reduce­LT
  122. String.reduce­Mk
  123. String.reduce­Ne
  124. String.remove­Leading­Spaces
  125. String.replace
  126. String.rev­Find
  127. String.rev­Pos­Of
  128. String.set
  129. String.singleton
  130. String.split
  131. String.split­On
  132. String.starts­With
  133. String.substr­Eq
  134. String.take
  135. String.take­Right
  136. String.take­Right­While
  137. String.take­While
  138. String.to­File­Map
  139. String.to­Format
  140. String.to­Int!
  141. String.to­Int?
  142. String.to­List
  143. String.to­Lower
  144. String.to­Name
  145. String.to­Nat!
  146. String.to­Nat?
  147. String.to­Substring
  148. String.to­Substring'
  149. String.to­UTF8
  150. String.to­Upper
  151. String.trim
  152. String.trim­Left
  153. String.trim­Right
  154. String.utf16Length
  155. String.utf16Pos­To­Codepoint­Pos
  156. String.utf16Pos­To­Codepoint­Pos­From
  157. String.utf8Byte­Size
  158. String.utf8Decode­Char?
  159. String.utf8Encode­Char
  160. String.validate­UTF8
  161. Sub
  162. Sub.sub
  163. Subarray
  164. Subarray.all
  165. Subarray.all­M
  166. Subarray.any
  167. Subarray.any­M
  168. Subarray.drop
  169. Subarray.empty
  170. Subarray.find­Rev?
  171. Subarray.find­Rev­M?
  172. Subarray.find­Some­Rev­M?
  173. Subarray.foldl
  174. Subarray.foldl­M
  175. Subarray.foldr
  176. Subarray.foldr­M
  177. Subarray.for­In
  178. Subarray.for­M
  179. Subarray.for­Rev­M
  180. Subarray.get
  181. Subarray.get!
  182. Subarray.get­D
  183. Subarray.mk
    1. Constructor of Subarray
  184. Subarray.pop­Front
  185. Subarray.size
  186. Subarray.split
  187. Subarray.take
  188. Subarray.to­Array
  189. Syntax
    1. Lean.Syntax
  190. Syntax­Node­Kind
    1. Lean.Syntax­Node­Kind
  191. System.File­Path
  192. System.FilePath.add­Extension
  193. System.FilePath.components
  194. System.FilePath.exe­Extension
  195. System.FilePath.ext­Separator
  196. System.FilePath.extension
  197. System.FilePath.file­Name
  198. System.FilePath.file­Stem
  199. System.FilePath.is­Absolute
  200. System.FilePath.is­Dir
  201. System.FilePath.is­Relative
  202. System.FilePath.join
  203. System.FilePath.metadata
  204. System.FilePath.mk
    1. Constructor of System.File­Path
  205. System.FilePath.normalize
  206. System.FilePath.parent
  207. System.FilePath.path­Exists
  208. System.FilePath.path­Separator
  209. System.FilePath.path­Separators
  210. System.FilePath.read­Dir
  211. System.FilePath.walk­Dir
  212. System.FilePath.with­Extension
  213. System.FilePath.with­File­Name
  214. System.mk­File­Path
  215. s
    1. String.Iterator.i (structure field)
  216. s1
    1. StdGen.s2 (structure field)
  217. s2
    1. StdGen.s1 (structure field)
  218. save
  219. scientific­Lit­Kind
    1. Lean.scientific­Lit­Kind
  220. semi­Out­Param
  221. sequence­Map
    1. Array.sequence­Map
  222. set
    1. Array.set
    2. ST.Ref.set
    3. String.set
  223. set!
    1. Array.set!
  224. set­Access­Rights
    1. IO.set­Access­Rights
  225. set­Curr
    1. String.Iterator.set­Curr
  226. set­Current­Dir
    1. IO.Process.set­Current­Dir
  227. set­D
    1. Array.set­D
  228. set­Goals
    1. Lean.Elab.Tactic.set­Goals
  229. set­Kind
    1. Lean.Syntax.set­Kind
  230. set­Rand­Seed
    1. IO.set­Rand­Seed
  231. set­Stderr
    1. IO.set­Stderr
  232. set­Stdin
    1. IO.set­Stdin
  233. set­Stdout
    1. IO.set­Stdout
  234. set_option
  235. setsid
    1. IO.Process.SpawnArgs.setsid (structure field)
  236. shift­Left
    1. Nat.shift­Left
    2. ShiftLeft.shift­Left (class method)
  237. shift­Right
    1. Nat.shift­Right
    2. ShiftRight.shift­Right (class method)
  238. show
  239. show_term
  240. simp (0) (1)
  241. simp!
  242. simp?
  243. simp?!
  244. simp_all
  245. simp_all!
  246. simp_all?
  247. simp_all?!
  248. simp_all_arith
  249. simp_all_arith!
  250. simp_arith
  251. simp_arith!
  252. simp_match
  253. simp_wf
  254. simpa
  255. simpa!
  256. simpa?
  257. simpa?!
  258. simprocs
  259. single­Pass
    1. Lean.Meta.Simp.Config.single­Pass (structure field)
  260. singleton
    1. Array.singleton
    2. String.singleton
  261. size
    1. Array.size
    2. Subarray.size
  262. size­Of
    1. SizeOf.size­Of (class method)
  263. skip (0) (1)
  264. skip­Assigned­Instances
    1. tactic.skip­Assigned­Instances
  265. sleep
    1. IO.sleep
  266. solve
  267. solve_by_elim
  268. sorry
  269. sort­MVar­Id­Array­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  270. sort­MVar­Ids­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  271. spawn
    1. IO.Process.spawn
    2. Task.spawn
  272. specialize
  273. split
    1. Array.split
    2. RandomGen.split (class method)
    3. String.split
    4. Subarray.split
  274. split­On
    1. String.split­On
  275. start
    1. Subarray.stop (structure field)
  276. start_le_stop
    1. Subarray.stop_le_array_size (structure field)
  277. starts­With
    1. String.starts­With
  278. std­Next
  279. std­Range
  280. std­Split
  281. stderr
    1. IO.Process.Child.stdin (structure field)
    2. IO.Process.Output.exit­Code (structure field)
    3. IO.Process.StdioConfig.stdin (structure field)
  282. stdin
    1. IO.Process.Child.stderr (structure field)
    2. IO.Process.StdioConfig.stderr (structure field)
  283. stdout
    1. IO.Process.Child.stdout (structure field)
    2. IO.Process.Output.stdout (structure field)
    3. IO.Process.StdioConfig.stdout (structure field)
  284. stop
    1. Subarray.start (structure field)
  285. stop_le_array_size
    1. Subarray.array (structure field)
  286. str­Lit­Kind
    1. Lean.str­Lit­Kind
  287. strong­Induction­On
    1. Nat.strong­Induction­On
  288. sub
    1. Nat.sub
    2. Sub.sub (class method)
  289. sub­Digit­Char
    1. Nat.sub­Digit­Char
  290. subst
  291. subst_eqs
  292. subst_vars
  293. substr­Eq
    1. String.substr­Eq
  294. suffices
  295. super­Digit­Char
    1. Nat.super­Digit­Char
  296. swap
    1. Array.swap
    2. ST.Ref.swap
  297. swap!
    1. Array.swap!
  298. swap­At
    1. Array.swap­At
  299. swap­At!
    1. Array.swap­At!
  300. symm
  301. symm_saturate
  302. synthInstance.max­Heartbeats
  303. synthInstance.max­Size
  304. 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.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. test­Bit
    1. Nat.test­Bit
  35. threshold
    1. pp.deepTerms.threshold
    2. pp.proofs.threshold
  36. throw­Error
    1. Lean.Macro.throw­Error
  37. throw­Error­At
    1. Lean.Macro.throw­Error­At
  38. throw­Unsupported
    1. Lean.Macro.throw­Unsupported
  39. to­Array
    1. Subarray.to­Array
  40. to­Base­IO
    1. EIO.to­Base­IO
  41. to­Digits
    1. Nat.to­Digits
  42. to­Digits­Core
    1. Nat.to­Digits­Core
  43. to­EIO
    1. BaseIO.to­EIO
    2. IO.to­EIO
  44. to­End
    1. String.Iterator.to­End
  45. to­File­Map
    1. String.to­File­Map
  46. to­Float
    1. Nat.to­Float
  47. to­Format
    1. String.to­Format
  48. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  49. to­Handle­Type
    1. IO.Process.Stdio.to­Handle­Type
  50. to­IO
    1. BaseIO.to­IO
    2. EIO.to­IO
  51. to­IO'
    1. EIO.to­IO'
  52. to­Int!
    1. String.to­Int!
  53. to­Int?
    1. String.to­Int?
  54. to­Level
    1. Nat.to­Level
  55. to­List
    1. Array.to­List
    2. Array.to­List (structure field)
    3. String.to­List
  56. to­List­Append
    1. Array.to­List­Append
  57. to­List­Rev
    1. Array.to­List­Rev
  58. to­Lower
    1. String.to­Lower
  59. to­Monad­State­Of
    1. ST.Ref.to­Monad­State­Of
  60. to­Name
    1. String.to­Name
  61. to­Nat!
    1. String.to­Nat!
  62. to­Nat?
    1. String.to­Nat?
  63. to­PArray'
    1. Array.to­PArray'
  64. to­Stdio­Config
    1. IO.Process.SpawnArgs.to­Stdio­Config (structure field)
  65. to­String
    1. IO.Error.to­String
    2. System.FilePath.to­String (structure field)
    3. ToString.to­String (class method)
  66. to­Sub­Digits
    1. Nat.to­Sub­Digits
  67. to­Subarray
    1. Array.to­Subarray
  68. to­Subscript­String
    1. Nat.to­Subscript­String
  69. to­Substring
    1. String.to­Substring
  70. to­Substring'
    1. String.to­Substring'
  71. to­Super­Digits
    1. Nat.to­Super­Digits
  72. to­Superscript­String
    1. Nat.to­Superscript­String
  73. to­UInt16
    1. Nat.to­UInt16
  74. to­UInt32
    1. Nat.to­UInt32
  75. to­UInt64
    1. Nat.to­UInt64
  76. to­UInt8
    1. Nat.to­UInt8
  77. to­USize
    1. Nat.to­USize
  78. to­UTF8
    1. String.to­UTF8
  79. to­Upper
    1. String.to­Upper
  80. trace
    1. Lean.Macro.trace
    2. tactic.simp.trace (0) (1)
  81. trace.Meta.Tactic.simp.discharge
  82. trace.Meta.Tactic.simp.rewrite
  83. trace_state (0) (1)
  84. transparency
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  85. trim
    1. String.trim
  86. trim­Left
    1. String.trim­Left
  87. trim­Right
    1. String.trim­Right
  88. trivial
  89. truncate
    1. IO.FS.Handle.truncate
  90. try (0) (1)
  91. try­Catch
    1. Lean.Elab.Tactic.try­Catch
  92. try­Lock
    1. IO.FS.Handle.try­Lock
  93. try­Tactic
    1. Lean.Elab.Tactic.try­Tactic
  94. try­Tactic?
    1. Lean.Elab.Tactic.try­Tactic?
  95. try­Wait
    1. IO.Process.Child.try­Wait
  96. type
    1. IO.FS.Metadata.accessed (structure field)
  97. type constructor

U

  1. Unit
  2. Unit.unit
  3. uget
    1. Array.uget
  4. unattach
    1. Array.unattach
  5. unfold (0) (1)
  6. unfold­Partial­App
    1. Lean.Meta.DSimp.Config.beta (structure field)
    2. Lean.Meta.Simp.Config.beta (structure field)
  7. unhygienic
  8. unit
    1. Unit.unit
  9. universe
  10. universe polymorphism
  11. unlock
    1. IO.FS.Handle.unlock
  12. unnecessary­Simpa
    1. linter.unnecessary­Simpa
  13. unsupported­Syntax
    1. Lean.Macro.Exception.unsupported­Syntax
  14. unzip
    1. Array.unzip
  15. user
    1. IO.FileRight.group (structure field)
  16. user­Error
    1. IO.user­Error
  17. uset
    1. Array.uset
  18. usize
    1. Array.usize
  19. utf16Length
    1. String.utf16Length
  20. utf16Pos­To­Codepoint­Pos
    1. String.utf16Pos­To­Codepoint­Pos
  21. utf16Pos­To­Codepoint­Pos­From
    1. String.utf16Pos­To­Codepoint­Pos­From
  22. utf8Byte­Size
    1. String.utf8Byte­Size
  23. utf8Decode­Char?
    1. String.utf8Decode­Char?
  24. utf8Encode­Char
    1. String.utf8Encode­Char

V

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

W

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

X

  1. xor
    1. Nat.xor

Z

  1. Zero
  2. Zero.zero
  3. zero
    1. Zero.zero (class method)
  4. zeta
    1. Lean.Meta.DSimp.Config.zeta­Delta (structure field)
    2. Lean.Meta.Simp.Config.eta (structure field)
  5. zeta­Delta
    1. Lean.Meta.DSimp.Config.proj (structure field)
    2. Lean.Meta.Simp.Config.proj (structure field)
  6. zip
    1. Array.zip
  7. zip­With
    1. Array.zip­With
  8. zip­With­Index
    1. Array.zip­With­Index