Index

Symbols

  1. ( ... )
  2. . ...
  3. <;> (0) (1)
  4. _private.Init.Dynamic.0.TypeName.mk'
    1. Instance constructor of Type­Name
  5. { ... }
  6. ·
  7. · ...
  8. Σ-types
  9. ι-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. List.all
    3. Nat.all
    4. Option.all
    5. String.all
    6. Subarray.all
  150. all­Diff
    1. Array.all­Diff
  151. all­I
    1. Prod.all­I
  152. all­M
    1. Array.all­M
    2. List.all­M
    3. Nat.all­M
    4. Subarray.all­M
  153. all­TR
    1. Nat.all­TR
  154. all_goals (0) (1)
  155. and
    1. Bool.and
    2. List.and
  156. and­M
  157. and_intros
  158. any
    1. Array.any
    2. List.any
    3. Nat.any
    4. Option.any
    5. String.any
    6. Subarray.any
  159. any­I
    1. Prod.any­I
  160. any­M
    1. Array.any­M
    2. List.any­M
    3. Nat.any­M
    4. Subarray.any­M
  161. any­TR
    1. Nat.any­TR
  162. any_goals (0) (1)
  163. app­Dir
    1. IO.app­Dir
  164. app­Path
    1. IO.app­Path
  165. append
    1. Append.append (class method)
    2. Array.append
    3. List.append
    4. String.append
  166. append­Goals
    1. Lean.Elab.Tactic.append­Goals
  167. append­List
    1. Array.append­List
  168. append­TR
    1. List.append­TR
  169. apply (0) (1)
  170. apply?
  171. apply­Eq­Lemma
    1. Nat.apply­Eq­Lemma
  172. apply­Simproc­Const
    1. Nat.apply­Simproc­Const
  173. apply_assumption
  174. apply_ext_theorem
  175. apply_mod_cast
  176. apply_rfl
  177. apply_rules
  178. arg [@]i
  179. args
    1. [anonymous] (structure field)
  180. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  181. array
    1. Subarray.array (structure field)
  182. as­String
    1. List.as­String
  183. as­Task
    1. BaseIO.as­Task
    2. EIO.as­Task
    3. IO.as­Task
  184. assumption
    1. inaccessible
  185. assumption_mod_cast
  186. at­End
    1. String.Iterator.at­End
    2. String.at­End
  187. at­Least­Two
    1. Bool.at­Least­Two
  188. attach
    1. Array.attach
    2. List.attach
    3. Option.attach
  189. attach­With
    1. Array.attach­With
    2. List.attach­With
    3. Option.attach­With
  190. auto­Lift
  191. auto­Param
  192. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  193. 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. List.beq
    3. 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. binder­Name­Hint
  60. bitwise
    1. Nat.bitwise
  61. ble
    1. Nat.ble
  62. blt
    1. Nat.blt
  63. bmod
    1. Int.bmod
  64. bootstrap.inductive­Check­Resulting­Universe
  65. build (Lake command)
  66. bv_check
  67. bv_decide
  68. bv_decide?
  69. bv_normalize
  70. bv_omega
  71. by­Cases
    1. Decidable.by­Cases
  72. by_cases
  73. byte­Idx
    1. String.Pos.byte­Idx (structure field)
  74. byte­Size
    1. IO.FS.Metadata.byte­Size (structure field)

