Index

Symbols

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

A

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

B

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

C

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

D

  1. Decidable
  2. Decidable.by­Cases
  3. Decidable.decide
  4. Decidable.is­False
    1. Constructor of Decidable
  5. Decidable.is­True
    1. Constructor of Decidable
  6. Decidable­Eq
  7. Decidable­Rel
  8. Dir­Entry
    1. IO.FS.Dir­Entry
  9. Div
  10. Div.mk
    1. Instance constructor of Div
  11. Dvd
  12. Dvd.mk
    1. Instance constructor of Dvd
  13. Dynamic
  14. Dynamic.get?
  15. Dynamic.mk
  16. data
    1. IO.FS.Stream.Buffer.data
    2. IO.FS.Stream.Buffer.data (structure field)
    3. String.data (structure field)
    4. _private.Init.Dynamic.0.TypeName.data (class method)
  17. dbg_cache
    1. tactic.dbg_cache
  18. dbg_trace
  19. dec­Eq
    1. Bool.dec­Eq
    2. ISize.dec­Eq
    3. Int.dec­Eq
    4. Int16.dec­Eq
    5. Int32.dec­Eq
    6. Int64.dec­Eq
    7. Int8.dec­Eq
    8. Nat.dec­Eq
    9. String.dec­Eq
    10. UInt16.dec­Eq
    11. UInt32.dec­Eq
    12. UInt64.dec­Eq
    13. UInt8.dec­Eq
    14. USize.dec­Eq
  20. dec­Le
    1. ISize.dec­Le
    2. Int16.dec­Le
    3. Int32.dec­Le
    4. Int64.dec­Le
    5. Int8.dec­Le
    6. Nat.dec­Le
    7. UInt16.dec­Le
    8. UInt32.dec­Le
    9. UInt64.dec­Le
    10. UInt8.dec­Le
    11. USize.dec­Le
  21. dec­Lt
    1. ISize.dec­Lt
    2. Int16.dec­Lt
    3. Int32.dec­Lt
    4. Int64.dec­Lt
    5. Int8.dec­Lt
    6. Nat.dec­Lt
    7. UInt16.dec­Lt
    8. UInt32.dec­Lt
    9. UInt64.dec­Lt
    10. UInt8.dec­Lt
    11. USize.dec­Lt
  22. decapitalize
    1. String.decapitalize
  23. decidable
  24. decidable_eq_none
    1. Option.decidable_eq_none
  25. decide
    1. Decidable.decide
    2. Lean.Meta.DSimp.Config.decide (structure field)
    3. Lean.Meta.Simp.Config.decide (structure field)
  26. decreasing_tactic
  27. decreasing_trivial
  28. decreasing_with
  29. dedicated
    1. Task.Priority.dedicated
  30. deep­Terms
    1. pp.deep­Terms
  31. default
    1. Inhabited.default (class method)
    2. Task.Priority.default
  32. default­Facets
    1. [anonymous] (structure field)
  33. delta (0) (1)
  34. digit­Char
    1. Nat.digit­Char
  35. discard
    1. Functor.discard
  36. discharge
    1. trace.Meta.Tactic.simp.discharge
  37. div
    1. Div.div (class method)
    2. Fin.div
    3. ISize.div
    4. Int16.div
    5. Int32.div
    6. Int64.div
    7. Int8.div
    8. Nat.div
    9. UInt16.div
    10. UInt32.div
    11. UInt64.div
    12. UInt8.div
    13. USize.div
  38. div2Induction
    1. Nat.div2Induction
  39. done (0) (1)
  40. down
    1. PLift.down (structure field)
    2. ULift.down (structure field)
  41. drop
    1. String.drop
    2. Subarray.drop
  42. drop­Right
    1. String.drop­Right
  43. drop­Right­While
    1. String.drop­Right­While
  44. drop­While
    1. String.drop­While
  45. dsimp (0) (1)
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  46. dsimp!
  47. dsimp?
  48. dsimp?!
  49. dsimp­Location'
    1. Lean.Elab.Tactic.dsimp­Location'
  50. 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. ELAN (environment variable)
  11. ELAN_HOME (environment variable)
  12. EST
  13. EState­M
  14. EStateM.Backtrackable
  15. EStateM.Backtrackable.mk
    1. Instance constructor of EStateM.Backtrackable
  16. EStateM.Result
  17. EStateM.Result.error
    1. Constructor of EStateM.Result
  18. EStateM.Result.ok
    1. Constructor of EStateM.Result
  19. EStateM.adapt­Except
  20. EStateM.bind
  21. EStateM.from­State­M
  22. EStateM.get
  23. EStateM.map
  24. EStateM.modify­Get
  25. EStateM.non­Backtrackable
  26. EStateM.or­Else
  27. EStateM.or­Else'
  28. EStateM.pure
  29. EStateM.run
  30. EStateM.run'
  31. EStateM.seq­Right
  32. EStateM.set
  33. EStateM.throw
  34. EStateM.try­Catch
  35. Empty
  36. Empty.elim
  37. Error
    1. IO.Error
  38. Even
  39. Even.plus­Two
    1. Constructor of Even
  40. Even.zero
    1. Constructor of Even
  41. Except
  42. Except.bind
  43. Except.error
    1. Constructor of Except
  44. Except.is­Ok
  45. Except.map
  46. Except.map­Error
  47. Except.ok
    1. Constructor of Except
  48. Except.or­Else­Lazy
  49. Except.pure
  50. Except.to­Bool
  51. Except.to­Option
  52. Except.try­Catch
  53. Except­Cps­T
  54. Except­CpsT.lift
  55. Except­CpsT.run
  56. Except­CpsT.run­Catch
  57. Except­CpsT.run­K
  58. Except­T
  59. ExceptT.adapt
  60. ExceptT.bind
  61. ExceptT.bind­Cont
  62. ExceptT.lift
  63. ExceptT.map
  64. ExceptT.mk
  65. ExceptT.pure
  66. ExceptT.run
  67. ExceptT.try­Catch
  68. ediv
    1. Int.ediv
  69. elab­Cases­Targets
    1. Lean.Elab.Tactic.elab­Cases­Targets
  70. elab­DSimp­Config­Core
    1. Lean.Elab.Tactic.elab­DSimp­Config­Core
  71. elab­Simp­Args
    1. Lean.Elab.Tactic.elab­Simp­Args
  72. elab­Simp­Config
    1. Lean.Elab.Tactic.elab­Simp­Config
  73. elab­Simp­Config­Ctx­Core
    1. Lean.Elab.Tactic.elab­Simp­Config­Ctx­Core
  74. elab­Term
    1. Lean.Elab.Tactic.elab­Term
  75. elab­Term­Ensuring­Type
    1. Lean.Elab.Tactic.elab­Term­Ensuring­Type
  76. elab­Term­With­Holes
    1. Lean.Elab.Tactic.elab­Term­With­Holes
  77. elem
    1. Array.elem
  78. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  79. elim
    1. Empty.elim
    2. Option.elim
    3. PEmpty.elim
  80. elim0
    1. Fin.elim0
  81. elim­M
    1. Option.elim­M
  82. elim­Offset
    1. Nat.elim­Offset
  83. emod
    1. Int.emod
  84. empty
    1. Array.empty
    2. Subarray.empty
  85. end­Pos
    1. String.end­Pos
  86. ends­With
    1. String.ends­With
  87. ensure­Has­No­MVars
    1. Lean.Elab.Tactic.ensure­Has­No­MVars
  88. enter
  89. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  90. env (Lake command)
  91. environment variables
  92. eprint
    1. IO.eprint
  93. eprintln
    1. IO.eprintln
  94. eq_of_beq
    1. LawfulBEq.eq_of_beq (class method)
  95. eq_refl
  96. erase
    1. Array.erase
  97. erase­Idx
    1. Array.erase­Idx
  98. erase­Reps
    1. Array.erase­Reps
  99. erw (0) (1)
  100. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.eta (structure field)
  101. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
    2. Lean.Meta.Simp.Config.eta­Struct (structure field)
  102. exact
  103. exact?
  104. exact_mod_cast
  105. exe (Lake command)
  106. exe­Extension
    1. System.FilePath.exe­Extension
  107. exe­Name
    1. [anonymous] (structure field)
  108. exfalso
  109. exists
  110. exit
    1. IO.Process.exit
  111. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  112. expand­Macro?
    1. Lean.Macro.expand­Macro?
  113. ext (0) (1)
  114. ext1
  115. ext­Separator
    1. System.FilePath.ext­Separator
  116. extension
    1. System.FilePath.extension
  117. extensionality
    1. of propositions
  118. extra­Dep­Targets
    1. [anonymous] (structure field) (0) (1)
  119. extract
    1. Array.extract
    2. String.Iterator.extract
    3. String.extract

