Index

Symbols

  1. ( ... )
  2. . ...
  3. <;> (0) (1)
  4. _private.Init.Data.SInt.Basic.0.ISize.of­USize
    1. Constructor of ISize
  5. _private.Init.Data.SInt.Basic.0.Int16.of­UInt16
    1. Constructor of Int16
  6. _private.Init.Data.SInt.Basic.0.Int32.of­UInt32
    1. Constructor of Int32
  7. _private.Init.Data.SInt.Basic.0.Int64.of­UInt64
    1. Constructor of Int64
  8. _private.Init.Data.SInt.Basic.0.Int8.of­UInt8
    1. Constructor of Int8
  9. _private.Init.Dynamic.0.TypeName.mk'
    1. Instance constructor of Type­Name
  10. { ... }
  11. ·
  12. · ...
  13. Σ-types
  14. ι-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. And
  9. And.elim
  10. And.intro
    1. Constructor of And
  11. Append
  12. Append.mk
    1. Instance constructor of Append
  13. Applicative
  14. Applicative.mk
    1. Instance constructor of Applicative
  15. Array
  16. Array.all
  17. Array.all­Diff
  18. Array.all­M
  19. Array.any
  20. Array.any­M
  21. Array.append
  22. Array.append­List
  23. Array.attach
  24. Array.attach­With
  25. Array.back
  26. Array.back!
  27. Array.back?
  28. Array.bin­Insert
  29. Array.bin­Insert­M
  30. Array.bin­Search
  31. Array.bin­Search­Contains
  32. Array.contains
  33. Array.count
  34. Array.count­P
  35. Array.drop
  36. Array.elem
  37. Array.empty
  38. Array.erase
  39. Array.erase­Idx
  40. Array.erase­Idx!
  41. Array.erase­Idx­If­In­Bounds
  42. Array.erase­P
  43. Array.erase­Reps
  44. Array.extract
  45. Array.filter
  46. Array.filter­M
  47. Array.filter­Map
  48. Array.filter­Map­M
  49. Array.filter­Pairs­M
  50. Array.filter­Rev­M
  51. Array.filter­Sep­Elems
  52. Array.filter­Sep­Elems­M
  53. Array.fin­Idx­Of?
  54. Array.fin­Range
  55. Array.find?
  56. Array.find­Fin­Idx?
  57. Array.find­Idx
  58. Array.find­Idx?
  59. Array.find­Idx­M?
  60. Array.find­M?
  61. Array.find­Rev?
  62. Array.find­Rev­M?
  63. Array.find­Some!
  64. Array.find­Some?
  65. Array.find­Some­M?
  66. Array.find­Some­Rev?
  67. Array.find­Some­Rev­M?
  68. Array.first­M
  69. Array.flat­Map (0) (1)
  70. Array.flat­Map­M (0) (1)
  71. Array.flatten
  72. Array.foldl
  73. Array.foldl­M
  74. Array.foldr
  75. Array.foldr­M
  76. Array.for­In'
  77. Array.for­M
  78. Array.for­Rev­M
  79. Array.get­D
  80. Array.get­Even­Elems
  81. Array.get­Max?
  82. Array.group­By­Key
  83. Array.idx­Of
  84. Array.idx­Of?
  85. Array.insert­Idx
  86. Array.insert­Idx!
  87. Array.insert­Idx­If­In­Bounds
  88. Array.insertion­Sort
  89. Array.is­Empty
  90. Array.is­Eqv
  91. Array.is­Prefix­Of
  92. Array.lex
  93. Array.map
  94. Array.map­Fin­Idx
  95. Array.map­Fin­Idx­M
  96. Array.map­Idx
  97. Array.map­Idx­M
  98. Array.map­Indexed
  99. Array.map­Indexed­M
  100. Array.map­M
  101. Array.map­M'
  102. Array.map­Mono
  103. Array.map­Mono­M
  104. Array.mk
    1. Constructor of Array
  105. Array.mk­Array
  106. Array.modify
  107. Array.modify­M
  108. Array.modify­Op
  109. Array.of­Fn
  110. Array.of­Subarray
  111. Array.partition
  112. Array.pmap
  113. Array.pop
  114. Array.pop­While
  115. Array.push
  116. Array.qsort
  117. Array.qsort­Ord
  118. Array.range
  119. Array.range'
  120. Array.reduce­Get­Elem
  121. Array.reduce­Get­Elem!
  122. Array.reduce­Get­Elem?
  123. Array.reduce­Option
  124. Array.reverse
  125. Array.set
  126. Array.set!
  127. Array.set­If­In­Bounds
  128. Array.shrink
  129. Array.singleton
  130. Array.size
  131. Array.sum
  132. Array.swap
  133. Array.swap­At
  134. Array.swap­At!
  135. Array.swap­If­In­Bounds
  136. Array.take
  137. Array.take­While
  138. Array.to­List
  139. Array.to­List­Append
  140. Array.to­List­Rev
  141. Array.to­PArray'
  142. Array.to­Subarray
  143. Array.to­Vector
  144. Array.uget
  145. Array.unattach
  146. Array.unzip
  147. Array.uset
  148. Array.usize
  149. Array.zip
  150. Array.zip­Idx
  151. Array.zip­With
  152. Array.zip­With­All
  153. abs
    1. BitVec.abs
    2. Float.abs
    3. Float32.abs
    4. ISize.abs
    5. Int16.abs
    6. Int32.abs
    7. Int64.abs
    8. Int8.abs
  154. absurd
  155. ac_nf
  156. ac_nf0
  157. ac_rfl
  158. accessed
    1. IO.FS.Metadata.accessed (structure field)
  159. acos
    1. Float.acos
    2. Float32.acos
  160. acosh
    1. Float.acosh
    2. Float32.acosh
  161. adapt
    1. ExceptT.adapt
    2. ReaderT.adapt
  162. adapt­Except
    1. EStateM.adapt­Except
  163. adapt­Expander
    1. Lean.Elab.Tactic.adapt­Expander
  164. adc
    1. BitVec.adc
  165. adcb
    1. BitVec.adcb
  166. add
    1. Add.add (class method)
    2. BitVec.add
    3. Fin.add
    4. Float.add
    5. Float32.add
    6. ISize.add
    7. Int.add
    8. Int16.add
    9. Int32.add
    10. Int64.add
    11. Int8.add
    12. Nat.add
    13. UInt16.add
    14. UInt32.add
    15. UInt64.add
    16. UInt8.add
    17. USize.add
  167. add­Cases
    1. Fin.add­Cases
  168. add­Extension
    1. System.FilePath.add­Extension
  169. add­Heartbeats
    1. IO.add­Heartbeats
  170. add­Macro­Scope
    1. Lean.Macro.add­Macro­Scope
  171. add­Nat
    1. Fin.add­Nat
  172. admit
  173. all
    1. Array.all
    2. List.all
    3. Nat.all
    4. Option.all
    5. String.all
    6. Subarray.all
  174. all­Diff
    1. Array.all­Diff
  175. all­I
    1. Prod.all­I
  176. all­M
    1. Array.all­M
    2. List.all­M
    3. Nat.all­M
    4. Subarray.all­M
  177. all­Ones
    1. BitVec.all­Ones
  178. all­TR
    1. Nat.all­TR
  179. all_goals (0) (1)
  180. and
    1. BitVec.and
    2. Bool.and
    3. List.and
  181. and­M
  182. and_intros
  183. any
    1. Array.any
    2. List.any
    3. Nat.any
    4. Option.any
    5. String.any
    6. Subarray.any
  184. any­I
    1. Prod.any­I
  185. any­M
    1. Array.any­M
    2. List.any­M
    3. Nat.any­M
    4. Subarray.any­M
  186. any­TR
    1. Nat.any­TR
  187. any_goals (0) (1)
  188. app­Dir
    1. IO.app­Dir
  189. app­Path
    1. IO.app­Path
  190. append
    1. Append.append (class method)
    2. Array.append
    3. BitVec.append
    4. List.append
    5. String.append
  191. append­Goals
    1. Lean.Elab.Tactic.append­Goals
  192. append­List
    1. Array.append­List
  193. append­TR
    1. List.append­TR
  194. apply (0) (1)
  195. apply?
  196. apply­Eq­Lemma
    1. Nat.apply­Eq­Lemma
  197. apply­Simproc­Const
    1. Nat.apply­Simproc­Const
  198. apply_assumption
  199. apply_ext_theorem
  200. apply_mod_cast
  201. apply_rfl
  202. apply_rules
  203. arg [@]i
  204. args
    1. [anonymous] (structure field)
  205. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  206. array
    1. Subarray.array (structure field)
  207. as­String
    1. List.as­String
  208. as­Task
    1. BaseIO.as­Task
    2. EIO.as­Task
    3. IO.as­Task
  209. as_aux_lemma
  210. asin
    1. Float.asin
    2. Float32.asin
  211. asinh
    1. Float.asinh
    2. Float32.asinh
  212. assumption
    1. inaccessible
  213. assumption_mod_cast
  214. at­End
    1. String.Iterator.at­End
    2. String.at­End
  215. at­Least­Two
    1. Bool.at­Least­Two
  216. atan
    1. Float.atan
    2. Float32.atan
  217. atan2
    1. Float.atan2
    2. Float32.atan2
  218. atanh
    1. Float.atanh
    2. Float32.atanh
  219. attach
    1. Array.attach
    2. List.attach
    3. Option.attach
  220. attach­With
    1. Array.attach­With
    2. List.attach­With
    3. Option.attach­With
  221. auto­Lift
  222. auto­Param
  223. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  224. 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. Bit­Vec
  18. BitVec.abs
  19. BitVec.adc
  20. BitVec.adcb
  21. BitVec.add
  22. BitVec.all­Ones
  23. BitVec.and
  24. BitVec.append
  25. BitVec.carry
  26. BitVec.cast
  27. BitVec.concat
  28. BitVec.cons
  29. BitVec.dec­Eq
  30. BitVec.div­Rec
  31. BitVec.div­Subtract­Shift
  32. BitVec.extract­Lsb
  33. BitVec.extract­Lsb'
  34. BitVec.fill
  35. BitVec.from­Expr?
  36. BitVec.get­Lsb'
  37. BitVec.get­Lsb?
  38. BitVec.get­Lsb­D
  39. BitVec.get­Msb'
  40. BitVec.get­Msb?
  41. BitVec.get­Msb­D
  42. BitVec.hash
  43. BitVec.int­Max
  44. BitVec.int­Min
  45. BitVec.iunfoldr
  46. BitVec.msb
  47. BitVec.mul
  48. BitVec.mul­Rec
  49. BitVec.neg
  50. BitVec.nil
  51. BitVec.not
  52. BitVec.of­Bool
  53. BitVec.of­Bool­List­BE
  54. BitVec.of­Bool­List­LE
  55. BitVec.of­Fin
    1. Constructor of Bit­Vec
  56. BitVec.of­Int
  57. BitVec.of­Nat
  58. BitVec.of­Nat­LT
  59. BitVec.or
  60. BitVec.reduce­Abs
  61. BitVec.reduce­Add
  62. BitVec.reduce­All­Ones
  63. BitVec.reduce­And
  64. BitVec.reduce­Append
  65. BitVec.reduce­BEq
  66. BitVec.reduce­BNe
  67. BitVec.reduce­Bin
  68. BitVec.reduce­Bin­Pred
  69. BitVec.reduce­Bit­Vec­Of­Fin
  70. BitVec.reduce­Bit­Vec­To­Fin
  71. BitVec.reduce­Bool­Pred
  72. BitVec.reduce­Cast
  73. BitVec.reduce­Div
  74. BitVec.reduce­Eq
  75. BitVec.reduce­Extend
  76. BitVec.reduce­Extrac­Lsb'
  77. BitVec.reduce­GE
  78. BitVec.reduce­GT
  79. BitVec.reduce­Get­Bit
  80. BitVec.reduce­Get­Elem
  81. BitVec.reduce­Get­Lsb
  82. BitVec.reduce­Get­Msb
  83. BitVec.reduce­HShift­Left
  84. BitVec.reduce­HShift­Left'
  85. BitVec.reduce­HShift­Right
  86. BitVec.reduce­HShift­Right'
  87. BitVec.reduce­LE
  88. BitVec.reduce­LT
  89. BitVec.reduce­Mod
  90. BitVec.reduce­Mul
  91. BitVec.reduce­Ne
  92. BitVec.reduce­Neg
  93. BitVec.reduce­Not
  94. BitVec.reduce­Of­Int
  95. BitVec.reduce­Of­Nat
  96. BitVec.reduce­Or
  97. BitVec.reduce­Replicate
  98. BitVec.reduce­Rotate­Left
  99. BitVec.reduce­Rotate­Right
  100. BitVec.reduce­SDiv
  101. BitVec.reduce­SLE
  102. BitVec.reduce­SLT
  103. BitVec.reduce­SMTSDiv
  104. BitVec.reduce­SMTUDiv
  105. BitVec.reduce­SMod
  106. BitVec.reduce­SRem
  107. BitVec.reduce­SShift­Right
  108. BitVec.reduce­Set­Width
  109. BitVec.reduce­Set­Width'
  110. BitVec.reduce­Shift
  111. BitVec.reduce­Shift­Left
  112. BitVec.reduce­Shift­Left­Shift­Left
  113. BitVec.reduce­Shift­Left­Zero­Extend
  114. BitVec.reduce­Shift­Right­Shift­Right
  115. BitVec.reduce­Shift­Shift
  116. BitVec.reduce­Shift­With­Bit­Vec­Lit
  117. BitVec.reduce­Sign­Extend
  118. BitVec.reduce­Sub
  119. BitVec.reduce­To­Int
  120. BitVec.reduce­To­Nat
  121. BitVec.reduce­UDiv
  122. BitVec.reduce­ULE
  123. BitVec.reduce­ULT
  124. BitVec.reduce­UMod
  125. BitVec.reduce­UShift­Right
  126. BitVec.reduce­Unary
  127. BitVec.reduce­XOr
  128. BitVec.reduce­Zero­Extend
  129. BitVec.replicate
  130. BitVec.reverse
  131. BitVec.rotate­Left
  132. BitVec.rotate­Right
  133. BitVec.sadd­Overflow
  134. BitVec.sdiv
  135. BitVec.set­Width
  136. BitVec.set­Width'
  137. BitVec.shift­Concat
  138. BitVec.shift­Left
  139. BitVec.shift­Left­Rec
  140. BitVec.shift­Left­Zero­Extend
  141. BitVec.sign­Extend
  142. BitVec.sle
  143. BitVec.slt
  144. BitVec.smod
  145. BitVec.smt­SDiv
  146. BitVec.smt­UDiv
  147. BitVec.srem
  148. BitVec.sshift­Right
  149. BitVec.sshift­Right'
  150. BitVec.sshift­Right­Rec
  151. BitVec.sub
  152. BitVec.to­Hex
  153. BitVec.to­Int
  154. BitVec.to­Nat
  155. BitVec.truncate
  156. BitVec.two­Pow
  157. BitVec.uadd­Overflow
  158. BitVec.udiv
  159. BitVec.ule
  160. BitVec.ult
  161. BitVec.umod
  162. BitVec.ushift­Right
  163. BitVec.ushift­Right­Rec
  164. BitVec.xor
  165. BitVec.zero
  166. BitVec.zero­Extend
  167. Bool
  168. Bool.and
  169. Bool.at­Least­Two
  170. Bool.dec­Eq
  171. Bool.false
    1. Constructor of Bool
  172. Bool.not
  173. Bool.or
  174. Bool.to­ISize
  175. Bool.to­Int
  176. Bool.to­Int16
  177. Bool.to­Int32
  178. Bool.to­Int64
  179. Bool.to­Int8
  180. Bool.to­Nat
  181. Bool.to­UInt16
  182. Bool.to­UInt32
  183. Bool.to­UInt64
  184. Bool.to­UInt8
  185. Bool.to­USize
  186. Bool.true
    1. Constructor of Bool
  187. Bool.xor
  188. Buffer
    1. IO.FS.Stream.Buffer
  189. Build­Type
    1. Lake.Build­Type
  190. back
    1. Array.back
    2. String.back
  191. back!
    1. Array.back!
  192. back?
    1. Array.back?
  193. backward.synthInstance.canon­Instances
  194. bdiv
    1. Int.bdiv
  195. below
    1. Nat.below
  196. beq
    1. BEq.beq (class method)
    2. Float.beq
    3. Float32.beq
    4. List.beq
    5. Nat.beq
  197. beta
    1. Lean.Meta.DSimp.Config.beta (structure field)
    2. Lean.Meta.Simp.Config.beta (structure field)
  198. bin­Insert
    1. Array.bin­Insert
  199. bin­Insert­M
    1. Array.bin­Insert­M
  200. bin­Search
    1. Array.bin­Search
  201. bin­Search­Contains
    1. Array.bin­Search­Contains
  202. 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
    9. Task.bind
    10. Thunk.bind
  203. bind­Cont
    1. ExceptT.bind­Cont
  204. bind­Left
    1. Bind.bind­Left
  205. bind­M
    1. Option.bind­M
  206. bind­Task
    1. BaseIO.bind­Task
    2. EIO.bind­Task
    3. IO.bind­Task
  207. bind_assoc
    1. [anonymous] (class method)
  208. bind_map
    1. [anonymous] (class method)
  209. bind_pure_comp
    1. [anonymous] (class method)
  210. binder­Name­Hint
  211. bitwise
    1. Nat.bitwise
  212. ble
    1. Nat.ble
  213. blt
    1. Nat.blt
  214. bmod
    1. Int.bmod
  215. bootstrap.inductive­Check­Resulting­Universe
  216. build (Lake command)
  217. bv_check
  218. bv_decide
  219. bv_decide?
  220. bv_normalize
  221. bv_omega
  222. by­Cases
    1. Decidable.by­Cases
  223. by_cases
    1. Or.by_cases
  224. by_cases'
    1. Or.by_cases'
  225. byte­Idx
    1. String.Pos.byte­Idx (structure field)
  226. 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. call-by-need
  41. cancel
    1. IO.cancel
  42. canon­Instances
    1. backward.synthInstance.canon­Instances
  43. capitalize
    1. String.capitalize
  44. carry
    1. BitVec.carry
  45. case
  46. case ... => ...
  47. case'
  48. case' ... => ...
  49. case­Strong­Rec­On
    1. Nat.case­Strong­Rec­On
  50. cases
    1. Fin.cases
  51. cases­On
    1. Nat.cases­On
  52. cast
    1. BitVec.cast
    2. Fin.cast
    3. Int.cast
    4. Nat.cast
  53. cast­Add
    1. Fin.cast­Add
  54. cast­LE
    1. Fin.cast­LE
  55. cast­LT
    1. Fin.cast­LT
  56. cast­Succ
    1. Fin.cast­Succ
  57. cast_heq
  58. catch­Exceptions
    1. EIO.catch­Exceptions
  59. cbrt
    1. Float.cbrt
    2. Float32.cbrt
  60. ceil
    1. Float.ceil
    2. Float32.ceil
  61. chain
    1. of coercions
  62. change (0) (1)
  63. change ... with ...
  64. char­Lit­Kind
    1. Lean.char­Lit­Kind
  65. check-build (Lake command)
  66. check-lint (Lake command)
  67. check-test (Lake command)
  68. check­Canceled
    1. IO.check­Canceled
  69. choice
    1. Option.choice
  70. choice­Kind
    1. Lean.choice­Kind
  71. choose
    1. Exists.choose
  72. classical
  73. clean (Lake command)
  74. clear
  75. close­Main­Goal
    1. Lean.Elab.Tactic.close­Main­Goal
  76. close­Main­Goal­Using
    1. Lean.Elab.Tactic.close­Main­Goal­Using
  77. cmd
    1. [anonymous] (structure field)
  78. codepoint­Pos­To­Utf16Pos
    1. String.codepoint­Pos­To­Utf16Pos
  79. codepoint­Pos­To­Utf16Pos­From
    1. String.codepoint­Pos­To­Utf16Pos­From
  80. codepoint­Pos­To­Utf8Pos­From
    1. String.codepoint­Pos­To­Utf8Pos­From
  81. 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)
  82. col­Eq
  83. col­Ge
  84. col­Gt
  85. comment
    1. block
    2. line
  86. comp_map
    1. LawfulFunctor.comp_map (class method)
  87. compare
    1. Ord.compare (class method)
  88. 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
  89. components
    1. System.FilePath.components
  90. concat
    1. BitVec.concat
    2. List.concat
  91. cond
  92. configuration
    1. of tactics
  93. congr (0) (1) (2)
  94. congr­Arg
  95. congr­Fun
  96. cons
    1. BitVec.cons
  97. constructor (0) (1)
  98. contains
    1. Array.contains
    2. List.contains
    3. String.contains
  99. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  100. contradiction
  101. control
  102. control­At
  103. conv
  104. conv => ...
  105. conv' (0) (1)
  106. cos
    1. Float.cos
    2. Float32.cos
  107. cosh
    1. Float.cosh
    2. Float32.cosh
  108. count
    1. Array.count
    2. List.count
  109. count­P
    1. Array.count­P
    2. List.count­P
  110. create­Dir
    1. IO.FS.create­Dir
  111. create­Dir­All
    1. IO.FS.create­Dir­All
  112. create­Temp­Dir
    1. IO.FS.create­Temp­Dir
  113. create­Temp­File
    1. IO.FS.create­Temp­File
  114. crlf­To­Lf
    1. String.crlf­To­Lf
  115. csup
    1. [anonymous] (class method)
  116. csup_spec
    1. [anonymous] (class method)
  117. cumulativity
  118. curr
    1. String.Iterator.curr
  119. current­Dir
    1. IO.current­Dir
  120. custom­Eliminators
    1. tactic.custom­Eliminators
  121. 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_trace
  18. dec­Eq
    1. BitVec.dec­Eq
    2. Bool.dec­Eq
    3. ISize.dec­Eq
    4. Int.dec­Eq
    5. Int16.dec­Eq
    6. Int32.dec­Eq
    7. Int64.dec­Eq
    8. Int8.dec­Eq
    9. Nat.dec­Eq
    10. String.dec­Eq
    11. UInt16.dec­Eq
    12. UInt32.dec­Eq
    13. UInt64.dec­Eq
    14. UInt8.dec­Eq
    15. USize.dec­Eq
  19. dec­Le
    1. Float.dec­Le
    2. Float32.dec­Le
    3. ISize.dec­Le
    4. Int16.dec­Le
    5. Int32.dec­Le
    6. Int64.dec­Le
    7. Int8.dec­Le
    8. Nat.dec­Le
    9. UInt16.dec­Le
    10. UInt32.dec­Le
    11. UInt64.dec­Le
    12. UInt8.dec­Le
    13. USize.dec­Le
  20. dec­Lt
    1. Float.dec­Lt
    2. Float32.dec­Lt
    3. ISize.dec­Lt
    4. Int16.dec­Lt
    5. Int32.dec­Lt
    6. Int64.dec­Lt
    7. Int8.dec­Lt
    8. Nat.dec­Lt
    9. UInt16.dec­Lt
    10. UInt32.dec­Lt
    11. UInt64.dec­Lt
    12. UInt8.dec­Lt
    13. USize.dec­Lt
  21. decapitalize
    1. String.decapitalize
  22. decidable
  23. decidable_eq_none
    1. Option.decidable_eq_none
  24. decide
    1. Decidable.decide
    2. Lean.Meta.DSimp.Config.decide (structure field)
    3. Lean.Meta.Simp.Config.decide (structure field)
  25. decreasing_tactic
  26. decreasing_trivial
  27. decreasing_with
  28. dedicated
    1. Task.Priority.dedicated
  29. deep­Terms
    1. pp.deep­Terms
  30. default
    1. Inhabited.default (class method)
    2. Task.Priority.default
  31. default­Facets
    1. [anonymous] (structure field)
  32. delta (0) (1)
  33. diff
    1. guard_msgs.diff
  34. digit­Char
    1. Nat.digit­Char
  35. discard
    1. Functor.discard
  36. discharge
    1. trace.Meta.Tactic.simp.discharge
  37. div
    1. Div.div (class method)
    2. Fin.div
    3. Float.div
    4. Float32.div
    5. ISize.div
    6. Int16.div
    7. Int32.div
    8. Int64.div
    9. Int8.div
    10. Nat.div
    11. UInt16.div
    12. UInt32.div
    13. UInt64.div
    14. UInt8.div
    15. USize.div
  38. div2Induction
    1. Nat.div2Induction
  39. div­Rec
    1. BitVec.div­Rec
  40. div­Subtract­Shift
    1. BitVec.div­Subtract­Shift
  41. done (0) (1)
  42. down
    1. PLift.down (structure field)
    2. ULift.down (structure field)
  43. drop
    1. Array.drop
    2. List.drop
    3. String.drop
    4. Subarray.drop
  44. drop­Last
    1. List.drop­Last
  45. drop­Last­TR
    1. List.drop­Last­TR
  46. drop­Prefix?
    1. String.drop­Prefix?
  47. drop­Right
    1. String.drop­Right
  48. drop­Right­While
    1. String.drop­Right­While
  49. drop­Suffix?
    1. String.drop­Suffix?
  50. drop­While
    1. List.drop­While
    2. String.drop­While
  51. dsimp (0) (1)
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  52. dsimp!
  53. dsimp?
  54. dsimp?!
  55. dsimp­Location'
    1. Lean.Elab.Tactic.dsimp­Location'
  56. 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. Eq
  38. Eq.mp
  39. Eq.mpr
  40. Eq.refl
    1. Constructor of Eq
  41. Eq.subst
  42. Eq.symm
  43. Eq.trans
  44. Equiv
    1. HasEquiv.Equiv (class method)
  45. Equivalence
  46. Equivalence.mk
    1. Constructor of Equivalence
  47. Error
    1. IO.Error
  48. Even
  49. Even.plus­Two
    1. Constructor of Even
  50. Even.zero
    1. Constructor of Even
  51. Except
  52. Except.bind
  53. Except.error
    1. Constructor of Except
  54. Except.is­Ok
  55. Except.map
  56. Except.map­Error
  57. Except.ok
    1. Constructor of Except
  58. Except.or­Else­Lazy
  59. Except.pure
  60. Except.to­Bool
  61. Except.to­Option
  62. Except.try­Catch
  63. Except­Cps­T
  64. Except­CpsT.lift
  65. Except­CpsT.run
  66. Except­CpsT.run­Catch
  67. Except­CpsT.run­K
  68. Except­T
  69. ExceptT.adapt
  70. ExceptT.bind
  71. ExceptT.bind­Cont
  72. ExceptT.lift
  73. ExceptT.map
  74. ExceptT.mk
  75. ExceptT.pure
  76. ExceptT.run
  77. ExceptT.try­Catch
  78. Exists
  79. Exists.choose
  80. Exists.intro
    1. Constructor of Exists
  81. ediv
    1. Int.ediv
  82. elab­DSimp­Config­Core
    1. Lean.Elab.Tactic.elab­DSimp­Config­Core
  83. elab­Simp­Args
    1. Lean.Elab.Tactic.elab­Simp­Args
  84. elab­Simp­Config
    1. Lean.Elab.Tactic.elab­Simp­Config
  85. elab­Simp­Config­Ctx­Core
    1. Lean.Elab.Tactic.elab­Simp­Config­Ctx­Core
  86. elab­Term
    1. Lean.Elab.Tactic.elab­Term
  87. elab­Term­Ensuring­Type
    1. Lean.Elab.Tactic.elab­Term­Ensuring­Type
  88. elab­Term­With­Holes
    1. Lean.Elab.Tactic.elab­Term­With­Holes
  89. elem
    1. Array.elem
    2. List.elem
  90. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  91. elim
    1. And.elim
    2. Empty.elim
    3. False.elim
    4. HEq.elim
    5. Iff.elim
    6. Not.elim
    7. Option.elim
    8. PEmpty.elim
    9. Sum.elim
  92. elim0
    1. Fin.elim0
  93. elim­M
    1. Option.elim­M
  94. elim­Offset
    1. Nat.elim­Offset
  95. emod
    1. Int.emod
  96. empty
    1. Array.empty
    2. Subarray.empty
  97. end­Pos
    1. String.end­Pos
  98. ends­With
    1. String.ends­With
  99. ensure­Has­No­MVars
    1. Lean.Elab.Tactic.ensure­Has­No­MVars
  100. enter
  101. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  102. env (Lake command)
  103. environment variables
  104. eprint
    1. IO.eprint
  105. eprintln
    1. IO.eprintln
  106. eq­Rec_heq
  107. eq_of_beq
    1. LawfulBEq.eq_of_beq (class method)
  108. eq_of_heq
  109. eq_refl
  110. erase
    1. Array.erase
    2. List.erase
  111. erase­Dups
    1. List.erase­Dups
  112. erase­Idx
    1. Array.erase­Idx
    2. List.erase­Idx
  113. erase­Idx!
    1. Array.erase­Idx!
  114. erase­Idx­If­In­Bounds
    1. Array.erase­Idx­If­In­Bounds
  115. erase­Idx­TR
    1. List.erase­Idx­TR
  116. erase­P
    1. Array.erase­P
    2. List.erase­P
  117. erase­PTR
    1. List.erase­PTR
  118. erase­Reps
    1. Array.erase­Reps
    2. List.erase­Reps
  119. erase­TR
    1. List.erase­TR
  120. erw (0) (1)
  121. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.eta (structure field)
  122. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
    2. Lean.Meta.Simp.Config.eta­Struct (structure field)
  123. eval.derive.repr
  124. eval.pp
  125. eval.type
  126. exact
    1. Quotient.exact
  127. exact?
  128. exact_mod_cast
  129. exe (Lake command)
  130. exe­Extension
    1. System.FilePath.exe­Extension
  131. exe­Name
    1. [anonymous] (structure field)
  132. exfalso
  133. exists
  134. exit
    1. IO.Process.exit
  135. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  136. exp
    1. Float.exp
    2. Float32.exp
  137. exp2
    1. Float.exp2
    2. Float32.exp2
  138. expand­Macro?
    1. Lean.Macro.expand­Macro?
  139. expose_names
  140. ext (0) (1)
  141. ext1
  142. ext­Separator
    1. System.FilePath.ext­Separator
  143. extension
    1. System.FilePath.extension
  144. extensionality
    1. of propositions
  145. extra­Dep­Targets
    1. [anonymous] (structure field) (0) (1)
  146. extract
    1. Array.extract
    2. List.extract
    3. String.Iterator.extract
    4. String.extract
  147. extract­Lsb
    1. BitVec.extract­Lsb
  148. extract­Lsb'
    1. BitVec.extract­Lsb'