C

  1. CC (environment variable)
  2. CCPO
    1. Lean.Order.CCPO
  3. Char
  4. Char.is­Alpha
  5. Char.is­Alphanum
  6. Char.is­Digit
  7. Char.is­Lower
  8. Char.is­Upper
  9. Char.is­Whitespace
  10. Char.mk
    1. Constructor of Char
  11. Char­Lit
    1. Lean.Syntax.Char­Lit
  12. Child
    1. IO.Process.Child
  13. Coe
  14. Coe.mk
    1. Instance constructor of Coe
  15. Coe­Dep
  16. CoeDep.mk
    1. Instance constructor of Coe­Dep
  17. Coe­Fun
  18. CoeFun.mk
    1. Instance constructor of Coe­Fun
  19. Coe­HTC
  20. CoeHTC.mk
    1. Instance constructor of Coe­HTC
  21. Coe­HTCT
  22. CoeHTCT.mk
    1. Instance constructor of Coe­HTCT
  23. Coe­Head
  24. CoeHead.mk
    1. Instance constructor of Coe­Head
  25. Coe­OTC
  26. CoeOTC.mk
    1. Instance constructor of Coe­OTC
  27. Coe­Out
  28. CoeOut.mk
    1. Instance constructor of Coe­Out
  29. Coe­Sort
  30. CoeSort.mk
    1. Instance constructor of Coe­Sort
  31. Coe­T
  32. CoeT.mk
    1. Instance constructor of Coe­T
  33. Coe­TC
  34. CoeTC.mk
    1. Instance constructor of Coe­TC
  35. Coe­Tail
  36. CoeTail.mk
    1. Instance constructor of Coe­Tail
  37. Command
    1. Lean.Syntax.Command
  38. Config
    1. Lean.Meta.DSimp.Config
    2. Lean.Meta.Rewrite.Config
    3. Lean.Meta.Simp.Config
  39. calc
  40. cancel
    1. IO.cancel
  41. canon­Instances
    1. backward.synthInstance.canon­Instances
  42. capitalize
    1. String.capitalize
  43. case
  44. case ... => ...
  45. case'
  46. case' ... => ...
  47. case­Strong­Induction­On
    1. Nat.case­Strong­Induction­On
  48. cases
    1. Fin.cases
  49. cases­On
    1. Nat.cases­On
  50. cast
    1. Fin.cast
    2. Int.cast
    3. Nat.cast
  51. cast­Add
    1. Fin.cast­Add
  52. cast­LE
    1. Fin.cast­LE
  53. cast­LT
    1. Fin.cast­LT
  54. cast­Succ
    1. Fin.cast­Succ
  55. catch­Exceptions
    1. EIO.catch­Exceptions
  56. chain
    1. of coercions
  57. change (0) (1)
  58. change ... with ...
  59. char­Lit­Kind
    1. Lean.char­Lit­Kind
  60. check-build (Lake command)
  61. check-lint (Lake command)
  62. check-test (Lake command)
  63. check­Canceled
    1. IO.check­Canceled
  64. checkpoint
  65. choice
    1. Option.choice
  66. choice­Kind
    1. Lean.choice­Kind
  67. clean (Lake command)
  68. clear
  69. close­Main­Goal
    1. Lean.Elab.Tactic.close­Main­Goal
  70. close­Main­Goal­Using
    1. Lean.Elab.Tactic.close­Main­Goal­Using
  71. cmd
    1. [anonymous] (structure field)
  72. codepoint­Pos­To­Utf16Pos
    1. String.codepoint­Pos­To­Utf16Pos
  73. codepoint­Pos­To­Utf16Pos­From
    1. String.codepoint­Pos­To­Utf16Pos­From
  74. codepoint­Pos­To­Utf8Pos­From
    1. String.codepoint­Pos­To­Utf8Pos­From
  75. coe
    1. Coe.coe (class method)
    2. CoeDep.coe (class method)
    3. CoeFun.coe (class method)
    4. CoeHTC.coe (class method)
    5. CoeHTCT.coe (class method)
    6. CoeHead.coe (class method)
    7. CoeOTC.coe (class method)
    8. CoeOut.coe (class method)
    9. CoeSort.coe (class method)
    10. CoeT.coe (class method)
    11. CoeTC.coe (class method)
    12. CoeTail.coe (class method)
  76. col­Eq
  77. col­Ge
  78. col­Gt
  79. comment
    1. block
    2. line
  80. comp_map
    1. LawfulFunctor.comp_map (class method)
  81. compare
    1. Ord.compare (class method)
  82. 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
  83. components
    1. System.FilePath.components
  84. concat
    1. List.concat
  85. concat­Map
    1. Array.concat­Map
  86. concat­Map­M
    1. Array.concat­Map­M
  87. cond
  88. configuration
    1. of tactics
  89. congr (0) (1)
  90. constructor (0) (1)
  91. contains
    1. Array.contains
    2. List.contains
    3. String.contains
  92. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  93. contradiction
  94. control
  95. control­At
  96. conv
  97. conv => ...
  98. conv' (0) (1)
  99. count
    1. List.count
  100. count­P
    1. List.count­P
  101. create­Dir
    1. IO.FS.create­Dir
  102. create­Dir­All
    1. IO.FS.create­Dir­All
  103. create­Temp­File
    1. IO.FS.create­Temp­File
  104. crlf­To­Lf
    1. String.crlf­To­Lf
  105. csup
    1. [anonymous] (class method)
  106. csup_spec
    1. [anonymous] (class method)
  107. cumulativity
  108. curr
    1. String.Iterator.curr
  109. current­Dir
    1. IO.current­Dir
  110. custom­Eliminators
    1. tactic.custom­Eliminators
  111. 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. diff
    1. guard_msgs.diff
  35. digit­Char
    1. Nat.digit­Char
  36. discard
    1. Functor.discard
  37. discharge
    1. trace.Meta.Tactic.simp.discharge
  38. 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
  39. div2Induction
    1. Nat.div2Induction
  40. done (0) (1)
  41. down
    1. PLift.down (structure field)
    2. ULift.down (structure field)
  42. drop
    1. List.drop
    2. String.drop
    3. Subarray.drop
  43. drop­Last
    1. List.drop­Last
  44. drop­Last­TR
    1. List.drop­Last­TR
  45. drop­Right
    1. String.drop­Right
  46. drop­Right­While
    1. String.drop­Right­While
  47. drop­While
    1. List.drop­While
    2. String.drop­While
  48. dsimp (0) (1)
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  49. dsimp!
  50. dsimp?
  51. dsimp?!
  52. dsimp­Location'
    1. Lean.Elab.Tactic.dsimp­Location'
  53. 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. Equiv
    1. HasEquiv.Equiv (class method)
  38. Equivalence
  39. Equivalence.mk
    1. Constructor of Equivalence
  40. Error
    1. IO.Error
  41. Even
  42. Even.plus­Two
    1. Constructor of Even
  43. Even.zero
    1. Constructor of Even
  44. Except
  45. Except.bind
  46. Except.error
    1. Constructor of Except
  47. Except.is­Ok
  48. Except.map
  49. Except.map­Error
  50. Except.ok
    1. Constructor of Except
  51. Except.or­Else­Lazy
  52. Except.pure
  53. Except.to­Bool
  54. Except.to­Option
  55. Except.try­Catch
  56. Except­Cps­T
  57. Except­CpsT.lift
  58. Except­CpsT.run
  59. Except­CpsT.run­Catch
  60. Except­CpsT.run­K
  61. Except­T
  62. ExceptT.adapt
  63. ExceptT.bind
  64. ExceptT.bind­Cont
  65. ExceptT.lift
  66. ExceptT.map
  67. ExceptT.mk
  68. ExceptT.pure
  69. ExceptT.run
  70. ExceptT.try­Catch
  71. ediv
    1. Int.ediv
  72. elab­Cases­Targets
    1. Lean.Elab.Tactic.elab­Cases­Targets
  73. elab­DSimp­Config­Core
    1. Lean.Elab.Tactic.elab­DSimp­Config­Core
  74. elab­Simp­Args
    1. Lean.Elab.Tactic.elab­Simp­Args
  75. elab­Simp­Config
    1. Lean.Elab.Tactic.elab­Simp­Config
  76. elab­Simp­Config­Ctx­Core
    1. Lean.Elab.Tactic.elab­Simp­Config­Ctx­Core
  77. elab­Term
    1. Lean.Elab.Tactic.elab­Term
  78. elab­Term­Ensuring­Type
    1. Lean.Elab.Tactic.elab­Term­Ensuring­Type
  79. elab­Term­With­Holes
    1. Lean.Elab.Tactic.elab­Term­With­Holes
  80. elem
    1. Array.elem
    2. List.elem
  81. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  82. elim
    1. Empty.elim
    2. Option.elim
    3. PEmpty.elim
    4. Sum.elim
  83. elim0
    1. Fin.elim0
  84. elim­M
    1. Option.elim­M
  85. elim­Offset
    1. Nat.elim­Offset
  86. emod
    1. Int.emod
  87. empty
    1. Array.empty
    2. Subarray.empty
  88. end­Pos
    1. String.end­Pos
  89. ends­With
    1. String.ends­With
  90. ensure­Has­No­MVars
    1. Lean.Elab.Tactic.ensure­Has­No­MVars
  91. enter
  92. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  93. env (Lake command)
  94. environment variables
  95. eprint
    1. IO.eprint
  96. eprintln
    1. IO.eprintln
  97. eq_of_beq
    1. LawfulBEq.eq_of_beq (class method)
  98. eq_refl
  99. erase
    1. Array.erase
    2. List.erase
  100. erase­Dups
    1. List.erase­Dups
  101. erase­Idx
    1. Array.erase­Idx
    2. List.erase­Idx
  102. erase­Idx­TR
    1. List.erase­Idx­TR
  103. erase­P
    1. List.erase­P
  104. erase­PTR
    1. List.erase­PTR
  105. erase­Reps
    1. Array.erase­Reps
    2. List.erase­Reps
  106. erase­TR
    1. List.erase­TR
  107. erw (0) (1)
  108. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.eta (structure field)
  109. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
    2. Lean.Meta.Simp.Config.eta­Struct (structure field)
  110. eval.derive.repr
  111. eval.pp
  112. eval.type
  113. exact
    1. Quotient.exact
  114. exact?
  115. exact_mod_cast
  116. exe (Lake command)
  117. exe­Extension
    1. System.FilePath.exe­Extension
  118. exe­Name
    1. [anonymous] (structure field)
  119. exfalso
  120. exists
  121. exit
    1. IO.Process.exit
  122. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  123. expand­Macro?
    1. Lean.Macro.expand­Macro?
  124. ext (0) (1)
  125. ext1
  126. ext­Separator
    1. System.FilePath.ext­Separator
  127. extension
    1. System.FilePath.extension
  128. extensionality
    1. of propositions
  129. extra­Dep­Targets
    1. [anonymous] (structure field) (0) (1)
  130. extract
    1. Array.extract
    2. List.extract
    3. String.Iterator.extract
    4. 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. List.filter
    3. Option.filter
  108. filter­M
    1. Array.filter­M
    2. List.filter­M
  109. filter­Map
    1. Array.filter­Map
    2. List.filter­Map
  110. filter­Map­M
    1. Array.filter­Map­M
    2. List.filter­Map­M
  111. filter­Map­TR
    1. List.filter­Map­TR
  112. filter­Pairs­M
    1. Array.filter­Pairs­M
  113. filter­Rev­M
    1. List.filter­Rev­M
  114. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  115. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  116. filter­TR
    1. List.filter­TR
  117. fin­Idx­Of?
    1. List.fin­Idx­Of?
  118. fin­Range
    1. List.fin­Range
  119. find
    1. String.find
  120. find?
    1. Array.find?
    2. List.find?
  121. find­Extern­Lib?
    1. Lake.find­Extern­Lib?
  122. find­Fin­Idx?
    1. List.find­Fin­Idx?
  123. find­Idx
    1. List.find­Idx
  124. find­Idx?
    1. Array.find­Idx?
    2. List.find­Idx?
  125. find­Idx­M?
    1. Array.find­Idx­M?
  126. find­Lean­Exe?
    1. Lake.find­Lean­Exe?
  127. find­Lean­Lib?
    1. Lake.find­Lean­Lib?
  128. find­Line­Start
    1. String.find­Line­Start
  129. find­M?
    1. Array.find­M?
    2. List.find­M?
  130. find­Module?
    1. Lake.find­Module?
  131. find­Package?
    1. Lake.find­Package?
  132. find­Rev?
    1. Array.find­Rev?
    2. Subarray.find­Rev?
  133. find­Rev­M?
    1. Array.find­Rev­M?
    2. Subarray.find­Rev­M?
  134. find­Some!
    1. Array.find­Some!
  135. find­Some?
    1. Array.find­Some?
    2. List.find­Some?
  136. find­Some­M?
    1. Array.find­Some­M?
    2. List.find­Some­M?
  137. find­Some­Rev?
    1. Array.find­Some­Rev?
  138. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
    2. Subarray.find­Some­Rev­M?
  139. first (0) (1)
  140. first­Diff­Pos
    1. String.first­Diff­Pos
  141. first­M
    1. List.first­M
  142. fix
    1. Lean.Order.fix
    2. WellFounded.fix
  143. fix_eq
    1. Lean.Order.fix_eq
  144. flags
    1. IO.FileRight.flags
  145. flat­Map
    1. Array.flat­Map
    2. List.flat­Map
  146. flat­Map­M
    1. Array.flat­Map­M
    2. List.flat­Map­M
  147. flat­Map­TR
    1. List.flat­Map­TR
  148. flatten
    1. Array.flatten
    2. List.flatten
  149. flatten­TR
    1. List.flatten­TR
  150. flush
    1. IO.FS.Handle.flush
    2. IO.FS.Stream.flush (structure field)
  151. fmod
    1. Int.fmod
  152. focus (0) (1)
    1. Lean.Elab.Tactic.focus
  153. fold
    1. Nat.fold
  154. fold­I
    1. Prod.fold­I
  155. fold­M
    1. Nat.fold­M
  156. fold­Rev
    1. Nat.fold­Rev
  157. fold­Rev­M
    1. Nat.fold­Rev­M
  158. fold­TR
    1. Nat.fold­TR
  159. foldl
    1. Array.foldl
    2. Fin.foldl
    3. List.foldl
    4. String.foldl
    5. Subarray.foldl
  160. foldl­M
    1. Array.foldl­M
    2. Fin.foldl­M
    3. List.foldl­M
    4. Subarray.foldl­M
  161. foldl­Rec­On
    1. List.foldl­Rec­On
  162. foldr
    1. Array.foldr
    2. Fin.foldr
    3. List.foldr
    4. String.foldr
    5. Subarray.foldr
  163. foldr­M
    1. Array.foldr­M
    2. Fin.foldr­M
    3. List.foldr­M
    4. Subarray.foldr­M
  164. foldr­Rec­On
    1. List.foldr­Rec­On
  165. foldr­TR
    1. List.foldr­TR
  166. fopen­Error­To­String
    1. IO.Error.fopen­Error­To­String
  167. for­A
    1. List.for­A
  168. for­In
    1. ForIn.for­In (class method)
    2. ForM.for­In
    3. Subarray.for­In
  169. for­In'
    1. Array.for­In'
    2. ForIn'.for­In' (class method)
    3. List.for­In'
  170. for­M
    1. Array.for­M
    2. ForM.for­M (class method)
    3. List.for­M
    4. Nat.for­M
    5. Option.for­M
    6. Subarray.for­M
  171. for­Rev­M
    1. Array.for­Rev­M
    2. Nat.for­Rev­M
    3. Subarray.for­Rev­M
  172. format
    1. Option.format
  173. forward
    1. String.Iterator.forward
  174. from­Expr
    1. UInt16.from­Expr
    2. UInt32.from­Expr
    3. UInt64.from­Expr
    4. UInt8.from­Expr
    5. USize.from­Expr
  175. from­Expr?
    1. Fin.from­Expr?
    2. Int.from­Expr?
    3. Nat.from­Expr?
    4. String.from­Expr?
  176. from­State­M
    1. EStateM.from­State­M
  177. from­UTF8
    1. String.from­UTF8
  178. from­UTF8!
    1. String.from­UTF8!
  179. from­UTF8?
    1. String.from­UTF8?
  180. front
    1. String.front
  181. 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)
  182. fun
  183. 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. List.get
    4. MonadState.get
    5. MonadState.get (class method)
    6. Monad­StateOf.get (class method)
    7. Option.get
    8. ST.Ref.get
    9. State­RefT'.get
    10. StateT.get
    11. String.get
    12. Subarray.get
    13. Task.get
    14. Task.get (structure field)
  9. get!
    1. Array.get!
    2. List.get!
    3. Option.get!
    4. String.get!
    5. Subarray.get!
  10. get'
    1. String.get'
  11. get?
    1. Array.get?
    2. Dynamic.get?
    3. List.get?
    4. 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. List.get­D
    3. Option.get­D
    4. 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­Last
    1. List.get­Last
  50. get­Last!
    1. List.get­Last!
  51. get­Last?
    1. List.get­Last?
  52. get­Last­D
    1. List.get­Last­D
  53. get­Lean
    1. Lake.get­Lean
  54. get­Lean­Ar
    1. Lake.get­Lean­Ar
  55. get­Lean­Cc
    1. Lake.get­Lean­Cc
  56. get­Lean­Cc?
    1. Lake.get­Lean­Cc?
  57. get­Lean­Include­Dir
    1. Lake.get­Lean­Include­Dir
  58. get­Lean­Install
    1. Lake.get­Lean­Install
  59. get­Lean­Lib­Dir
    1. Lake.get­Lean­Lib­Dir
  60. get­Lean­Path
    1. Lake.get­Lean­Path
  61. get­Lean­Shared­Lib
    1. Lake.get­Lean­Shared­Lib
  62. get­Lean­Src­Dir
    1. Lake.get­Lean­Src­Dir
  63. get­Lean­Src­Path
    1. Lake.get­Lean­Src­Path
  64. get­Lean­Sysroot
    1. Lake.get­Lean­Sysroot
  65. get­Lean­System­Lib­Dir
    1. Lake.get­Lean­System­Lib­Dir
  66. get­Leanc
    1. Lake.get­Leanc
  67. get­Left
    1. Sum.get­Left
  68. get­Left?
    1. Sum.get­Left?
  69. get­Line
    1. IO.FS.Handle.get­Line
    2. IO.FS.Stream.get­Line (structure field)
  70. get­M
    1. Option.get­M
  71. get­Main­Goal
    1. Lean.Elab.Tactic.get­Main­Goal
  72. get­Main­Module
    1. Lean.Elab.Tactic.get­Main­Module
  73. get­Main­Tag
    1. Lean.Elab.Tactic.get­Main­Tag
  74. get­Max?
    1. Array.get­Max?
  75. get­Modify
  76. get­Name
    1. Lean.TSyntax.get­Name
  77. get­Nat
    1. Lean.TSyntax.get­Nat
  78. get­No­Cache
    1. Lake.get­No­Cache
  79. get­Num­Heartbeats
    1. IO.get­Num­Heartbeats
  80. get­PID
    1. IO.Process.get­PID
  81. get­Pkg­Url­Map
    1. Lake.get­Pkg­Url­Map
  82. get­Random­Bytes
    1. IO.get­Random­Bytes
  83. get­Right
    1. Sum.get­Right
  84. get­Right?
    1. Sum.get­Right?
  85. get­Root­Package
    1. Lake.get­Root­Package
  86. get­Scientific
    1. Lean.TSyntax.get­Scientific
  87. get­Shared­Lib­Path
    1. Lake.get­Shared­Lib­Path
  88. get­Stderr
    1. IO.get­Stderr
  89. get­Stdin
    1. IO.get­Stdin
  90. get­Stdout
    1. IO.get­Stdout
  91. get­String
    1. Lean.TSyntax.get­String
  92. get­Task­State
    1. IO.get­Task­State
  93. get­The
  94. get­Try­Cache
    1. Lake.get­Try­Cache
  95. get­Unsolved­Goals
    1. Lean.Elab.Tactic.get­Unsolved­Goals
  96. get­Utf8Byte
    1. String.get­Utf8Byte
  97. get­Workspace
    1. Lake.MonadWorkspace.get­Workspace (class method)
  98. get_elem_tactic
  99. get_elem_tactic_trivial
  100. globs
    1. [anonymous] (structure field)
  101. goal
    1. main
  102. ground
    1. Lean.Meta.Simp.Config.ground (structure field)
  103. group
    1. IO.FileRight.group (structure field)
  104. group­By­Key
    1. Array.group­By­Key
    2. List.group­By­Key
  105. group­Kind
    1. Lean.group­Kind
  106. guard
    1. Option.guard
  107. guard_expr
  108. guard_hyp
  109. guard_msgs.diff
  110. 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. Has­Equiv
  27. HasEquiv.mk
    1. Instance constructor of Has­Equiv
  28. Hashable
  29. Hashable.mk
    1. Instance constructor of Hashable
  30. Homogeneous­Pow
  31. HomogeneousPow.mk
    1. Instance constructor of Homogeneous­Pow
  32. Hygiene­Info
    1. Lean.Syntax.Hygiene­Info
  33. h
    1. ST.Ref.h (structure field)
  34. h­Add
    1. HAdd.h­Add (class method)
  35. h­And
    1. HAnd.h­And (class method)
  36. h­Append
    1. HAppend.h­Append (class method)
  37. h­Div
    1. HDiv.h­Div (class method)
  38. h­Iterate
    1. Fin.h­Iterate
  39. h­Iterate­From
    1. Fin.h­Iterate­From
  40. h­Mod
    1. HMod.h­Mod (class method)
  41. h­Mul
    1. HMul.h­Mul (class method)
  42. h­Or
    1. HOr.h­Or (class method)
  43. h­Pow
    1. HPow.h­Pow (class method)
  44. h­Shift­Left
    1. HShiftLeft.h­Shift­Left (class method)
  45. h­Shift­Right
    1. HShiftRight.h­Shift­Right (class method)
  46. h­Sub
    1. HSub.h­Sub (class method)
  47. h­Xor
    1. HXor.h­Xor (class method)
  48. has­Bind
    1. Id.has­Bind
  49. has­Dec­Eq
    1. List.has­Dec­Eq
  50. has­Decl
    1. Lean.Macro.has­Decl
  51. has­Finished
    1. IO.has­Finished
  52. has­Next
    1. String.Iterator.has­Next
  53. has­Prev
    1. String.Iterator.has­Prev
  54. hash
    1. Hashable.hash (class method)
    2. String.hash
  55. have
  56. have'
  57. have­I
  58. head
    1. List.head
  59. head!
    1. List.head!
  60. head?
    1. List.head?
  61. head­D
    1. List.head­D
  62. hrec­On
    1. Quot.hrec­On
    2. Quotient.hrec­On
  63. hygiene
    1. in tactics
  64. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  65. 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. Is­Infix
    1. List.Is­Infix
  391. Is­Prefix
    1. List.Is­Prefix
  392. Is­Suffix
    1. List.Is­Suffix
  393. Iterator
    1. String.Iterator
  394. i
    1. String.Iterator.i (structure field)
  395. ibelow
    1. Nat.ibelow
  396. id_map
    1. LawfulFunctor.id_map (class method)
  397. ident­Kind
    1. Lean.ident­Kind
  398. identifier
    1. raw
  399. idx­Of
    1. List.idx­Of
  400. idx­Of?
    1. List.idx­Of?
  401. if ... then ... else ...
  402. if h : ... then ... else ...
  403. imax
    1. Nat.imax
  404. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  405. impredicative
  406. inaccessible
  407. ind
    1. Quot.ind
    2. Quotient.ind
  408. index
    1. Lean.Meta.DSimp.Config.index (structure field)
    2. Lean.Meta.Simp.Config.index (structure field)
    3. of inductive type
  409. index­Of?
    1. Array.index­Of?
  410. indexed family
    1. of types
  411. induction
    1. Fin.induction
  412. induction­On
    1. Fin.induction­On
    2. Nat.div.induction­On
    3. Nat.mod.induction­On
  413. inductive.auto­Promote­Indices
  414. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  415. infer­Instance
  416. infer­Instance­As
  417. infer_instance
  418. inhabited­Left
    1. PSum.inhabited­Left
    2. Sum.inhabited­Left
  419. inhabited­Right
    1. PSum.inhabited­Right
    2. Sum.inhabited­Right
  420. init (Lake command)
  421. injection
  422. injections
  423. insert
    1. List.insert
  424. insert­At
    1. Array.insert­At
  425. insert­At!
    1. Array.insert­At!
  426. insert­Idx
    1. List.insert­Idx
  427. insert­Idx­TR
    1. List.insert­Idx­TR
  428. insertion­Sort
    1. Array.insertion­Sort
  429. instance synthesis
  430. int­Cast
    1. IntCast.int­Cast (class method)
  431. intercalate
    1. List.intercalate
    2. String.intercalate
  432. intercalate­TR
    1. List.intercalate­TR
  433. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  434. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  435. intersperse
    1. List.intersperse
  436. intersperse­TR
    1. List.intersperse­TR
  437. intro (0) (1)
  438. intro | ... => ... | ... => ...
  439. intros
  440. inv­Image
  441. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  442. is­Absolute
    1. System.FilePath.is­Absolute
  443. is­Alpha
    1. Char.is­Alpha
  444. is­Alphanum
    1. Char.is­Alphanum
  445. is­Digit
    1. Char.is­Digit
  446. is­Dir
    1. System.FilePath.is­Dir
  447. is­Empty
    1. Array.is­Empty
    2. List.is­Empty
    3. String.is­Empty
  448. is­Eq­Some
    1. Option.is­Eq­Some
  449. is­Eqv
    1. Array.is­Eqv
    2. List.is­Eqv
  450. is­Int
    1. String.is­Int
  451. is­Left
    1. Sum.is­Left
  452. is­Lower
    1. Char.is­Lower
  453. is­Lt
    1. Fin.is­Lt (structure field)
  454. is­Nat
    1. String.is­Nat
  455. is­None
    1. Option.is­None
  456. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  457. is­Ok
    1. Except.is­Ok
  458. is­Perm
    1. List.is­Perm
  459. is­Pos­Value
    1. Int.is­Pos­Value
  460. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  461. is­Prefix­Of
    1. Array.is­Prefix­Of
    2. List.is­Prefix­Of
    3. String.is­Prefix­Of
  462. is­Prefix­Of?
    1. List.is­Prefix­Of?
  463. is­Relative
    1. System.FilePath.is­Relative
  464. is­Right
    1. Sum.is­Right
  465. is­Some
    1. Option.is­Some
  466. is­Sublist
    1. List.is­Sublist
  467. is­Suffix­Of
    1. List.is­Suffix­Of
  468. is­Suffix­Of?
    1. List.is­Suffix­Of?
  469. is­Tty
    1. IO.FS.Handle.is­Tty
    2. IO.FS.Stream.is­Tty (structure field)
  470. is­Upper
    1. Char.is­Upper
  471. is­Valid
    1. String.Pos.is­Valid
  472. is­Valid­Char
    1. Nat.is­Valid­Char
    2. UInt32.is­Valid­Char
  473. is­Value
    1. Fin.is­Value
    2. Nat.is­Value
  474. is­Whitespace
    1. Char.is­Whitespace
  475. iseqv
    1. Setoid.iseqv (class method)
  476. iter
    1. String.iter
  477. 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.Order.CCPO
  163. Lean.Order.CCPO.mk
    1. Instance constructor of Lean.Order.CCPO
  164. Lean.Order.Partial­Order
  165. Lean.Order.PartialOrder.mk
    1. Instance constructor of Lean.Order.Partial­Order
  166. Lean.Order.fix
  167. Lean.Order.fix_eq
  168. Lean.Order.monotone
  169. Lean.Parser.Leading­Ident­Behavior
  170. Lean.Parser.Leading­IdentBehavior.both
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  171. Lean.Parser.Leading­IdentBehavior.default
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  172. Lean.Parser.Leading­IdentBehavior.symbol
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  173. Lean.Source­Info
  174. Lean.SourceInfo.none
    1. Constructor of Lean.Source­Info
  175. Lean.SourceInfo.original
    1. Constructor of Lean.Source­Info
  176. Lean.SourceInfo.synthetic
    1. Constructor of Lean.Source­Info
  177. Lean.Syntax
  178. Lean.Syntax.Char­Lit
  179. Lean.Syntax.Command
  180. Lean.Syntax.Hygiene­Info
  181. Lean.Syntax.Ident
  182. Lean.Syntax.Level
  183. Lean.Syntax.Name­Lit
  184. Lean.Syntax.Num­Lit
  185. Lean.Syntax.Prec
  186. Lean.Syntax.Preresolved
  187. Lean.Syntax.Preresolved.decl
    1. Constructor of Lean.Syntax.Preresolved
  188. Lean.Syntax.Preresolved.namespace
    1. Constructor of Lean.Syntax.Preresolved
  189. Lean.Syntax.Prio
  190. Lean.Syntax.Scientific­Lit
  191. Lean.Syntax.Str­Lit
  192. Lean.Syntax.TSep­Array
  193. Lean.Syntax.TSepArray.mk
    1. Constructor of Lean.Syntax.TSep­Array
  194. Lean.Syntax.Tactic
  195. Lean.Syntax.Term
  196. Lean.Syntax.atom
    1. Constructor of Lean.Syntax
  197. Lean.Syntax.get­Kind
  198. Lean.Syntax.ident
    1. Constructor of Lean.Syntax
  199. Lean.Syntax.is­Of­Kind
  200. Lean.Syntax.missing
    1. Constructor of Lean.Syntax
  201. Lean.Syntax.node
    1. Constructor of Lean.Syntax
  202. Lean.Syntax.set­Kind
  203. Lean.Syntax­Node­Kind
  204. Lean.TSyntax
  205. Lean.TSyntax.get­Char
  206. Lean.TSyntax.get­Hygiene­Info
  207. Lean.TSyntax.get­Id
  208. Lean.TSyntax.get­Name
  209. Lean.TSyntax.get­Nat
  210. Lean.TSyntax.get­Scientific
  211. Lean.TSyntax.get­String
  212. Lean.TSyntax.mk
    1. Constructor of Lean.TSyntax
  213. Lean.TSyntax­Array
  214. Lean.char­Lit­Kind
  215. Lean.choice­Kind
  216. Lean.field­Idx­Kind
  217. Lean.group­Kind
  218. Lean.hygiene­Info­Kind
  219. Lean.ident­Kind
  220. Lean.interpolated­Str­Kind
  221. Lean.interpolated­Str­Lit­Kind
  222. Lean.name­Lit­Kind
  223. Lean.null­Kind
  224. Lean.num­Lit­Kind
  225. Lean.scientific­Lit­Kind
  226. Lean.str­Lit­Kind
  227. Lean­Exe­Config
    1. Lake.Lean­Exe­Config
  228. Lean­Lib­Config
    1. Lake.Lean­Lib­Config
  229. Lean­Option
    1. Lake.Lean­Option
  230. Level
    1. Lean.Syntax.Level
  231. Lex
    1. List.Lex
  232. List
  233. List.Is­Infix
  234. List.Is­Prefix
  235. List.Is­Suffix
  236. List.Lex
  237. List.Lex.cons
    1. Constructor of List.Lex
  238. List.Lex.nil
    1. Constructor of List.Lex
  239. List.Lex.rel
    1. Constructor of List.Lex
  240. List.Mem
  241. List.Mem.head
    1. Constructor of List.Mem
  242. List.Mem.tail
    1. Constructor of List.Mem
  243. List.Nodup
  244. List.Pairwise
  245. List.Pairwise.cons
    1. Constructor of List.Pairwise
  246. List.Pairwise.nil
    1. Constructor of List.Pairwise
  247. List.Perm
  248. List.Perm.cons
    1. Constructor of List.Perm
  249. List.Perm.nil
    1. Constructor of List.Perm
  250. List.Perm.swap
    1. Constructor of List.Perm
  251. List.Perm.trans
    1. Constructor of List.Perm
  252. List.all
  253. List.all­M
  254. List.and
  255. List.any
  256. List.any­M
  257. List.append
  258. List.append­TR
  259. List.as­String
  260. List.attach
  261. List.attach­With
  262. List.beq
  263. List.concat
  264. List.cons
    1. Constructor of List
  265. List.contains
  266. List.count
  267. List.count­P
  268. List.drop
  269. List.drop­Last
  270. List.drop­Last­TR
  271. List.drop­While
  272. List.elem
  273. List.erase
  274. List.erase­Dups
  275. List.erase­Idx
  276. List.erase­Idx­TR
  277. List.erase­P
  278. List.erase­PTR
  279. List.erase­Reps
  280. List.erase­TR
  281. List.extract
  282. List.filter
  283. List.filter­M
  284. List.filter­Map
  285. List.filter­Map­M
  286. List.filter­Map­TR
  287. List.filter­Rev­M
  288. List.filter­TR
  289. List.fin­Idx­Of?
  290. List.fin­Range
  291. List.find?
  292. List.find­Fin­Idx?
  293. List.find­Idx
  294. List.find­Idx?
  295. List.find­M?
  296. List.find­Some?
  297. List.find­Some­M?
  298. List.first­M
  299. List.flat­Map
  300. List.flat­Map­M
  301. List.flat­Map­TR
  302. List.flatten
  303. List.flatten­TR
  304. List.foldl
  305. List.foldl­M
  306. List.foldl­Rec­On
  307. List.foldr
  308. List.foldr­M
  309. List.foldr­Rec­On
  310. List.foldr­TR
  311. List.for­A
  312. List.for­In'
  313. List.for­M
  314. List.get
  315. List.get!
  316. List.get?
  317. List.get­D
  318. List.get­Last
  319. List.get­Last!
  320. List.get­Last?
  321. List.get­Last­D
  322. List.group­By­Key
  323. List.has­Dec­Eq
  324. List.head
  325. List.head!
  326. List.head?
  327. List.head­D
  328. List.idx­Of
  329. List.idx­Of?
  330. List.insert
  331. List.insert­Idx
  332. List.insert­Idx­TR
  333. List.intercalate
  334. List.intercalate­TR
  335. List.intersperse
  336. List.intersperse­TR
  337. List.is­Empty
  338. List.is­Eqv
  339. List.is­Perm
  340. List.is­Prefix­Of
  341. List.is­Prefix­Of?
  342. List.is­Sublist
  343. List.is­Suffix­Of
  344. List.is­Suffix­Of?
  345. List.le
  346. List.leftpad
  347. List.leftpad­TR
  348. List.length
  349. List.length­TR
  350. List.lex
  351. List.lookup
  352. List.lt
  353. List.map
  354. List.map­A
  355. List.map­Fin­Idx
  356. List.map­Fin­Idx­M
  357. List.map­Idx
  358. List.map­Idx­M
  359. List.map­M
  360. List.map­M'
  361. List.map­Mono
  362. List.map­Mono­M
  363. List.map­TR
  364. List.max?
  365. List.max­Nat­Abs
  366. List.merge
  367. List.merge­Sort
  368. List.min?
  369. List.min­Nat­Abs
  370. List.modify
  371. List.modify­Head
  372. List.modify­TR
  373. List.modify­Tail­Idx
  374. List.nil
    1. Constructor of List
  375. List.nonzero­Minimum
  376. List.of­Fn
  377. List.or
  378. List.partition
  379. List.partition­M
  380. List.partition­Map
  381. List.pmap
  382. List.range
  383. List.range'
  384. List.range'TR
  385. List.reduce­Option
  386. List.reduce­Replicate
  387. List.remove­All
  388. List.replace
  389. List.replace­TR
  390. List.replicate
  391. List.replicate­TR
  392. List.reverse
  393. List.rightpad
  394. List.rotate­Left
  395. List.rotate­Right
  396. List.set
  397. List.set­TR
  398. List.singleton
  399. List.span
  400. List.split­At
  401. List.split­By
  402. List.sum
  403. List.tail
  404. List.tail!
  405. List.tail?
  406. List.tail­D
  407. List.take
  408. List.take­TR
  409. List.take­While
  410. List.take­While­TR
  411. List.to­Array
  412. List.to­Array­Impl
  413. List.to­Byte­Array
  414. List.to­Float­Array
  415. List.to­PArray'
  416. List.to­String
  417. List.unattach
  418. List.unzip
  419. List.unzip­TR
  420. List.zip
  421. List.zip­Idx
  422. List.zip­Idx­LE
  423. List.zip­Idx­TR
  424. List.zip­With
  425. List.zip­With­All
  426. List.zip­With­TR
  427. 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
  428. last
    1. Fin.last
  429. last­Cases
    1. Fin.last­Cases
  430. lazy­Pure
    1. IO.lazy­Pure
  431. lcm
    1. Int.lcm
    2. Nat.lcm
  432. 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. List.le
    9. Nat.le
    10. String.le
    11. UInt16.le
    12. UInt64.le
    13. UInt8.le
    14. USize.le
  433. lean (Lake command)
  434. lean_is_array
  435. lean_is_string
  436. lean_string_object (0) (1)
  437. lean_to_array
  438. lean_to_string
  439. left (0) (1)
  440. leftpad
    1. List.leftpad
  441. leftpad­TR
    1. List.leftpad­TR
  442. length
    1. List.length
    2. String.length
  443. length­TR
    1. List.length­TR
  444. let
  445. let rec
  446. let'
  447. let­I
  448. level
    1. of universe
  449. lex
    1. List.lex
  450. lex­Lt
    1. Prod.lex­Lt
  451. lhs
  452. lib­Name
    1. [anonymous] (structure field)
  453. lift
    1. Except­CpsT.lift
    2. ExceptT.lift
    3. OptionT.lift
    4. Quot.lift
    5. Quotient.lift
    6. Squash.lift
    7. State­CpsT.lift
    8. State­RefT'.lift
    9. StateT.lift
  454. lift­Meta­MAt­Main
    1. Lean.Elab.Tactic.lift­Meta­MAt­Main
  455. lift­On
    1. Quot.lift­On
    2. Quotient.lift­On
  456. lift­On₂
    1. Quotient.lift­On₂
  457. lift­Or­Get
    1. Option.lift­Or­Get
  458. lift­With
    1. MonadControl.lift­With (class method)
    2. Monad­ControlT.lift­With (class method)
  459. lift₂
    1. Quotient.lift₂
  460. line­Eq
  461. lines
    1. IO.FS.lines
  462. lint (Lake command)
  463. linter.unnecessary­Simpa
  464. literal
    1. raw string
    2. string
  465. lock
    1. IO.FS.Handle.lock
  466. log2
    1. Fin.log2
    2. Nat.log2
    3. UInt16.log2
    4. UInt32.log2
    5. UInt64.log2
    6. UInt8.log2
    7. USize.log2
  467. lookup
    1. List.lookup
  468. 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
  469. 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. List.lt
    9. Nat.lt
    10. Option.lt
    11. UInt16.lt
    12. UInt64.lt
    13. UInt8.lt
    14. USize.lt
  470. 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. Mem
    1. List.Mem
  5. Metadata
    1. IO.FS.Metadata
  6. Mod
  7. Mod.mk
    1. Instance constructor of Mod
  8. Mode
    1. IO.FS.Mode
  9. Monad
  10. Monad.mk
    1. Instance constructor of Monad
  11. Monad­Control
  12. MonadControl.mk
    1. Instance constructor of Monad­Control
  13. Monad­Control­T
  14. Monad­ControlT.mk
    1. Instance constructor of Monad­Control­T
  15. Monad­Eval
  16. MonadEval.mk
    1. Instance constructor of Monad­Eval
  17. Monad­Eval­T
  18. Monad­EvalT.mk
    1. Instance constructor of Monad­Eval­T
  19. Monad­Except
  20. MonadExcept.mk
    1. Instance constructor of Monad­Except
  21. MonadExcept.of­Except
  22. MonadExcept.or­Else
  23. MonadExcept.orelse'
  24. Monad­Except­Of
  25. Monad­ExceptOf.mk
    1. Instance constructor of Monad­Except­Of
  26. Monad­Finally
  27. MonadFinally.mk
    1. Instance constructor of Monad­Finally
  28. Monad­Functor
  29. MonadFunctor.mk
    1. Instance constructor of Monad­Functor
  30. Monad­Functor­T
  31. Monad­FunctorT.mk
    1. Instance constructor of Monad­Functor­T
  32. Monad­Lake­Env
    1. Lake.Monad­Lake­Env
  33. Monad­Lift
  34. MonadLift.mk
    1. Instance constructor of Monad­Lift
  35. Monad­Lift­T
  36. Monad­LiftT.mk
    1. Instance constructor of Monad­Lift­T
  37. Monad­Reader
  38. MonadReader.mk
    1. Instance constructor of Monad­Reader
  39. Monad­Reader­Of
  40. Monad­ReaderOf.mk
    1. Instance constructor of Monad­Reader­Of
  41. Monad­State
  42. MonadState.get
  43. MonadState.mk
    1. Instance constructor of Monad­State
  44. MonadState.modify­Get
  45. Monad­State­Of
  46. Monad­StateOf.mk
    1. Instance constructor of Monad­State­Of
  47. Monad­With­Reader
  48. Monad­WithReader.mk
    1. Instance constructor of Monad­With­Reader
  49. Monad­With­Reader­Of
  50. Monad­With­ReaderOf.mk
    1. Instance constructor of Monad­With­Reader­Of
  51. Monad­Workspace
    1. Lake.Monad­Workspace
  52. Mul
  53. Mul.mk
    1. Instance constructor of Mul
  54. main goal
  55. map
    1. Array.map
    2. EStateM.map
    3. Except.map
    4. ExceptT.map
    5. Functor.map (class method)
    6. List.map
    7. Option.map
    8. Prod.map
    9. StateT.map
    10. String.map
    11. Sum.map
  56. map­A
    1. List.map­A
    2. Option.map­A
  57. map­Const
    1. Functor.map­Const (class method)
  58. map­Error
    1. Except.map­Error
  59. map­Fin­Idx
    1. Array.map­Fin­Idx
    2. List.map­Fin­Idx
  60. map­Fin­Idx­M
    1. Array.map­Fin­Idx­M
    2. List.map­Fin­Idx­M
  61. map­Idx
    1. Array.map­Idx
    2. List.map­Idx
  62. map­Idx­M
    1. Array.map­Idx­M
    2. List.map­Idx­M
  63. map­Indexed
    1. Array.map­Indexed
  64. map­Indexed­M
    1. Array.map­Indexed­M
  65. map­M
    1. Array.map­M
    2. List.map­M
    3. Option.map­M
  66. map­M'
    1. Array.map­M'
    2. List.map­M'
  67. map­Mono
    1. Array.map­Mono
    2. List.map­Mono
  68. map­Mono­M
    1. Array.map­Mono­M
    2. List.map­Mono­M
  69. map­Rev
    1. Functor.map­Rev
  70. map­TR
    1. List.map­TR
  71. map­Task
    1. BaseIO.map­Task
    2. EIO.map­Task
    3. IO.map­Task
  72. map­Tasks
    1. BaseIO.map­Tasks
    2. EIO.map­Tasks
    3. IO.map­Tasks
  73. map_const
    1. LawfulFunctor.map_const (class method)
  74. map_pure
    1. LawfulApplicative.seq­Left_eq (class method)
  75. match
    1. pp.match
  76. max
    1. Nat.max
    2. Option.max
    3. Task.Priority.max
  77. max?
    1. List.max?
  78. max­Discharge­Depth
    1. Lean.Meta.Simp.Config.max­Discharge­Depth (structure field)
  79. max­Heartbeats
    1. synthInstance.max­Heartbeats
  80. max­Nat­Abs
    1. List.max­Nat­Abs
  81. max­Size
    1. synthInstance.max­Size
  82. max­Steps
    1. Lean.Meta.Simp.Config.max­Steps (structure field)
    2. pp.max­Steps
  83. memoize
    1. Lean.Meta.Simp.Config.memoize (structure field)
  84. merge
    1. List.merge
    2. Option.merge
  85. merge­Sort
    1. List.merge­Sort
  86. metadata
    1. System.FilePath.metadata
  87. min
    1. Nat.min
    2. Option.min
    3. String.Pos.min
  88. min?
    1. List.min?
  89. min­Nat­Abs
    1. List.min­Nat­Abs
  90. mk
    1. Dynamic.mk
    2. ExceptT.mk
    3. IO.FS.Handle.mk
    4. OptionT.mk
    5. Quot.mk
    6. Quotient.mk
    7. Squash.mk
  91. mk'
    1. LawfulMonad.mk'
    2. Quotient.mk'
  92. mk­Already­Exists
    1. IO.Error.mk­Already­Exists
  93. mk­Already­Exists­File
    1. IO.Error.mk­Already­Exists­File
  94. mk­Array
    1. Array.mk­Array
  95. mk­Eof­Error
    1. IO.Error.mk­Eof­Error
  96. mk­File­Path
    1. System.mk­File­Path
  97. mk­Hardware­Fault
    1. IO.Error.mk­Hardware­Fault
  98. mk­Illegal­Operation
    1. IO.Error.mk­Illegal­Operation
  99. mk­Inappropriate­Type
    1. IO.Error.mk­Inappropriate­Type
  100. mk­Inappropriate­Type­File
    1. IO.Error.mk­Inappropriate­Type­File
  101. mk­Interrupted
    1. IO.Error.mk­Interrupted
  102. mk­Invalid­Argument
    1. IO.Error.mk­Invalid­Argument
  103. mk­Invalid­Argument­File
    1. IO.Error.mk­Invalid­Argument­File
  104. mk­Iterator
    1. String.mk­Iterator
  105. mk­No­File­Or­Directory
    1. IO.Error.mk­No­File­Or­Directory
  106. mk­No­Such­Thing
    1. IO.Error.mk­No­Such­Thing
  107. mk­No­Such­Thing­File
    1. IO.Error.mk­No­Such­Thing­File
  108. mk­Other­Error
    1. IO.Error.mk­Other­Error
  109. mk­Permission­Denied
    1. IO.Error.mk­Permission­Denied
  110. mk­Permission­Denied­File
    1. IO.Error.mk­Permission­Denied­File
  111. mk­Protocol­Error
    1. IO.Error.mk­Protocol­Error
  112. mk­Ref
    1. IO.mk­Ref
    2. ST.mk­Ref
  113. mk­Resource­Busy
    1. IO.Error.mk­Resource­Busy
  114. mk­Resource­Exhausted
    1. IO.Error.mk­Resource­Exhausted
  115. mk­Resource­Exhausted­File
    1. IO.Error.mk­Resource­Exhausted­File
  116. mk­Resource­Vanished
    1. IO.Error.mk­Resource­Vanished
  117. mk­Std­Gen
  118. mk­Tactic­Attribute
    1. Lean.Elab.Tactic.mk­Tactic­Attribute
  119. mk­Time­Expired
    1. IO.Error.mk­Time­Expired
  120. mk­Unsatisfied­Constraints
    1. IO.Error.mk­Unsatisfied­Constraints
  121. mk­Unsupported­Operation
    1. IO.Error.mk­Unsupported­Operation
  122. 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
  123. mod­Core
    1. Nat.mod­Core
  124. modified
    1. IO.FS.Metadata.modified (structure field)
  125. modify
    1. Array.modify
    2. List.modify
    3. ST.Ref.modify
    4. String.modify
  126. 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
  127. modify­Get­The
  128. modify­Head
    1. List.modify­Head
  129. modify­M
    1. Array.modify­M
  130. modify­Op
    1. Array.modify­Op
  131. modify­TR
    1. List.modify­TR
  132. modify­Tail­Idx
    1. List.modify­Tail­Idx
  133. modify­The
  134. modn
    1. Fin.modn
  135. monad­Eval
    1. MonadEval.monad­Eval (class method)
    2. Monad­EvalT.monad­Eval (class method)
  136. monad­Lift
    1. MonadLift.monad­Lift (class method)
    2. Monad­LiftT.monad­Lift (class method)
  137. monad­Map
    1. MonadFunctor.monad­Map (class method)
    2. Monad­FunctorT.monad­Map (class method)
  138. mono­Ms­Now
    1. IO.mono­Ms­Now
  139. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  140. monotone
    1. Lean.Order.monotone
  141. 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
  142. 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. Nodup
    1. List.Nodup
  123. Nonempty
  124. Nonempty.intro
    1. Constructor of Nonempty
  125. Num­Lit
    1. Lean.Syntax.Num­Lit
  126. name
    1. Lake.LeanOption.name (structure field)
    2. [anonymous] (structure field) (0) (1)
  127. name­Lit­Kind
    1. Lean.name­Lit­Kind
  128. namespace
    1. of inductive type
  129. nat­Abs
    1. Int.nat­Abs
  130. nat­Add
    1. Fin.nat­Add
  131. nat­Cast
    1. NatCast.nat­Cast (class method)
  132. native­Facets
    1. [anonymous] (structure field) (0) (1)
  133. native_decide
  134. neg
    1. ISize.neg
    2. Int.neg
    3. Int16.neg
    4. Int32.neg
    5. Int64.neg
    6. Int8.neg
    7. Neg.neg (class method)
  135. neg­Of­Nat
    1. Int.neg­Of­Nat
  136. neutral­Config
    1. Lean.Meta.Simp.neutral­Config
  137. new (Lake command)
  138. new­Goals
    1. Lean.Meta.Rewrite.Config.new­Goals (structure field)
  139. next
    1. RandomGen.next (class method)
    2. String.Iterator.next
    3. String.next
  140. next ... => ...
  141. next'
    1. String.next'
  142. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  143. next­Until
    1. String.next­Until
  144. next­While
    1. String.next­While
  145. nextn
    1. String.Iterator.nextn
  146. no­Confusion
    1. Nat.no­Confusion
  147. no­Confusion­Type
    1. Nat.no­Confusion­Type
  148. nofun
  149. nomatch
  150. non­Backtrackable
    1. EStateM.non­Backtrackable
  151. nonzero­Minimum
    1. List.nonzero­Minimum
  152. norm_cast (0) (1)
  153. normalize
    1. System.FilePath.normalize
  154. not
    1. Bool.not
    2. Int.not
  155. not­M
  156. null­Kind
    1. Lean.null­Kind
  157. 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
    2. List.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. List.or
    3. 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.inhabited­Left
  11. PSum.inhabited­Right
  12. PSum.inl
    1. Constructor of PSum
  13. PSum.inr
    1. Constructor of PSum
  14. PUnit
  15. PUnit.unit
    1. Constructor of PUnit
  16. Pairwise
    1. List.Pairwise
  17. Partial­Order
    1. Lean.Order.Partial­Order
  18. Perm
    1. List.Perm
  19. Pos
    1. String.Pos
  20. Pow
  21. Pow.mk
    1. Instance constructor of Pow
  22. Prec
    1. Lean.Syntax.Prec
  23. Preresolved
    1. Lean.Syntax.Preresolved
  24. Prio
    1. Lean.Syntax.Prio
  25. Priority
    1. Task.Priority
  26. Prod
  27. Prod.all­I
  28. Prod.any­I
  29. Prod.fold­I
  30. Prod.lex­Lt
  31. Prod.map
  32. Prod.mk
    1. Constructor of Prod
  33. Prod.swap
  34. Prop
  35. Pure
  36. Pure.mk
    1. Instance constructor of Pure
  37. pack (Lake command)
  38. parameter
    1. of inductive type
  39. parent
    1. System.FilePath.parent
  40. parser
  41. partition
    1. Array.partition
    2. List.partition
  42. partition­M
    1. List.partition­M
  43. partition­Map
    1. List.partition­Map
  44. path
    1. IO.FS.DirEntry.path
  45. path­Exists
    1. System.FilePath.path­Exists
  46. path­Separator
    1. System.FilePath.path­Separator
  47. path­Separators
    1. System.FilePath.path­Separators
  48. pattern
  49. pbind
    1. Option.pbind
  50. pelim
    1. Option.pelim
  51. placeholder term
  52. pmap
    1. List.pmap
    2. Option.pmap
  53. polymorphism
    1. universe
  54. pop
    1. Array.pop
  55. pop­Front
    1. Subarray.pop­Front
  56. pop­While
    1. Array.pop­While
  57. pos
    1. IO.FS.Stream.Buffer.pos
    2. IO.FS.Stream.Buffer.pos (structure field)
    3. String.Iterator.pos
  58. pos­Of
    1. String.pos­Of
  59. pow
    1. HomogeneousPow.pow (class method)
    2. Int.pow
    3. Nat.pow
    4. NatPow.pow (class method)
    5. Pow.pow (class method)
  60. pp
    1. eval.pp
  61. pp.deep­Terms
  62. pp.deepTerms.threshold
  63. pp.field­Notation
  64. pp.match
  65. pp.max­Steps
  66. pp.mvars
  67. pp.proofs
  68. pp.proofs.threshold
  69. precompile­Modules
    1. [anonymous] (structure field)
  70. pred
    1. Fin.pred
    2. Nat.pred
  71. predicative
  72. prev
    1. String.Iterator.prev
    2. String.prev
  73. prevn
    1. String.Iterator.prevn
  74. print
    1. IO.print
  75. println
    1. IO.println
  76. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
    2. Lean.Meta.Simp.Config.proj (structure field)
  77. proof state
  78. proofs
    1. pp.proofs
  79. property
    1. Subtype.property (structure field)
  80. propext
  81. proposition
    1. decidable
  82. prune­Solved­Goals
    1. Lean.Elab.Tactic.prune­Solved­Goals
  83. ptr­Eq
    1. ST.Ref.ptr­Eq
  84. pure
    1. EStateM.pure
    2. Except.pure
    3. ExceptT.pure
    4. OptionT.pure
    5. Pure.pure (class method)
    6. ReaderT.pure
    7. StateT.pure
  85. pure_bind
    1. [anonymous] (class method)
  86. pure_seq
    1. [anonymous] (class method)
  87. push
    1. Array.push
    2. String.push
  88. push_cast
  89. pushn
    1. String.pushn
  90. put­Str
    1. IO.FS.Handle.put­Str
    2. IO.FS.Stream.put­Str (structure field)
  91. put­Str­Ln
    1. IO.FS.Handle.put­Str­Ln
    2. IO.FS.Stream.put­Str­Ln