F

  1. File­Path
    1. System.File­Path
  2. File­Right
    1. IO.File­Right
  3. Fin
  4. Fin.add
  5. Fin.add­Cases
  6. Fin.add­Nat
  7. Fin.cases
  8. Fin.cast
  9. Fin.cast­Add
  10. Fin.cast­LE
  11. Fin.cast­LT
  12. Fin.cast­Succ
  13. Fin.div
  14. Fin.elim0
  15. Fin.foldl
  16. Fin.foldl­M
  17. Fin.foldr
  18. Fin.foldr­M
  19. Fin.from­Expr?
  20. Fin.h­Iterate
  21. Fin.h­Iterate­From
  22. Fin.induction
  23. Fin.induction­On
  24. Fin.is­Value
  25. Fin.land
  26. Fin.last
  27. Fin.last­Cases
  28. Fin.log2
  29. Fin.lor
  30. Fin.mk
    1. Constructor of Fin
  31. Fin.mod
  32. Fin.modn
  33. Fin.mul
  34. Fin.nat­Add
  35. Fin.of­Nat'
  36. Fin.pred
  37. Fin.reduce­Add
  38. Fin.reduce­Add­Nat
  39. Fin.reduce­And
  40. Fin.reduce­BEq
  41. Fin.reduce­BNe
  42. Fin.reduce­Bin
  43. Fin.reduce­Bin­Pred
  44. Fin.reduce­Bool­Pred
  45. Fin.reduce­Cast­Add
  46. Fin.reduce­Cast­LE
  47. Fin.reduce­Cast­LT
  48. Fin.reduce­Cast­Succ
  49. Fin.reduce­Div
  50. Fin.reduce­Eq
  51. Fin.reduce­Fin­Mk
  52. Fin.reduce­GE
  53. Fin.reduce­GT
  54. Fin.reduce­LE
  55. Fin.reduce­LT
  56. Fin.reduce­Last
  57. Fin.reduce­Mod
  58. Fin.reduce­Mul
  59. Fin.reduce­Nat­Add
  60. Fin.reduce­Nat­Op
  61. Fin.reduce­Ne
  62. Fin.reduce­Of­Nat'
  63. Fin.reduce­Op
  64. Fin.reduce­Or
  65. Fin.reduce­Pred
  66. Fin.reduce­Rev
  67. Fin.reduce­Shift­Left
  68. Fin.reduce­Shift­Right
  69. Fin.reduce­Sub
  70. Fin.reduce­Sub­Nat
  71. Fin.reduce­Succ
  72. Fin.reduce­Xor
  73. Fin.rev
  74. Fin.reverse­Induction
  75. Fin.shift­Left
  76. Fin.shift­Right
  77. Fin.sub
  78. Fin.sub­Nat
  79. Fin.succ
  80. Fin.succ­Rec
  81. Fin.succ­Rec­On
  82. Fin.xor
  83. For­In
  84. For­In'
  85. ForIn'.mk
    1. Instance constructor of For­In'
  86. ForIn.mk
    1. Instance constructor of For­In
  87. For­In­Step
  88. For­InStep.done
    1. Constructor of For­In­Step
  89. For­InStep.yield
    1. Constructor of For­In­Step
  90. For­M
  91. ForM.for­In
  92. ForM.mk
    1. Instance constructor of For­M
  93. Functor
  94. Functor.discard
  95. Functor.map­Rev
  96. Functor.mk
    1. Instance constructor of Functor
  97. fail
    1. OptionT.fail
  98. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
    2. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  99. fail_if_success (0) (1)
  100. failure
    1. ReaderT.failure
    2. StateT.failure
    3. [anonymous] (class method)
  101. false_or_by_contra
  102. fdiv
    1. Int.fdiv
  103. field­Idx­Kind
    1. Lean.field­Idx­Kind
  104. field­Notation
    1. pp.field­Notation
  105. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
    2. System.FilePath.file­Name
  106. file­Stem
    1. System.FilePath.file­Stem
  107. filter
    1. Array.filter
    2. Option.filter
  108. filter­M
    1. Array.filter­M
  109. filter­Map
    1. Array.filter­Map
  110. filter­Map­M
    1. Array.filter­Map­M
  111. filter­Pairs­M
    1. Array.filter­Pairs­M
  112. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  113. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  114. find
    1. String.find
  115. find?
    1. Array.find?
  116. find­Extern­Lib?
    1. Lake.find­Extern­Lib?
  117. find­Idx?
    1. Array.find­Idx?
  118. find­Idx­M?
    1. Array.find­Idx­M?
  119. find­Lean­Exe?
    1. Lake.find­Lean­Exe?
  120. find­Lean­Lib?
    1. Lake.find­Lean­Lib?
  121. find­Line­Start
    1. String.find­Line­Start
  122. find­M?
    1. Array.find­M?
  123. find­Module?
    1. Lake.find­Module?
  124. find­Package?
    1. Lake.find­Package?
  125. find­Rev?
    1. Array.find­Rev?
    2. Subarray.find­Rev?
  126. find­Rev­M?
    1. Array.find­Rev­M?
    2. Subarray.find­Rev­M?
  127. find­Some!
    1. Array.find­Some!
  128. find­Some?
    1. Array.find­Some?
  129. find­Some­M?
    1. Array.find­Some­M?
  130. find­Some­Rev?
    1. Array.find­Some­Rev?
  131. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
    2. Subarray.find­Some­Rev­M?
  132. first (0) (1)
  133. first­Diff­Pos
    1. String.first­Diff­Pos
  134. fix
    1. WellFounded.fix
  135. flags
    1. IO.FileRight.flags
  136. flat­Map
    1. Array.flat­Map
  137. flat­Map­M
    1. Array.flat­Map­M
  138. flatten
    1. Array.flatten
  139. flush
    1. IO.FS.Handle.flush
    2. IO.FS.Stream.flush (structure field)
  140. fmod
    1. Int.fmod
  141. focus (0) (1)
    1. Lean.Elab.Tactic.focus
  142. fold
    1. Nat.fold
  143. fold­M
    1. Nat.fold­M
  144. fold­Rev
    1. Nat.fold­Rev
  145. fold­Rev­M
    1. Nat.fold­Rev­M
  146. fold­TR
    1. Nat.fold­TR
  147. foldl
    1. Array.foldl
    2. Fin.foldl
    3. String.foldl
    4. Subarray.foldl
  148. foldl­M
    1. Array.foldl­M
    2. Fin.foldl­M
    3. Subarray.foldl­M
  149. foldr
    1. Array.foldr
    2. Fin.foldr
    3. String.foldr
    4. Subarray.foldr
  150. foldr­M
    1. Array.foldr­M
    2. Fin.foldr­M
    3. Subarray.foldr­M
  151. fopen­Error­To­String
    1. IO.Error.fopen­Error­To­String
  152. for­In
    1. ForIn.for­In (class method)
    2. ForM.for­In
    3. Subarray.for­In
  153. for­In'
    1. Array.for­In'
    2. ForIn'.for­In' (class method)
  154. for­M
    1. Array.for­M
    2. ForM.for­M (class method)
    3. Nat.for­M
    4. Option.for­M
    5. Subarray.for­M
  155. for­Rev­M
    1. Array.for­Rev­M
    2. Nat.for­Rev­M
    3. Subarray.for­Rev­M
  156. format
    1. Option.format
  157. forward
    1. String.Iterator.forward
  158. from­Expr
    1. UInt16.from­Expr
    2. UInt32.from­Expr
    3. UInt64.from­Expr
    4. UInt8.from­Expr
    5. USize.from­Expr
  159. from­Expr?
    1. Fin.from­Expr?
    2. Int.from­Expr?
    3. Nat.from­Expr?
    4. String.from­Expr?
  160. from­State­M
    1. EStateM.from­State­M
  161. from­UTF8
    1. String.from­UTF8
  162. from­UTF8!
    1. String.from­UTF8!
  163. from­UTF8?
    1. String.from­UTF8?
  164. front
    1. String.front
  165. fst
    1. MProd.fst (structure field)
    2. PProd.fst (structure field)
    3. PSigma.fst (structure field)
    4. Prod.fst (structure field)
    5. Sigma.fst (structure field)
  166. fun
  167. funext (0) (1)