F

  1. False
  2. False.elim
  3. File­Path
    1. System.File­Path
  4. File­Right
    1. IO.File­Right
  5. Fin
  6. Fin.add
  7. Fin.add­Cases
  8. Fin.add­Nat
  9. Fin.cases
  10. Fin.cast
  11. Fin.cast­Add
  12. Fin.cast­LE
  13. Fin.cast­LT
  14. Fin.cast­Succ
  15. Fin.div
  16. Fin.elim0
  17. Fin.foldl
  18. Fin.foldl­M
  19. Fin.foldr
  20. Fin.foldr­M
  21. Fin.from­Expr?
  22. Fin.h­Iterate
  23. Fin.h­Iterate­From
  24. Fin.induction
  25. Fin.induction­On
  26. Fin.is­Value
  27. Fin.land
  28. Fin.last
  29. Fin.last­Cases
  30. Fin.log2
  31. Fin.lor
  32. Fin.mk
    1. Constructor of Fin
  33. Fin.mod
  34. Fin.modn
  35. Fin.mul
  36. Fin.nat­Add
  37. Fin.of­Nat'
  38. Fin.pred
  39. Fin.reduce­Add
  40. Fin.reduce­Add­Nat
  41. Fin.reduce­And
  42. Fin.reduce­BEq
  43. Fin.reduce­BNe
  44. Fin.reduce­Bin
  45. Fin.reduce­Bin­Pred
  46. Fin.reduce­Bool­Pred
  47. Fin.reduce­Cast­Add
  48. Fin.reduce­Cast­LE
  49. Fin.reduce­Cast­LT
  50. Fin.reduce­Cast­Succ
  51. Fin.reduce­Div
  52. Fin.reduce­Eq
  53. Fin.reduce­Fin­Mk
  54. Fin.reduce­GE
  55. Fin.reduce­GT
  56. Fin.reduce­LE
  57. Fin.reduce­LT
  58. Fin.reduce­Last
  59. Fin.reduce­Mod
  60. Fin.reduce­Mul
  61. Fin.reduce­Nat­Add
  62. Fin.reduce­Nat­Op
  63. Fin.reduce­Ne
  64. Fin.reduce­Of­Nat'
  65. Fin.reduce­Op
  66. Fin.reduce­Or
  67. Fin.reduce­Pred
  68. Fin.reduce­Rev
  69. Fin.reduce­Shift­Left
  70. Fin.reduce­Shift­Right
  71. Fin.reduce­Sub
  72. Fin.reduce­Sub­Nat
  73. Fin.reduce­Succ
  74. Fin.reduce­Xor
  75. Fin.rev
  76. Fin.reverse­Induction
  77. Fin.shift­Left
  78. Fin.shift­Right
  79. Fin.sub
  80. Fin.sub­Nat
  81. Fin.succ
  82. Fin.succ­Rec
  83. Fin.succ­Rec­On
  84. Fin.to­Nat
  85. Fin.xor
  86. Float
  87. Float.abs
  88. Float.acos
  89. Float.acosh
  90. Float.add
  91. Float.asin
  92. Float.asinh
  93. Float.atan
  94. Float.atan2
  95. Float.atanh
  96. Float.beq
  97. Float.cbrt
  98. Float.ceil
  99. Float.cos
  100. Float.cosh
  101. Float.dec­Le
  102. Float.dec­Lt
  103. Float.div
  104. Float.exp
  105. Float.exp2
  106. Float.floor
  107. Float.fr­Exp
  108. Float.is­Finite
  109. Float.is­Inf
  110. Float.is­Na­N
  111. Float.le
  112. Float.log
  113. Float.log10
  114. Float.log2
  115. Float.lt
  116. Float.mk
    1. Constructor of Float
  117. Float.mul
  118. Float.neg
  119. Float.of­Binary­Scientific
  120. Float.of­Bits
  121. Float.of­Int
  122. Float.of­Nat
  123. Float.of­Scientific
  124. Float.pow
  125. Float.round
  126. Float.scale­B
  127. Float.sin
  128. Float.sinh
  129. Float.sqrt
  130. Float.sub
  131. Float.tan
  132. Float.tanh
  133. Float.to­Bits
  134. Float.to­Float32
  135. Float.to­ISize
  136. Float.to­Int16
  137. Float.to­Int32
  138. Float.to­Int64
  139. Float.to­Int8
  140. Float.to­String
  141. Float.to­UInt16
  142. Float.to­UInt32
  143. Float.to­UInt64
  144. Float.to­UInt8
  145. Float.to­USize
  146. Float32
  147. Float32.abs
  148. Float32.acos
  149. Float32.acosh
  150. Float32.add
  151. Float32.asin
  152. Float32.asinh
  153. Float32.atan
  154. Float32.atan2
  155. Float32.atanh
  156. Float32.beq
  157. Float32.cbrt
  158. Float32.ceil
  159. Float32.cos
  160. Float32.cosh
  161. Float32.dec­Le
  162. Float32.dec­Lt
  163. Float32.div
  164. Float32.exp
  165. Float32.exp2
  166. Float32.floor
  167. Float32.fr­Exp
  168. Float32.is­Finite
  169. Float32.is­Inf
  170. Float32.is­Na­N
  171. Float32.le
  172. Float32.log
  173. Float32.log10
  174. Float32.log2
  175. Float32.lt
  176. Float32.mk
    1. Constructor of Float32
  177. Float32.mul
  178. Float32.neg
  179. Float32.of­Binary­Scientific
  180. Float32.of­Bits
  181. Float32.of­Int
  182. Float32.of­Nat
  183. Float32.of­Scientific
  184. Float32.pow
  185. Float32.round
  186. Float32.scale­B
  187. Float32.sin
  188. Float32.sinh
  189. Float32.sqrt
  190. Float32.sub
  191. Float32.tan
  192. Float32.tanh
  193. Float32.to­Bits
  194. Float32.to­Float
  195. Float32.to­ISize
  196. Float32.to­Int16
  197. Float32.to­Int32
  198. Float32.to­Int64
  199. Float32.to­Int8
  200. Float32.to­String
  201. Float32.to­UInt16
  202. Float32.to­UInt32
  203. Float32.to­UInt64
  204. Float32.to­UInt8
  205. Float32.to­USize
  206. For­In
  207. For­In'
  208. ForIn'.mk
    1. Instance constructor of For­In'
  209. ForIn.mk
    1. Instance constructor of For­In
  210. For­In­Step
  211. For­InStep.done
    1. Constructor of For­In­Step
  212. For­InStep.yield
    1. Constructor of For­In­Step
  213. For­M
  214. ForM.for­In
  215. ForM.mk
    1. Instance constructor of For­M
  216. Functor
  217. Functor.discard
  218. Functor.map­Rev
  219. Functor.mk
    1. Instance constructor of Functor
  220. fail
    1. OptionT.fail
  221. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
    2. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  222. fail_if_success (0) (1)
  223. failure
    1. ReaderT.failure
    2. StateT.failure
    3. [anonymous] (class method)
  224. false_or_by_contra
  225. fdiv
    1. Int.fdiv
  226. field­Idx­Kind
    1. Lean.field­Idx­Kind
  227. field­Notation
    1. pp.field­Notation
  228. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
    2. System.FilePath.file­Name
  229. file­Stem
    1. System.FilePath.file­Stem
  230. fill
    1. BitVec.fill
  231. filter
    1. Array.filter
    2. List.filter
    3. Option.filter
  232. filter­M
    1. Array.filter­M
    2. List.filter­M
  233. filter­Map
    1. Array.filter­Map
    2. List.filter­Map
  234. filter­Map­M
    1. Array.filter­Map­M
    2. List.filter­Map­M
  235. filter­Map­TR
    1. List.filter­Map­TR
  236. filter­Pairs­M
    1. Array.filter­Pairs­M
  237. filter­Rev­M
    1. Array.filter­Rev­M
    2. List.filter­Rev­M
  238. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  239. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  240. filter­TR
    1. List.filter­TR
  241. fin­Idx­Of?
    1. Array.fin­Idx­Of?
    2. List.fin­Idx­Of?
  242. fin­Range
    1. Array.fin­Range
    2. List.fin­Range
  243. find
    1. String.find
  244. find?
    1. Array.find?
    2. List.find?
  245. find­Extern­Lib?
    1. Lake.find­Extern­Lib?
  246. find­Fin­Idx?
    1. Array.find­Fin­Idx?
    2. List.find­Fin­Idx?
  247. find­Idx
    1. Array.find­Idx
    2. List.find­Idx
  248. find­Idx?
    1. Array.find­Idx?
    2. List.find­Idx?
  249. find­Idx­M?
    1. Array.find­Idx­M?
  250. find­Lean­Exe?
    1. Lake.find­Lean­Exe?
  251. find­Lean­Lib?
    1. Lake.find­Lean­Lib?
  252. find­Line­Start
    1. String.find­Line­Start
  253. find­M?
    1. Array.find­M?
    2. List.find­M?
  254. find­Module?
    1. Lake.find­Module?
  255. find­Package?
    1. Lake.find­Package?
  256. find­Rev?
    1. Array.find­Rev?
    2. Subarray.find­Rev?
  257. find­Rev­M?
    1. Array.find­Rev­M?
    2. Subarray.find­Rev­M?
  258. find­Some!
    1. Array.find­Some!
  259. find­Some?
    1. Array.find­Some?
    2. List.find­Some?
  260. find­Some­M?
    1. Array.find­Some­M?
    2. List.find­Some­M?
  261. find­Some­Rev?
    1. Array.find­Some­Rev?
  262. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
    2. Subarray.find­Some­Rev­M?
  263. first (0) (1)
  264. first­Diff­Pos
    1. String.first­Diff­Pos
  265. first­M
    1. Array.first­M
    2. List.first­M
  266. fix
    1. Lean.Order.fix
    2. WellFounded.fix
  267. fix_eq
    1. Lean.Order.fix_eq
  268. flags
    1. IO.FileRight.flags
  269. flat­Map
    1. Array.flat­Map (0) (1)
    2. List.flat­Map
  270. flat­Map­M
    1. Array.flat­Map­M (0) (1)
    2. List.flat­Map­M
  271. flat­Map­TR
    1. List.flat­Map­TR
  272. flatten
    1. Array.flatten
    2. List.flatten
  273. flatten­TR
    1. List.flatten­TR
  274. floor
    1. Float.floor
    2. Float32.floor
  275. flush
    1. IO.FS.Handle.flush
    2. IO.FS.Stream.flush (structure field)
  276. fmod
    1. Int.fmod
  277. fn
    1. _private.Init.Core.0.Thunk.fn (structure field)
  278. focus (0) (1)
    1. Lean.Elab.Tactic.focus
  279. fold
    1. Nat.fold
  280. fold­I
    1. Prod.fold­I
  281. fold­M
    1. Nat.fold­M
  282. fold­Rev
    1. Nat.fold­Rev
  283. fold­Rev­M
    1. Nat.fold­Rev­M
  284. fold­TR
    1. Nat.fold­TR
  285. foldl
    1. Array.foldl
    2. Fin.foldl
    3. List.foldl
    4. String.foldl
    5. Subarray.foldl
  286. foldl­M
    1. Array.foldl­M
    2. Fin.foldl­M
    3. List.foldl­M
    4. Subarray.foldl­M
  287. foldl­Rec­On
    1. List.foldl­Rec­On
  288. foldr
    1. Array.foldr
    2. Fin.foldr
    3. List.foldr
    4. String.foldr
    5. Subarray.foldr
  289. foldr­M
    1. Array.foldr­M
    2. Fin.foldr­M
    3. List.foldr­M
    4. Subarray.foldr­M
  290. foldr­Rec­On
    1. List.foldr­Rec­On
  291. foldr­TR
    1. List.foldr­TR
  292. fopen­Error­To­String
    1. IO.Error.fopen­Error­To­String
  293. for­A
    1. List.for­A
  294. for­In
    1. ForIn.for­In (class method)
    2. ForM.for­In
    3. Subarray.for­In
  295. for­In'
    1. Array.for­In'
    2. ForIn'.for­In' (class method)
    3. List.for­In'
  296. 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
  297. for­Rev­M
    1. Array.for­Rev­M
    2. Nat.for­Rev­M
    3. Subarray.for­Rev­M
  298. format
    1. Option.format
  299. forward
    1. String.Iterator.forward
  300. fr­Exp
    1. Float.fr­Exp
    2. Float32.fr­Exp
  301. from­Expr
    1. UInt16.from­Expr
    2. UInt32.from­Expr
    3. UInt64.from­Expr
    4. UInt8.from­Expr
    5. USize.from­Expr
  302. from­Expr?
    1. BitVec.from­Expr?
    2. Fin.from­Expr?
    3. Int.from­Expr?
    4. Nat.from­Expr?
    5. String.from­Expr?
  303. from­State­M
    1. EStateM.from­State­M
  304. from­UTF8
    1. String.from­UTF8
  305. from­UTF8!
    1. String.from­UTF8!
  306. from­UTF8?
    1. String.from­UTF8?
  307. front
    1. String.front
  308. 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)
  309. fun
  310. fun_cases
  311. fun_induction
  312. 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. EStateM.get
    2. List.get
    3. MonadState.get
    4. MonadState.get (class method)
    5. Monad­StateOf.get (class method)
    6. Option.get
    7. ST.Ref.get
    8. State­RefT'.get
    9. StateT.get
    10. String.get
    11. Subarray.get
    12. Task.get
    13. Task.get (structure field)
    14. Thunk.get
  9. get!
    1. Option.get!
    2. String.get!
    3. Subarray.get!
  10. get'
    1. String.get'
  11. get?
    1. Dynamic.get?
    2. 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­Kind
    1. Lean.Syntax.get­Kind
  42. get­Lake
    1. Lake.get­Lake
  43. get­Lake­Env
    1. Lake.get­Lake­Env
  44. get­Lake­Home
    1. Lake.get­Lake­Home
  45. get­Lake­Install
    1. Lake.get­Lake­Install
  46. get­Lake­Lib­Dir
    1. Lake.get­Lake­Lib­Dir
  47. get­Lake­Src­Dir
    1. Lake.get­Lake­Src­Dir
  48. get­Last
    1. List.get­Last
  49. get­Last!
    1. List.get­Last!
  50. get­Last?
    1. List.get­Last?
  51. get­Last­D
    1. List.get­Last­D
  52. get­Lean
    1. Lake.get­Lean
  53. get­Lean­Ar
    1. Lake.get­Lean­Ar
  54. get­Lean­Cc
    1. Lake.get­Lean­Cc
  55. get­Lean­Cc?
    1. Lake.get­Lean­Cc?
  56. get­Lean­Include­Dir
    1. Lake.get­Lean­Include­Dir
  57. get­Lean­Install
    1. Lake.get­Lean­Install
  58. get­Lean­Lib­Dir
    1. Lake.get­Lean­Lib­Dir
  59. get­Lean­Path
    1. Lake.get­Lean­Path
  60. get­Lean­Shared­Lib
    1. Lake.get­Lean­Shared­Lib
  61. get­Lean­Src­Dir
    1. Lake.get­Lean­Src­Dir
  62. get­Lean­Src­Path
    1. Lake.get­Lean­Src­Path
  63. get­Lean­Sysroot
    1. Lake.get­Lean­Sysroot
  64. get­Lean­System­Lib­Dir
    1. Lake.get­Lean­System­Lib­Dir
  65. get­Leanc
    1. Lake.get­Leanc
  66. get­Left
    1. Sum.get­Left
  67. get­Left?
    1. Sum.get­Left?
  68. get­Line
    1. IO.FS.Handle.get­Line
    2. IO.FS.Stream.get­Line (structure field)
  69. get­Lsb'
    1. BitVec.get­Lsb'
  70. get­Lsb?
    1. BitVec.get­Lsb?
  71. get­Lsb­D
    1. BitVec.get­Lsb­D
  72. get­M
    1. Option.get­M
  73. get­Main­Goal
    1. Lean.Elab.Tactic.get­Main­Goal
  74. get­Main­Module
    1. Lean.Elab.Tactic.get­Main­Module
  75. get­Main­Tag
    1. Lean.Elab.Tactic.get­Main­Tag
  76. get­Max?
    1. Array.get­Max?
  77. get­Modify
  78. get­Msb'
    1. BitVec.get­Msb'
  79. get­Msb?
    1. BitVec.get­Msb?
  80. get­Msb­D
    1. BitVec.get­Msb­D
  81. get­Name
    1. Lean.TSyntax.get­Name
  82. get­Nat
    1. Lean.TSyntax.get­Nat
  83. get­No­Cache
    1. Lake.get­No­Cache
  84. get­Num­Heartbeats
    1. IO.get­Num­Heartbeats
  85. get­PID
    1. IO.Process.get­PID
  86. get­Pkg­Url­Map
    1. Lake.get­Pkg­Url­Map
  87. get­Random­Bytes
    1. IO.get­Random­Bytes
  88. get­Right
    1. Sum.get­Right
  89. get­Right?
    1. Sum.get­Right?
  90. get­Root­Package
    1. Lake.get­Root­Package
  91. get­Scientific
    1. Lean.TSyntax.get­Scientific
  92. get­Shared­Lib­Path
    1. Lake.get­Shared­Lib­Path
  93. get­Stderr
    1. IO.get­Stderr
  94. get­Stdin
    1. IO.get­Stdin
  95. get­Stdout
    1. IO.get­Stdout
  96. get­String
    1. Lean.TSyntax.get­String
  97. get­TID
    1. IO.get­TID
  98. get­Task­State
    1. IO.get­Task­State
  99. get­The
  100. get­Try­Cache
    1. Lake.get­Try­Cache
  101. get­Unsolved­Goals
    1. Lean.Elab.Tactic.get­Unsolved­Goals
  102. get­Utf8Byte
    1. String.get­Utf8Byte
  103. get­Workspace
    1. Lake.MonadWorkspace.get­Workspace (class method)
  104. get_elem_tactic
  105. get_elem_tactic_trivial
  106. globs
    1. [anonymous] (structure field)
  107. goal
    1. main
  108. ground
    1. Lean.Meta.Simp.Config.ground (structure field)
  109. group
    1. IO.FileRight.group (structure field)
  110. group­By­Key
    1. Array.group­By­Key
    2. List.group­By­Key
  111. group­Kind
    1. Lean.group­Kind
  112. guard
    1. Option.guard
  113. guard_expr
  114. guard_hyp
  115. guard_msgs.diff
  116. 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. HEq
  10. HEq.elim
  11. HEq.ndrec
  12. HEq.ndrec­On
  13. HEq.refl
    1. Constructor of HEq
  14. HEq.rfl
  15. HEq.subst
  16. HMod
  17. HMod.mk
    1. Instance constructor of HMod
  18. HMul
  19. HMul.mk
    1. Instance constructor of HMul
  20. HOr
  21. HOr.mk
    1. Instance constructor of HOr
  22. HPow
  23. HPow.mk
    1. Instance constructor of HPow
  24. HShift­Left
  25. HShiftLeft.mk
    1. Instance constructor of HShift­Left
  26. HShift­Right
  27. HShiftRight.mk
    1. Instance constructor of HShift­Right
  28. HSub
  29. HSub.mk
    1. Instance constructor of HSub
  30. HXor
  31. HXor.mk
    1. Instance constructor of HXor
  32. Handle
    1. IO.FS.Handle
  33. Has­Equiv
  34. HasEquiv.mk
    1. Instance constructor of Has­Equiv
  35. Hashable
  36. Hashable.mk
    1. Instance constructor of Hashable
  37. Homogeneous­Pow
  38. HomogeneousPow.mk
    1. Instance constructor of Homogeneous­Pow
  39. Hygiene­Info
    1. Lean.Syntax.Hygiene­Info
  40. h
    1. ST.Ref.h (structure field)
  41. h­Add
    1. HAdd.h­Add (class method)
  42. h­And
    1. HAnd.h­And (class method)
  43. h­Append
    1. HAppend.h­Append (class method)
  44. h­Div
    1. HDiv.h­Div (class method)
  45. h­Iterate
    1. Fin.h­Iterate
  46. h­Iterate­From
    1. Fin.h­Iterate­From
  47. h­Mod
    1. HMod.h­Mod (class method)
  48. h­Mul
    1. HMul.h­Mul (class method)
  49. h­Or
    1. HOr.h­Or (class method)
  50. h­Pow
    1. HPow.h­Pow (class method)
  51. h­Shift­Left
    1. HShiftLeft.h­Shift­Left (class method)
  52. h­Shift­Right
    1. HShiftRight.h­Shift­Right (class method)
  53. h­Sub
    1. HSub.h­Sub (class method)
  54. h­Xor
    1. HXor.h­Xor (class method)
  55. has­Bind
    1. Id.has­Bind
  56. has­Dec­Eq
    1. List.has­Dec­Eq
  57. has­Decl
    1. Lean.Macro.has­Decl
  58. has­Finished
    1. IO.has­Finished
  59. has­Next
    1. String.Iterator.has­Next
  60. has­Prev
    1. String.Iterator.has­Prev
  61. hash
    1. BitVec.hash
    2. Hashable.hash (class method)
    3. String.hash
  62. have
  63. have'
  64. have­I
  65. head
    1. List.head
  66. head!
    1. List.head!
  67. head?
    1. List.head?
  68. head­D
    1. List.head­D
  69. heq_of_eq
  70. heq_of_eq­Rec_eq
  71. heq_of_heq_of_eq
  72. hrec­On
    1. Quot.hrec­On
    2. Quotient.hrec­On
  73. hygiene
    1. in tactics
  74. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  75. 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­Dir
  89. IO.FS.create­Temp­File
  90. IO.FS.lines
  91. IO.FS.read­Bin­File
  92. IO.FS.read­File
  93. IO.FS.real­Path
  94. IO.FS.remove­Dir
  95. IO.FS.remove­Dir­All
  96. IO.FS.remove­File
  97. IO.FS.rename
  98. IO.FS.with­File
  99. IO.FS.with­Isolated­Streams (0) (1)
  100. IO.FS.with­Temp­Dir
  101. IO.FS.with­Temp­File
  102. IO.FS.write­Bin­File
  103. IO.FS.write­File
  104. IO.File­Right
  105. IO.FileRight.flags
  106. IO.FileRight.mk
    1. Constructor of IO.File­Right
  107. IO.Process.Child
  108. IO.Process.Child.kill
  109. IO.Process.Child.mk
    1. Constructor of IO.Process.Child
  110. IO.Process.Child.take­Stdin
  111. IO.Process.Child.try­Wait
  112. IO.Process.Child.wait
  113. IO.Process.Output
  114. IO.Process.Output.mk
    1. Constructor of IO.Process.Output
  115. IO.Process.Spawn­Args
  116. IO.Process.SpawnArgs.mk
    1. Constructor of IO.Process.Spawn­Args
  117. IO.Process.Stdio
  118. IO.Process.Stdio.inherit
    1. Constructor of IO.Process.Stdio
  119. IO.Process.Stdio.null
    1. Constructor of IO.Process.Stdio
  120. IO.Process.Stdio.piped
    1. Constructor of IO.Process.Stdio
  121. IO.Process.Stdio.to­Handle­Type
  122. IO.Process.Stdio­Config
  123. IO.Process.StdioConfig.mk
    1. Constructor of IO.Process.Stdio­Config
  124. IO.Process.exit
  125. IO.Process.get­Current­Dir
  126. IO.Process.get­PID
  127. IO.Process.output
  128. IO.Process.run
  129. IO.Process.set­Current­Dir
  130. IO.Process.spawn
  131. IO.Ref
  132. IO.add­Heartbeats
  133. IO.app­Dir
  134. IO.app­Path
  135. IO.as­Task
  136. IO.bind­Task
  137. IO.cancel
  138. IO.check­Canceled
  139. IO.current­Dir
  140. IO.eprint
  141. IO.eprintln
  142. IO.get­Env
  143. IO.get­Num­Heartbeats
  144. IO.get­Random­Bytes
  145. IO.get­Stderr
  146. IO.get­Stdin
  147. IO.get­Stdout
  148. IO.get­TID
  149. IO.get­Task­State
  150. IO.has­Finished
  151. IO.iterate
  152. IO.lazy­Pure
  153. IO.map­Task
  154. IO.map­Tasks
  155. IO.mk­Ref
  156. IO.mono­Ms­Now
  157. IO.mono­Nanos­Now
  158. IO.of­Except
  159. IO.print
  160. IO.println
  161. IO.rand
  162. IO.set­Access­Rights
  163. IO.set­Rand­Seed
  164. IO.set­Stderr
  165. IO.set­Stdin
  166. IO.set­Stdout
  167. IO.sleep
  168. IO.to­EIO
  169. IO.user­Error
  170. IO.wait
  171. IO.wait­Any
  172. IO.with­Stderr
  173. IO.with­Stdin
  174. IO.with­Stdout
  175. ISize
  176. ISize.abs
  177. ISize.add
  178. ISize.complement
  179. ISize.dec­Eq
  180. ISize.dec­Le
  181. ISize.dec­Lt
  182. ISize.div
  183. ISize.land
  184. ISize.le
  185. ISize.lor
  186. ISize.lt
  187. ISize.max­Value
  188. ISize.min­Value
  189. ISize.mod
  190. ISize.mul
  191. ISize.neg
  192. ISize.of­Bit­Vec
  193. ISize.of­Int
  194. ISize.of­Int­LE
  195. ISize.of­Int­Truncate
  196. ISize.of­Nat
  197. ISize.shift­Left
  198. ISize.shift­Right
  199. ISize.size
  200. ISize.sub
  201. ISize.to­Bit­Vec
  202. ISize.to­Float
  203. ISize.to­Float32
  204. ISize.to­Int
  205. ISize.to­Int16
  206. ISize.to­Int32
  207. ISize.to­Int64
  208. ISize.to­Int8
  209. ISize.to­Nat­Clamp­Neg
  210. ISize.xor
  211. Id
  212. Id.has­Bind
  213. Id.run
  214. Ident
    1. Lean.Syntax.Ident
  215. Iff
  216. Iff.elim
  217. Iff.intro
    1. Constructor of Iff
  218. Inhabited
  219. Inhabited.mk
    1. Instance constructor of Inhabited
  220. Int
  221. Int.add
  222. Int.bdiv
  223. Int.bmod
  224. Int.cast
  225. Int.dec­Eq
  226. Int.ediv
  227. Int.emod
  228. Int.fdiv
  229. Int.fmod
  230. Int.from­Expr?
  231. Int.gcd
  232. Int.is­Pos­Value
  233. Int.lcm
  234. Int.le
  235. Int.lt
  236. Int.mul
  237. Int.nat­Abs
  238. Int.neg
  239. Int.neg­Of­Nat
  240. Int.neg­Succ
    1. Constructor of Int
  241. Int.not
  242. Int.of­Nat
    1. Constructor of Int
  243. Int.pow
  244. Int.reduce­Abs
  245. Int.reduce­Add
  246. Int.reduce­BEq
  247. Int.reduce­BNe
  248. Int.reduce­Bdiv
  249. Int.reduce­Bin
  250. Int.reduce­Bin­Int­Nat­Op
  251. Int.reduce­Bin­Pred
  252. Int.reduce­Bmod
  253. Int.reduce­Bool­Pred
  254. Int.reduce­Div
  255. Int.reduce­Dvd
  256. Int.reduce­Eq
  257. Int.reduce­FDiv
  258. Int.reduce­FMod
  259. Int.reduce­GE
  260. Int.reduce­GT
  261. Int.reduce­LE
  262. Int.reduce­LT
  263. Int.reduce­Mod
  264. Int.reduce­Mul
  265. Int.reduce­Nat­Core
  266. Int.reduce­Ne
  267. Int.reduce­Neg
  268. Int.reduce­Neg­Succ
  269. Int.reduce­Of­Nat
  270. Int.reduce­Pow
  271. Int.reduce­Sub
  272. Int.reduce­TDiv
  273. Int.reduce­TMod
  274. Int.reduce­To­Nat
  275. Int.reduce­Unary
  276. Int.repr
  277. Int.shift­Right
  278. Int.sign
  279. Int.sub
  280. Int.sub­Nat­Nat
  281. Int.tdiv
  282. Int.tmod
  283. Int.to­ISize
  284. Int.to­Int16
  285. Int.to­Int32
  286. Int.to­Int64
  287. Int.to­Int8
  288. Int.to­Nat
  289. Int.to­Nat'
  290. Int16
  291. Int16.abs
  292. Int16.add
  293. Int16.complement
  294. Int16.dec­Eq
  295. Int16.dec­Le
  296. Int16.dec­Lt
  297. Int16.div
  298. Int16.land
  299. Int16.le
  300. Int16.lor
  301. Int16.lt
  302. Int16.max­Value
  303. Int16.min­Value
  304. Int16.mod
  305. Int16.mul
  306. Int16.neg
  307. Int16.of­Bit­Vec
  308. Int16.of­Int
  309. Int16.of­Int­LE
  310. Int16.of­Int­Truncate
  311. Int16.of­Nat
  312. Int16.shift­Left
  313. Int16.shift­Right
  314. Int16.size
  315. Int16.sub
  316. Int16.to­Bit­Vec
  317. Int16.to­Float
  318. Int16.to­Float32
  319. Int16.to­ISize
  320. Int16.to­Int
  321. Int16.to­Int32 (0) (1)
  322. Int16.to­Int64
  323. Int16.to­Int8
  324. Int16.to­Nat­Clamp­Neg
  325. Int16.xor
  326. Int32
  327. Int32.abs
  328. Int32.add
  329. Int32.complement
  330. Int32.dec­Eq
  331. Int32.dec­Le
  332. Int32.dec­Lt
  333. Int32.div
  334. Int32.land
  335. Int32.le
  336. Int32.lor
  337. Int32.lt
  338. Int32.max­Value
  339. Int32.min­Value
  340. Int32.mod
  341. Int32.mul
  342. Int32.neg
  343. Int32.of­Bit­Vec
  344. Int32.of­Int
  345. Int32.of­Int­LE
  346. Int32.of­Int­Truncate
  347. Int32.of­Nat
  348. Int32.shift­Left
  349. Int32.shift­Right
  350. Int32.size
  351. Int32.sub
  352. Int32.to­Bit­Vec
  353. Int32.to­Float
  354. Int32.to­Float32
  355. Int32.to­ISize
  356. Int32.to­Int
  357. Int32.to­Int16
  358. Int32.to­Int64
  359. Int32.to­Int8
  360. Int32.to­Nat­Clamp­Neg
  361. Int32.xor
  362. Int64
  363. Int64.abs
  364. Int64.add
  365. Int64.complement
  366. Int64.dec­Eq
  367. Int64.dec­Le
  368. Int64.dec­Lt
  369. Int64.div
  370. Int64.land
  371. Int64.le
  372. Int64.lor
  373. Int64.lt
  374. Int64.max­Value
  375. Int64.min­Value
  376. Int64.mod
  377. Int64.mul
  378. Int64.neg
  379. Int64.of­Bit­Vec
  380. Int64.of­Int
  381. Int64.of­Int­LE
  382. Int64.of­Int­Truncate
  383. Int64.of­Nat
  384. Int64.shift­Left
  385. Int64.shift­Right
  386. Int64.size
  387. Int64.sub
  388. Int64.to­Bit­Vec
  389. Int64.to­Float
  390. Int64.to­Float32
  391. Int64.to­ISize
  392. Int64.to­Int
  393. Int64.to­Int16
  394. Int64.to­Int32
  395. Int64.to­Int8
  396. Int64.to­Nat­Clamp­Neg
  397. Int64.xor
  398. Int8
  399. Int8.abs
  400. Int8.add
  401. Int8.complement
  402. Int8.dec­Eq
  403. Int8.dec­Le
  404. Int8.dec­Lt
  405. Int8.div
  406. Int8.land
  407. Int8.le
  408. Int8.lor
  409. Int8.lt
  410. Int8.max­Value
  411. Int8.min­Value
  412. Int8.mod
  413. Int8.mul
  414. Int8.neg
  415. Int8.of­Bit­Vec
  416. Int8.of­Int
  417. Int8.of­Int­LE
  418. Int8.of­Int­Truncate
  419. Int8.of­Nat
  420. Int8.shift­Left
  421. Int8.shift­Right
  422. Int8.size
  423. Int8.sub
  424. Int8.to­Bit­Vec
  425. Int8.to­Float
  426. Int8.to­Float32
  427. Int8.to­ISize
  428. Int8.to­Int
  429. Int8.to­Int16
  430. Int8.to­Int32 (0) (1)
  431. Int8.to­Int64
  432. Int8.to­Nat­Clamp­Neg
  433. Int8.xor
  434. Int­Cast
  435. IntCast.mk
    1. Instance constructor of Int­Cast
  436. Is­Infix
    1. List.Is­Infix
  437. Is­Prefix
    1. List.Is­Prefix
  438. Is­Suffix
    1. List.Is­Suffix
  439. Iterator
    1. String.Iterator
  440. i
    1. String.Iterator.i (structure field)
  441. ibelow
    1. Nat.ibelow
  442. id_map
    1. LawfulFunctor.id_map (class method)
  443. ident­Kind
    1. Lean.ident­Kind
  444. identifier
    1. raw
  445. idx­Of
    1. Array.idx­Of
    2. List.idx­Of
  446. idx­Of?
    1. Array.idx­Of?
    2. List.idx­Of?
  447. if ... then ... else ...
  448. if h : ... then ... else ...
  449. imax
    1. Nat.imax
  450. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  451. impredicative
  452. inaccessible
  453. ind
    1. Quot.ind
    2. Quotient.ind
  454. index
    1. Lean.Meta.DSimp.Config.index (structure field)
    2. Lean.Meta.Simp.Config.index (structure field)
    3. of inductive type
  455. indexed family
    1. of types
  456. induction
    1. Fin.induction
  457. induction­On
    1. Fin.induction­On
    2. Nat.div.induction­On
    3. Nat.mod.induction­On
  458. inductive.auto­Promote­Indices
  459. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  460. infer­Instance
  461. infer­Instance­As
  462. infer_instance
  463. inhabited­Left
    1. PSum.inhabited­Left
    2. Sum.inhabited­Left
  464. inhabited­Right
    1. PSum.inhabited­Right
    2. Sum.inhabited­Right
  465. init (Lake command)
  466. injection
  467. injections
  468. insert
    1. List.insert
  469. insert­Idx
    1. Array.insert­Idx
    2. List.insert­Idx
  470. insert­Idx!
    1. Array.insert­Idx!
  471. insert­Idx­If­In­Bounds
    1. Array.insert­Idx­If­In­Bounds
  472. insert­Idx­TR
    1. List.insert­Idx­TR
  473. insertion­Sort
    1. Array.insertion­Sort
  474. instance synthesis
  475. int­Cast
    1. IntCast.int­Cast (class method)
  476. int­Max
    1. BitVec.int­Max
  477. int­Min
    1. BitVec.int­Min
  478. intercalate
    1. List.intercalate
    2. String.intercalate
  479. intercalate­TR
    1. List.intercalate­TR
  480. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  481. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  482. intersperse
    1. List.intersperse
  483. intersperse­TR
    1. List.intersperse­TR
  484. intro (0) (1)
  485. intro | ... => ... | ... => ...
  486. intros
  487. inv­Image
  488. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  489. is­Absolute
    1. System.FilePath.is­Absolute
  490. is­Alpha
    1. Char.is­Alpha
  491. is­Alphanum
    1. Char.is­Alphanum
  492. is­Digit
    1. Char.is­Digit
  493. is­Dir
    1. System.FilePath.is­Dir
  494. is­Empty
    1. Array.is­Empty
    2. List.is­Empty
    3. String.is­Empty
  495. is­Emscripten
    1. System.Platform.is­Emscripten
  496. is­Eq­Some
    1. Option.is­Eq­Some
  497. is­Eqv
    1. Array.is­Eqv
    2. List.is­Eqv
  498. is­Finite
    1. Float.is­Finite
    2. Float32.is­Finite
  499. is­Inf
    1. Float.is­Inf
    2. Float32.is­Inf
  500. is­Int
    1. String.is­Int
  501. is­Left
    1. Sum.is­Left
  502. is­Lower
    1. Char.is­Lower
  503. is­Lt
    1. Fin.is­Lt (structure field)
  504. is­Na­N
    1. Float.is­Na­N
    2. Float32.is­Na­N
  505. is­Nat
    1. String.is­Nat
  506. is­None
    1. Option.is­None
  507. is­OSX
    1. System.Platform.is­OSX
  508. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  509. is­Ok
    1. Except.is­Ok
  510. is­Perm
    1. List.is­Perm
  511. is­Pos­Value
    1. Int.is­Pos­Value
  512. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  513. is­Prefix­Of
    1. Array.is­Prefix­Of
    2. List.is­Prefix­Of
    3. String.is­Prefix­Of
  514. is­Prefix­Of?
    1. List.is­Prefix­Of?
  515. is­Relative
    1. System.FilePath.is­Relative
  516. is­Right
    1. Sum.is­Right
  517. is­Some
    1. Option.is­Some
  518. is­Sublist
    1. List.is­Sublist
  519. is­Suffix­Of
    1. List.is­Suffix­Of
  520. is­Suffix­Of?
    1. List.is­Suffix­Of?
  521. is­Tty
    1. IO.FS.Handle.is­Tty
    2. IO.FS.Stream.is­Tty (structure field)
  522. is­Upper
    1. Char.is­Upper
  523. is­Valid
    1. String.Pos.is­Valid
  524. is­Valid­Char
    1. Nat.is­Valid­Char
    2. UInt32.is­Valid­Char
  525. is­Value
    1. Fin.is­Value
    2. Nat.is­Value
  526. is­Whitespace
    1. Char.is­Whitespace
  527. is­Windows
    1. System.Platform.is­Windows
  528. iseqv
    1. Setoid.iseqv (class method)
  529. iter
    1. String.iter
  530. iterate
    1. IO.iterate
  531. iunfoldr
    1. BitVec.iunfoldr

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­DSimp­Config­Core
  97. Lean.Elab.Tactic.elab­Simp­Args
  98. Lean.Elab.Tactic.elab­Simp­Config
  99. Lean.Elab.Tactic.elab­Simp­Config­Ctx­Core
  100. Lean.Elab.Tactic.elab­Term
  101. Lean.Elab.Tactic.elab­Term­Ensuring­Type
  102. Lean.Elab.Tactic.elab­Term­With­Holes
  103. Lean.Elab.Tactic.ensure­Has­No­MVars
  104. Lean.Elab.Tactic.focus
  105. Lean.Elab.Tactic.get­Curr­Macro­Scope
  106. Lean.Elab.Tactic.get­FVar­Id
  107. Lean.Elab.Tactic.get­FVar­Ids
  108. Lean.Elab.Tactic.get­Goals
  109. Lean.Elab.Tactic.get­Main­Goal
  110. Lean.Elab.Tactic.get­Main­Module
  111. Lean.Elab.Tactic.get­Main­Tag
  112. Lean.Elab.Tactic.get­Unsolved­Goals
  113. Lean.Elab.Tactic.lift­Meta­MAt­Main
  114. Lean.Elab.Tactic.mk­Tactic­Attribute
  115. Lean.Elab.Tactic.or­Else
  116. Lean.Elab.Tactic.prune­Solved­Goals
  117. Lean.Elab.Tactic.run
  118. Lean.Elab.Tactic.run­Term­Elab
  119. Lean.Elab.Tactic.set­Goals
  120. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  121. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  122. Lean.Elab.Tactic.tactic­Elab­Attribute
  123. Lean.Elab.Tactic.tag­Untagged­Goals
  124. Lean.Elab.Tactic.try­Catch
  125. Lean.Elab.Tactic.try­Tactic
  126. Lean.Elab.Tactic.try­Tactic?
  127. Lean.Elab.Tactic.with­Location
  128. Lean.Elab.register­Deriving­Handler
  129. Lean.Macro.Exception.unsupported­Syntax
  130. Lean.Macro.add­Macro­Scope
  131. Lean.Macro.expand­Macro?
  132. Lean.Macro.get­Curr­Namespace
  133. Lean.Macro.has­Decl
  134. Lean.Macro.resolve­Global­Name
  135. Lean.Macro.resolve­Namespace
  136. Lean.Macro.throw­Error
  137. Lean.Macro.throw­Error­At
  138. Lean.Macro.throw­Unsupported
  139. Lean.Macro.trace
  140. Lean.Macro.with­Fresh­Macro­Scope
  141. Lean.Macro­M
  142. Lean.Meta.DSimp.Config
  143. Lean.Meta.DSimp.Config.mk
    1. Constructor of Lean.Meta.DSimp.Config
  144. Lean.Meta.Occurrences
  145. Lean.Meta.Occurrences.all
    1. Constructor of Lean.Meta.Occurrences
  146. Lean.Meta.Occurrences.neg
    1. Constructor of Lean.Meta.Occurrences
  147. Lean.Meta.Occurrences.pos
    1. Constructor of Lean.Meta.Occurrences
  148. Lean.Meta.Rewrite.Config
  149. Lean.Meta.Rewrite.Config.mk
    1. Constructor of Lean.Meta.Rewrite.Config
  150. Lean.Meta.Rewrite.New­Goals
  151. Lean.Meta.Simp.Config
  152. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  153. Lean.Meta.Simp.neutral­Config
  154. Lean.Meta.Simp­Extension
  155. Lean.Meta.Transparency­Mode
  156. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.Transparency­Mode
  157. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.Transparency­Mode
  158. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.Transparency­Mode
  159. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.Transparency­Mode
  160. Lean.Meta.register­Simp­Attr
  161. Lean.Order.CCPO
  162. Lean.Order.CCPO.mk
    1. Instance constructor of Lean.Order.CCPO
  163. Lean.Order.Partial­Order
  164. Lean.Order.PartialOrder.mk
    1. Instance constructor of Lean.Order.Partial­Order
  165. Lean.Order.fix
  166. Lean.Order.fix_eq
  167. Lean.Order.monotone
  168. Lean.Parser.Leading­Ident­Behavior
  169. Lean.Parser.Leading­IdentBehavior.both
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  170. Lean.Parser.Leading­IdentBehavior.default
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  171. Lean.Parser.Leading­IdentBehavior.symbol
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  172. Lean.Source­Info
  173. Lean.SourceInfo.none
    1. Constructor of Lean.Source­Info
  174. Lean.SourceInfo.original
    1. Constructor of Lean.Source­Info
  175. Lean.SourceInfo.synthetic
    1. Constructor of Lean.Source­Info
  176. Lean.Syntax
  177. Lean.Syntax.Char­Lit
  178. Lean.Syntax.Command
  179. Lean.Syntax.Hygiene­Info
  180. Lean.Syntax.Ident
  181. Lean.Syntax.Level
  182. Lean.Syntax.Name­Lit
  183. Lean.Syntax.Num­Lit
  184. Lean.Syntax.Prec
  185. Lean.Syntax.Preresolved
  186. Lean.Syntax.Preresolved.decl
    1. Constructor of Lean.Syntax.Preresolved
  187. Lean.Syntax.Preresolved.namespace
    1. Constructor of Lean.Syntax.Preresolved
  188. Lean.Syntax.Prio
  189. Lean.Syntax.Scientific­Lit
  190. Lean.Syntax.Str­Lit
  191. Lean.Syntax.TSep­Array
  192. Lean.Syntax.TSepArray.mk
    1. Constructor of Lean.Syntax.TSep­Array
  193. Lean.Syntax.Tactic
  194. Lean.Syntax.Term
  195. Lean.Syntax.atom
    1. Constructor of Lean.Syntax
  196. Lean.Syntax.get­Kind
  197. Lean.Syntax.ident
    1. Constructor of Lean.Syntax
  198. Lean.Syntax.is­Of­Kind
  199. Lean.Syntax.missing
    1. Constructor of Lean.Syntax
  200. Lean.Syntax.node
    1. Constructor of Lean.Syntax
  201. Lean.Syntax.set­Kind
  202. Lean.Syntax­Node­Kind
  203. Lean.TSyntax
  204. Lean.TSyntax.get­Char
  205. Lean.TSyntax.get­Hygiene­Info
  206. Lean.TSyntax.get­Id
  207. Lean.TSyntax.get­Name
  208. Lean.TSyntax.get­Nat
  209. Lean.TSyntax.get­Scientific
  210. Lean.TSyntax.get­String
  211. Lean.TSyntax.mk
    1. Constructor of Lean.TSyntax
  212. Lean.TSyntax­Array
  213. Lean.char­Lit­Kind
  214. Lean.choice­Kind
  215. Lean.field­Idx­Kind
  216. Lean.group­Kind
  217. Lean.hygiene­Info­Kind
  218. Lean.ident­Kind
  219. Lean.interpolated­Str­Kind
  220. Lean.interpolated­Str­Lit­Kind
  221. Lean.name­Lit­Kind
  222. Lean.null­Kind
  223. Lean.num­Lit­Kind
  224. Lean.scientific­Lit­Kind
  225. Lean.str­Lit­Kind
  226. Lean­Exe­Config
    1. Lake.Lean­Exe­Config
  227. Lean­Lib­Config
    1. Lake.Lean­Lib­Config
  228. Lean­Option
    1. Lake.Lean­Option
  229. Level
    1. Lean.Syntax.Level
  230. Lex
    1. List.Lex
  231. List
  232. List.Is­Infix
  233. List.Is­Prefix
  234. List.Is­Suffix
  235. List.Lex
  236. List.Lex.cons
    1. Constructor of List.Lex
  237. List.Lex.nil
    1. Constructor of List.Lex
  238. List.Lex.rel
    1. Constructor of List.Lex
  239. List.Mem
  240. List.Mem.head
    1. Constructor of List.Mem
  241. List.Mem.tail
    1. Constructor of List.Mem
  242. List.Nodup
  243. List.Pairwise
  244. List.Pairwise.cons
    1. Constructor of List.Pairwise
  245. List.Pairwise.nil
    1. Constructor of List.Pairwise
  246. List.Perm
  247. List.Perm.cons
    1. Constructor of List.Perm
  248. List.Perm.nil
    1. Constructor of List.Perm
  249. List.Perm.swap
    1. Constructor of List.Perm
  250. List.Perm.trans
    1. Constructor of List.Perm
  251. List.all
  252. List.all­M
  253. List.and
  254. List.any
  255. List.any­M
  256. List.append
  257. List.append­TR
  258. List.as­String
  259. List.attach
  260. List.attach­With
  261. List.beq
  262. List.concat
  263. List.cons
    1. Constructor of List
  264. List.contains
  265. List.count
  266. List.count­P
  267. List.drop
  268. List.drop­Last
  269. List.drop­Last­TR
  270. List.drop­While
  271. List.elem
  272. List.erase
  273. List.erase­Dups
  274. List.erase­Idx
  275. List.erase­Idx­TR
  276. List.erase­P
  277. List.erase­PTR
  278. List.erase­Reps
  279. List.erase­TR
  280. List.extract
  281. List.filter
  282. List.filter­M
  283. List.filter­Map
  284. List.filter­Map­M
  285. List.filter­Map­TR
  286. List.filter­Rev­M
  287. List.filter­TR
  288. List.fin­Idx­Of?
  289. List.fin­Range
  290. List.find?
  291. List.find­Fin­Idx?
  292. List.find­Idx
  293. List.find­Idx?
  294. List.find­M?
  295. List.find­Some?
  296. List.find­Some­M?
  297. List.first­M
  298. List.flat­Map
  299. List.flat­Map­M
  300. List.flat­Map­TR
  301. List.flatten
  302. List.flatten­TR
  303. List.foldl
  304. List.foldl­M
  305. List.foldl­Rec­On
  306. List.foldr
  307. List.foldr­M
  308. List.foldr­Rec­On
  309. List.foldr­TR
  310. List.for­A
  311. List.for­In'
  312. List.for­M
  313. List.get
  314. List.get­D
  315. List.get­Last
  316. List.get­Last!
  317. List.get­Last?
  318. List.get­Last­D
  319. List.group­By­Key
  320. List.has­Dec­Eq
  321. List.head
  322. List.head!
  323. List.head?
  324. List.head­D
  325. List.idx­Of
  326. List.idx­Of?
  327. List.insert
  328. List.insert­Idx
  329. List.insert­Idx­TR
  330. List.intercalate
  331. List.intercalate­TR
  332. List.intersperse
  333. List.intersperse­TR
  334. List.is­Empty
  335. List.is­Eqv
  336. List.is­Perm
  337. List.is­Prefix­Of
  338. List.is­Prefix­Of?
  339. List.is­Sublist
  340. List.is­Suffix­Of
  341. List.is­Suffix­Of?
  342. List.le
  343. List.leftpad
  344. List.leftpad­TR
  345. List.length
  346. List.length­TR
  347. List.lex
  348. List.lookup
  349. List.lt
  350. List.map
  351. List.map­A
  352. List.map­Fin­Idx
  353. List.map­Fin­Idx­M
  354. List.map­Idx
  355. List.map­Idx­M
  356. List.map­M
  357. List.map­M'
  358. List.map­Mono
  359. List.map­Mono­M
  360. List.map­TR
  361. List.max?
  362. List.max­Nat­Abs
  363. List.merge
  364. List.merge­Sort
  365. List.min?
  366. List.min­Nat­Abs
  367. List.modify
  368. List.modify­Head
  369. List.modify­TR
  370. List.modify­Tail­Idx
  371. List.nil
    1. Constructor of List
  372. List.nonzero­Minimum
  373. List.of­Fn
  374. List.or
  375. List.partition
  376. List.partition­M
  377. List.partition­Map
  378. List.pmap
  379. List.range
  380. List.range'
  381. List.range'TR
  382. List.reduce­Option
  383. List.reduce­Replicate
  384. List.remove­All
  385. List.replace
  386. List.replace­TR
  387. List.replicate
  388. List.replicate­TR
  389. List.reverse
  390. List.rightpad
  391. List.rotate­Left
  392. List.rotate­Right
  393. List.set
  394. List.set­TR
  395. List.singleton
  396. List.span
  397. List.split­At
  398. List.split­By
  399. List.sum
  400. List.tail
  401. List.tail!
  402. List.tail?
  403. List.tail­D
  404. List.take
  405. List.take­TR
  406. List.take­While
  407. List.take­While­TR
  408. List.to­Array
  409. List.to­Array­Impl
  410. List.to­Byte­Array
  411. List.to­Float­Array
  412. List.to­PArray'
  413. List.to­String
  414. List.unattach
  415. List.unzip
  416. List.unzip­TR
  417. List.zip
  418. List.zip­Idx
  419. List.zip­Idx­LE
  420. List.zip­Idx­TR
  421. List.zip­With
  422. List.zip­With­All
  423. List.zip­With­TR
  424. 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
  425. last
    1. Fin.last
  426. last­Cases
    1. Fin.last­Cases
  427. lazy­Pure
    1. IO.lazy­Pure
  428. lcm
    1. Int.lcm
    2. Nat.lcm
  429. le
    1. Float.le
    2. Float32.le
    3. ISize.le
    4. Int.le
    5. Int16.le
    6. Int32.le
    7. Int64.le
    8. Int8.le
    9. LE.le (class method)
    10. List.le
    11. Nat.le
    12. String.le
    13. UInt16.le
    14. UInt32.le
    15. UInt64.le
    16. UInt8.le
    17. USize.le
  430. lean (Lake command)
  431. lean_is_array
  432. lean_is_string
  433. lean_string_object (0) (1)
  434. lean_to_array
  435. lean_to_string
  436. left (0) (1)
    1. And.left (structure field)
  437. leftpad
    1. List.leftpad
  438. leftpad­TR
    1. List.leftpad­TR
  439. length
    1. List.length
    2. String.length
  440. length­TR
    1. List.length­TR
  441. let
  442. let rec
  443. let'
  444. let­I
  445. level
    1. of universe
  446. lex
    1. Array.lex
    2. List.lex
    3. Prod.lex
  447. lex­Lt
    1. Prod.lex­Lt
  448. lhs
  449. lib­Name
    1. [anonymous] (structure field)
  450. 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
  451. lift­Meta­MAt­Main
    1. Lean.Elab.Tactic.lift­Meta­MAt­Main
  452. lift­On
    1. Quot.lift­On
    2. Quotient.lift­On
  453. lift­On₂
    1. Quotient.lift­On₂
  454. lift­Or­Get
    1. Option.lift­Or­Get
  455. lift­With
    1. MonadControl.lift­With (class method)
    2. Monad­ControlT.lift­With (class method)
  456. lift₂
    1. Quotient.lift₂
  457. line­Eq
  458. lines
    1. IO.FS.lines
  459. lint (Lake command)
  460. linter.unnecessary­Simpa
  461. literal
    1. raw string
    2. string
  462. lock
    1. IO.FS.Handle.lock
  463. log
    1. Float.log
    2. Float32.log
  464. log10
    1. Float.log10
    2. Float32.log10
  465. log2
    1. Fin.log2
    2. Float.log2
    3. Float32.log2
    4. Nat.log2
    5. UInt16.log2
    6. UInt32.log2
    7. UInt64.log2
    8. UInt8.log2
    9. USize.log2
  466. lookup
    1. List.lookup
  467. 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
  468. lt
    1. Float.lt
    2. Float32.lt
    3. ISize.lt
    4. Int.lt
    5. Int16.lt
    6. Int32.lt
    7. Int64.lt
    8. Int8.lt
    9. LT.lt (class method)
    10. List.lt
    11. Nat.lt
    12. Option.lt
    13. UInt16.lt
    14. UInt32.lt
    15. UInt64.lt
    16. UInt8.lt
    17. USize.lt
  469. 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
    12. Task.map
    13. Thunk.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. max­Value
    1. ISize.max­Value
    2. Int16.max­Value
    3. Int32.max­Value
    4. Int64.max­Value
    5. Int8.max­Value
  84. memoize
    1. Lean.Meta.Simp.Config.memoize (structure field)
  85. merge
    1. List.merge
    2. Option.merge
  86. merge­Sort
    1. List.merge­Sort
  87. metadata
    1. System.FilePath.metadata
  88. min
    1. Nat.min
    2. Option.min
    3. String.Pos.min
  89. min?
    1. List.min?
  90. min­Nat­Abs
    1. List.min­Nat­Abs
  91. min­Value
    1. ISize.min­Value
    2. Int16.min­Value
    3. Int32.min­Value
    4. Int64.min­Value
    5. Int8.min­Value
  92. mk
    1. Dynamic.mk
    2. ExceptT.mk
    3. IO.FS.Handle.mk
    4. OptionT.mk
    5. Quot.mk
    6. Quotient.mk
    7. Squash.mk
  93. mk'
    1. LawfulMonad.mk'
    2. Quotient.mk'
  94. mk­Already­Exists
    1. IO.Error.mk­Already­Exists
  95. mk­Already­Exists­File
    1. IO.Error.mk­Already­Exists­File
  96. mk­Array
    1. Array.mk­Array
  97. mk­Eof­Error
    1. IO.Error.mk­Eof­Error
  98. mk­File­Path
    1. System.mk­File­Path
  99. mk­Hardware­Fault
    1. IO.Error.mk­Hardware­Fault
  100. mk­Illegal­Operation
    1. IO.Error.mk­Illegal­Operation
  101. mk­Inappropriate­Type
    1. IO.Error.mk­Inappropriate­Type
  102. mk­Inappropriate­Type­File
    1. IO.Error.mk­Inappropriate­Type­File
  103. mk­Interrupted
    1. IO.Error.mk­Interrupted
  104. mk­Invalid­Argument
    1. IO.Error.mk­Invalid­Argument
  105. mk­Invalid­Argument­File
    1. IO.Error.mk­Invalid­Argument­File
  106. mk­Iterator
    1. String.mk­Iterator
  107. mk­No­File­Or­Directory
    1. IO.Error.mk­No­File­Or­Directory
  108. mk­No­Such­Thing
    1. IO.Error.mk­No­Such­Thing
  109. mk­No­Such­Thing­File
    1. IO.Error.mk­No­Such­Thing­File
  110. mk­Other­Error
    1. IO.Error.mk­Other­Error
  111. mk­Permission­Denied
    1. IO.Error.mk­Permission­Denied
  112. mk­Permission­Denied­File
    1. IO.Error.mk­Permission­Denied­File
  113. mk­Protocol­Error
    1. IO.Error.mk­Protocol­Error
  114. mk­Ref
    1. IO.mk­Ref
    2. ST.mk­Ref
  115. mk­Resource­Busy
    1. IO.Error.mk­Resource­Busy
  116. mk­Resource­Exhausted
    1. IO.Error.mk­Resource­Exhausted
  117. mk­Resource­Exhausted­File
    1. IO.Error.mk­Resource­Exhausted­File
  118. mk­Resource­Vanished
    1. IO.Error.mk­Resource­Vanished
  119. mk­Std­Gen
  120. mk­Tactic­Attribute
    1. Lean.Elab.Tactic.mk­Tactic­Attribute
  121. mk­Time­Expired
    1. IO.Error.mk­Time­Expired
  122. mk­Unsatisfied­Constraints
    1. IO.Error.mk­Unsatisfied­Constraints
  123. mk­Unsupported­Operation
    1. IO.Error.mk­Unsupported­Operation
  124. 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
  125. mod­Core
    1. Nat.mod­Core
  126. modified
    1. IO.FS.Metadata.modified (structure field)
  127. modify
    1. Array.modify
    2. List.modify
    3. ST.Ref.modify
    4. String.modify
  128. 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
  129. modify­Get­The
  130. modify­Head
    1. List.modify­Head
  131. modify­M
    1. Array.modify­M
  132. modify­Op
    1. Array.modify­Op
  133. modify­TR
    1. List.modify­TR
  134. modify­Tail­Idx
    1. List.modify­Tail­Idx
  135. modify­The
  136. modn
    1. Fin.modn
  137. monad­Eval
    1. MonadEval.monad­Eval (class method)
    2. Monad­EvalT.monad­Eval (class method)
  138. monad­Lift
    1. MonadLift.monad­Lift (class method)
    2. Monad­LiftT.monad­Lift (class method)
  139. monad­Map
    1. MonadFunctor.monad­Map (class method)
    2. Monad­FunctorT.monad­Map (class method)
  140. mono­Ms­Now
    1. IO.mono­Ms­Now
  141. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  142. monotone
    1. Lean.Order.monotone
  143. mp
    1. Eq.mp
    2. Iff.mp (structure field)
  144. mpr
    1. Eq.mpr
    2. Iff.mpr (structure field)
  145. msb
    1. BitVec.msb
  146. mul
    1. BitVec.mul
    2. Fin.mul
    3. Float.mul
    4. Float32.mul
    5. ISize.mul
    6. Int.mul
    7. Int16.mul
    8. Int32.mul
    9. Int64.mul
    10. Int8.mul
    11. Mul.mul (class method)
    12. Nat.mul
    13. UInt16.mul
    14. UInt32.mul
    15. UInt64.mul
    16. UInt8.mul
    17. USize.mul
  147. mul­Rec
    1. BitVec.mul­Rec
  148. 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­Rec­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­And
  66. Nat.reduce­BEq
  67. Nat.reduce­BNe
  68. Nat.reduce­Beq­Diff
  69. Nat.reduce­Bin
  70. Nat.reduce­Bin­Pred
  71. Nat.reduce­Bne­Diff
  72. Nat.reduce­Bool­Pred
  73. Nat.reduce­Div
  74. Nat.reduce­Dvd
  75. Nat.reduce­Eq­Diff
  76. Nat.reduce­GT
  77. Nat.reduce­Gcd
  78. Nat.reduce­LT
  79. Nat.reduce­LTLE
  80. Nat.reduce­Le­Diff
  81. Nat.reduce­Mod
  82. Nat.reduce­Mul
  83. Nat.reduce­Nat­Eq­Expr
  84. Nat.reduce­Or
  85. Nat.reduce­Pow
  86. Nat.reduce­Shift­Left
  87. Nat.reduce­Shift­Right
  88. Nat.reduce­Sub
  89. Nat.reduce­Sub­Diff
  90. Nat.reduce­Succ
  91. Nat.reduce­Unary
  92. Nat.reduce­Xor
  93. Nat.repeat
  94. Nat.repeat­TR
  95. Nat.repr
  96. Nat.shift­Left
  97. Nat.shift­Right
  98. Nat.strong­Rec­On
  99. Nat.sub
  100. Nat.sub­Digit­Char
  101. Nat.succ
    1. Constructor of Nat
  102. Nat.super­Digit­Char
  103. Nat.test­Bit
  104. Nat.to­Digits
  105. Nat.to­Digits­Core
  106. Nat.to­Float
  107. Nat.to­Float32
  108. Nat.to­ISize
  109. Nat.to­Int16
  110. Nat.to­Int32
  111. Nat.to­Int64
  112. Nat.to­Int8
  113. Nat.to­Level
  114. Nat.to­Sub­Digits
  115. Nat.to­Subscript­String
  116. Nat.to­Super­Digits
  117. Nat.to­Superscript­String
  118. Nat.to­UInt16
  119. Nat.to­UInt32
  120. Nat.to­UInt64
  121. Nat.to­UInt8
  122. Nat.to­USize
  123. Nat.xor
  124. Nat.zero
    1. Constructor of Nat
  125. Nat­Cast
  126. NatCast.mk
    1. Instance constructor of Nat­Cast
  127. Nat­Pow
  128. NatPow.mk
    1. Instance constructor of Nat­Pow
  129. Ne­Zero
  130. NeZero.mk
    1. Instance constructor of Ne­Zero
  131. Neg
  132. Neg.mk
    1. Instance constructor of Neg
  133. New­Goals
    1. Lean.Meta.Rewrite.New­Goals
  134. Nodup
    1. List.Nodup
  135. Nonempty
  136. Nonempty.intro
    1. Constructor of Nonempty
  137. Not
  138. Not.elim
  139. Num­Lit
    1. Lean.Syntax.Num­Lit
  140. name
    1. Lake.LeanOption.name (structure field)
    2. [anonymous] (structure field) (0) (1)
  141. name­Lit­Kind
    1. Lean.name­Lit­Kind
  142. namespace
    1. of inductive type
  143. nat­Abs
    1. Int.nat­Abs
  144. nat­Add
    1. Fin.nat­Add
  145. nat­Cast
    1. NatCast.nat­Cast (class method)
  146. native­Facets
    1. [anonymous] (structure field) (0) (1)
  147. native_decide
  148. ndrec
    1. HEq.ndrec
  149. ndrec­On
    1. HEq.ndrec­On
  150. neg
    1. BitVec.neg
    2. Float.neg
    3. Float32.neg
    4. ISize.neg
    5. Int.neg
    6. Int16.neg
    7. Int32.neg
    8. Int64.neg
    9. Int8.neg
    10. Neg.neg (class method)
  151. neg­Of­Nat
    1. Int.neg­Of­Nat
  152. neutral­Config
    1. Lean.Meta.Simp.neutral­Config
  153. new (Lake command)
  154. new­Goals
    1. Lean.Meta.Rewrite.Config.new­Goals (structure field)
  155. next
    1. RandomGen.next (class method)
    2. String.Iterator.next
    3. String.next
  156. next ... => ...
  157. next'
    1. String.next'
  158. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  159. next­Until
    1. String.next­Until
  160. next­While
    1. String.next­While
  161. nextn
    1. String.Iterator.nextn
  162. nil
    1. BitVec.nil
  163. no­Confusion
    1. Nat.no­Confusion
  164. no­Confusion­Type
    1. Nat.no­Confusion­Type
  165. nofun
  166. nomatch
  167. non­Backtrackable
    1. EStateM.non­Backtrackable
  168. nonzero­Minimum
    1. List.nonzero­Minimum
  169. norm_cast (0) (1)
  170. normalize
    1. System.FilePath.normalize
  171. not
    1. BitVec.not
    2. Bool.not
    3. Int.not
  172. not­M
  173. null­Kind
    1. Lean.null­Kind
  174. num­Bits
    1. System.Platform.num­Bits
  175. 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. Or
  61. Or.by_cases
  62. Or.by_cases'
  63. Or.inl
    1. Constructor of Or
  64. Or.inr
    1. Constructor of Or
  65. Ord
  66. Ord.mk
    1. Instance constructor of Ord
  67. Ordering
  68. Ordering.eq
    1. Constructor of Ordering
  69. Ordering.gt
    1. Constructor of Ordering
  70. Ordering.lt
    1. Constructor of Ordering
  71. Output
    1. IO.Process.Output
  72. obtain
  73. occs
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  74. of­Binary­Scientific
    1. Float.of­Binary­Scientific
    2. Float32.of­Binary­Scientific
  75. of­Bit­Vec
    1. ISize.of­Bit­Vec
    2. Int16.of­Bit­Vec
    3. Int32.of­Bit­Vec
    4. Int64.of­Bit­Vec
    5. Int8.of­Bit­Vec
  76. of­Bits
    1. Float.of­Bits
    2. Float32.of­Bits
  77. of­Bool
    1. BitVec.of­Bool
  78. of­Bool­List­BE
    1. BitVec.of­Bool­List­BE
  79. of­Bool­List­LE
    1. BitVec.of­Bool­List­LE
  80. of­Buffer
    1. IO.FS.Stream.of­Buffer
  81. of­Except
    1. IO.of­Except
    2. MonadExcept.of­Except
  82. of­Fin
    1. UInt16.of­Fin
    2. UInt32.of­Fin
    3. UInt64.of­Fin
    4. UInt8.of­Fin
    5. USize.of­Fin
  83. of­Fn
    1. Array.of­Fn
    2. List.of­Fn
  84. of­Handle
    1. IO.FS.Stream.of­Handle
  85. of­Int
    1. BitVec.of­Int
    2. Float.of­Int
    3. Float32.of­Int
    4. ISize.of­Int
    5. Int16.of­Int
    6. Int32.of­Int
    7. Int64.of­Int
    8. Int8.of­Int
  86. of­Int­LE
    1. ISize.of­Int­LE
    2. Int16.of­Int­LE
    3. Int32.of­Int­LE
    4. Int64.of­Int­LE
    5. Int8.of­Int­LE
  87. of­Int­Truncate
    1. ISize.of­Int­Truncate
    2. Int16.of­Int­Truncate
    3. Int32.of­Int­Truncate
    4. Int64.of­Int­Truncate
    5. Int8.of­Int­Truncate
  88. of­Nat
    1. BitVec.of­Nat
    2. Float.of­Nat
    3. Float32.of­Nat
    4. ISize.of­Nat
    5. Int16.of­Nat
    6. Int32.of­Nat
    7. Int64.of­Nat
    8. Int8.of­Nat
    9. OfNat.of­Nat (class method)
    10. UInt16.of­Nat
    11. UInt32.of­Nat
    12. UInt64.of­Nat
    13. UInt8.of­Nat
    14. USize.of­Nat
  89. of­Nat'
    1. Fin.of­Nat'
  90. of­Nat32
    1. USize.of­Nat32
  91. of­Nat­LT
    1. BitVec.of­Nat­LT
    2. UInt16.of­Nat­LT
    3. UInt32.of­Nat­LT
    4. UInt64.of­Nat­LT
    5. UInt8.of­Nat­LT
    6. USize.of­Nat­LT
  92. of­Nat­Truncate
    1. UInt16.of­Nat­Truncate
    2. UInt32.of­Nat­Truncate
    3. UInt64.of­Nat­Truncate
    4. UInt8.of­Nat­Truncate
    5. USize.of­Nat­Truncate
  93. of­Scientific
    1. Float.of­Scientific
    2. Float32.of­Scientific
    3. OfScientific.of­Scientific (class method)
  94. of­Subarray
    1. Array.of­Subarray
  95. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  96. offset­Of­Pos
    1. String.offset­Of­Pos
  97. omega
  98. open
  99. opt­Param
  100. optional
  101. or
    1. BitVec.or
    2. Bool.or
    3. List.or
    4. Option.or
  102. 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)
  103. or­Else'
    1. EStateM.or­Else'
  104. or­Else­Lazy
    1. Except.or­Else­Lazy
  105. or­M
  106. orelse'
    1. MonadExcept.orelse'
  107. other
    1. IO.FileRight.other (structure field)
  108. other­Error­To­String
    1. IO.Error.other­Error­To­String
  109. out
    1. NeZero.out (class method)
  110. out­Param
  111. 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
  31. Prod.lex­Lt
  32. Prod.map
  33. Prod.mk
    1. Constructor of Prod
  34. Prod.swap
  35. Prop
  36. Pure
  37. Pure.mk
    1. Instance constructor of Pure
  38. pack (Lake command)
  39. parameter
    1. of inductive type
  40. parent
    1. System.FilePath.parent
  41. parser
  42. partition
    1. Array.partition
    2. List.partition
  43. partition­M
    1. List.partition­M
  44. partition­Map
    1. List.partition­Map
  45. path
    1. IO.FS.DirEntry.path
  46. path­Exists
    1. System.FilePath.path­Exists
  47. path­Separator
    1. System.FilePath.path­Separator
  48. path­Separators
    1. System.FilePath.path­Separators
  49. pattern
  50. pbind
    1. Option.pbind
  51. pelim
    1. Option.pelim
  52. placeholder term
  53. pmap
    1. Array.pmap
    2. List.pmap
    3. Option.pmap
  54. polymorphism
    1. universe
  55. pop
    1. Array.pop
  56. pop­Front
    1. Subarray.pop­Front
  57. pop­While
    1. Array.pop­While
  58. pos
    1. IO.FS.Stream.Buffer.pos
    2. IO.FS.Stream.Buffer.pos (structure field)
    3. String.Iterator.pos
  59. pos­Of
    1. String.pos­Of
  60. pow
    1. Float.pow
    2. Float32.pow
    3. HomogeneousPow.pow (class method)
    4. Int.pow
    5. Nat.pow
    6. NatPow.pow (class method)
    7. Pow.pow (class method)
  61. pp
    1. eval.pp
  62. pp.deep­Terms
  63. pp.deepTerms.threshold
  64. pp.field­Notation
  65. pp.match
  66. pp.max­Steps
  67. pp.mvars
  68. pp.proofs
  69. pp.proofs.threshold
  70. precompile­Modules
    1. [anonymous] (structure field)
  71. pred
    1. Fin.pred
    2. Nat.pred
  72. predicative
  73. prev
    1. String.Iterator.prev
    2. String.prev
  74. prevn
    1. String.Iterator.prevn
  75. print
    1. IO.print
  76. println
    1. IO.println
  77. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
    2. Lean.Meta.Simp.Config.proj (structure field)
  78. proof state
  79. proofs
    1. pp.proofs
  80. property
    1. Subtype.property (structure field)
  81. propext
  82. proposition
    1. decidable
  83. prune­Solved­Goals
    1. Lean.Elab.Tactic.prune­Solved­Goals
  84. ptr­Eq
    1. ST.Ref.ptr­Eq
  85. pure
    1. EStateM.pure
    2. Except.pure
    3. ExceptT.pure
    4. OptionT.pure
    5. Pure.pure (class method)
    6. ReaderT.pure
    7. StateT.pure
    8. Thunk.pure
  86. pure_bind
    1. [anonymous] (class method)
  87. pure_seq
    1. [anonymous] (class method)
  88. push
    1. Array.push
    2. String.push
  89. push_cast
  90. pushn
    1. String.pushn
  91. put­Str
    1. IO.FS.Handle.put­Str
    2. IO.FS.Stream.put­Str (structure field)
  92. 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. Array.range'
    2. 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. BitVec.reduce­Abs
    2. Int.reduce­Abs
  41. reduce­Add
    1. BitVec.reduce­Add
    2. Fin.reduce­Add
    3. Int.reduce­Add
    4. Nat.reduce­Add
    5. UInt16.reduce­Add
    6. UInt32.reduce­Add
    7. UInt64.reduce­Add
    8. UInt8.reduce­Add
  42. reduce­Add­Nat
    1. Fin.reduce­Add­Nat
  43. reduce­All­Ones
    1. BitVec.reduce­All­Ones
  44. reduce­And
    1. BitVec.reduce­And
    2. Fin.reduce­And
    3. Nat.reduce­And
  45. reduce­Append
    1. BitVec.reduce­Append
    2. String.reduce­Append
  46. reduce­BEq
    1. BitVec.reduce­BEq
    2. Fin.reduce­BEq
    3. Int.reduce­BEq
    4. Nat.reduce­BEq
    5. String.reduce­BEq
  47. reduce­BNe
    1. BitVec.reduce­BNe
    2. Fin.reduce­BNe
    3. Int.reduce­BNe
    4. Nat.reduce­BNe
    5. String.reduce­BNe
  48. reduce­Bdiv
    1. Int.reduce­Bdiv
  49. reduce­Beq­Diff
    1. Nat.reduce­Beq­Diff
  50. reduce­Bin
    1. BitVec.reduce­Bin
    2. Fin.reduce­Bin
    3. Int.reduce­Bin
    4. Nat.reduce­Bin
  51. reduce­Bin­Int­Nat­Op
    1. Int.reduce­Bin­Int­Nat­Op
  52. reduce­Bin­Pred
    1. BitVec.reduce­Bin­Pred
    2. Fin.reduce­Bin­Pred
    3. Int.reduce­Bin­Pred
    4. Nat.reduce­Bin­Pred
    5. String.reduce­Bin­Pred
  53. reduce­Bit­Vec­Of­Fin
    1. BitVec.reduce­Bit­Vec­Of­Fin
  54. reduce­Bit­Vec­To­Fin
    1. BitVec.reduce­Bit­Vec­To­Fin
  55. reduce­Bmod
    1. Int.reduce­Bmod
  56. reduce­Bne­Diff
    1. Nat.reduce­Bne­Diff
  57. reduce­Bool­Pred
    1. BitVec.reduce­Bool­Pred
    2. Fin.reduce­Bool­Pred
    3. Int.reduce­Bool­Pred
    4. Nat.reduce­Bool­Pred
    5. String.reduce­Bool­Pred
  58. reduce­Cast
    1. BitVec.reduce­Cast
  59. reduce­Cast­Add
    1. Fin.reduce­Cast­Add
  60. reduce­Cast­LE
    1. Fin.reduce­Cast­LE
  61. reduce­Cast­LT
    1. Fin.reduce­Cast­LT
  62. reduce­Cast­Succ
    1. Fin.reduce­Cast­Succ
  63. reduce­Div
    1. BitVec.reduce­Div
    2. Fin.reduce­Div
    3. Int.reduce­Div
    4. Nat.reduce­Div
    5. UInt16.reduce­Div
    6. UInt32.reduce­Div
    7. UInt64.reduce­Div
    8. UInt8.reduce­Div
  64. reduce­Dvd
    1. Int.reduce­Dvd
    2. Nat.reduce­Dvd
  65. reduce­Eq
    1. BitVec.reduce­Eq
    2. Fin.reduce­Eq
    3. Int.reduce­Eq
    4. String.reduce­Eq
  66. reduce­Eq­Diff
    1. Nat.reduce­Eq­Diff
  67. reduce­Extend
    1. BitVec.reduce­Extend
  68. reduce­Extrac­Lsb'
    1. BitVec.reduce­Extrac­Lsb'
  69. reduce­FDiv
    1. Int.reduce­FDiv
  70. reduce­FMod
    1. Int.reduce­FMod
  71. reduce­Fin­Mk
    1. Fin.reduce­Fin­Mk
  72. reduce­GE
    1. BitVec.reduce­GE
    2. Fin.reduce­GE
    3. Int.reduce­GE
    4. String.reduce­GE
    5. UInt16.reduce­GE
    6. UInt32.reduce­GE
    7. UInt64.reduce­GE
    8. UInt8.reduce­GE
  73. reduce­GT
    1. BitVec.reduce­GT
    2. Fin.reduce­GT
    3. Int.reduce­GT
    4. Nat.reduce­GT
    5. String.reduce­GT
    6. UInt16.reduce­GT
    7. UInt32.reduce­GT
    8. UInt64.reduce­GT
    9. UInt8.reduce­GT
  74. reduce­Gcd
    1. Nat.reduce­Gcd
  75. reduce­Get­Bit
    1. BitVec.reduce­Get­Bit
  76. reduce­Get­Elem
    1. Array.reduce­Get­Elem
    2. BitVec.reduce­Get­Elem
  77. reduce­Get­Elem!
    1. Array.reduce­Get­Elem!
  78. reduce­Get­Elem?
    1. Array.reduce­Get­Elem?
  79. reduce­Get­Lsb
    1. BitVec.reduce­Get­Lsb
  80. reduce­Get­Msb
    1. BitVec.reduce­Get­Msb
  81. reduce­HShift­Left
    1. BitVec.reduce­HShift­Left
  82. reduce­HShift­Left'
    1. BitVec.reduce­HShift­Left'
  83. reduce­HShift­Right
    1. BitVec.reduce­HShift­Right
  84. reduce­HShift­Right'
    1. BitVec.reduce­HShift­Right'
  85. reduce­LE
    1. BitVec.reduce­LE
    2. Fin.reduce­LE
    3. Int.reduce­LE
    4. String.reduce­LE
    5. UInt16.reduce­LE
    6. UInt32.reduce­LE
    7. UInt64.reduce­LE
    8. UInt8.reduce­LE
  86. reduce­LT
    1. BitVec.reduce­LT
    2. Fin.reduce­LT
    3. Int.reduce­LT
    4. Nat.reduce­LT
    5. String.reduce­LT
    6. UInt16.reduce­LT
    7. UInt32.reduce­LT
    8. UInt64.reduce­LT
    9. UInt8.reduce­LT
  87. reduce­LTLE
    1. Nat.reduce­LTLE
  88. reduce­Last
    1. Fin.reduce­Last
  89. reduce­Le­Diff
    1. Nat.reduce­Le­Diff
  90. reduce­Mk
    1. String.reduce­Mk
  91. reduce­Mod
    1. BitVec.reduce­Mod
    2. Fin.reduce­Mod
    3. Int.reduce­Mod
    4. Nat.reduce­Mod
    5. UInt16.reduce­Mod
    6. UInt32.reduce­Mod
    7. UInt64.reduce­Mod
    8. UInt8.reduce­Mod
  92. reduce­Mul
    1. BitVec.reduce­Mul
    2. Fin.reduce­Mul
    3. Int.reduce­Mul
    4. Nat.reduce­Mul
    5. UInt16.reduce­Mul
    6. UInt32.reduce­Mul
    7. UInt64.reduce­Mul
    8. UInt8.reduce­Mul
  93. reduce­Nat­Add
    1. Fin.reduce­Nat­Add
  94. reduce­Nat­Core
    1. Int.reduce­Nat­Core
  95. reduce­Nat­Eq­Expr
    1. Nat.reduce­Nat­Eq­Expr
  96. reduce­Nat­Op
    1. Fin.reduce­Nat­Op
  97. reduce­Ne
    1. BitVec.reduce­Ne
    2. Fin.reduce­Ne
    3. Int.reduce­Ne
    4. String.reduce­Ne
  98. reduce­Neg
    1. BitVec.reduce­Neg
    2. Int.reduce­Neg
  99. reduce­Neg­Succ
    1. Int.reduce­Neg­Succ
  100. reduce­Not
    1. BitVec.reduce­Not
  101. reduce­Of­Int
    1. BitVec.reduce­Of­Int
  102. reduce­Of­Nat
    1. BitVec.reduce­Of­Nat
    2. Int.reduce­Of­Nat
    3. UInt16.reduce­Of­Nat
    4. UInt32.reduce­Of­Nat
    5. UInt64.reduce­Of­Nat
    6. UInt8.reduce­Of­Nat
  103. reduce­Of­Nat'
    1. Fin.reduce­Of­Nat'
  104. reduce­Of­Nat­LT
    1. UInt16.reduce­Of­Nat­LT
    2. UInt32.reduce­Of­Nat­LT
    3. UInt64.reduce­Of­Nat­LT
    4. UInt8.reduce­Of­Nat­LT
  105. reduce­Op
    1. Fin.reduce­Op
  106. reduce­Option
    1. Array.reduce­Option
    2. List.reduce­Option
  107. reduce­Or
    1. BitVec.reduce­Or
    2. Fin.reduce­Or
    3. Nat.reduce­Or
  108. reduce­Pow
    1. Int.reduce­Pow
    2. Nat.reduce­Pow
  109. reduce­Pred
    1. Fin.reduce­Pred
  110. reduce­Replicate
    1. BitVec.reduce­Replicate
    2. List.reduce­Replicate
  111. reduce­Rev
    1. Fin.reduce­Rev
  112. reduce­Rotate­Left
    1. BitVec.reduce­Rotate­Left
  113. reduce­Rotate­Right
    1. BitVec.reduce­Rotate­Right
  114. reduce­SDiv
    1. BitVec.reduce­SDiv
  115. reduce­SLE
    1. BitVec.reduce­SLE
  116. reduce­SLT
    1. BitVec.reduce­SLT
  117. reduce­SMTSDiv
    1. BitVec.reduce­SMTSDiv
  118. reduce­SMTUDiv
    1. BitVec.reduce­SMTUDiv
  119. reduce­SMod
    1. BitVec.reduce­SMod
  120. reduce­SRem
    1. BitVec.reduce­SRem
  121. reduce­SShift­Right
    1. BitVec.reduce­SShift­Right
  122. reduce­Set­Width
    1. BitVec.reduce­Set­Width
  123. reduce­Set­Width'
    1. BitVec.reduce­Set­Width'
  124. reduce­Shift
    1. BitVec.reduce­Shift
  125. reduce­Shift­Left
    1. BitVec.reduce­Shift­Left
    2. Fin.reduce­Shift­Left
    3. Nat.reduce­Shift­Left
  126. reduce­Shift­Left­Shift­Left
    1. BitVec.reduce­Shift­Left­Shift­Left
  127. reduce­Shift­Left­Zero­Extend
    1. BitVec.reduce­Shift­Left­Zero­Extend
  128. reduce­Shift­Right
    1. Fin.reduce­Shift­Right
    2. Nat.reduce­Shift­Right
  129. reduce­Shift­Right­Shift­Right
    1. BitVec.reduce­Shift­Right­Shift­Right
  130. reduce­Shift­Shift
    1. BitVec.reduce­Shift­Shift
  131. reduce­Shift­With­Bit­Vec­Lit
    1. BitVec.reduce­Shift­With­Bit­Vec­Lit
  132. reduce­Sign­Extend
    1. BitVec.reduce­Sign­Extend
  133. reduce­Sub
    1. BitVec.reduce­Sub
    2. Fin.reduce­Sub
    3. Int.reduce­Sub
    4. Nat.reduce­Sub
    5. UInt16.reduce­Sub
    6. UInt32.reduce­Sub
    7. UInt64.reduce­Sub
    8. UInt8.reduce­Sub
  134. reduce­Sub­Diff
    1. Nat.reduce­Sub­Diff
  135. reduce­Sub­Nat
    1. Fin.reduce­Sub­Nat
  136. reduce­Succ
    1. Fin.reduce­Succ
    2. Nat.reduce­Succ
  137. reduce­TDiv
    1. Int.reduce­TDiv
  138. reduce­TMod
    1. Int.reduce­TMod
  139. reduce­To­Int
    1. BitVec.reduce­To­Int
  140. reduce­To­Nat
    1. BitVec.reduce­To­Nat
    2. Int.reduce­To­Nat
    3. UInt16.reduce­To­Nat
    4. UInt32.reduce­To­Nat
    5. UInt64.reduce­To­Nat
    6. UInt8.reduce­To­Nat
    7. USize.reduce­To­Nat
  141. reduce­UDiv
    1. BitVec.reduce­UDiv
  142. reduce­ULE
    1. BitVec.reduce­ULE
  143. reduce­ULT
    1. BitVec.reduce­ULT
  144. reduce­UMod
    1. BitVec.reduce­UMod
  145. reduce­UShift­Right
    1. BitVec.reduce­UShift­Right
  146. reduce­Unary
    1. BitVec.reduce­Unary
    2. Int.reduce­Unary
    3. Nat.reduce­Unary
  147. reduce­XOr
    1. BitVec.reduce­XOr
  148. reduce­Xor
    1. Fin.reduce­Xor
    2. Nat.reduce­Xor
  149. reduce­Zero­Extend
    1. BitVec.reduce­Zero­Extend
  150. reduction
    1. ι (iota)
  151. ref
    1. ST.Ref.ref (structure field)
  152. refine
  153. refine'
  154. refl
    1. Equivalence.refl (structure field)
  155. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  156. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  157. rel
    1. Lean.Order.PartialOrder.rel (class method)
    2. Well­FoundedRelation.rel (class method)
  158. rel_antisymm
    1. Lean.Order.PartialOrder.rel_antisymm (class method)
  159. rel_refl
    1. Lean.Order.PartialOrder.rel_refl (class method)
  160. rel_trans
    1. Lean.Order.PartialOrder.rel_trans (class method)
  161. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  162. remaining­To­String
    1. String.Iterator.remaining­To­String
  163. remove­All
    1. List.remove­All
  164. remove­Dir
    1. IO.FS.remove­Dir
  165. remove­Dir­All
    1. IO.FS.remove­Dir­All
  166. remove­File
    1. IO.FS.remove­File
  167. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  168. rename
    1. IO.FS.rename
  169. rename_i
  170. repeat (0) (1)
    1. Nat.repeat
  171. repeat'
  172. repeat1'
  173. repeat­TR
    1. Nat.repeat­TR
  174. replace
    1. List.replace
    2. String.replace
  175. replace­TR
    1. List.replace­TR
  176. replicate
    1. BitVec.replicate
    2. List.replicate
  177. replicate­TR
    1. List.replicate­TR
  178. repr
    1. Int.repr
    2. Nat.repr
    3. Option.repr
    4. USize.repr
    5. eval.derive.repr
  179. repr­Prec
    1. Repr.repr­Prec (class method)
  180. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  181. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  182. restore
    1. EStateM.Backtrackable.restore (class method)
  183. restore­M
    1. MonadControl.restore­M (class method)
    2. Monad­ControlT.restore­M (class method)
  184. rev
    1. Fin.rev
  185. rev­Find
    1. String.rev­Find
  186. rev­Pos­Of
    1. String.rev­Pos­Of
  187. reverse
    1. Array.reverse
    2. BitVec.reverse
    3. List.reverse
  188. reverse­Induction
    1. Fin.reverse­Induction
  189. revert
  190. rewind
    1. IO.FS.Handle.rewind
  191. rewrite (0) (1)
    1. trace.Meta.Tactic.simp.rewrite
  192. rfl (0) (1) (2)
    1. HEq.rfl
    2. LawfulBEq.rfl (class method)
  193. rfl'
  194. rhs
  195. right (0) (1)
    1. And.right (structure field)
  196. rightpad
    1. List.rightpad
  197. rintro
  198. root
    1. IO.FS.DirEntry.root (structure field)
    2. [anonymous] (structure field)
  199. roots
    1. [anonymous] (structure field)
  200. rotate­Left
    1. BitVec.rotate­Left
    2. List.rotate­Left
  201. rotate­Right
    1. BitVec.rotate­Right
    2. List.rotate­Right
  202. rotate_left
  203. rotate_right
  204. round
    1. Float.round
    2. Float32.round
  205. 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
  206. run'
    1. EStateM.run'
    2. State­CpsT.run'
    3. State­RefT'.run'
    4. StateT.run'
  207. run­Catch
    1. Except­CpsT.run­Catch
  208. run­EST
  209. run­K
    1. Except­CpsT.run­K
    2. State­CpsT.run­K
  210. run­ST
  211. run­Term­Elab
    1. Lean.Elab.Tactic.run­Term­Elab
  212. run_tac
  213. rw (0) (1)
  214. rw?
  215. rw_mod_cast
  216. 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­Prefix?
  108. String.drop­Right
  109. String.drop­Right­While
  110. String.drop­Suffix?
  111. String.drop­While
  112. String.end­Pos
  113. String.ends­With
  114. String.extract
  115. String.find
  116. String.find­Line­Start
  117. String.first­Diff­Pos
  118. String.foldl
  119. String.foldr
  120. String.from­Expr?
  121. String.from­UTF8
  122. String.from­UTF8!
  123. String.from­UTF8?
  124. String.front
  125. String.get
  126. String.get!
  127. String.get'
  128. String.get?
  129. String.get­Utf8Byte
  130. String.hash
  131. String.intercalate
  132. String.is­Empty
  133. String.is­Int
  134. String.is­Nat
  135. String.is­Prefix­Of
  136. String.iter
  137. String.join
  138. String.le
  139. String.length
  140. String.map
  141. String.mk
    1. Constructor of String
  142. String.mk­Iterator
  143. String.modify
  144. String.next
  145. String.next'
  146. String.next­Until
  147. String.next­While
  148. String.offset­Of­Pos
  149. String.pos­Of
  150. String.prev
  151. String.push
  152. String.pushn
  153. String.quote
  154. String.reduce­Append
  155. String.reduce­BEq
  156. String.reduce­BNe
  157. String.reduce­Bin­Pred
  158. String.reduce­Bool­Pred
  159. String.reduce­Eq
  160. String.reduce­GE
  161. String.reduce­GT
  162. String.reduce­LE
  163. String.reduce­LT
  164. String.reduce­Mk
  165. String.reduce­Ne
  166. String.remove­Leading­Spaces
  167. String.replace
  168. String.rev­Find
  169. String.rev­Pos­Of
  170. String.set
  171. String.singleton
  172. String.split
  173. String.split­On
  174. String.starts­With
  175. String.strip­Prefix
  176. String.strip­Suffix
  177. String.substr­Eq
  178. String.take
  179. String.take­Right
  180. String.take­Right­While
  181. String.take­While
  182. String.to­File­Map
  183. String.to­Format
  184. String.to­Int!
  185. String.to­Int?
  186. String.to­List
  187. String.to­Lower
  188. String.to­Name
  189. String.to­Nat!
  190. String.to­Nat?
  191. String.to­Substring
  192. String.to­Substring'
  193. String.to­UTF8
  194. String.to­Upper
  195. String.trim
  196. String.trim­Left
  197. String.trim­Right
  198. String.utf16Length
  199. String.utf16Pos­To­Codepoint­Pos
  200. String.utf16Pos­To­Codepoint­Pos­From
  201. String.utf8Byte­Size
  202. String.utf8Decode­Char?
  203. String.utf8Encode­Char
  204. String.validate­UTF8
  205. Sub
  206. Sub.mk
    1. Instance constructor of Sub
  207. Subarray
  208. Subarray.all
  209. Subarray.all­M
  210. Subarray.any
  211. Subarray.any­M
  212. Subarray.drop
  213. Subarray.empty
  214. Subarray.find­Rev?
  215. Subarray.find­Rev­M?
  216. Subarray.find­Some­Rev­M?
  217. Subarray.foldl
  218. Subarray.foldl­M
  219. Subarray.foldr
  220. Subarray.foldr­M
  221. Subarray.for­In
  222. Subarray.for­M
  223. Subarray.for­Rev­M
  224. Subarray.get
  225. Subarray.get!
  226. Subarray.get­D
  227. Subarray.mk
    1. Constructor of Subarray
  228. Subarray.pop­Front
  229. Subarray.size
  230. Subarray.split
  231. Subarray.take
  232. Subarray.to­Array
  233. Subtype
  234. Subtype.mk
    1. Constructor of Subtype
  235. Sum
  236. Sum.elim
  237. Sum.get­Left
  238. Sum.get­Left?
  239. Sum.get­Right
  240. Sum.get­Right?
  241. Sum.inhabited­Left
  242. Sum.inhabited­Right
  243. Sum.inl
    1. Constructor of Sum
  244. Sum.inr
    1. Constructor of Sum
  245. Sum.is­Left
  246. Sum.is­Right
  247. Sum.map
  248. Sum.swap
  249. Syntax
    1. Lean.Syntax
  250. Syntax­Node­Kind
    1. Lean.Syntax­Node­Kind
  251. System.File­Path
  252. System.FilePath.add­Extension
  253. System.FilePath.components
  254. System.FilePath.exe­Extension
  255. System.FilePath.ext­Separator
  256. System.FilePath.extension
  257. System.FilePath.file­Name
  258. System.FilePath.file­Stem
  259. System.FilePath.is­Absolute
  260. System.FilePath.is­Dir
  261. System.FilePath.is­Relative
  262. System.FilePath.join
  263. System.FilePath.metadata
  264. System.FilePath.mk
    1. Constructor of System.File­Path
  265. System.FilePath.normalize
  266. System.FilePath.parent
  267. System.FilePath.path­Exists
  268. System.FilePath.path­Separator
  269. System.FilePath.path­Separators
  270. System.FilePath.read­Dir
  271. System.FilePath.walk­Dir
  272. System.FilePath.with­Extension
  273. System.FilePath.with­File­Name
  274. System.Platform.is­Emscripten
  275. System.Platform.is­OSX
  276. System.Platform.is­Windows
  277. System.Platform.num­Bits
  278. System.Platform.target
  279. System.mk­File­Path
  280. s
    1. String.Iterator.s (structure field)
  281. s1
    1. StdGen.s1 (structure field)
  282. s2
    1. StdGen.s2 (structure field)
  283. sadd­Overflow
    1. BitVec.sadd­Overflow
  284. save
    1. EStateM.Backtrackable.save (class method)
  285. scale­B
    1. Float.scale­B
    2. Float32.scale­B
  286. scientific­Lit­Kind
    1. Lean.scientific­Lit­Kind
  287. script doc (Lake command)
  288. script list (Lake command)
  289. script run (Lake command)
  290. sdiv
    1. BitVec.sdiv
  291. semi­Out­Param
  292. seq
    1. Seq.seq (class method)
  293. seq­Left
    1. SeqLeft.seq­Left (class method)
  294. seq­Left_eq
    1. [anonymous] (class method)
  295. seq­Right
    1. EStateM.seq­Right
    2. SeqRight.seq­Right (class method)
  296. seq­Right_eq
    1. [anonymous] (class method)
  297. seq_assoc
    1. LawfulApplicative.pure_seq (class method)
  298. seq_pure
    1. LawfulApplicative.seq­Right_eq (class method)
  299. sequence
    1. Option.sequence
  300. serve (Lake command)
  301. 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
  302. set!
    1. Array.set!
  303. set­Access­Rights
    1. IO.set­Access­Rights
  304. set­Curr
    1. String.Iterator.set­Curr
  305. set­Current­Dir
    1. IO.Process.set­Current­Dir
  306. set­Goals
    1. Lean.Elab.Tactic.set­Goals
  307. set­If­In­Bounds
    1. Array.set­If­In­Bounds
  308. set­Kind
    1. Lean.Syntax.set­Kind
  309. set­Rand­Seed
    1. IO.set­Rand­Seed
  310. set­Stderr
    1. IO.set­Stderr
  311. set­Stdin
    1. IO.set­Stdin
  312. set­Stdout
    1. IO.set­Stdout
  313. set­TR
    1. List.set­TR
  314. set­Width
    1. BitVec.set­Width
  315. set­Width'
    1. BitVec.set­Width'
  316. set_option
  317. setsid
    1. IO.Process.SpawnArgs.args (structure field)
  318. shift­Concat
    1. BitVec.shift­Concat
  319. shift­Left
    1. BitVec.shift­Left
    2. Fin.shift­Left
    3. ISize.shift­Left
    4. Int16.shift­Left
    5. Int32.shift­Left
    6. Int64.shift­Left
    7. Int8.shift­Left
    8. Nat.shift­Left
    9. ShiftLeft.shift­Left (class method)
    10. UInt16.shift­Left
    11. UInt32.shift­Left
    12. UInt64.shift­Left
    13. UInt8.shift­Left
    14. USize.shift­Left
  320. shift­Left­Rec
    1. BitVec.shift­Left­Rec
  321. shift­Left­Zero­Extend
    1. BitVec.shift­Left­Zero­Extend
  322. 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
  323. show
  324. show_term
  325. shrink
    1. Array.shrink
  326. sign
    1. Int.sign
  327. sign­Extend
    1. BitVec.sign­Extend
  328. simp (0) (1)
  329. simp!
  330. simp?
  331. simp?!
  332. simp_all
  333. simp_all!
  334. simp_all?
  335. simp_all?!
  336. simp_all_arith
  337. simp_all_arith!
  338. simp_arith
  339. simp_arith!
  340. simp_match
  341. simp_wf
  342. simpa
  343. simpa!
  344. simpa?
  345. simpa?!
  346. simprocs
  347. sin
    1. Float.sin
    2. Float32.sin
  348. single­Pass
    1. Lean.Meta.Simp.Config.single­Pass (structure field)
  349. singleton
    1. Array.singleton
    2. List.singleton
    3. String.singleton
  350. sinh
    1. Float.sinh
    2. Float32.sinh
  351. 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
  352. size­Of
    1. SizeOf.size­Of (class method)
  353. skip (0) (1)
  354. skip­Assigned­Instances
    1. tactic.skip­Assigned­Instances
  355. sle
    1. BitVec.sle
  356. sleep
    1. IO.sleep
  357. slt
    1. BitVec.slt
  358. smod
    1. BitVec.smod
  359. smt­SDiv
    1. BitVec.smt­SDiv
  360. smt­UDiv
    1. BitVec.smt­UDiv
  361. 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)
  362. solve
  363. solve_by_elim
  364. sorry
  365. sort­MVar­Id­Array­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  366. sort­MVar­Ids­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  367. sound
    1. Quot.sound
    2. Quotient.sound
  368. span
    1. List.span
  369. spawn
    1. IO.Process.spawn
    2. Task.spawn
  370. specialize
  371. split
    1. RandomGen.split (class method)
    2. String.split
    3. Subarray.split
  372. split­At
    1. List.split­At
  373. split­By
    1. List.split­By
  374. split­On
    1. String.split­On
  375. sqrt
    1. Float.sqrt
    2. Float32.sqrt
  376. src­Dir
    1. [anonymous] (structure field) (0) (1)
  377. srem
    1. BitVec.srem
  378. sshift­Right
    1. BitVec.sshift­Right
  379. sshift­Right'
    1. BitVec.sshift­Right'
  380. sshift­Right­Rec
    1. BitVec.sshift­Right­Rec
  381. st­M
    1. MonadControl.st­M (class method)
    2. Monad­ControlT.st­M (class method)
  382. start
    1. Subarray.start (structure field)
  383. start_le_stop
    1. Subarray.start_le_stop (structure field)
  384. starts­With
    1. String.starts­With
  385. std­Next
  386. std­Range
  387. std­Split
  388. stderr
    1. IO.Process.Child.stderr (structure field)
    2. IO.Process.Output.stderr (structure field)
    3. IO.Process.StdioConfig.stderr (structure field)
  389. stdin
    1. IO.Process.Child.stdin (structure field)
    2. IO.Process.StdioConfig.stdin (structure field)
  390. stdout
    1. IO.Process.Child.stdout (structure field)
    2. IO.Process.Output.stdout (structure field)
    3. IO.Process.StdioConfig.stdout (structure field)
  391. stop
    1. Subarray.stop (structure field)
  392. stop_le_array_size
    1. Subarray.stop_le_array_size (structure field)
  393. str­Lit­Kind
    1. Lean.str­Lit­Kind
  394. strip­Prefix
    1. String.strip­Prefix
  395. strip­Suffix
    1. String.strip­Suffix
  396. strong­Rec­On
    1. Nat.strong­Rec­On
  397. sub
    1. BitVec.sub
    2. Fin.sub
    3. Float.sub
    4. Float32.sub
    5. ISize.sub
    6. Int.sub
    7. Int16.sub
    8. Int32.sub
    9. Int64.sub
    10. Int8.sub
    11. Nat.sub
    12. Sub.sub (class method)
    13. UInt16.sub
    14. UInt32.sub
    15. UInt64.sub
    16. UInt8.sub
    17. USize.sub
  398. sub­Digit­Char
    1. Nat.sub­Digit­Char
  399. sub­Nat
    1. Fin.sub­Nat
  400. sub­Nat­Nat
    1. Int.sub­Nat­Nat
  401. subst
    1. Eq.subst
    2. HEq.subst
  402. subst_eqs
  403. subst_vars
  404. substr­Eq
    1. String.substr­Eq
  405. succ
    1. Fin.succ
  406. succ­Rec
    1. Fin.succ­Rec
  407. succ­Rec­On
    1. Fin.succ­Rec­On
  408. suffices
  409. sum
    1. Array.sum
    2. List.sum
  410. super­Digit­Char
    1. Nat.super­Digit­Char
  411. support­Interpreter
    1. [anonymous] (structure field)
  412. swap
    1. Array.swap
    2. Prod.swap
    3. ST.Ref.swap
    4. Sum.swap
  413. swap­At
    1. Array.swap­At
  414. swap­At!
    1. Array.swap­At!
  415. swap­If­In­Bounds
    1. Array.swap­If­In­Bounds
  416. symm
    1. Eq.symm
    2. Equivalence.symm (structure field)
  417. symm_saturate
  418. synthInstance.max­Heartbeats
  419. synthInstance.max­Size
  420. 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.bind
  12. Task.get
  13. Task.map
  14. Task.pure
    1. Constructor of Task
  15. Task.spawn
  16. Term
    1. Lean.Syntax.Term
  17. Thunk
  18. Thunk.bind
  19. Thunk.get
  20. Thunk.map
  21. Thunk.mk
    1. Constructor of Thunk
  22. Thunk.pure
  23. To­String
  24. ToString.mk
    1. Instance constructor of To­String
  25. Transparency­Mode
    1. Lean.Meta.Transparency­Mode
  26. True
  27. True.intro
    1. Constructor of True
  28. Type
  29. Type­Name
  30. tactic
  31. tactic'
  32. tactic.custom­Eliminators
  33. tactic.hygienic
  34. tactic.simp.trace (0) (1)
  35. tactic.skip­Assigned­Instances
  36. tactic­Elab­Attribute
    1. Lean.Elab.Tactic.tactic­Elab­Attribute
  37. tag­Untagged­Goals
    1. Lean.Elab.Tactic.tag­Untagged­Goals
  38. tail
    1. List.tail
  39. tail!
    1. List.tail!
  40. tail?
    1. List.tail?
  41. tail­D
    1. List.tail­D
  42. take
    1. Array.take
    2. List.take
    3. ST.Ref.take
    4. String.take
    5. Subarray.take
  43. take­Right
    1. String.take­Right
  44. take­Right­While
    1. String.take­Right­While
  45. take­Stdin
    1. IO.Process.Child.take­Stdin
  46. take­TR
    1. List.take­TR
  47. take­While
    1. Array.take­While
    2. List.take­While
    3. String.take­While
  48. take­While­TR
    1. List.take­While­TR
  49. tan
    1. Float.tan
    2. Float32.tan
  50. tanh
    1. Float.tanh
    2. Float32.tanh
  51. target
    1. System.Platform.target
  52. tdiv
    1. Int.tdiv
  53. term
    1. placeholder
  54. test (Lake command)
  55. test­Bit
    1. Nat.test­Bit
  56. threshold
    1. pp.deepTerms.threshold
    2. pp.proofs.threshold
  57. throw
    1. EStateM.throw
    2. MonadExcept.throw (class method)
    3. Monad­ExceptOf.throw (class method)
  58. throw­Error
    1. Lean.Macro.throw­Error
  59. throw­Error­At
    1. Lean.Macro.throw­Error­At
  60. throw­The
  61. throw­Unsupported
    1. Lean.Macro.throw­Unsupported
  62. tmod
    1. Int.tmod
  63. to­Applicative
    1. Alternative.to­Applicative (class method)
    2. Monad.to­Applicative (class method)
  64. to­Array
    1. List.to­Array
    2. Option.to­Array
    3. Subarray.to­Array
  65. to­Array­Impl
    1. List.to­Array­Impl
  66. to­Base­IO
    1. EIO.to­Base­IO
  67. to­Bind
    1. [anonymous] (class method)
  68. 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)
  69. to­Bits
    1. Float.to­Bits
    2. Float32.to­Bits
  70. to­Bool
    1. Except.to­Bool
  71. to­Byte­Array
    1. List.to­Byte­Array
  72. to­Digits
    1. Nat.to­Digits
  73. to­Digits­Core
    1. Nat.to­Digits­Core
  74. to­EIO
    1. BaseIO.to­EIO
    2. IO.to­EIO
  75. to­End
    1. String.Iterator.to­End
  76. to­File­Map
    1. String.to­File­Map
  77. to­Fin
    1. BitVec.to­Fin (structure field)
    2. UInt16.to­Fin
    3. UInt32.to­Fin
    4. UInt64.to­Fin
    5. UInt8.to­Fin
    6. USize.to­Fin
  78. to­Float
    1. Float32.to­Float
    2. ISize.to­Float
    3. Int16.to­Float
    4. Int32.to­Float
    5. Int64.to­Float
    6. Int8.to­Float
    7. Nat.to­Float
    8. UInt16.to­Float
    9. UInt32.to­Float
    10. UInt64.to­Float
    11. UInt8.to­Float
    12. USize.to­Float
  79. to­Float32
    1. Float.to­Float32
    2. ISize.to­Float32
    3. Int16.to­Float32
    4. Int32.to­Float32
    5. Int64.to­Float32
    6. Int8.to­Float32
    7. Nat.to­Float32
    8. UInt16.to­Float32
    9. UInt32.to­Float32
    10. UInt64.to­Float32
    11. UInt8.to­Float32
    12. USize.to­Float32
  80. to­Float­Array
    1. List.to­Float­Array
  81. to­Format
    1. String.to­Format
  82. to­Functor
    1. Applicative.to­Functor (class method)
  83. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  84. to­Handle­Type
    1. IO.Process.Stdio.to­Handle­Type
  85. to­Hex
    1. BitVec.to­Hex
  86. to­IO
    1. BaseIO.to­IO
    2. EIO.to­IO
  87. to­IO'
    1. EIO.to­IO'
  88. to­ISize
    1. Bool.to­ISize
    2. Float.to­ISize
    3. Float32.to­ISize
    4. Int.to­ISize
    5. Int16.to­ISize
    6. Int32.to­ISize
    7. Int64.to­ISize
    8. Int8.to­ISize
    9. Nat.to­ISize
    10. USize.to­ISize
  89. to­Int
    1. BitVec.to­Int
    2. Bool.to­Int
    3. ISize.to­Int
    4. Int16.to­Int
    5. Int32.to­Int
    6. Int64.to­Int
    7. Int8.to­Int
  90. to­Int!
    1. String.to­Int!
  91. to­Int16
    1. Bool.to­Int16
    2. Float.to­Int16
    3. Float32.to­Int16
    4. ISize.to­Int16
    5. Int.to­Int16
    6. Int32.to­Int16
    7. Int64.to­Int16
    8. Int8.to­Int16
    9. Nat.to­Int16
    10. UInt16.to­Int16
  92. to­Int32
    1. Bool.to­Int32
    2. Float.to­Int32
    3. Float32.to­Int32
    4. ISize.to­Int32
    5. Int.to­Int32
    6. Int16.to­Int32 (0) (1)
    7. Int64.to­Int32
    8. Int8.to­Int32 (0) (1)
    9. Nat.to­Int32
    10. UInt32.to­Int32
  93. to­Int64
    1. Bool.to­Int64
    2. Float.to­Int64
    3. Float32.to­Int64
    4. ISize.to­Int64
    5. Int.to­Int64
    6. Int16.to­Int64
    7. Int32.to­Int64
    8. Int8.to­Int64
    9. Nat.to­Int64
    10. UInt64.to­Int64
  94. to­Int8
    1. Bool.to­Int8
    2. Float.to­Int8
    3. Float32.to­Int8
    4. ISize.to­Int8
    5. Int.to­Int8
    6. Int16.to­Int8
    7. Int32.to­Int8
    8. Int64.to­Int8
    9. Nat.to­Int8
    10. UInt8.to­Int8
  95. to­Int?
    1. String.to­Int?
  96. to­Lawful­Applicative
    1. LawfulMonad.to­Lawful­Applicative (class method)
  97. to­Lawful­Functor
    1. LawfulApplicative.to­Lawful­Functor (class method)
  98. to­Lean­Config
    1. Lake.Lean­ExeConfig.to­Lean­Config (structure field)
    2. Lake.Lean­LibConfig.to­Lean­Config (structure field)
  99. to­Level
    1. Nat.to­Level
  100. to­List
    1. Array.to­List
    2. Array.to­List (structure field)
    3. Option.to­List
    4. String.to­List
  101. to­List­Append
    1. Array.to­List­Append
  102. to­List­Rev
    1. Array.to­List­Rev
  103. to­Lower
    1. String.to­Lower
  104. to­Monad­State­Of
    1. ST.Ref.to­Monad­State­Of
  105. to­Name
    1. String.to­Name
  106. to­Nat
    1. BitVec.to­Nat
    2. Bool.to­Nat
    3. Fin.to­Nat
    4. Int.to­Nat
    5. UInt16.to­Nat
    6. UInt32.to­Nat
    7. UInt64.to­Nat
    8. UInt8.to­Nat
    9. USize.to­Nat
  107. to­Nat!
    1. String.to­Nat!
  108. to­Nat'
    1. Int.to­Nat'
  109. to­Nat?
    1. String.to­Nat?
  110. to­Nat­Clamp­Neg
    1. ISize.to­Nat­Clamp­Neg
    2. Int16.to­Nat­Clamp­Neg
    3. Int32.to­Nat­Clamp­Neg
    4. Int64.to­Nat­Clamp­Neg
    5. Int8.to­Nat­Clamp­Neg
  111. to­Option
    1. Except.to­Option
  112. to­PArray'
    1. Array.to­PArray'
    2. List.to­PArray'
  113. to­Partial­Order
    1. Lean.Order.CCPO.to­Partial­Order (class method)
  114. to­Pure
    1. [anonymous] (class method)
  115. to­Seq
    1. [anonymous] (class method)
  116. to­Seq­Left
    1. Applicative.to­Pure (class method)
  117. to­Seq­Right
    1. [anonymous] (class method)
  118. to­Stdio­Config
    1. IO.Process.SpawnArgs.to­Stdio­Config (structure field)
  119. to­String
    1. Float.to­String
    2. Float32.to­String
    3. IO.Error.to­String
    4. List.to­String
    5. System.FilePath.to­String (structure field)
    6. ToString.to­String (class method)
  120. to­Sub­Digits
    1. Nat.to­Sub­Digits
  121. to­Subarray
    1. Array.to­Subarray
  122. to­Subscript­String
    1. Nat.to­Subscript­String
  123. to­Substring
    1. String.to­Substring
  124. to­Substring'
    1. String.to­Substring'
  125. to­Super­Digits
    1. Nat.to­Super­Digits
  126. to­Superscript­String
    1. Nat.to­Superscript­String
  127. to­UInt16
    1. Bool.to­UInt16
    2. Float.to­UInt16
    3. Float32.to­UInt16
    4. Int16.to­UInt16 (structure field)
    5. Nat.to­UInt16
    6. UInt32.to­UInt16
    7. UInt64.to­UInt16
    8. UInt8.to­UInt16
    9. USize.to­UInt16
  128. to­UInt32
    1. Bool.to­UInt32
    2. Float.to­UInt32
    3. Float32.to­UInt32
    4. Int32.to­UInt32 (structure field)
    5. Nat.to­UInt32
    6. UInt16.to­UInt32
    7. UInt64.to­UInt32
    8. UInt8.to­UInt32
    9. USize.to­UInt32
  129. to­UInt64
    1. Bool.to­UInt64
    2. Float.to­UInt64
    3. Float32.to­UInt64
    4. Int64.to­UInt64 (structure field)
    5. Nat.to­UInt64
    6. UInt16.to­UInt64
    7. UInt32.to­UInt64
    8. UInt8.to­UInt64
    9. USize.to­UInt64
  130. to­UInt8
    1. Bool.to­UInt8
    2. Float.to­UInt8
    3. Float32.to­UInt8
    4. Int8.to­UInt8 (structure field)
    5. Nat.to­UInt8
    6. UInt16.to­UInt8
    7. UInt32.to­UInt8
    8. UInt64.to­UInt8
    9. USize.to­UInt8
  131. to­USize
    1. Bool.to­USize
    2. Float.to­USize
    3. Float32.to­USize
    4. ISize.to­USize (structure field)
    5. Nat.to­USize
    6. UInt16.to­USize
    7. UInt32.to­USize
    8. UInt64.to­USize
    9. UInt8.to­USize
  132. to­UTF8
    1. String.to­UTF8
  133. to­Upper
    1. String.to­Upper
  134. to­Vector
    1. Array.to­Vector
  135. trace
    1. Lean.Macro.trace
    2. tactic.simp.trace (0) (1)
  136. trace.Elab.definition.wf
  137. trace.Meta.Tactic.simp.discharge
  138. trace.Meta.Tactic.simp.rewrite
  139. trace_state (0) (1)
  140. trans
    1. Eq.trans
    2. Equivalence.trans (structure field)
  141. translate-config (Lake command)
  142. transparency
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  143. trim
    1. String.trim
  144. trim­Left
    1. String.trim­Left
  145. trim­Right
    1. String.trim­Right
  146. trivial
  147. truncate
    1. BitVec.truncate
    2. IO.FS.Handle.truncate
  148. try (0) (1)
  149. 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
  150. try­Catch­The
  151. try­Finally'
    1. MonadFinally.try­Finally' (class method)
  152. try­Lock
    1. IO.FS.Handle.try­Lock
  153. try­Tactic
    1. Lean.Elab.Tactic.try­Tactic
  154. try­Tactic?
    1. Lean.Elab.Tactic.try­Tactic?
  155. try­Wait
    1. IO.Process.Child.try­Wait
  156. two­Pow
    1. BitVec.two­Pow
  157. type
    1. IO.FS.Metadata.type (structure field)
    2. eval.type
  158. type constructor
  159. type_eq_of_heq

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

