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
    1. Bool.and
  144. and_intros
  145. any
    1. Array.any
    2. Nat.any
    3. String.any
    4. Subarray.any
  146. any­M
    1. Array.any­M
    2. Nat.any­M
    3. Subarray.any­M
  147. any­TR
    1. Nat.any­TR
  148. any_goals (0) (1)
  149. app­Dir
    1. IO.app­Dir
  150. app­Path
    1. IO.app­Path
  151. append
    1. Append.append (class method)
    2. Array.append
    3. String.append
  152. append­Goals
    1. Lean.Elab.Tactic.append­Goals
  153. append­List
    1. Array.append­List
  154. apply (0) (1)
  155. apply?
  156. apply­Eq­Lemma
    1. Nat.apply­Eq­Lemma
  157. apply­Simproc­Const
    1. Nat.apply­Simproc­Const
  158. apply_assumption
  159. apply_ext_theorem
  160. apply_mod_cast
  161. apply_rfl
  162. apply_rules
  163. arg [@]i
  164. args
    1. IO.Process.SpawnArgs.cwd (structure field)
  165. arith
    1. Lean.Meta.Simp.Config.ground (structure field)
  166. array
    1. Subarray.start_le_stop (structure field)
  167. array_get_dec
  168. as­Task
    1. BaseIO.as­Task
    2. EIO.as­Task
    3. IO.as­Task
  169. assumption
    1. inaccessible
  170. assumption_mod_cast
  171. at­End
    1. String.Iterator.at­End
    2. String.at­End
  172. at­Least­Two
    1. Bool.at­Least­Two
  173. attach
    1. Array.attach
  174. attach­With
    1. Array.attach­With
  175. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  176. 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.and
  12. Bool.at­Least­Two
  13. Bool.dec­Eq
  14. Bool.false
    1. Constructor of Bool
  15. Bool.not
  16. Bool.or
  17. Bool.to­ISize
  18. Bool.to­Int16
  19. Bool.to­Int32
  20. Bool.to­Int64
  21. Bool.to­Int8
  22. Bool.to­Nat
  23. Bool.to­UInt16
  24. Bool.to­UInt32
  25. Bool.to­UInt64
  26. Bool.to­UInt8
  27. Bool.to­USize
  28. Bool.true
    1. Constructor of Bool
  29. Bool.xor
  30. Buffer
    1. IO.FS.Stream.Buffer
  31. back
    1. Array.back
    2. String.back
  32. back!
    1. Array.back!
  33. back?
    1. Array.back?
  34. backward.synthInstance.canon­Instances
  35. below
    1. Nat.below
  36. beq
    1. BEq.beq (class method)
    2. Nat.beq
  37. beta
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
    2. Lean.Meta.Simp.Config.arith (structure field)
  38. bin­Insert
    1. Array.bin­Insert
  39. bin­Insert­M
    1. Array.bin­Insert­M
  40. bin­Search
    1. Array.bin­Search
  41. bin­Search­Contains
    1. Array.bin­Search­Contains
  42. bind­Task
    1. BaseIO.bind­Task
    2. EIO.bind­Task
    3. IO.bind­Task
  43. bitwise
    1. Nat.bitwise
  44. ble
    1. Nat.ble
  45. blt
    1. Nat.blt
  46. bootstrap.inductive­Check­Resulting­Universe
  47. bv_check
  48. bv_decide
  49. bv_decide?
  50. bv_normalize
  51. bv_omega
  52. by­Cases
    1. Decidable.by­Cases
  53. by_cases
  54. byte­Idx
    1. String.Pos.byte­Idx (structure field)
  55. 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. cond
  48. configuration
    1. of tactics
  49. congr (0) (1)
  50. constructor (0) (1)
  51. contains
    1. Array.contains
    2. String.contains
  52. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  53. contradiction
  54. conv
  55. conv => ...
  56. conv' (0) (1)
  57. create­Dir
    1. IO.FS.create­Dir
  58. create­Dir­All
    1. IO.FS.create­Dir­All
  59. create­Temp­File
    1. IO.FS.create­Temp­File
  60. crlf­To­Lf
    1. String.crlf­To­Lf
  61. csize
    1. String.csize
  62. cumulativity
  63. curr
    1. String.Iterator.curr
  64. current­Dir
    1. IO.current­Dir
  65. custom­Eliminators
    1. tactic.custom­Eliminators
  66. cwd
    1. IO.Process.SpawnArgs.cmd (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.div
  11. Dvd
  12. Dvd.dvd
  13. Dynamic
  14. Dynamic.get?
  15. Dynamic.mk
  16. 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)
  17. dbg_cache
    1. tactic.dbg_cache
  18. dbg_trace
  19. dec­Eq
    1. Bool.dec­Eq
    2. Nat.dec­Eq
    3. String.dec­Eq
  20. dec­Le
    1. Nat.dec­Le
  21. dec­Lt
    1. Nat.dec­Lt
  22. decapitalize
    1. String.decapitalize
  23. decidable
  24. decide
    1. Decidable.decide
    2. Lean.Meta.DSimp.Config.zeta (structure field)
    3. Lean.Meta.Simp.Config.zeta (structure field)
  25. decreasing_tactic
  26. decreasing_trivial
  27. decreasing_with
  28. dedicated
    1. Task.Priority.dedicated
  29. deep­Terms
    1. pp.deep­Terms
  30. default
    1. Inhabited.default (class method)
    2. Task.Priority.default
  31. delta (0) (1)
  32. digit­Char
    1. Nat.digit­Char
  33. discharge
    1. trace.Meta.Tactic.simp.discharge
  34. div
    1. Div.div (class method)
    2. Nat.div
  35. div2Induction
    1. Nat.div2Induction
  36. done (0) (1)
  37. down
    1. PLift.down (structure field)
    2. ULift.down (structure field)
  38. drop
    1. String.drop
    2. Subarray.drop
  39. drop­Right
    1. String.drop­Right
  40. drop­Right­While
    1. String.drop­Right­While
  41. drop­While
    1. String.drop­While
  42. dsimp (0) (1)
    1. Lean.Meta.Simp.Config.max­Discharge­Depth (structure field)
  43. dsimp!
  44. dsimp?
  45. dsimp?!
  46. dsimp­Location'
    1. Lean.Elab.Tactic.dsimp­Location'
  47. 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. Empty
  12. Error
    1. IO.Error
  13. Even
  14. Even.plus­Two
    1. Constructor of Even
  15. Even.zero
    1. Constructor of Even
  16. elab­Cases­Targets
    1. Lean.Elab.Tactic.elab­Cases­Targets
  17. elab­DSimp­Config­Core
    1. Lean.Elab.Tactic.elab­DSimp­Config­Core
  18. elab­Simp­Args
    1. Lean.Elab.Tactic.elab­Simp­Args
  19. elab­Simp­Config
    1. Lean.Elab.Tactic.elab­Simp­Config
  20. elab­Simp­Config­Ctx­Core
    1. Lean.Elab.Tactic.elab­Simp­Config­Ctx­Core
  21. elab­Term
    1. Lean.Elab.Tactic.elab­Term
  22. elab­Term­Ensuring­Type
    1. Lean.Elab.Tactic.elab­Term­Ensuring­Type
  23. elab­Term­With­Holes
    1. Lean.Elab.Tactic.elab­Term­With­Holes
  24. elem
    1. Array.elem
  25. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  26. elim­Offset
    1. Nat.elim­Offset
  27. empty
    1. Array.empty
    2. Subarray.empty
  28. end­Pos
    1. String.end­Pos
  29. ends­With
    1. String.ends­With
  30. ensure­Has­No­MVars
    1. Lean.Elab.Tactic.ensure­Has­No­MVars
  31. enter
  32. env
    1. IO.Process.SpawnArgs.args (structure field)
  33. eprint
    1. IO.eprint
  34. eprintln
    1. IO.eprintln
  35. eq_of_beq
    1. LawfulBEq.eq_of_beq (class method)
  36. eq_refl
  37. erase
    1. Array.erase
  38. erase­Idx
    1. Array.erase­Idx
  39. erase­Reps
    1. Array.erase­Reps
  40. erw (0) (1)
  41. eta
    1. Lean.Meta.DSimp.Config.index (structure field)
    2. Lean.Meta.Simp.Config.max­Steps (structure field)
  42. eta­Struct
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  43. exact
  44. exact?
  45. exact_mod_cast
  46. exe­Extension
    1. System.FilePath.exe­Extension
  47. exfalso
  48. exists
  49. exit
    1. IO.Process.exit
  50. exit­Code
    1. IO.Process.Output.stderr (structure field)
  51. expand­Macro?
    1. Lean.Macro.expand­Macro?
  52. ext (0) (1)
  53. ext1
  54. ext­Separator
    1. System.FilePath.ext­Separator
  55. extension
    1. System.FilePath.extension
  56. extensionality
    1. of propositions
  57. extract
    1. Array.extract
    2. String.Iterator.extract
    3. String.extract