G

  1. Get­Elem
  2. GetElem.mk
    1. Instance constructor of Get­Elem
  3. Get­Elem?
  4. GetElem?.mk
    1. Instance constructor of Get­Elem?
  5. Glob
    1. Lake.Glob
  6. gcd
    1. Int.gcd
    2. Nat.gcd
  7. generalize
  8. get
    1. Array.get
    2. EStateM.get
    3. MonadState.get
    4. MonadState.get (class method)
    5. Monad­StateOf.get (class method)
    6. Option.get
    7. ST.Ref.get
    8. State­RefT'.get
    9. StateT.get
    10. String.get
    11. Subarray.get
    12. Task.get
    13. Task.get (structure field)
  9. get!
    1. Array.get!
    2. Option.get!
    3. String.get!
    4. Subarray.get!
  10. get'
    1. String.get'
  11. get?
    1. Array.get?
    2. Dynamic.get?
    3. String.get?
  12. get­Augmented­Env
    1. Lake.get­Augmented­Env
  13. get­Augmented­Lean­Path
    1. Lake.get­Augmented­Lean­Path
  14. get­Augmented­Lean­Src­Path
    1. Lake.get­Augmented­Lean­Src­Path
  15. get­Augmented­Shared­Lib­Path
    1. Lake.get­Augmented­Shared­Lib­Path
  16. get­Char
    1. Lean.TSyntax.get­Char
  17. get­Curr­Macro­Scope
    1. Lean.Elab.Tactic.get­Curr­Macro­Scope
  18. get­Curr­Namespace
    1. Lean.Macro.get­Curr­Namespace
  19. get­Current­Dir
    1. IO.Process.get­Current­Dir
  20. get­D
    1. Array.get­D
    2. Option.get­D
    3. Subarray.get­D
  21. get­DM
    1. Option.get­DM
  22. get­Elan?
    1. Lake.get­Elan?
  23. get­Elan­Home?
    1. Lake.get­Elan­Home?
  24. get­Elan­Install?
    1. Lake.get­Elan­Install?
  25. get­Elan­Toolchain
    1. Lake.get­Elan­Toolchain
  26. get­Elem
    1. GetElem.get­Elem (class method)
  27. get­Elem!
    1. GetElem?.get­Elem? (class method)
  28. get­Elem!_def
    1. Lawful­GetElem.get­Elem!_def (class method)
  29. get­Elem?
    1. [anonymous] (class method)
  30. get­Elem?_def
    1. Lawful­GetElem.get­Elem?_def (class method)
  31. get­Env
    1. IO.get­Env
  32. get­Env­Lean­Path
    1. Lake.get­Env­Lean­Path
  33. get­Env­Lean­Src­Path
    1. Lake.get­Env­Lean­Src­Path
  34. get­Env­Shared­Lib­Path
    1. Lake.get­Env­Shared­Lib­Path
  35. get­Even­Elems
    1. Array.get­Even­Elems
  36. get­FVar­Id
    1. Lean.Elab.Tactic.get­FVar­Id
  37. get­FVar­Ids
    1. Lean.Elab.Tactic.get­FVar­Ids
  38. get­Goals
    1. Lean.Elab.Tactic.get­Goals
  39. get­Hygiene­Info
    1. Lean.TSyntax.get­Hygiene­Info
  40. get­Id
    1. Lean.TSyntax.get­Id
  41. get­Idx?
    1. Array.get­Idx?
  42. get­Kind
    1. Lean.Syntax.get­Kind
  43. get­Lake
    1. Lake.get­Lake
  44. get­Lake­Env
    1. Lake.get­Lake­Env
  45. get­Lake­Home
    1. Lake.get­Lake­Home
  46. get­Lake­Install
    1. Lake.get­Lake­Install
  47. get­Lake­Lib­Dir
    1. Lake.get­Lake­Lib­Dir
  48. get­Lake­Src­Dir
    1. Lake.get­Lake­Src­Dir
  49. get­Lean
    1. Lake.get­Lean
  50. get­Lean­Ar
    1. Lake.get­Lean­Ar
  51. get­Lean­Cc
    1. Lake.get­Lean­Cc
  52. get­Lean­Cc?
    1. Lake.get­Lean­Cc?
  53. get­Lean­Include­Dir
    1. Lake.get­Lean­Include­Dir
  54. get­Lean­Install
    1. Lake.get­Lean­Install
  55. get­Lean­Lib­Dir
    1. Lake.get­Lean­Lib­Dir
  56. get­Lean­Path
    1. Lake.get­Lean­Path
  57. get­Lean­Shared­Lib
    1. Lake.get­Lean­Shared­Lib
  58. get­Lean­Src­Dir
    1. Lake.get­Lean­Src­Dir
  59. get­Lean­Src­Path
    1. Lake.get­Lean­Src­Path
  60. get­Lean­Sysroot
    1. Lake.get­Lean­Sysroot
  61. get­Lean­System­Lib­Dir
    1. Lake.get­Lean­System­Lib­Dir
  62. get­Leanc
    1. Lake.get­Leanc
  63. get­Line
    1. IO.FS.Handle.get­Line
    2. IO.FS.Stream.get­Line (structure field)
  64. get­M
    1. Option.get­M
  65. get­Main­Goal
    1. Lean.Elab.Tactic.get­Main­Goal
  66. get­Main­Module
    1. Lean.Elab.Tactic.get­Main­Module
  67. get­Main­Tag
    1. Lean.Elab.Tactic.get­Main­Tag
  68. get­Max?
    1. Array.get­Max?
  69. get­Modify
  70. get­Name
    1. Lean.TSyntax.get­Name
  71. get­Nat
    1. Lean.TSyntax.get­Nat
  72. get­No­Cache
    1. Lake.get­No­Cache
  73. get­Num­Heartbeats
    1. IO.get­Num­Heartbeats
  74. get­PID
    1. IO.Process.get­PID
  75. get­Pkg­Url­Map
    1. Lake.get­Pkg­Url­Map
  76. get­Random­Bytes
    1. IO.get­Random­Bytes
  77. get­Root­Package
    1. Lake.get­Root­Package
  78. get­Scientific
    1. Lean.TSyntax.get­Scientific
  79. get­Shared­Lib­Path
    1. Lake.get­Shared­Lib­Path
  80. get­Stderr
    1. IO.get­Stderr
  81. get­Stdin
    1. IO.get­Stdin
  82. get­Stdout
    1. IO.get­Stdout
  83. get­String
    1. Lean.TSyntax.get­String
  84. get­Task­State
    1. IO.get­Task­State
  85. get­The
  86. get­Try­Cache
    1. Lake.get­Try­Cache
  87. get­Unsolved­Goals
    1. Lean.Elab.Tactic.get­Unsolved­Goals
  88. get­Utf8Byte
    1. String.get­Utf8Byte
  89. get­Workspace
    1. Lake.MonadWorkspace.get­Workspace (class method)
  90. get_elem_tactic
  91. get_elem_tactic_trivial
  92. globs
    1. [anonymous] (structure field)
  93. goal
    1. main
  94. ground
    1. Lean.Meta.Simp.Config.ground (structure field)
  95. group
    1. IO.FileRight.group (structure field)
  96. group­By­Key
    1. Array.group­By­Key
  97. group­Kind
    1. Lean.group­Kind
  98. guard
    1. Option.guard
  99. guard_expr
  100. guard_hyp
  101. guard_target