V

  1. val
    1. Char.val (structure field)
    2. Fin.val (structure field)
    3. Float.val (structure field)
    4. Float32.val (structure field)
    5. Subtype.val (structure field)
  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­Dir
    1. IO.FS.with­Temp­Dir
  25. with­Temp­File
    1. IO.FS.with­Temp­File
  26. with­The­Reader
  27. with_reducible
  28. with_reducible_and_instances
  29. with_unfolding_all
  30. without­Position
  31. write
    1. IO.FS.Handle.write
    2. IO.FS.Stream.write (structure field)
  32. write­Bin­File
    1. IO.FS.write­Bin­File
  33. write­File
    1. IO.FS.write­File

X

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

Z

  1. Zero
  2. Zero.mk
    1. Instance constructor of Zero
  3. zero
    1. BitVec.zero
    2. Zero.zero (class method)
  4. zero­Extend
    1. BitVec.zero­Extend
  5. zeta
    1. Lean.Meta.DSimp.Config.zeta (structure field)
    2. Lean.Meta.Simp.Config.zeta (structure field)
  6. zeta­Delta
    1. Lean.Meta.DSimp.Config.zeta­Delta (structure field)
    2. Lean.Meta.Simp.Config.zeta­Delta (structure field)
  7. zeta­Unused
    1. Lean.Meta.DSimp.Config.zeta­Unused (structure field)
    2. Lean.Meta.Simp.Config.zeta­Unused (structure field)
  8. zip
    1. Array.zip
    2. List.zip
  9. zip­Idx
    1. Array.zip­Idx
    2. List.zip­Idx
  10. zip­Idx­LE
    1. List.zip­Idx­LE
  11. zip­Idx­TR
    1. List.zip­Idx­TR
  12. zip­With
    1. Array.zip­With
    2. List.zip­With
  13. zip­With­All
    1. Array.zip­With­All
    2. List.zip­With­All
  14. zip­With­TR
    1. List.zip­With­TR