F

  1. File­Path
    1. System.File­Path
  2. File­Right
    1. IO.File­Right
  3. Fin
  4. Fin.mk
    1. Constructor of Fin
  5. fail
  6. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
    2. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  7. fail_if_success (0) (1)
  8. false_or_by_contra
  9. field­Idx­Kind
    1. Lean.field­Idx­Kind
  10. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
    2. System.FilePath.file­Name
  11. file­Stem
    1. System.FilePath.file­Stem
  12. filter
    1. Array.filter
  13. filter­M
    1. Array.filter­M
  14. filter­Map
    1. Array.filter­Map
  15. filter­Map­M
    1. Array.filter­Map­M
  16. filter­Pairs­M
    1. Array.filter­Pairs­M
  17. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  18. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  19. find
    1. String.find
  20. find?
    1. Array.find?
  21. find­Idx?
    1. Array.find­Idx?
  22. find­Idx­M?
    1. Array.find­Idx­M?
  23. find­Line­Start
    1. String.find­Line­Start
  24. find­M?
    1. Array.find­M?
  25. find­Rev?
    1. Array.find­Rev?
    2. Subarray.find­Rev?
  26. find­Rev­M?
    1. Array.find­Rev­M?
    2. Subarray.find­Rev­M?
  27. find­Some!
    1. Array.find­Some!
  28. find­Some?
    1. Array.find­Some?
  29. find­Some­M?
    1. Array.find­Some­M?
  30. find­Some­Rev?
    1. Array.find­Some­Rev?
  31. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
    2. Subarray.find­Some­Rev­M?
  32. first (0) (1)
  33. first­Diff­Pos
    1. String.first­Diff­Pos
  34. flags
    1. IO.FileRight.flags
  35. flat­Map
    1. Array.flat­Map
  36. flat­Map­M
    1. Array.flat­Map­M
  37. flatten
    1. Array.flatten
  38. flush
    1. IO.FS.Handle.flush
    2. IO.FS.Stream.flush (structure field)
  39. focus (0) (1)
    1. Lean.Elab.Tactic.focus
  40. fold
    1. Nat.fold
  41. fold­M
    1. Nat.fold­M
  42. fold­Rev
    1. Nat.fold­Rev
  43. fold­Rev­M
    1. Nat.fold­Rev­M
  44. fold­TR
    1. Nat.fold­TR
  45. foldl
    1. Array.foldl
    2. String.foldl
    3. Subarray.foldl
  46. foldl­M
    1. Array.foldl­M
    2. Subarray.foldl­M
  47. foldr
    1. Array.foldr
    2. String.foldr
    3. Subarray.foldr
  48. foldr­M
    1. Array.foldr­M
    2. Subarray.foldr­M
  49. fopen­Error­To­String
    1. IO.Error.fopen­Error­To­String
  50. for­In
    1. Subarray.for­In
  51. for­In'
    1. Array.for­In'
  52. for­M
    1. Array.for­M
    2. Nat.for­M
    3. Subarray.for­M
  53. for­Rev­M
    1. Array.for­Rev­M
    2. Nat.for­Rev­M
    3. Subarray.for­Rev­M
  54. forward
    1. String.Iterator.forward
  55. from­Expr?
    1. Nat.from­Expr?
    2. String.from­Expr?
  56. from­UTF8
    1. String.from­UTF8
  57. from­UTF8!
    1. String.from­UTF8!
  58. from­UTF8?
    1. String.from­UTF8?
  59. front
    1. String.front
  60. fst
    1. MProd.snd (structure field)
    2. PProd.snd (structure field)
    3. Prod.snd (structure field)
  61. fun
  62. 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. Int
  176. Int.neg­Succ
    1. Constructor of Int
  177. Int.of­Nat
    1. Constructor of Int
  178. Int16
  179. Int16.mk
    1. Constructor of Int16
  180. Int32
  181. Int32.mk
    1. Constructor of Int32
  182. Int64
  183. Int64.mk
    1. Constructor of Int64
  184. Int8
  185. Int8.mk
    1. Constructor of Int8
  186. Iterator
    1. String.Iterator
  187. i
    1. String.Iterator.s (structure field)
  188. ibelow
    1. Nat.ibelow
  189. ident­Kind
    1. Lean.ident­Kind
  190. identifier
    1. raw
  191. if ... then ... else ...
  192. if h : ... then ... else ...
  193. imax
    1. Nat.imax
  194. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  195. impredicative
  196. inaccessible
  197. 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
  198. index­Of?
    1. Array.index­Of?
  199. indexed family
    1. of types
  200. induction
  201. induction­On
    1. Nat.div.induction­On
    2. Nat.mod.induction­On
  202. inductive.auto­Promote­Indices
  203. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  204. infer­Instance
  205. infer­Instance­As
  206. infer_instance
  207. injection
  208. injections
  209. insert­At
    1. Array.insert­At
  210. insert­At!
    1. Array.insert­At!
  211. insertion­Sort
    1. Array.insertion­Sort
  212. instance synthesis
  213. intercalate
    1. String.intercalate
  214. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  215. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  216. intro (0) (1)
  217. intro | ... => ... | ... => ...
  218. intros
  219. iota
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  220. is­Absolute
    1. System.FilePath.is­Absolute
  221. is­Alpha
    1. Char.is­Alpha
  222. is­Alphanum
    1. Char.is­Alphanum
  223. is­Digit
    1. Char.is­Digit
  224. is­Dir
    1. System.FilePath.is­Dir
  225. is­Empty
    1. Array.is­Empty
    2. String.is­Empty
  226. is­Eqv
    1. Array.is­Eqv
  227. is­Int
    1. String.is­Int
  228. is­Lower
    1. Char.is­Lower
  229. is­Lt
    1. Fin.val (structure field)
  230. is­Nat
    1. String.is­Nat
  231. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  232. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  233. is­Prefix­Of
    1. Array.is­Prefix­Of
    2. String.is­Prefix­Of
  234. is­Relative
    1. System.FilePath.is­Relative
  235. is­Tty
    1. IO.FS.Handle.is­Tty
    2. IO.FS.Stream.get­Line (structure field)
  236. is­Upper
    1. Char.is­Upper
  237. is­Valid
    1. String.Pos.is­Valid
  238. is­Valid­Char
    1. Nat.is­Valid­Char
  239. is­Value
    1. Nat.is­Value
  240. is­Whitespace
    1. Char.is­Whitespace
  241. iter
    1. String.iter
  242. 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. 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.mod
  7. Mode
    1. IO.FS.Mode
  8. Mul
  9. Mul.mul
  10. main goal
  11. map
    1. Array.map
    2. String.map
  12. map­Fin­Idx
    1. Array.map­Fin­Idx
  13. map­Fin­Idx­M
    1. Array.map­Fin­Idx­M
  14. map­Idx
    1. Array.map­Idx
  15. map­Idx­M
    1. Array.map­Idx­M
  16. map­Indexed
    1. Array.map­Indexed
  17. map­Indexed­M
    1. Array.map­Indexed­M
  18. map­M
    1. Array.map­M
  19. map­M'
    1. Array.map­M'
  20. map­Mono
    1. Array.map­Mono
  21. map­Mono­M
    1. Array.map­Mono­M
  22. map­Task
    1. BaseIO.map­Task
    2. EIO.map­Task
    3. IO.map­Task
  23. map­Tasks
    1. BaseIO.map­Tasks
    2. EIO.map­Tasks
    3. IO.map­Tasks
  24. match
    1. pp.match
  25. max
    1. Nat.max
    2. Task.Priority.max
  26. max­Discharge­Depth
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  27. max­Heartbeats
    1. synthInstance.max­Heartbeats
  28. max­Size
    1. synthInstance.max­Size
  29. max­Steps
    1. Lean.Meta.Simp.Config.zeta­Delta (structure field)
    2. pp.max­Steps
  30. memoize
    1. Lean.Meta.Simp.Config.index (structure field)
  31. metadata
    1. System.FilePath.metadata
  32. min
    1. Nat.min
    2. String.Pos.min
  33. mk
    1. Dynamic.mk
    2. IO.FS.Handle.mk
  34. mk­Already­Exists
    1. IO.Error.mk­Already­Exists
  35. mk­Already­Exists­File
    1. IO.Error.mk­Already­Exists­File
  36. mk­Array
    1. Array.mk­Array
  37. mk­Eof­Error
    1. IO.Error.mk­Eof­Error
  38. mk­File­Path
    1. System.mk­File­Path
  39. mk­Hardware­Fault
    1. IO.Error.mk­Hardware­Fault
  40. mk­Illegal­Operation
    1. IO.Error.mk­Illegal­Operation
  41. mk­Inappropriate­Type
    1. IO.Error.mk­Inappropriate­Type
  42. mk­Inappropriate­Type­File
    1. IO.Error.mk­Inappropriate­Type­File
  43. mk­Interrupted
    1. IO.Error.mk­Interrupted
  44. mk­Invalid­Argument
    1. IO.Error.mk­Invalid­Argument
  45. mk­Invalid­Argument­File
    1. IO.Error.mk­Invalid­Argument­File
  46. mk­Iterator
    1. String.mk­Iterator
  47. mk­No­File­Or­Directory
    1. IO.Error.mk­No­File­Or­Directory
  48. mk­No­Such­Thing
    1. IO.Error.mk­No­Such­Thing
  49. mk­No­Such­Thing­File
    1. IO.Error.mk­No­Such­Thing­File
  50. mk­Other­Error
    1. IO.Error.mk­Other­Error
  51. mk­Permission­Denied
    1. IO.Error.mk­Permission­Denied
  52. mk­Permission­Denied­File
    1. IO.Error.mk­Permission­Denied­File
  53. mk­Protocol­Error
    1. IO.Error.mk­Protocol­Error
  54. mk­Ref
    1. IO.mk­Ref
    2. ST.mk­Ref
  55. mk­Resource­Busy
    1. IO.Error.mk­Resource­Busy
  56. mk­Resource­Exhausted
    1. IO.Error.mk­Resource­Exhausted
  57. mk­Resource­Exhausted­File
    1. IO.Error.mk­Resource­Exhausted­File
  58. mk­Resource­Vanished
    1. IO.Error.mk­Resource­Vanished
  59. mk­Std­Gen
  60. mk­Tactic­Attribute
    1. Lean.Elab.Tactic.mk­Tactic­Attribute
  61. mk­Time­Expired
    1. IO.Error.mk­Time­Expired
  62. mk­Unsatisfied­Constraints
    1. IO.Error.mk­Unsatisfied­Constraints
  63. mk­Unsupported­Operation
    1. IO.Error.mk­Unsupported­Operation
  64. mod
    1. Mod.mod (class method)
    2. Nat.mod
  65. mod­Core
    1. Nat.mod­Core
  66. modified
    1. IO.FS.Metadata.type (structure field)
  67. modify
    1. Array.modify
    2. ST.Ref.modify
    3. String.modify
  68. modify­Get
    1. ST.Ref.modify­Get
  69. modify­M
    1. Array.modify­M
  70. modify­Op
    1. Array.modify­Op
  71. mono­Ms­Now
    1. IO.mono­Ms­Now
  72. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  73. mul
    1. Mul.mul (class method)
    2. Nat.mul
  74. 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. not
    1. Bool.not
  146. null­Kind
    1. Lean.null­Kind
  147. 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
    1. Bool.or
  20. or­Else
    1. Lean.Elab.Tactic.or­Else
  21. other
    1. IO.FileRight.user (structure field)
  22. other­Error­To­String
    1. IO.Error.other­Error­To­String
  23. out
    1. NeZero.out (class method)
  24. out­Param
  25. 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. PSum
  7. PSum.inl
    1. Constructor of PSum
  8. PSum.inr
    1. Constructor of PSum
  9. PUnit
  10. PUnit.unit
    1. Constructor of PUnit
  11. Pos
    1. String.Pos
  12. Pow
  13. Pow.pow
  14. Prec
    1. Lean.Syntax.Prec
  15. Preresolved
    1. Lean.Syntax.Preresolved
  16. Prio
    1. Lean.Syntax.Prio
  17. Priority
    1. Task.Priority
  18. Prod
  19. Prod.mk
    1. Constructor of Prod
  20. Prop
  21. parameter
    1. of inductive type
  22. parent
    1. System.FilePath.parent
  23. parser
  24. partition
    1. Array.partition
  25. path
    1. IO.FS.DirEntry.path
  26. path­Exists
    1. System.FilePath.path­Exists
  27. path­Separator
    1. System.FilePath.path­Separator
  28. path­Separators
    1. System.FilePath.path­Separators
  29. pattern
  30. polymorphism
    1. universe
  31. pop
    1. Array.pop
  32. pop­Front
    1. Subarray.pop­Front
  33. pop­While
    1. Array.pop­While
  34. pos
    1. IO.FS.Stream.Buffer.data (structure field)
    2. IO.FS.Stream.Buffer.pos
    3. String.Iterator.pos
  35. pos­Of
    1. String.pos­Of
  36. pow
    1. HomogeneousPow.pow (class method)
    2. Nat.pow
    3. NatPow.pow (class method)
    4. Pow.pow (class method)
  37. pp.deep­Terms
  38. pp.deepTerms.threshold
  39. pp.match
  40. pp.max­Steps
  41. pp.mvars
  42. pp.proofs
  43. pp.proofs.threshold
  44. pred
    1. Nat.pred
  45. predicative
  46. prev
    1. String.Iterator.prev
    2. String.prev
  47. prevn
    1. String.Iterator.prevn
  48. print
    1. IO.print
  49. println
    1. IO.println
  50. proj
    1. Lean.Meta.DSimp.Config.iota (structure field)
    2. Lean.Meta.Simp.Config.memoize (structure field)
  51. proof state
  52. proofs
    1. pp.proofs
  53. property
    1. Subtype.val (structure field)
  54. propext
  55. proposition
    1. decidable
  56. prune­Solved­Goals
    1. Lean.Elab.Tactic.prune­Solved­Goals
  57. ptr­Eq
    1. ST.Ref.ptr­Eq
  58. push
    1. Array.push
    2. String.push
  59. push_cast
  60. pushn
    1. String.pushn
  61. put­Str
    1. IO.FS.Handle.put­Str
    2. IO.FS.Stream.read (structure field)
  62. 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. Subtype
  190. Subtype.mk
    1. Constructor of Subtype
  191. Sum
  192. Sum.inl
    1. Constructor of Sum
  193. Sum.inr
    1. Constructor of Sum
  194. Syntax
    1. Lean.Syntax
  195. Syntax­Node­Kind
    1. Lean.Syntax­Node­Kind
  196. System.File­Path
  197. System.FilePath.add­Extension
  198. System.FilePath.components
  199. System.FilePath.exe­Extension
  200. System.FilePath.ext­Separator
  201. System.FilePath.extension
  202. System.FilePath.file­Name
  203. System.FilePath.file­Stem
  204. System.FilePath.is­Absolute
  205. System.FilePath.is­Dir
  206. System.FilePath.is­Relative
  207. System.FilePath.join
  208. System.FilePath.metadata
  209. System.FilePath.mk
    1. Constructor of System.File­Path
  210. System.FilePath.normalize
  211. System.FilePath.parent
  212. System.FilePath.path­Exists
  213. System.FilePath.path­Separator
  214. System.FilePath.path­Separators
  215. System.FilePath.read­Dir
  216. System.FilePath.walk­Dir
  217. System.FilePath.with­Extension
  218. System.FilePath.with­File­Name
  219. System.mk­File­Path
  220. s
    1. String.Iterator.i (structure field)
  221. s1
    1. StdGen.s2 (structure field)
  222. s2
    1. StdGen.s1 (structure field)
  223. save
  224. scientific­Lit­Kind
    1. Lean.scientific­Lit­Kind
  225. semi­Out­Param
  226. sequence­Map
    1. Array.sequence­Map
  227. set
    1. Array.set
    2. ST.Ref.set
    3. String.set
  228. set!
    1. Array.set!
  229. set­Access­Rights
    1. IO.set­Access­Rights
  230. set­Curr
    1. String.Iterator.set­Curr
  231. set­Current­Dir
    1. IO.Process.set­Current­Dir
  232. set­D
    1. Array.set­D
  233. set­Goals
    1. Lean.Elab.Tactic.set­Goals
  234. set­Kind
    1. Lean.Syntax.set­Kind
  235. set­Rand­Seed
    1. IO.set­Rand­Seed
  236. set­Stderr
    1. IO.set­Stderr
  237. set­Stdin
    1. IO.set­Stdin
  238. set­Stdout
    1. IO.set­Stdout
  239. set_option
  240. setsid
    1. IO.Process.SpawnArgs.setsid (structure field)
  241. shift­Left
    1. Nat.shift­Left
    2. ShiftLeft.shift­Left (class method)
  242. shift­Right
    1. Nat.shift­Right
    2. ShiftRight.shift­Right (class method)
  243. show
  244. show_term
  245. simp (0) (1)
  246. simp!
  247. simp?
  248. simp?!
  249. simp_all
  250. simp_all!
  251. simp_all?
  252. simp_all?!
  253. simp_all_arith
  254. simp_all_arith!
  255. simp_arith
  256. simp_arith!
  257. simp_match
  258. simp_wf
  259. simpa
  260. simpa!
  261. simpa?
  262. simpa?!
  263. simprocs
  264. single­Pass
    1. Lean.Meta.Simp.Config.single­Pass (structure field)
  265. singleton
    1. Array.singleton
    2. String.singleton
  266. size
    1. Array.size
    2. Subarray.size
  267. size­Of
    1. SizeOf.size­Of (class method)
  268. skip (0) (1)
  269. skip­Assigned­Instances
    1. tactic.skip­Assigned­Instances
  270. sleep
    1. IO.sleep
  271. snd
    1. MProd.fst (structure field)
    2. PProd.fst (structure field)
    3. Prod.fst (structure field)
  272. solve
  273. solve_by_elim
  274. sorry
  275. sort­MVar­Id­Array­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  276. sort­MVar­Ids­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  277. spawn
    1. IO.Process.spawn
    2. Task.spawn
  278. specialize
  279. split
    1. Array.split
    2. RandomGen.split (class method)
    3. String.split
    4. Subarray.split
  280. split­On
    1. String.split­On
  281. start
    1. Subarray.stop (structure field)
  282. start_le_stop
    1. Subarray.stop_le_array_size (structure field)
  283. starts­With
    1. String.starts­With
  284. std­Next
  285. std­Range
  286. std­Split
  287. stderr
    1. IO.Process.Child.stdin (structure field)
    2. IO.Process.Output.exit­Code (structure field)
    3. IO.Process.StdioConfig.stdin (structure field)
  288. stdin
    1. IO.Process.Child.stderr (structure field)
    2. IO.Process.StdioConfig.stderr (structure field)
  289. stdout
    1. IO.Process.Child.stdout (structure field)
    2. IO.Process.Output.stdout (structure field)
    3. IO.Process.StdioConfig.stdout (structure field)
  290. stop
    1. Subarray.start (structure field)
  291. stop_le_array_size
    1. Subarray.array (structure field)
  292. str­Lit­Kind
    1. Lean.str­Lit­Kind
  293. strong­Induction­On
    1. Nat.strong­Induction­On
  294. sub
    1. Nat.sub
    2. Sub.sub (class method)
  295. sub­Digit­Char
    1. Nat.sub­Digit­Char
  296. subst
  297. subst_eqs
  298. subst_vars
  299. substr­Eq
    1. String.substr­Eq
  300. suffices
  301. super­Digit­Char
    1. Nat.super­Digit­Char
  302. swap
    1. Array.swap
    2. ST.Ref.swap
  303. swap!
    1. Array.swap!
  304. swap­At
    1. Array.swap­At
  305. swap­At!
    1. Array.swap­At!
  306. symm
  307. symm_saturate
  308. synthInstance.max­Heartbeats
  309. synthInstance.max­Size
  310. 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­Bit­Vec
    1. UInt16.to­Bit­Vec (structure field)
    2. UInt32.to­Bit­Vec (structure field)
    3. UInt64.to­Bit­Vec (structure field)
    4. UInt8.to­Bit­Vec (structure field)
    5. USize.to­Bit­Vec (structure field)
  42. to­Digits
    1. Nat.to­Digits
  43. to­Digits­Core
    1. Nat.to­Digits­Core
  44. to­EIO
    1. BaseIO.to­EIO
    2. IO.to­EIO
  45. to­End
    1. String.Iterator.to­End
  46. to­File­Map
    1. String.to­File­Map
  47. to­Float
    1. Nat.to­Float
  48. to­Format
    1. String.to­Format
  49. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  50. to­Handle­Type
    1. IO.Process.Stdio.to­Handle­Type
  51. to­IO
    1. BaseIO.to­IO
    2. EIO.to­IO
  52. to­IO'
    1. EIO.to­IO'
  53. to­ISize
    1. Bool.to­ISize
  54. to­Int!
    1. String.to­Int!
  55. to­Int16
    1. Bool.to­Int16
  56. to­Int32
    1. Bool.to­Int32
  57. to­Int64
    1. Bool.to­Int64
  58. to­Int8
    1. Bool.to­Int8
  59. to­Int?
    1. String.to­Int?
  60. to­Level
    1. Nat.to­Level
  61. to­List
    1. Array.to­List
    2. Array.to­List (structure field)
    3. String.to­List
  62. to­List­Append
    1. Array.to­List­Append
  63. to­List­Rev
    1. Array.to­List­Rev
  64. to­Lower
    1. String.to­Lower
  65. to­Monad­State­Of
    1. ST.Ref.to­Monad­State­Of
  66. to­Name
    1. String.to­Name
  67. to­Nat
    1. Bool.to­Nat
  68. to­Nat!
    1. String.to­Nat!
  69. to­Nat?
    1. String.to­Nat?
  70. to­PArray'
    1. Array.to­PArray'
  71. to­Stdio­Config
    1. IO.Process.SpawnArgs.to­Stdio­Config (structure field)
  72. to­String
    1. IO.Error.to­String
    2. System.FilePath.to­String (structure field)
    3. ToString.to­String (class method)
  73. to­Sub­Digits
    1. Nat.to­Sub­Digits
  74. to­Subarray
    1. Array.to­Subarray
  75. to­Subscript­String
    1. Nat.to­Subscript­String
  76. to­Substring
    1. String.to­Substring
  77. to­Substring'
    1. String.to­Substring'
  78. to­Super­Digits
    1. Nat.to­Super­Digits
  79. to­Superscript­String
    1. Nat.to­Superscript­String
  80. to­UInt16
    1. Bool.to­UInt16
    2. Int16.to­UInt16 (structure field)
    3. Nat.to­UInt16
  81. to­UInt32
    1. Bool.to­UInt32
    2. Int32.to­UInt32 (structure field)
    3. Nat.to­UInt32
  82. to­UInt64
    1. Bool.to­UInt64
    2. Int64.to­UInt64 (structure field)
    3. Nat.to­UInt64
  83. to­UInt8
    1. Bool.to­UInt8
    2. Int8.to­UInt8 (structure field)
    3. Nat.to­UInt8
  84. to­USize
    1. Bool.to­USize
    2. Nat.to­USize
  85. to­UTF8
    1. String.to­UTF8
  86. to­Upper
    1. String.to­Upper
  87. trace
    1. Lean.Macro.trace
    2. tactic.simp.trace (0) (1)
  88. trace.Meta.Tactic.simp.discharge
  89. trace.Meta.Tactic.simp.rewrite
  90. trace_state (0) (1)
  91. transparency
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  92. trim
    1. String.trim
  93. trim­Left
    1. String.trim­Left
  94. trim­Right
    1. String.trim­Right
  95. trivial
  96. truncate
    1. IO.FS.Handle.truncate
  97. try (0) (1)
  98. try­Catch
    1. Lean.Elab.Tactic.try­Catch
  99. try­Lock
    1. IO.FS.Handle.try­Lock
  100. try­Tactic
    1. Lean.Elab.Tactic.try­Tactic
  101. try­Tactic?
    1. Lean.Elab.Tactic.try­Tactic?
  102. try­Wait
    1. IO.Process.Child.try­Wait
  103. type
    1. IO.FS.Metadata.accessed (structure field)
  104. type constructor

U

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

V

  1. val
    1. Char.val (structure field)
    2. Fin.is­Lt (structure field)
    3. Subtype.property (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. Bool.xor
    2. 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