H

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

I

  1. IO
  2. IO.Error
  3. IO.Error.already­Exists
    1. Constructor of IO.Error
  4. IO.Error.fopen­Error­To­String
  5. IO.Error.hardware­Fault
    1. Constructor of IO.Error
  6. IO.Error.illegal­Operation
    1. Constructor of IO.Error
  7. IO.Error.inappropriate­Type
    1. Constructor of IO.Error
  8. IO.Error.interrupted
    1. Constructor of IO.Error
  9. IO.Error.invalid­Argument
    1. Constructor of IO.Error
  10. IO.Error.mk­Already­Exists
  11. IO.Error.mk­Already­Exists­File
  12. IO.Error.mk­Eof­Error
  13. IO.Error.mk­Hardware­Fault
  14. IO.Error.mk­Illegal­Operation
  15. IO.Error.mk­Inappropriate­Type
  16. IO.Error.mk­Inappropriate­Type­File
  17. IO.Error.mk­Interrupted
  18. IO.Error.mk­Invalid­Argument
  19. IO.Error.mk­Invalid­Argument­File
  20. IO.Error.mk­No­File­Or­Directory
  21. IO.Error.mk­No­Such­Thing
  22. IO.Error.mk­No­Such­Thing­File
  23. IO.Error.mk­Other­Error
  24. IO.Error.mk­Permission­Denied
  25. IO.Error.mk­Permission­Denied­File
  26. IO.Error.mk­Protocol­Error
  27. IO.Error.mk­Resource­Busy
  28. IO.Error.mk­Resource­Exhausted
  29. IO.Error.mk­Resource­Exhausted­File
  30. IO.Error.mk­Resource­Vanished
  31. IO.Error.mk­Time­Expired
  32. IO.Error.mk­Unsatisfied­Constraints
  33. IO.Error.mk­Unsupported­Operation
  34. IO.Error.no­File­Or­Directory
    1. Constructor of IO.Error
  35. IO.Error.no­Such­Thing
    1. Constructor of IO.Error
  36. IO.Error.other­Error
    1. Constructor of IO.Error
  37. IO.Error.other­Error­To­String
  38. IO.Error.permission­Denied
    1. Constructor of IO.Error
  39. IO.Error.protocol­Error
    1. Constructor of IO.Error
  40. IO.Error.resource­Busy
    1. Constructor of IO.Error
  41. IO.Error.resource­Exhausted
    1. Constructor of IO.Error
  42. IO.Error.resource­Vanished
    1. Constructor of IO.Error
  43. IO.Error.time­Expired
    1. Constructor of IO.Error
  44. IO.Error.to­String
  45. IO.Error.unexpected­Eof
    1. Constructor of IO.Error
  46. IO.Error.unsatisfied­Constraints
    1. Constructor of IO.Error
  47. IO.Error.unsupported­Operation
    1. Constructor of IO.Error
  48. IO.Error.user­Error
    1. Constructor of IO.Error
  49. IO.FS.Dir­Entry
  50. IO.FS.DirEntry.mk
    1. Constructor of IO.FS.Dir­Entry
  51. IO.FS.DirEntry.path
  52. IO.FS.Handle
  53. IO.FS.Handle.flush
  54. IO.FS.Handle.get­Line
  55. IO.FS.Handle.is­Tty
  56. IO.FS.Handle.lock
  57. IO.FS.Handle.mk
  58. IO.FS.Handle.put­Str
  59. IO.FS.Handle.put­Str­Ln
  60. IO.FS.Handle.read
  61. IO.FS.Handle.read­Bin­To­End
  62. IO.FS.Handle.read­Bin­To­End­Into
  63. IO.FS.Handle.read­To­End
  64. IO.FS.Handle.rewind
  65. IO.FS.Handle.truncate
  66. IO.FS.Handle.try­Lock
  67. IO.FS.Handle.unlock
  68. IO.FS.Handle.write
  69. IO.FS.Metadata
  70. IO.FS.Metadata.mk
    1. Constructor of IO.FS.Metadata
  71. IO.FS.Mode
  72. IO.FS.Mode.append
    1. Constructor of IO.FS.Mode
  73. IO.FS.Mode.read
    1. Constructor of IO.FS.Mode
  74. IO.FS.Mode.read­Write
    1. Constructor of IO.FS.Mode
  75. IO.FS.Mode.write
    1. Constructor of IO.FS.Mode
  76. IO.FS.Mode.write­New
    1. Constructor of IO.FS.Mode
  77. IO.FS.Stream
  78. IO.FS.Stream.Buffer
  79. IO.FS.Stream.Buffer.data
  80. IO.FS.Stream.Buffer.mk
    1. Constructor of IO.FS.Stream.Buffer
  81. IO.FS.Stream.Buffer.pos
  82. IO.FS.Stream.mk
    1. Constructor of IO.FS.Stream
  83. IO.FS.Stream.of­Buffer
  84. IO.FS.Stream.of­Handle
  85. IO.FS.Stream.put­Str­Ln
  86. IO.FS.create­Dir
  87. IO.FS.create­Dir­All
  88. IO.FS.create­Temp­File
  89. IO.FS.lines
  90. IO.FS.read­Bin­File
  91. IO.FS.read­File
  92. IO.FS.real­Path
  93. IO.FS.remove­Dir
  94. IO.FS.remove­Dir­All
  95. IO.FS.remove­File
  96. IO.FS.rename
  97. IO.FS.with­File
  98. IO.FS.with­Isolated­Streams (0) (1)
  99. IO.FS.with­Temp­File
  100. IO.FS.write­Bin­File
  101. IO.FS.write­File
  102. IO.File­Right
  103. IO.FileRight.flags
  104. IO.FileRight.mk
    1. Constructor of IO.File­Right
  105. IO.Process.Child
  106. IO.Process.Child.kill
  107. IO.Process.Child.mk
    1. Constructor of IO.Process.Child
  108. IO.Process.Child.take­Stdin
  109. IO.Process.Child.try­Wait
  110. IO.Process.Child.wait
  111. IO.Process.Output
  112. IO.Process.Output.mk
    1. Constructor of IO.Process.Output
  113. IO.Process.Spawn­Args
  114. IO.Process.SpawnArgs.mk
    1. Constructor of IO.Process.Spawn­Args
  115. IO.Process.Stdio
  116. IO.Process.Stdio.inherit
    1. Constructor of IO.Process.Stdio
  117. IO.Process.Stdio.null
    1. Constructor of IO.Process.Stdio
  118. IO.Process.Stdio.piped
    1. Constructor of IO.Process.Stdio
  119. IO.Process.Stdio.to­Handle­Type
  120. IO.Process.Stdio­Config
  121. IO.Process.StdioConfig.mk
    1. Constructor of IO.Process.Stdio­Config
  122. IO.Process.exit
  123. IO.Process.get­Current­Dir
  124. IO.Process.get­PID
  125. IO.Process.output
  126. IO.Process.run
  127. IO.Process.set­Current­Dir
  128. IO.Process.spawn
  129. IO.Ref
  130. IO.add­Heartbeats
  131. IO.app­Dir
  132. IO.app­Path
  133. IO.as­Task
  134. IO.bind­Task
  135. IO.cancel
  136. IO.check­Canceled
  137. IO.current­Dir
  138. IO.eprint
  139. IO.eprintln
  140. IO.get­Env
  141. IO.get­Num­Heartbeats
  142. IO.get­Random­Bytes
  143. IO.get­Stderr
  144. IO.get­Stdin
  145. IO.get­Stdout
  146. IO.get­Task­State
  147. IO.has­Finished
  148. IO.iterate
  149. IO.lazy­Pure
  150. IO.map­Task
  151. IO.map­Tasks
  152. IO.mk­Ref
  153. IO.mono­Ms­Now
  154. IO.mono­Nanos­Now
  155. IO.of­Except
  156. IO.print
  157. IO.println
  158. IO.rand
  159. IO.set­Access­Rights
  160. IO.set­Rand­Seed
  161. IO.set­Stderr
  162. IO.set­Stdin
  163. IO.set­Stdout
  164. IO.sleep
  165. IO.to­EIO
  166. IO.user­Error
  167. IO.wait
  168. IO.wait­Any
  169. IO.with­Stderr
  170. IO.with­Stdin
  171. IO.with­Stdout
  172. ISize
  173. ISize.add
  174. ISize.complement
  175. ISize.dec­Eq
  176. ISize.dec­Le
  177. ISize.dec­Lt
  178. ISize.div
  179. ISize.land
  180. ISize.le
  181. ISize.lor
  182. ISize.lt
  183. ISize.mk
    1. Constructor of ISize
  184. ISize.mod
  185. ISize.mul
  186. ISize.neg
  187. ISize.of­Int
  188. ISize.of­Nat
  189. ISize.shift­Left
  190. ISize.shift­Right
  191. ISize.size
  192. ISize.sub
  193. ISize.to­Bit­Vec
  194. ISize.to­Int
  195. ISize.to­Int32
  196. ISize.to­Int64
  197. ISize.to­Nat
  198. ISize.xor
  199. Id
  200. Id.has­Bind
  201. Id.run
  202. Ident
    1. Lean.Syntax.Ident
  203. Inhabited
  204. Inhabited.mk
    1. Instance constructor of Inhabited
  205. Int
  206. Int.add
  207. Int.bdiv
  208. Int.bmod
  209. Int.cast
  210. Int.dec­Eq
  211. Int.ediv
  212. Int.emod
  213. Int.fdiv
  214. Int.fmod
  215. Int.from­Expr?
  216. Int.gcd
  217. Int.is­Pos­Value
  218. Int.lcm
  219. Int.le
  220. Int.lt
  221. Int.mul
  222. Int.nat­Abs
  223. Int.neg
  224. Int.neg­Of­Nat
  225. Int.neg­Succ
    1. Constructor of Int
  226. Int.not
  227. Int.of­Nat
    1. Constructor of Int
  228. Int.pow
  229. Int.reduce­Abs
  230. Int.reduce­Add
  231. Int.reduce­BEq
  232. Int.reduce­BNe
  233. Int.reduce­Bdiv
  234. Int.reduce­Bin
  235. Int.reduce­Bin­Int­Nat­Op
  236. Int.reduce­Bin­Pred
  237. Int.reduce­Bmod
  238. Int.reduce­Bool­Pred
  239. Int.reduce­Div
  240. Int.reduce­Eq
  241. Int.reduce­FDiv
  242. Int.reduce­FMod
  243. Int.reduce­GE
  244. Int.reduce­GT
  245. Int.reduce­LE
  246. Int.reduce­LT
  247. Int.reduce­Mod
  248. Int.reduce­Mul
  249. Int.reduce­Nat­Core
  250. Int.reduce­Ne
  251. Int.reduce­Neg
  252. Int.reduce­Neg­Succ
  253. Int.reduce­Of­Nat
  254. Int.reduce­Pow
  255. Int.reduce­Sub
  256. Int.reduce­TDiv
  257. Int.reduce­TMod
  258. Int.reduce­To­Nat
  259. Int.reduce­Unary
  260. Int.repr
  261. Int.shift­Right
  262. Int.sign
  263. Int.sub
  264. Int.sub­Nat­Nat
  265. Int.tdiv
  266. Int.tmod
  267. Int.to­ISize
  268. Int.to­Int16
  269. Int.to­Int32
  270. Int.to­Int64
  271. Int.to­Int8
  272. Int.to­Nat
  273. Int.to­Nat'
  274. Int16
  275. Int16.add
  276. Int16.complement
  277. Int16.dec­Eq
  278. Int16.dec­Le
  279. Int16.dec­Lt
  280. Int16.div
  281. Int16.land
  282. Int16.le
  283. Int16.lor
  284. Int16.lt
  285. Int16.mk
    1. Constructor of Int16
  286. Int16.mod
  287. Int16.mul
  288. Int16.neg
  289. Int16.of­Int
  290. Int16.of­Nat
  291. Int16.shift­Left
  292. Int16.shift­Right
  293. Int16.size
  294. Int16.sub
  295. Int16.to­Bit­Vec
  296. Int16.to­Int
  297. Int16.to­Int32 (0) (1)
  298. Int16.to­Int64
  299. Int16.to­Int8
  300. Int16.to­Nat
  301. Int16.xor
  302. Int32
  303. Int32.add
  304. Int32.complement
  305. Int32.dec­Eq
  306. Int32.dec­Le
  307. Int32.dec­Lt
  308. Int32.div
  309. Int32.land
  310. Int32.le
  311. Int32.lor
  312. Int32.lt
  313. Int32.mk
    1. Constructor of Int32
  314. Int32.mod
  315. Int32.mul
  316. Int32.neg
  317. Int32.of­Int
  318. Int32.of­Nat
  319. Int32.shift­Left
  320. Int32.shift­Right
  321. Int32.size
  322. Int32.sub
  323. Int32.to­Bit­Vec
  324. Int32.to­ISize
  325. Int32.to­Int
  326. Int32.to­Int16
  327. Int32.to­Int64
  328. Int32.to­Int8
  329. Int32.to­Nat
  330. Int32.xor
  331. Int64
  332. Int64.add
  333. Int64.complement
  334. Int64.dec­Eq
  335. Int64.dec­Le
  336. Int64.dec­Lt
  337. Int64.div
  338. Int64.land
  339. Int64.le
  340. Int64.lor
  341. Int64.lt
  342. Int64.mk
    1. Constructor of Int64
  343. Int64.mod
  344. Int64.mul
  345. Int64.neg
  346. Int64.of­Int
  347. Int64.of­Nat
  348. Int64.shift­Left
  349. Int64.shift­Right
  350. Int64.size
  351. Int64.sub
  352. Int64.to­Bit­Vec
  353. Int64.to­ISize
  354. Int64.to­Int
  355. Int64.to­Int16
  356. Int64.to­Int32
  357. Int64.to­Int8
  358. Int64.to­Nat
  359. Int64.xor
  360. Int8
  361. Int8.add
  362. Int8.complement
  363. Int8.dec­Eq
  364. Int8.dec­Le
  365. Int8.dec­Lt
  366. Int8.div
  367. Int8.land
  368. Int8.le
  369. Int8.lor
  370. Int8.lt
  371. Int8.mk
    1. Constructor of Int8
  372. Int8.mod
  373. Int8.mul
  374. Int8.neg
  375. Int8.of­Int
  376. Int8.of­Nat
  377. Int8.shift­Left
  378. Int8.shift­Right
  379. Int8.size
  380. Int8.sub
  381. Int8.to­Bit­Vec
  382. Int8.to­Int
  383. Int8.to­Int16
  384. Int8.to­Int32 (0) (1)
  385. Int8.to­Int64
  386. Int8.to­Nat
  387. Int8.xor
  388. Int­Cast
  389. IntCast.mk
    1. Instance constructor of Int­Cast
  390. Iterator
    1. String.Iterator
  391. i
    1. String.Iterator.i (structure field)
  392. ibelow
    1. Nat.ibelow
  393. id_map
    1. LawfulFunctor.id_map (class method)
  394. ident­Kind
    1. Lean.ident­Kind
  395. identifier
    1. raw
  396. if ... then ... else ...
  397. if h : ... then ... else ...
  398. imax
    1. Nat.imax
  399. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  400. impredicative
  401. inaccessible
  402. index
    1. Lean.Meta.DSimp.Config.index (structure field)
    2. Lean.Meta.Simp.Config.index (structure field)
    3. of inductive type
  403. index­Of?
    1. Array.index­Of?
  404. indexed family
    1. of types
  405. induction
    1. Fin.induction
  406. induction­On
    1. Fin.induction­On
    2. Nat.div.induction­On
    3. Nat.mod.induction­On
  407. inductive.auto­Promote­Indices
  408. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  409. infer­Instance
  410. infer­Instance­As
  411. infer_instance
  412. init (Lake command)
  413. injection
  414. injections
  415. insert­At
    1. Array.insert­At
  416. insert­At!
    1. Array.insert­At!
  417. insertion­Sort
    1. Array.insertion­Sort
  418. instance synthesis
  419. int­Cast
    1. IntCast.int­Cast (class method)
  420. intercalate
    1. String.intercalate
  421. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  422. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  423. intro (0) (1)
  424. intro | ... => ... | ... => ...
  425. intros
  426. inv­Image
  427. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  428. is­Absolute
    1. System.FilePath.is­Absolute
  429. is­Alpha
    1. Char.is­Alpha
  430. is­Alphanum
    1. Char.is­Alphanum
  431. is­Digit
    1. Char.is­Digit
  432. is­Dir
    1. System.FilePath.is­Dir
  433. is­Empty
    1. Array.is­Empty
    2. String.is­Empty
  434. is­Eq­Some
    1. Option.is­Eq­Some
  435. is­Eqv
    1. Array.is­Eqv
  436. is­Int
    1. String.is­Int
  437. is­Lower
    1. Char.is­Lower
  438. is­Lt
    1. Fin.is­Lt (structure field)
  439. is­Nat
    1. String.is­Nat
  440. is­None
    1. Option.is­None
  441. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  442. is­Ok
    1. Except.is­Ok
  443. is­Pos­Value
    1. Int.is­Pos­Value
  444. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  445. is­Prefix­Of
    1. Array.is­Prefix­Of
    2. String.is­Prefix­Of
  446. is­Relative
    1. System.FilePath.is­Relative
  447. is­Some
    1. Option.is­Some
  448. is­Tty
    1. IO.FS.Handle.is­Tty
    2. IO.FS.Stream.is­Tty (structure field)
  449. is­Upper
    1. Char.is­Upper
  450. is­Valid
    1. String.Pos.is­Valid
  451. is­Valid­Char
    1. Nat.is­Valid­Char
    2. UInt32.is­Valid­Char
  452. is­Value
    1. Fin.is­Value
    2. Nat.is­Value
  453. is­Whitespace
    1. Char.is­Whitespace
  454. iter
    1. String.iter
  455. iterate
    1. IO.iterate