Q

  1. Quot
  2. Quot.hrec­On
  3. Quot.ind
  4. Quot.lift
  5. Quot.lift­On
  6. Quot.mk
  7. Quot.rec
  8. Quot.rec­On
  9. Quot.rec­On­Subsingleton
  10. Quot.sound
  11. Quotient
  12. Quotient.exact
  13. Quotient.hrec­On
  14. Quotient.ind
  15. Quotient.lift
  16. Quotient.lift­On
  17. Quotient.lift­On₂
  18. Quotient.lift₂
  19. Quotient.mk
  20. Quotient.mk'
  21. Quotient.rec
  22. Quotient.rec­On
  23. Quotient.rec­On­Subsingleton
  24. Quotient.rec­On­Subsingleton₂
  25. Quotient.sound
  26. qsort
    1. Array.qsort
  27. qsort­Ord
    1. Array.qsort­Ord
  28. quantification
    1. impredicative
    2. predicative
  29. query (Lake command)
  30. 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. r
    1. Setoid.r (class method)
  17. rand
    1. IO.rand
  18. rand­Bool
  19. rand­Nat
  20. range
    1. Array.range
    2. List.range
    3. RandomGen.range (class method)
  21. range'
    1. List.range'
  22. range'TR
    1. List.range'TR
  23. raw
    1. Lean.TSyntax.raw (structure field)
  24. rcases
  25. 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
  26. read­Bin­File
    1. IO.FS.read­Bin­File
  27. read­Bin­To­End
    1. IO.FS.Handle.read­Bin­To­End
  28. read­Bin­To­End­Into
    1. IO.FS.Handle.read­Bin­To­End­Into
  29. read­Dir
    1. System.FilePath.read­Dir
  30. read­File
    1. IO.FS.read­File
  31. read­The
  32. read­To­End
    1. IO.FS.Handle.read­To­End
  33. real­Path
    1. IO.FS.real­Path
  34. rec
    1. Nat.rec
    2. Quot.rec
    3. Quotient.rec
  35. rec­On
    1. Nat.rec­On
    2. Quot.rec­On
    3. Quotient.rec­On
  36. rec­On­Subsingleton
    1. Quot.rec­On­Subsingleton
    2. Quotient.rec­On­Subsingleton
  37. rec­On­Subsingleton₂
    1. Quotient.rec­On­Subsingleton₂
  38. recursor
  39. reduce
  40. reduce­Abs
    1. Int.reduce­Abs
  41. 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
  42. reduce­Add­Nat
    1. Fin.reduce­Add­Nat
  43. reduce­And
    1. Fin.reduce­And
  44. reduce­Append
    1. String.reduce­Append
  45. reduce­BEq
    1. Fin.reduce­BEq
    2. Int.reduce­BEq
    3. Nat.reduce­BEq
    4. String.reduce­BEq
  46. reduce­BNe
    1. Fin.reduce­BNe
    2. Int.reduce­BNe
    3. Nat.reduce­BNe
    4. String.reduce­BNe
  47. reduce­Bdiv
    1. Int.reduce­Bdiv
  48. reduce­Beq­Diff
    1. Nat.reduce­Beq­Diff
  49. reduce­Bin
    1. Fin.reduce­Bin
    2. Int.reduce­Bin
    3. Nat.reduce­Bin
  50. reduce­Bin­Int­Nat­Op
    1. Int.reduce­Bin­Int­Nat­Op
  51. reduce­Bin­Pred
    1. Fin.reduce­Bin­Pred
    2. Int.reduce­Bin­Pred
    3. Nat.reduce­Bin­Pred
    4. String.reduce­Bin­Pred
  52. reduce­Bmod
    1. Int.reduce­Bmod
  53. reduce­Bne­Diff
    1. Nat.reduce­Bne­Diff
  54. reduce­Bool­Pred
    1. Fin.reduce­Bool­Pred
    2. Int.reduce­Bool­Pred
    3. Nat.reduce­Bool­Pred
    4. String.reduce­Bool­Pred
  55. reduce­Cast­Add
    1. Fin.reduce­Cast­Add
  56. reduce­Cast­LE
    1. Fin.reduce­Cast­LE
  57. reduce­Cast­LT
    1. Fin.reduce­Cast­LT
  58. reduce­Cast­Succ
    1. Fin.reduce­Cast­Succ
  59. 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
  60. reduce­Eq
    1. Fin.reduce­Eq
    2. Int.reduce­Eq
    3. String.reduce­Eq
  61. reduce­Eq­Diff
    1. Nat.reduce­Eq­Diff
  62. reduce­FDiv
    1. Int.reduce­FDiv
  63. reduce­FMod
    1. Int.reduce­FMod
  64. reduce­Fin­Mk
    1. Fin.reduce­Fin­Mk
  65. 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
  66. 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
  67. reduce­Gcd
    1. Nat.reduce­Gcd
  68. reduce­Get­Elem
    1. Array.reduce­Get­Elem
  69. reduce­Get­Elem!
    1. Array.reduce­Get­Elem!
  70. reduce­Get­Elem?
    1. Array.reduce­Get­Elem?
  71. 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
  72. 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
  73. reduce­LTLE
    1. Nat.reduce­LTLE
  74. reduce­Last
    1. Fin.reduce­Last
  75. reduce­Le­Diff
    1. Nat.reduce­Le­Diff
  76. reduce­Mk
    1. String.reduce­Mk
  77. 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
  78. 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
  79. reduce­Nat­Add
    1. Fin.reduce­Nat­Add
  80. reduce­Nat­Core
    1. Int.reduce­Nat­Core
  81. reduce­Nat­Eq­Expr
    1. Nat.reduce­Nat­Eq­Expr
  82. reduce­Nat­Op
    1. Fin.reduce­Nat­Op
  83. reduce­Ne
    1. Fin.reduce­Ne
    2. Int.reduce­Ne
    3. String.reduce­Ne
  84. reduce­Neg
    1. Int.reduce­Neg
  85. reduce­Neg­Succ
    1. Int.reduce­Neg­Succ
  86. 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
  87. reduce­Of­Nat'
    1. Fin.reduce­Of­Nat'
  88. 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
  89. reduce­Op
    1. Fin.reduce­Op
  90. reduce­Option
    1. Array.reduce­Option
    2. List.reduce­Option
  91. reduce­Or
    1. Fin.reduce­Or
  92. reduce­Pow
    1. Int.reduce­Pow
    2. Nat.reduce­Pow
  93. reduce­Pred
    1. Fin.reduce­Pred
  94. reduce­Replicate
    1. List.reduce­Replicate
  95. reduce­Rev
    1. Fin.reduce­Rev
  96. reduce­Shift­Left
    1. Fin.reduce­Shift­Left
  97. reduce­Shift­Right
    1. Fin.reduce­Shift­Right
  98. 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
  99. reduce­Sub­Diff
    1. Nat.reduce­Sub­Diff
  100. reduce­Sub­Nat
    1. Fin.reduce­Sub­Nat
  101. reduce­Succ
    1. Fin.reduce­Succ
    2. Nat.reduce­Succ
  102. reduce­TDiv
    1. Int.reduce­TDiv
  103. reduce­TMod
    1. Int.reduce­TMod
  104. 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
  105. reduce­Unary
    1. Int.reduce­Unary
    2. Nat.reduce­Unary
  106. reduce­Xor
    1. Fin.reduce­Xor
  107. reduction
    1. ι (iota)
  108. ref
    1. ST.Ref.ref (structure field)
  109. refine
  110. refine'
  111. refl
    1. Equivalence.refl (structure field)
  112. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  113. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  114. rel
    1. Lean.Order.PartialOrder.rel (class method)
    2. Well­FoundedRelation.rel (class method)
  115. rel_antisymm
    1. Lean.Order.PartialOrder.rel_antisymm (class method)
  116. rel_refl
    1. Lean.Order.PartialOrder.rel_refl (class method)
  117. rel_trans
    1. Lean.Order.PartialOrder.rel_trans (class method)
  118. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  119. remaining­To­String
    1. String.Iterator.remaining­To­String
  120. remove­All
    1. List.remove­All
  121. remove­Dir
    1. IO.FS.remove­Dir
  122. remove­Dir­All
    1. IO.FS.remove­Dir­All
  123. remove­File
    1. IO.FS.remove­File
  124. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  125. rename
    1. IO.FS.rename
  126. rename_i
  127. repeat (0) (1)
    1. Nat.repeat
  128. repeat'
  129. repeat1'
  130. repeat­TR
    1. Nat.repeat­TR
  131. replace
    1. List.replace
    2. String.replace
  132. replace­TR
    1. List.replace­TR
  133. replicate
    1. List.replicate
  134. replicate­TR
    1. List.replicate­TR
  135. repr
    1. Int.repr
    2. Nat.repr
    3. Option.repr
    4. USize.repr
    5. eval.derive.repr
  136. repr­Prec
    1. Repr.repr­Prec (class method)
  137. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  138. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  139. restore
    1. EStateM.Backtrackable.restore (class method)
  140. restore­M
    1. MonadControl.restore­M (class method)
    2. Monad­ControlT.restore­M (class method)
  141. rev
    1. Fin.rev
  142. rev­Find
    1. String.rev­Find
  143. rev­Pos­Of
    1. String.rev­Pos­Of
  144. reverse
    1. Array.reverse
    2. List.reverse
  145. reverse­Induction
    1. Fin.reverse­Induction
  146. revert
  147. rewind
    1. IO.FS.Handle.rewind
  148. rewrite (0) (1)
    1. trace.Meta.Tactic.simp.rewrite
  149. rfl (0) (1)
    1. LawfulBEq.rfl (class method)
  150. rfl'
  151. rhs
  152. right (0) (1)
  153. rightpad
    1. List.rightpad
  154. rintro
  155. root
    1. IO.FS.DirEntry.root (structure field)
    2. [anonymous] (structure field)
  156. roots
    1. [anonymous] (structure field)
  157. rotate­Left
    1. List.rotate­Left
  158. rotate­Right
    1. List.rotate­Right
  159. rotate_left
  160. rotate_right
  161. 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
  162. run'
    1. EStateM.run'
    2. State­CpsT.run'
    3. State­RefT'.run'
    4. StateT.run'
  163. run­Catch
    1. Except­CpsT.run­Catch
  164. run­EST
  165. run­K
    1. Except­CpsT.run­K
    2. State­CpsT.run­K
  166. run­ST
  167. run­Term­Elab
    1. Lean.Elab.Tactic.run­Term­Elab
  168. run_tac
  169. rw (0) (1)
  170. rw?
  171. rw_mod_cast
  172. 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. Setoid
  24. Setoid.mk
    1. Instance constructor of Setoid
  25. Shift­Left
  26. ShiftLeft.mk
    1. Instance constructor of Shift­Left
  27. Shift­Right
  28. ShiftRight.mk
    1. Instance constructor of Shift­Right
  29. Sigma
  30. Sigma.mk
    1. Constructor of Sigma
  31. Simp­Extension
    1. Lean.Meta.Simp­Extension
  32. Size­Of
  33. SizeOf.mk
    1. Instance constructor of Size­Of
  34. Sort
  35. Source­Info
    1. Lean.Source­Info
  36. Spawn­Args
    1. IO.Process.Spawn­Args
  37. Squash
  38. Squash.lift
  39. Squash.mk
  40. State­Cps­T
  41. State­CpsT.lift
  42. State­CpsT.run
  43. State­CpsT.run'
  44. State­CpsT.run­K
  45. State­M
  46. State­Ref­T'
  47. State­RefT'.get
  48. State­RefT'.lift
  49. State­RefT'.modify­Get
  50. State­RefT'.run
  51. State­RefT'.run'
  52. State­RefT'.set
  53. State­T
  54. StateT.bind
  55. StateT.failure
  56. StateT.get
  57. StateT.lift
  58. StateT.map
  59. StateT.modify­Get
  60. StateT.or­Else
  61. StateT.pure
  62. StateT.run
  63. StateT.run'
  64. StateT.set
  65. Std­Gen
  66. StdGen.mk
    1. Constructor of Std­Gen
  67. Stdio
    1. IO.Process.Stdio
  68. Stdio­Config
    1. IO.Process.Stdio­Config
  69. Str­Lit
    1. Lean.Syntax.Str­Lit
  70. Stream
    1. IO.FS.Stream
  71. String
  72. String.Iterator
  73. String.Iterator.at­End
  74. String.Iterator.curr
  75. String.Iterator.extract
  76. String.Iterator.forward
  77. String.Iterator.has­Next
  78. String.Iterator.has­Prev
  79. String.Iterator.mk
    1. Constructor of String.Iterator
  80. String.Iterator.next
  81. String.Iterator.nextn
  82. String.Iterator.pos
  83. String.Iterator.prev
  84. String.Iterator.prevn
  85. String.Iterator.remaining­Bytes
  86. String.Iterator.remaining­To­String
  87. String.Iterator.set­Curr
  88. String.Iterator.to­End
  89. String.Pos
  90. String.Pos.is­Valid
  91. String.Pos.min
  92. String.Pos.mk
    1. Constructor of String.Pos
  93. String.all
  94. String.any
  95. String.append
  96. String.at­End
  97. String.back
  98. String.capitalize
  99. String.codepoint­Pos­To­Utf16Pos
  100. String.codepoint­Pos­To­Utf16Pos­From
  101. String.codepoint­Pos­To­Utf8Pos­From
  102. String.contains
  103. String.crlf­To­Lf
  104. String.dec­Eq
  105. String.decapitalize
  106. String.drop
  107. String.drop­Right
  108. String.drop­Right­While
  109. String.drop­While
  110. String.end­Pos
  111. String.ends­With
  112. String.extract
  113. String.find
  114. String.find­Line­Start
  115. String.first­Diff­Pos
  116. String.foldl
  117. String.foldr
  118. String.from­Expr?
  119. String.from­UTF8
  120. String.from­UTF8!
  121. String.from­UTF8?
  122. String.front
  123. String.get
  124. String.get!
  125. String.get'
  126. String.get?
  127. String.get­Utf8Byte
  128. String.hash
  129. String.intercalate
  130. String.is­Empty
  131. String.is­Int
  132. String.is­Nat
  133. String.is­Prefix­Of
  134. String.iter
  135. String.join
  136. String.le
  137. String.length
  138. String.map
  139. String.mk
    1. Constructor of String
  140. String.mk­Iterator
  141. String.modify
  142. String.next
  143. String.next'
  144. String.next­Until
  145. String.next­While
  146. String.offset­Of­Pos
  147. String.pos­Of
  148. String.prev
  149. String.push
  150. String.pushn
  151. String.quote
  152. String.reduce­Append
  153. String.reduce­BEq
  154. String.reduce­BNe
  155. String.reduce­Bin­Pred
  156. String.reduce­Bool­Pred
  157. String.reduce­Eq
  158. String.reduce­GE
  159. String.reduce­GT
  160. String.reduce­LE
  161. String.reduce­LT
  162. String.reduce­Mk
  163. String.reduce­Ne
  164. String.remove­Leading­Spaces
  165. String.replace
  166. String.rev­Find
  167. String.rev­Pos­Of
  168. String.set
  169. String.singleton
  170. String.split
  171. String.split­On
  172. String.starts­With
  173. String.substr­Eq
  174. String.take
  175. String.take­Right
  176. String.take­Right­While
  177. String.take­While
  178. String.to­File­Map
  179. String.to­Format
  180. String.to­Int!
  181. String.to­Int?
  182. String.to­List
  183. String.to­Lower
  184. String.to­Name
  185. String.to­Nat!
  186. String.to­Nat?
  187. String.to­Substring
  188. String.to­Substring'
  189. String.to­UTF8
  190. String.to­Upper
  191. String.trim
  192. String.trim­Left
  193. String.trim­Right
  194. String.utf16Length
  195. String.utf16Pos­To­Codepoint­Pos
  196. String.utf16Pos­To­Codepoint­Pos­From
  197. String.utf8Byte­Size
  198. String.utf8Decode­Char?
  199. String.utf8Encode­Char
  200. String.validate­UTF8
  201. Sub
  202. Sub.mk
    1. Instance constructor of Sub
  203. Subarray
  204. Subarray.all
  205. Subarray.all­M
  206. Subarray.any
  207. Subarray.any­M
  208. Subarray.drop
  209. Subarray.empty
  210. Subarray.find­Rev?
  211. Subarray.find­Rev­M?
  212. Subarray.find­Some­Rev­M?
  213. Subarray.foldl
  214. Subarray.foldl­M
  215. Subarray.foldr
  216. Subarray.foldr­M
  217. Subarray.for­In
  218. Subarray.for­M
  219. Subarray.for­Rev­M
  220. Subarray.get
  221. Subarray.get!
  222. Subarray.get­D
  223. Subarray.mk
    1. Constructor of Subarray
  224. Subarray.pop­Front
  225. Subarray.size
  226. Subarray.split
  227. Subarray.take
  228. Subarray.to­Array
  229. Subtype
  230. Subtype.mk
    1. Constructor of Subtype
  231. Sum
  232. Sum.elim
  233. Sum.get­Left
  234. Sum.get­Left?
  235. Sum.get­Right
  236. Sum.get­Right?
  237. Sum.inhabited­Left
  238. Sum.inhabited­Right
  239. Sum.inl
    1. Constructor of Sum
  240. Sum.inr
    1. Constructor of Sum
  241. Sum.is­Left
  242. Sum.is­Right
  243. Sum.map
  244. Sum.swap
  245. Syntax
    1. Lean.Syntax
  246. Syntax­Node­Kind
    1. Lean.Syntax­Node­Kind
  247. System.File­Path
  248. System.FilePath.add­Extension
  249. System.FilePath.components
  250. System.FilePath.exe­Extension
  251. System.FilePath.ext­Separator
  252. System.FilePath.extension
  253. System.FilePath.file­Name
  254. System.FilePath.file­Stem
  255. System.FilePath.is­Absolute
  256. System.FilePath.is­Dir
  257. System.FilePath.is­Relative
  258. System.FilePath.join
  259. System.FilePath.metadata
  260. System.FilePath.mk
    1. Constructor of System.File­Path
  261. System.FilePath.normalize
  262. System.FilePath.parent
  263. System.FilePath.path­Exists
  264. System.FilePath.path­Separator
  265. System.FilePath.path­Separators
  266. System.FilePath.read­Dir
  267. System.FilePath.walk­Dir
  268. System.FilePath.with­Extension
  269. System.FilePath.with­File­Name
  270. System.mk­File­Path
  271. s
    1. String.Iterator.s (structure field)
  272. s1
    1. StdGen.s1 (structure field)
  273. s2
    1. StdGen.s2 (structure field)
  274. save
    1. EStateM.Backtrackable.save (class method)
  275. scientific­Lit­Kind
    1. Lean.scientific­Lit­Kind
  276. script doc (Lake command)
  277. script list (Lake command)
  278. script run (Lake command)
  279. semi­Out­Param
  280. seq
    1. Seq.seq (class method)
  281. seq­Left
    1. SeqLeft.seq­Left (class method)
  282. seq­Left_eq
    1. [anonymous] (class method)
  283. seq­Right
    1. EStateM.seq­Right
    2. SeqRight.seq­Right (class method)
  284. seq­Right_eq
    1. [anonymous] (class method)
  285. seq_assoc
    1. LawfulApplicative.pure_seq (class method)
  286. seq_pure
    1. LawfulApplicative.seq­Right_eq (class method)
  287. sequence
    1. Option.sequence
  288. sequence­Map
    1. Array.sequence­Map
  289. serve (Lake command)
  290. set
    1. Array.set
    2. EStateM.set
    3. List.set
    4. MonadState.set (class method)
    5. Monad­StateOf.set (class method)
    6. ST.Ref.set
    7. State­RefT'.set
    8. StateT.set
    9. String.set
  291. set!
    1. Array.set!
  292. set­Access­Rights
    1. IO.set­Access­Rights
  293. set­Curr
    1. String.Iterator.set­Curr
  294. set­Current­Dir
    1. IO.Process.set­Current­Dir
  295. set­D
    1. Array.set­D
  296. set­Goals
    1. Lean.Elab.Tactic.set­Goals
  297. set­Kind
    1. Lean.Syntax.set­Kind
  298. set­Rand­Seed
    1. IO.set­Rand­Seed
  299. set­Stderr
    1. IO.set­Stderr
  300. set­Stdin
    1. IO.set­Stdin
  301. set­Stdout
    1. IO.set­Stdout
  302. set­TR
    1. List.set­TR
  303. set_option
  304. setsid
    1. IO.Process.SpawnArgs.args (structure field)
  305. 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
  306. 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
  307. show
  308. show_term
  309. sign
    1. Int.sign
  310. simp (0) (1)
  311. simp!
  312. simp?
  313. simp?!
  314. simp_all
  315. simp_all!
  316. simp_all?
  317. simp_all?!
  318. simp_all_arith
  319. simp_all_arith!
  320. simp_arith
  321. simp_arith!
  322. simp_match
  323. simp_wf
  324. simpa
  325. simpa!
  326. simpa?
  327. simpa?!
  328. simprocs
  329. single­Pass
    1. Lean.Meta.Simp.Config.single­Pass (structure field)
  330. singleton
    1. Array.singleton
    2. List.singleton
    3. String.singleton
  331. 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
  332. size­Of
    1. SizeOf.size­Of (class method)
  333. skip (0) (1)
  334. skip­Assigned­Instances
    1. tactic.skip­Assigned­Instances
  335. sleep
    1. IO.sleep
  336. 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)
  337. solve
  338. solve_by_elim
  339. sorry
  340. sort­MVar­Id­Array­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  341. sort­MVar­Ids­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  342. sound
    1. Quot.sound
    2. Quotient.sound
  343. span
    1. List.span
  344. spawn
    1. IO.Process.spawn
    2. Task.spawn
  345. specialize
  346. split
    1. Array.split
    2. RandomGen.split (class method)
    3. String.split
    4. Subarray.split
  347. split­At
    1. List.split­At
  348. split­By
    1. List.split­By
  349. split­On
    1. String.split­On
  350. src­Dir
    1. [anonymous] (structure field) (0) (1)
  351. st­M
    1. MonadControl.st­M (class method)
    2. Monad­ControlT.st­M (class method)
  352. start
    1. Subarray.start (structure field)
  353. start_le_stop
    1. Subarray.start_le_stop (structure field)
  354. starts­With
    1. String.starts­With
  355. std­Next
  356. std­Range
  357. std­Split
  358. stderr
    1. IO.Process.Child.stderr (structure field)
    2. IO.Process.Output.stderr (structure field)
    3. IO.Process.StdioConfig.stderr (structure field)
  359. stdin
    1. IO.Process.Child.stdin (structure field)
    2. IO.Process.StdioConfig.stdin (structure field)
  360. stdout
    1. IO.Process.Child.stdout (structure field)
    2. IO.Process.Output.stdout (structure field)
    3. IO.Process.StdioConfig.stdout (structure field)
  361. stop
    1. Subarray.stop (structure field)
  362. stop_le_array_size
    1. Subarray.stop_le_array_size (structure field)
  363. str­Lit­Kind
    1. Lean.str­Lit­Kind
  364. strong­Induction­On
    1. Nat.strong­Induction­On
  365. 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
  366. sub­Digit­Char
    1. Nat.sub­Digit­Char
  367. sub­Nat
    1. Fin.sub­Nat
  368. sub­Nat­Nat
    1. Int.sub­Nat­Nat
  369. subst
  370. subst_eqs
  371. subst_vars
  372. substr­Eq
    1. String.substr­Eq
  373. succ
    1. Fin.succ
  374. succ­Rec
    1. Fin.succ­Rec
  375. succ­Rec­On
    1. Fin.succ­Rec­On
  376. suffices
  377. sum
    1. List.sum
  378. super­Digit­Char
    1. Nat.super­Digit­Char
  379. support­Interpreter
    1. [anonymous] (structure field)
  380. swap
    1. Array.swap
    2. Prod.swap
    3. ST.Ref.swap
    4. Sum.swap
  381. swap!
    1. Array.swap!
  382. swap­At
    1. Array.swap­At
  383. swap­At!
    1. Array.swap­At!
  384. symm
    1. Equivalence.symm (structure field)
  385. symm_saturate
  386. synthInstance.max­Heartbeats
  387. synthInstance.max­Size
  388. 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. tail
    1. List.tail
  30. tail!
    1. List.tail!
  31. tail?
    1. List.tail?
  32. tail­D
    1. List.tail­D
  33. take
    1. Array.take
    2. List.take
    3. ST.Ref.take
    4. String.take
    5. Subarray.take
  34. take­Right
    1. String.take­Right
  35. take­Right­While
    1. String.take­Right­While
  36. take­Stdin
    1. IO.Process.Child.take­Stdin
  37. take­TR
    1. List.take­TR
  38. take­While
    1. Array.take­While
    2. List.take­While
    3. String.take­While
  39. take­While­TR
    1. List.take­While­TR
  40. tdiv
    1. Int.tdiv
  41. term
    1. placeholder
  42. test (Lake command)
  43. test­Bit
    1. Nat.test­Bit
  44. threshold
    1. pp.deepTerms.threshold
    2. pp.proofs.threshold
  45. throw
    1. EStateM.throw
    2. MonadExcept.throw (class method)
    3. Monad­ExceptOf.throw (class method)
  46. throw­Error
    1. Lean.Macro.throw­Error
  47. throw­Error­At
    1. Lean.Macro.throw­Error­At
  48. throw­The
  49. throw­Unsupported
    1. Lean.Macro.throw­Unsupported
  50. tmod
    1. Int.tmod
  51. to­Applicative
    1. Alternative.to­Applicative (class method)
    2. Monad.to­Applicative (class method)
  52. to­Array
    1. List.to­Array
    2. Option.to­Array
    3. Subarray.to­Array
  53. to­Array­Impl
    1. List.to­Array­Impl
  54. to­Base­IO
    1. EIO.to­Base­IO
  55. to­Bind
    1. [anonymous] (class method)
  56. 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)
  57. to­Bool
    1. Except.to­Bool
  58. to­Byte­Array
    1. List.to­Byte­Array
  59. to­Digits
    1. Nat.to­Digits
  60. to­Digits­Core
    1. Nat.to­Digits­Core
  61. to­EIO
    1. BaseIO.to­EIO
    2. IO.to­EIO
  62. to­End
    1. String.Iterator.to­End
  63. to­File­Map
    1. String.to­File­Map
  64. to­Float
    1. Nat.to­Float
    2. UInt64.to­Float
  65. to­Float32
    1. UInt64.to­Float32
  66. to­Float­Array
    1. List.to­Float­Array
  67. to­Format
    1. String.to­Format
  68. to­Functor
    1. Applicative.to­Functor (class method)
  69. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  70. to­Handle­Type
    1. IO.Process.Stdio.to­Handle­Type
  71. to­IO
    1. BaseIO.to­IO
    2. EIO.to­IO
  72. to­IO'
    1. EIO.to­IO'
  73. to­ISize
    1. Bool.to­ISize
    2. Int.to­ISize
    3. Int32.to­ISize
    4. Int64.to­ISize
  74. to­Int
    1. ISize.to­Int
    2. Int16.to­Int
    3. Int32.to­Int
    4. Int64.to­Int
    5. Int8.to­Int
  75. to­Int!
    1. String.to­Int!
  76. to­Int16
    1. Bool.to­Int16
    2. Int.to­Int16
    3. Int32.to­Int16
    4. Int64.to­Int16
    5. Int8.to­Int16
  77. 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)
  78. 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
  79. to­Int8
    1. Bool.to­Int8
    2. Int.to­Int8
    3. Int16.to­Int8
    4. Int32.to­Int8
    5. Int64.to­Int8
  80. to­Int?
    1. String.to­Int?
  81. to­Lawful­Applicative
    1. LawfulMonad.to­Lawful­Applicative (class method)
  82. to­Lawful­Functor
    1. LawfulApplicative.to­Lawful­Functor (class method)
  83. to­Lean­Config
    1. Lake.Lean­ExeConfig.to­Lean­Config (structure field)
    2. Lake.Lean­LibConfig.to­Lean­Config (structure field)
  84. to­Level
    1. Nat.to­Level
  85. to­List
    1. Array.to­List
    2. Array.to­List (structure field)
    3. Option.to­List
    4. String.to­List
  86. to­List­Append
    1. Array.to­List­Append
  87. to­List­Rev
    1. Array.to­List­Rev
  88. to­Lower
    1. String.to­Lower
  89. to­Monad­State­Of
    1. ST.Ref.to­Monad­State­Of
  90. to­Name
    1. String.to­Name
  91. 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
  92. to­Nat!
    1. String.to­Nat!
  93. to­Nat'
    1. Int.to­Nat'
  94. to­Nat?
    1. String.to­Nat?
  95. to­Option
    1. Except.to­Option
  96. to­PArray'
    1. Array.to­PArray'
    2. List.to­PArray'
  97. to­Partial­Order
    1. Lean.Order.CCPO.to­Partial­Order (class method)
  98. to­Pure
    1. [anonymous] (class method)
  99. to­Seq
    1. [anonymous] (class method)
  100. to­Seq­Left
    1. Applicative.to­Pure (class method)
  101. to­Seq­Right
    1. [anonymous] (class method)
  102. to­Stdio­Config
    1. IO.Process.SpawnArgs.to­Stdio­Config (structure field)
  103. to­String
    1. IO.Error.to­String
    2. List.to­String
    3. System.FilePath.to­String (structure field)
    4. ToString.to­String (class method)
  104. to­Sub­Digits
    1. Nat.to­Sub­Digits
  105. to­Subarray
    1. Array.to­Subarray
  106. to­Subscript­String
    1. Nat.to­Subscript­String
  107. to­Substring
    1. String.to­Substring
  108. to­Substring'
    1. String.to­Substring'
  109. to­Super­Digits
    1. Nat.to­Super­Digits
  110. to­Superscript­String
    1. Nat.to­Superscript­String
  111. 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
  112. 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
  113. 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
  114. 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
  115. 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
  116. to­UTF8
    1. String.to­UTF8
  117. to­Upper
    1. String.to­Upper
  118. trace
    1. Lean.Macro.trace
    2. tactic.simp.trace (0) (1)
  119. trace.Elab.definition.wf
  120. trace.Meta.Tactic.simp.discharge
  121. trace.Meta.Tactic.simp.rewrite
  122. trace_state (0) (1)
  123. trans
    1. Equivalence.trans (structure field)
  124. translate-config (Lake command)
  125. transparency
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  126. trim
    1. String.trim
  127. trim­Left
    1. String.trim­Left
  128. trim­Right
    1. String.trim­Right
  129. trivial
  130. truncate
    1. IO.FS.Handle.truncate
  131. try (0) (1)
  132. 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
  133. try­Catch­The
  134. try­Finally'
    1. MonadFinally.try­Finally' (class method)
  135. try­Lock
    1. IO.FS.Handle.try­Lock
  136. try­Tactic
    1. Lean.Elab.Tactic.try­Tactic
  137. try­Tactic?
    1. Lean.Elab.Tactic.try­Tactic?
  138. try­Wait
    1. IO.Process.Child.try­Wait
  139. type
    1. IO.FS.Metadata.type (structure field)
    2. eval.type
  140. 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. List.unattach
    3. 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
    2. List.unzip
  217. unzip­TR
    1. List.unzip­TR
  218. update (Lake command)
  219. upload (Lake command)
  220. user
    1. IO.FileRight.user (structure field)
  221. user­Error
    1. IO.user­Error
  222. uset
    1. Array.uset
  223. usize
    1. Array.usize
  224. utf16Length
    1. String.utf16Length
  225. utf16Pos­To­Codepoint­Pos
    1. String.utf16Pos­To­Codepoint­Pos
  226. utf16Pos­To­Codepoint­Pos­From
    1. String.utf16Pos­To­Codepoint­Pos­From
  227. utf8Byte­Size
    1. String.utf8Byte­Size
  228. utf8Decode­Char?
    1. String.utf8Decode­Char?
  229. 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)
    2. trace.Elab.definition.wf
  10. wf­Param
  11. whnf
  12. with­Extension
    1. System.FilePath.with­Extension
  13. with­File
    1. IO.FS.with­File
  14. with­File­Name
    1. System.FilePath.with­File­Name
  15. with­Fresh­Macro­Scope
    1. Lean.Macro.with­Fresh­Macro­Scope
  16. with­Isolated­Streams
    1. IO.FS.with­Isolated­Streams (0) (1)
  17. with­Location
    1. Lean.Elab.Tactic.with­Location
  18. with­Position
  19. with­Position­After­Linebreak
  20. with­Reader
    1. Monad­WithReader.with­Reader (class method)
    2. Monad­With­ReaderOf.with­Reader (class method)
  21. with­Stderr
    1. IO.with­Stderr
  22. with­Stdin
    1. IO.with­Stdin
  23. with­Stdout
    1. IO.with­Stdout
  24. with­Temp­File
    1. IO.FS.with­Temp­File
  25. with­The­Reader
  26. with_reducible
  27. with_reducible_and_instances
  28. with_unfolding_all
  29. without­Position
  30. write
    1. IO.FS.Handle.write
    2. IO.FS.Stream.write (structure field)
  31. write­Bin­File
    1. IO.FS.write­Bin­File
  32. 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
    2. List.zip
  8. zip­Idx
    1. List.zip­Idx
  9. zip­Idx­LE
    1. List.zip­Idx­LE
  10. zip­Idx­TR
    1. List.zip­Idx­TR
  11. zip­With
    1. Array.zip­With
    2. List.zip­With
  12. zip­With­All
    1. List.zip­With­All
  13. zip­With­Index
    1. Array.zip­With­Index
  14. zip­With­TR
    1. List.zip­With­TR