J

  1. join
    1. Option.join
    2. String.join
    3. System.FilePath.join

K

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

L

  1. LAKE (environment variable)
  2. LAKE_HOME (environment variable)
  3. LAKE_NO_CACHE (environment variable)
  4. LAKE_OVERRIDE_LEAN (environment variable)
  5. LE
  6. LE.mk
    1. Instance constructor of LE
  7. LEAN (environment variable)
  8. LEAN_AR (environment variable)
  9. LEAN_CC (environment variable)
  10. LEAN_SYSROOT (environment variable)
  11. LT
  12. LT.mk
    1. Instance constructor of LT
  13. Lake.Backend
  14. Lake.Backend.c
    1. Constructor of Lake.Backend
  15. Lake.Backend.default
    1. Constructor of Lake.Backend
  16. Lake.Backend.llvm
    1. Constructor of Lake.Backend
  17. Lake.Build­Type
  18. Lake.BuildType.debug
    1. Constructor of Lake.Build­Type
  19. Lake.BuildType.min­Size­Rel
    1. Constructor of Lake.Build­Type
  20. Lake.BuildType.rel­With­Deb­Info
    1. Constructor of Lake.Build­Type
  21. Lake.BuildType.release
    1. Constructor of Lake.Build­Type
  22. Lake.Glob
  23. Lake.Glob.and­Submodules
    1. Constructor of Lake.Glob
  24. Lake.Glob.one
    1. Constructor of Lake.Glob
  25. Lake.Glob.submodules
    1. Constructor of Lake.Glob
  26. Lake.Lean­Exe­Config
  27. Lake.Lean­ExeConfig.mk
    1. Constructor of Lake.Lean­Exe­Config
  28. Lake.Lean­Lib­Config
  29. Lake.Lean­LibConfig.mk
    1. Constructor of Lake.Lean­Lib­Config
  30. Lake.Lean­Option
  31. Lake.LeanOption.mk
    1. Constructor of Lake.Lean­Option
  32. Lake.Monad­Lake­Env
  33. Lake.Monad­Workspace
  34. Lake.MonadWorkspace.mk
    1. Instance constructor of Lake.Monad­Workspace
  35. Lake.Script­M (0) (1)
  36. Lake.find­Extern­Lib?
  37. Lake.find­Lean­Exe?
  38. Lake.find­Lean­Lib?
  39. Lake.find­Module?
  40. Lake.find­Package?
  41. Lake.get­Augmented­Env
  42. Lake.get­Augmented­Lean­Path
  43. Lake.get­Augmented­Lean­Src­Path
  44. Lake.get­Augmented­Shared­Lib­Path
  45. Lake.get­Elan?
  46. Lake.get­Elan­Home?
  47. Lake.get­Elan­Install?
  48. Lake.get­Elan­Toolchain
  49. Lake.get­Env­Lean­Path
  50. Lake.get­Env­Lean­Src­Path
  51. Lake.get­Env­Shared­Lib­Path
  52. Lake.get­Lake
  53. Lake.get­Lake­Env
  54. Lake.get­Lake­Home
  55. Lake.get­Lake­Install
  56. Lake.get­Lake­Lib­Dir
  57. Lake.get­Lake­Src­Dir
  58. Lake.get­Lean
  59. Lake.get­Lean­Ar
  60. Lake.get­Lean­Cc
  61. Lake.get­Lean­Cc?
  62. Lake.get­Lean­Include­Dir
  63. Lake.get­Lean­Install
  64. Lake.get­Lean­Lib­Dir
  65. Lake.get­Lean­Path
  66. Lake.get­Lean­Shared­Lib
  67. Lake.get­Lean­Src­Dir
  68. Lake.get­Lean­Src­Path
  69. Lake.get­Lean­Sysroot
  70. Lake.get­Lean­System­Lib­Dir
  71. Lake.get­Leanc
  72. Lake.get­No­Cache
  73. Lake.get­Pkg­Url­Map
  74. Lake.get­Root­Package
  75. Lake.get­Shared­Lib­Path
  76. Lake.get­Try­Cache
  77. Lawful­Applicative
  78. LawfulApplicative.mk
    1. Instance constructor of Lawful­Applicative
  79. Lawful­BEq
  80. LawfulBEq.mk
    1. Instance constructor of Lawful­BEq
  81. Lawful­Functor
  82. LawfulFunctor.mk
    1. Instance constructor of Lawful­Functor
  83. Lawful­Get­Elem
  84. Lawful­GetElem.mk
    1. Instance constructor of Lawful­Get­Elem
  85. Lawful­Monad
  86. LawfulMonad.mk
    1. Instance constructor of Lawful­Monad
  87. LawfulMonad.mk'
  88. Leading­Ident­Behavior
    1. Lean.Parser.Leading­Ident­Behavior
  89. Lean.Elab.Tactic.Tactic
  90. Lean.Elab.Tactic.Tactic­M
  91. Lean.Elab.Tactic.adapt­Expander
  92. Lean.Elab.Tactic.append­Goals
  93. Lean.Elab.Tactic.close­Main­Goal
  94. Lean.Elab.Tactic.close­Main­Goal­Using
  95. Lean.Elab.Tactic.dsimp­Location'
  96. Lean.Elab.Tactic.elab­Cases­Targets
  97. Lean.Elab.Tactic.elab­DSimp­Config­Core
  98. Lean.Elab.Tactic.elab­Simp­Args
  99. Lean.Elab.Tactic.elab­Simp­Config
  100. Lean.Elab.Tactic.elab­Simp­Config­Ctx­Core
  101. Lean.Elab.Tactic.elab­Term
  102. Lean.Elab.Tactic.elab­Term­Ensuring­Type
  103. Lean.Elab.Tactic.elab­Term­With­Holes
  104. Lean.Elab.Tactic.ensure­Has­No­MVars
  105. Lean.Elab.Tactic.focus
  106. Lean.Elab.Tactic.get­Curr­Macro­Scope
  107. Lean.Elab.Tactic.get­FVar­Id
  108. Lean.Elab.Tactic.get­FVar­Ids
  109. Lean.Elab.Tactic.get­Goals
  110. Lean.Elab.Tactic.get­Main­Goal
  111. Lean.Elab.Tactic.get­Main­Module
  112. Lean.Elab.Tactic.get­Main­Tag
  113. Lean.Elab.Tactic.get­Unsolved­Goals
  114. Lean.Elab.Tactic.lift­Meta­MAt­Main
  115. Lean.Elab.Tactic.mk­Tactic­Attribute
  116. Lean.Elab.Tactic.or­Else
  117. Lean.Elab.Tactic.prune­Solved­Goals
  118. Lean.Elab.Tactic.run
  119. Lean.Elab.Tactic.run­Term­Elab
  120. Lean.Elab.Tactic.set­Goals
  121. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  122. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  123. Lean.Elab.Tactic.tactic­Elab­Attribute
  124. Lean.Elab.Tactic.tag­Untagged­Goals
  125. Lean.Elab.Tactic.try­Catch
  126. Lean.Elab.Tactic.try­Tactic
  127. Lean.Elab.Tactic.try­Tactic?
  128. Lean.Elab.Tactic.with­Location
  129. Lean.Elab.register­Deriving­Handler
  130. Lean.Macro.Exception.unsupported­Syntax
  131. Lean.Macro.add­Macro­Scope
  132. Lean.Macro.expand­Macro?
  133. Lean.Macro.get­Curr­Namespace
  134. Lean.Macro.has­Decl
  135. Lean.Macro.resolve­Global­Name
  136. Lean.Macro.resolve­Namespace
  137. Lean.Macro.throw­Error
  138. Lean.Macro.throw­Error­At
  139. Lean.Macro.throw­Unsupported
  140. Lean.Macro.trace
  141. Lean.Macro.with­Fresh­Macro­Scope
  142. Lean.Macro­M
  143. Lean.Meta.DSimp.Config
  144. Lean.Meta.DSimp.Config.mk
    1. Constructor of Lean.Meta.DSimp.Config
  145. Lean.Meta.Occurrences
  146. Lean.Meta.Occurrences.all
    1. Constructor of Lean.Meta.Occurrences
  147. Lean.Meta.Occurrences.neg
    1. Constructor of Lean.Meta.Occurrences
  148. Lean.Meta.Occurrences.pos
    1. Constructor of Lean.Meta.Occurrences
  149. Lean.Meta.Rewrite.Config
  150. Lean.Meta.Rewrite.Config.mk
    1. Constructor of Lean.Meta.Rewrite.Config
  151. Lean.Meta.Rewrite.New­Goals
  152. Lean.Meta.Simp.Config
  153. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  154. Lean.Meta.Simp.neutral­Config
  155. Lean.Meta.Simp­Extension
  156. Lean.Meta.Transparency­Mode
  157. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.Transparency­Mode
  158. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.Transparency­Mode
  159. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.Transparency­Mode
  160. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.Transparency­Mode
  161. Lean.Meta.register­Simp­Attr
  162. Lean.Parser.Leading­Ident­Behavior
  163. Lean.Parser.Leading­IdentBehavior.both
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  164. Lean.Parser.Leading­IdentBehavior.default
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  165. Lean.Parser.Leading­IdentBehavior.symbol
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  166. Lean.Source­Info
  167. Lean.SourceInfo.none
    1. Constructor of Lean.Source­Info
  168. Lean.SourceInfo.original
    1. Constructor of Lean.Source­Info
  169. Lean.SourceInfo.synthetic
    1. Constructor of Lean.Source­Info
  170. Lean.Syntax
  171. Lean.Syntax.Char­Lit
  172. Lean.Syntax.Command
  173. Lean.Syntax.Hygiene­Info
  174. Lean.Syntax.Ident
  175. Lean.Syntax.Level
  176. Lean.Syntax.Name­Lit
  177. Lean.Syntax.Num­Lit
  178. Lean.Syntax.Prec
  179. Lean.Syntax.Preresolved
  180. Lean.Syntax.Preresolved.decl
    1. Constructor of Lean.Syntax.Preresolved
  181. Lean.Syntax.Preresolved.namespace
    1. Constructor of Lean.Syntax.Preresolved
  182. Lean.Syntax.Prio
  183. Lean.Syntax.Scientific­Lit
  184. Lean.Syntax.Str­Lit
  185. Lean.Syntax.TSep­Array
  186. Lean.Syntax.TSepArray.mk
    1. Constructor of Lean.Syntax.TSep­Array
  187. Lean.Syntax.Tactic
  188. Lean.Syntax.Term
  189. Lean.Syntax.atom
    1. Constructor of Lean.Syntax
  190. Lean.Syntax.get­Kind
  191. Lean.Syntax.ident
    1. Constructor of Lean.Syntax
  192. Lean.Syntax.is­Of­Kind
  193. Lean.Syntax.missing
    1. Constructor of Lean.Syntax
  194. Lean.Syntax.node
    1. Constructor of Lean.Syntax
  195. Lean.Syntax.set­Kind
  196. Lean.Syntax­Node­Kind
  197. Lean.TSyntax
  198. Lean.TSyntax.get­Char
  199. Lean.TSyntax.get­Hygiene­Info
  200. Lean.TSyntax.get­Id
  201. Lean.TSyntax.get­Name
  202. Lean.TSyntax.get­Nat
  203. Lean.TSyntax.get­Scientific
  204. Lean.TSyntax.get­String
  205. Lean.TSyntax.mk
    1. Constructor of Lean.TSyntax
  206. Lean.TSyntax­Array
  207. Lean.char­Lit­Kind
  208. Lean.choice­Kind
  209. Lean.field­Idx­Kind
  210. Lean.group­Kind
  211. Lean.hygiene­Info­Kind
  212. Lean.ident­Kind
  213. Lean.interpolated­Str­Kind
  214. Lean.interpolated­Str­Lit­Kind
  215. Lean.name­Lit­Kind
  216. Lean.null­Kind
  217. Lean.num­Lit­Kind
  218. Lean.scientific­Lit­Kind
  219. Lean.str­Lit­Kind
  220. Lean­Exe­Config
    1. Lake.Lean­Exe­Config
  221. Lean­Lib­Config
    1. Lake.Lean­Lib­Config
  222. Lean­Option
    1. Lake.Lean­Option
  223. Level
    1. Lean.Syntax.Level
  224. List
  225. List.cons
    1. Constructor of List
  226. List.nil
    1. Constructor of List
  227. land
    1. Fin.land
    2. ISize.land
    3. Int16.land
    4. Int32.land
    5. Int64.land
    6. Int8.land
    7. Nat.land
    8. UInt16.land
    9. UInt32.land
    10. UInt64.land
    11. UInt8.land
    12. USize.land
  228. last
    1. Fin.last
  229. last­Cases
    1. Fin.last­Cases
  230. lazy­Pure
    1. IO.lazy­Pure
  231. lcm
    1. Int.lcm
    2. Nat.lcm
  232. le
    1. ISize.le
    2. Int.le
    3. Int16.le
    4. Int32.le
    5. Int64.le
    6. Int8.le
    7. LE.le (class method)
    8. Nat.le
    9. String.le
    10. UInt16.le
    11. UInt64.le
    12. UInt8.le
    13. USize.le
  233. lean (Lake command)
  234. lean_is_array
  235. lean_is_string
  236. lean_string_object (0) (1)
  237. lean_to_array
  238. lean_to_string
  239. left (0) (1)
  240. length
    1. String.length
  241. let
  242. let rec
  243. let'
  244. let­I
  245. level
    1. of universe
  246. lhs
  247. lib­Name
    1. [anonymous] (structure field)
  248. lift
    1. Except­CpsT.lift
    2. ExceptT.lift
    3. OptionT.lift
    4. State­CpsT.lift
    5. State­RefT'.lift
    6. StateT.lift
  249. lift­Meta­MAt­Main
    1. Lean.Elab.Tactic.lift­Meta­MAt­Main
  250. lift­Or­Get
    1. Option.lift­Or­Get
  251. lift­With
    1. MonadControl.lift­With (class method)
    2. Monad­ControlT.lift­With (class method)
  252. line­Eq
  253. lines
    1. IO.FS.lines
  254. lint (Lake command)
  255. linter.unnecessary­Simpa
  256. literal
    1. raw string
    2. string
  257. lock
    1. IO.FS.Handle.lock
  258. log2
    1. Fin.log2
    2. Nat.log2
    3. UInt16.log2
    4. UInt32.log2
    5. UInt64.log2
    6. UInt8.log2
    7. USize.log2
  259. lor
    1. Fin.lor
    2. ISize.lor
    3. Int16.lor
    4. Int32.lor
    5. Int64.lor
    6. Int8.lor
    7. Nat.lor
    8. UInt16.lor
    9. UInt32.lor
    10. UInt64.lor
    11. UInt8.lor
    12. USize.lor
  260. lt
    1. ISize.lt
    2. Int.lt
    3. Int16.lt
    4. Int32.lt
    5. Int64.lt
    6. Int8.lt
    7. LT.lt (class method)
    8. Nat.lt
    9. Option.lt
    10. UInt16.lt
    11. UInt64.lt
    12. UInt8.lt
    13. USize.lt
  261. lt_wf­Rel
    1. Nat.lt_wf­Rel

M

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

N

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

O

  1. Occurrences
    1. Lean.Meta.Occurrences
  2. Of­Nat
  3. OfNat.mk
    1. Instance constructor of Of­Nat
  4. Of­Scientific
  5. OfScientific.mk
    1. Instance constructor of Of­Scientific
  6. Option
  7. Option.all
  8. Option.any
  9. Option.attach
  10. Option.attach­With
  11. Option.bind
  12. Option.bind­M
  13. Option.choice
  14. Option.decidable_eq_none
  15. Option.elim
  16. Option.elim­M
  17. Option.filter
  18. Option.for­M
  19. Option.format
  20. Option.get
  21. Option.get!
  22. Option.get­D
  23. Option.get­DM
  24. Option.get­M
  25. Option.guard
  26. Option.is­Eq­Some
  27. Option.is­None
  28. Option.is­Some
  29. Option.join
  30. Option.lift­Or­Get
  31. Option.lt
  32. Option.map
  33. Option.map­A
  34. Option.map­M
  35. Option.max
  36. Option.merge
  37. Option.min
  38. Option.none
    1. Constructor of Option
  39. Option.or
  40. Option.or­Else
  41. Option.pbind
  42. Option.pelim
  43. Option.pmap
  44. Option.repr
  45. Option.sequence
  46. Option.some
    1. Constructor of Option
  47. Option.to­Array
  48. Option.to­List
  49. Option.try­Catch
  50. Option.unattach
  51. Option­T
  52. OptionT.bind
  53. OptionT.fail
  54. OptionT.lift
  55. OptionT.mk
  56. OptionT.or­Else
  57. OptionT.pure
  58. OptionT.run
  59. OptionT.try­Catch
  60. Ord
  61. Ord.mk
    1. Instance constructor of Ord
  62. Ordering
  63. Ordering.eq
    1. Constructor of Ordering
  64. Ordering.gt
    1. Constructor of Ordering
  65. Ordering.lt
    1. Constructor of Ordering
  66. Output
    1. IO.Process.Output
  67. obtain
  68. occs
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  69. of­Buffer
    1. IO.FS.Stream.of­Buffer
  70. of­Except
    1. IO.of­Except
    2. MonadExcept.of­Except
  71. of­Fn
    1. Array.of­Fn
  72. of­Handle
    1. IO.FS.Stream.of­Handle
  73. of­Int
    1. ISize.of­Int
    2. Int16.of­Int
    3. Int32.of­Int
    4. Int64.of­Int
    5. Int8.of­Int
  74. of­Nat
    1. ISize.of­Nat
    2. Int16.of­Nat
    3. Int32.of­Nat
    4. Int64.of­Nat
    5. Int8.of­Nat
    6. OfNat.of­Nat (class method)
    7. UInt16.of­Nat
    8. UInt32.of­Nat
    9. UInt64.of­Nat
    10. UInt8.of­Nat
    11. USize.of­Nat
  75. of­Nat'
    1. Fin.of­Nat'
    2. UInt32.of­Nat'
  76. of­Nat32
    1. USize.of­Nat32
  77. of­Nat­Core
    1. UInt16.of­Nat­Core
    2. UInt32.of­Nat­Core
    3. UInt64.of­Nat­Core
    4. UInt8.of­Nat­Core
    5. USize.of­Nat­Core
  78. of­Nat­Truncate
    1. UInt32.of­Nat­Truncate
  79. of­Scientific
    1. OfScientific.of­Scientific (class method)
  80. of­Subarray
    1. Array.of­Subarray
  81. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  82. offset­Of­Pos
    1. String.offset­Of­Pos
  83. omega
  84. open
  85. opt­Param
  86. optional
  87. or
    1. Bool.or
    2. Option.or
  88. or­Else
    1. EStateM.or­Else
    2. Lean.Elab.Tactic.or­Else
    3. MonadExcept.or­Else
    4. Option.or­Else
    5. OptionT.or­Else
    6. ReaderT.or­Else
    7. StateT.or­Else
    8. [anonymous] (class method)
  89. or­Else'
    1. EStateM.or­Else'
  90. or­Else­Lazy
    1. Except.or­Else­Lazy
  91. or­M
  92. orelse'
    1. MonadExcept.orelse'
  93. other
    1. IO.FileRight.other (structure field)
  94. other­Error­To­String
    1. IO.Error.other­Error­To­String
  95. out
    1. NeZero.out (class method)
  96. out­Param
  97. output
    1. IO.Process.output

P

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

R

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

S

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

T

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

U

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

V

  1. val
    1. Char.val (structure field)
    2. Fin.val (structure field)
    3. Subtype.val (structure field)
    4. UInt16.val
    5. UInt32.val
    6. UInt64.val
    7. UInt8.val
    8. USize.val
  2. valid
    1. Char.valid (structure field)
  3. validate­UTF8
    1. String.validate­UTF8
  4. value
    1. Lake.LeanOption.value (structure field)

W

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

X

  1. xor
    1. Bool.xor
    2. Fin.xor
    3. ISize.xor
    4. Int16.xor
    5. Int32.xor
    6. Int64.xor
    7. Int8.xor
    8. Nat.xor
    9. UInt16.xor
    10. UInt32.xor
    11. UInt64.xor
    12. UInt8.xor
    13. USize.xor

Z

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