The Lean Language Reference

Index

Symbols

  1. ( ... )
  2. . ...
  3. <;> (0) (1)
  4. { ... }
  5. ·
  6. · ...
  7. Σ-types
  8. ι-reduction

A

  1. AR (environment variable)
  2. Acc
  3. Acc.intro
    1. Constructor of Acc
  4. Access­Right
    1. IO.Access­Right
  5. Add
  6. Add.mk
    1. Instance constructor of Add
  7. Alternative
  8. Alternative.mk
    1. Instance constructor of Alternative
  9. And
  10. And.elim
  11. And.intro
    1. Constructor of And
  12. Append
  13. Append.mk
    1. Instance constructor of Append
  14. Applicative
  15. Applicative.mk
    1. Instance constructor of Applicative
  16. Array
  17. Array.all
  18. Array.all­Diff
  19. Array.all­M
  20. Array.any
  21. Array.any­M
  22. Array.append
  23. Array.append­List
  24. Array.attach
  25. Array.attach­With
  26. Array.back
  27. Array.back!
  28. Array.back?
  29. Array.bin­Insert
  30. Array.bin­Insert­M
  31. Array.bin­Search
  32. Array.bin­Search­Contains
  33. Array.contains
  34. Array.count
  35. Array.count­P
  36. Array.drop
  37. Array.elem
  38. Array.empty
  39. Array.empty­With­Capacity
  40. Array.erase
  41. Array.erase­Idx
  42. Array.erase­Idx!
  43. Array.erase­Idx­If­In­Bounds
  44. Array.erase­P
  45. Array.erase­Reps
  46. Array.extract
  47. Array.filter
  48. Array.filter­M
  49. Array.filter­Map
  50. Array.filter­Map­M
  51. Array.filter­Rev­M
  52. Array.filter­Sep­Elems
  53. Array.filter­Sep­Elems­M
  54. Array.fin­Idx­Of?
  55. Array.fin­Range
  56. Array.find?
  57. Array.find­Fin­Idx?
  58. Array.find­Idx
  59. Array.find­Idx?
  60. Array.find­Idx­M?
  61. Array.find­M?
  62. Array.find­Rev?
  63. Array.find­Rev­M?
  64. Array.find­Some!
  65. Array.find­Some?
  66. Array.find­Some­M?
  67. Array.find­Some­Rev?
  68. Array.find­Some­Rev­M?
  69. Array.first­M
  70. Array.flat­Map
  71. Array.flat­Map­M
  72. Array.flatten
  73. Array.foldl
  74. Array.foldl­M
  75. Array.foldr
  76. Array.foldr­M
  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.leftpad
  93. Array.lex
  94. Array.map
  95. Array.map­Fin­Idx
  96. Array.map­Fin­Idx­M
  97. Array.map­Idx
  98. Array.map­Idx­M
  99. Array.map­M
  100. Array.map­M'
  101. Array.map­Mono
  102. Array.map­Mono­M
  103. Array.mk
    1. Constructor of Array
  104. Array.modify
  105. Array.modify­M
  106. Array.modify­Op
  107. Array.of­Fn
  108. Array.of­Subarray
  109. Array.partition
  110. Array.pmap
  111. Array.pop
  112. Array.pop­While
  113. Array.push
  114. Array.qsort
  115. Array.qsort­Ord
  116. Array.range
  117. Array.range'
  118. Array.replace
  119. Array.replicate
  120. Array.reverse
  121. Array.rightpad
  122. Array.set
  123. Array.set!
  124. Array.set­If­In­Bounds
  125. Array.shrink
  126. Array.singleton
  127. Array.size
  128. Array.sum
  129. Array.swap
  130. Array.swap­At
  131. Array.swap­At!
  132. Array.swap­If­In­Bounds
  133. Array.take
  134. Array.take­While
  135. Array.to­List
  136. Array.to­List­Append
  137. Array.to­List­Rev
  138. Array.to­Subarray
  139. Array.to­Vector
  140. Array.uget
  141. Array.unattach
  142. Array.unzip
  143. Array.uset
  144. Array.usize
  145. Array.zip
  146. Array.zip­Idx
  147. Array.zip­With
  148. Array.zip­With­All
  149. Atomic­T
    1. Std.Atomic­T
  150. abs
    1. BitVec.abs
  151. abs
    1. Float.abs
  152. abs
    1. Float32.abs
  153. abs
    1. ISize.abs
  154. abs
    1. Int16.abs
  155. abs
    1. Int32.abs
  156. abs
    1. Int64.abs
  157. abs
    1. Int8.abs
  158. absurd
  159. ac_nf
  160. ac_nf0
  161. ac_rfl
  162. accessed
    1. IO.FS.Metadata.accessed (structure field)
  163. acos
    1. Float.acos
  164. acos
    1. Float32.acos
  165. acosh
    1. Float.acosh
  166. acosh
    1. Float32.acosh
  167. adapt
    1. ExceptT.adapt
  168. adapt
    1. ReaderT.adapt
  169. adapt­Except
    1. EStateM.adapt­Except
  170. adc
    1. BitVec.adc
  171. adcb
    1. BitVec.adcb
  172. add
    1. Add.add (class method)
  173. add
    1. BitVec.add
  174. add
    1. Fin.add
  175. add
    1. Float.add
  176. add
    1. Float32.add
  177. add
    1. ISize.add
  178. add
    1. Int.add
  179. add
    1. Int16.add
  180. add
    1. Int32.add
  181. add
    1. Int64.add
  182. add
    1. Int8.add
  183. add
    1. Nat.add
  184. add
    1. UInt16.add
  185. add
    1. UInt32.add
  186. add
    1. UInt64.add
  187. add
    1. UInt8.add
  188. add
    1. USize.add
  189. add­Cases
    1. Fin.add­Cases
  190. add­Extension
    1. System.FilePath.add­Extension
  191. add­Heartbeats
    1. IO.add­Heartbeats
  192. add­Macro­Scope
    1. Lean.Macro.add­Macro­Scope
  193. add­Nat
    1. Fin.add­Nat
  194. admit
  195. all
    1. Array.all
  196. all
    1. List.all
  197. all
    1. Nat.all
  198. all
    1. Option.all
  199. all
    1. String.all
  200. all
    1. Subarray.all
  201. all
    1. Substring.all
  202. all­Diff
    1. Array.all­Diff
  203. all­Eq
    1. Subsingleton.all­Eq (class method)
  204. all­I
    1. Prod.all­I
  205. all­M
    1. Array.all­M
  206. all­M
    1. List.all­M
  207. all­M
    1. Nat.all­M
  208. all­M
    1. Subarray.all­M
  209. all­Ones
    1. BitVec.all­Ones
  210. all­TR
    1. Nat.all­TR
  211. all_goals (0) (1)
  212. allow­Unsafe­Reducibility
  213. and
    1. BitVec.and
  214. and
    1. Bool.and
  215. and
    1. List.and
  216. and­M
  217. and_intros
  218. any
    1. Array.any
  219. any
    1. List.any
  220. any
    1. Nat.any
  221. any
    1. Option.any
  222. any
    1. String.any
  223. any
    1. Subarray.any
  224. any
    1. Substring.any
  225. any­I
    1. Prod.any­I
  226. any­M
    1. Array.any­M
  227. any­M
    1. List.any­M
  228. any­M
    1. Nat.any­M
  229. any­M
    1. Subarray.any­M
  230. any­TR
    1. Nat.any­TR
  231. any_goals (0) (1)
  232. app­Dir
    1. IO.app­Dir
  233. app­Path
    1. IO.app­Path
  234. append
    1. Append.append (class method)
  235. append
    1. Array.append
  236. append
    1. BitVec.append
  237. append
    1. List.append
  238. append
    1. String.append
  239. append­List
    1. Array.append­List
  240. append­TR
    1. List.append­TR
  241. apply (0) (1)
  242. apply?
  243. apply_assumption
  244. apply_ext_theorem
  245. apply_mod_cast
  246. apply_rfl
  247. apply_rules
  248. arg [@]i
  249. args
  250. args
    1. [anonymous] (structure field)
  251. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  252. array
    1. Subarray.array (structure field)
  253. as­String
    1. List.as­String
  254. as­Task
    1. BaseIO.as­Task
  255. as­Task
    1. EIO.as­Task
  256. as­Task
    1. IO.as­Task
  257. as_aux_lemma
  258. asin
    1. Float.asin
  259. asin
    1. Float32.asin
  260. asinh
    1. Float.asinh
  261. asinh
    1. Float32.asinh
  262. assumption
  263. assumption
    1. inaccessible
  264. assumption_mod_cast
  265. at­End
    1. String.Iterator.at­End
  266. at­End
    1. String.at­End
  267. at­End
    1. Substring.at­End
  268. atan
    1. Float.atan
  269. atan
    1. Float32.atan
  270. atan2
    1. Float.atan2
  271. atan2
    1. Float32.atan2
  272. atanh
    1. Float.atanh
  273. atanh
    1. Float32.atanh
  274. atomically
    1. Std.Mutex.atomically
  275. atomically­Once
    1. Std.Mutex.atomically­Once
  276. attach
    1. Array.attach
  277. attach
    1. List.attach
  278. attach
    1. Option.attach
  279. attach­With
    1. Array.attach­With
  280. attach­With
    1. List.attach­With
  281. attach­With
    1. Option.attach­With
  282. auto­Implicit
  283. auto­Lift
  284. auto­Param
  285. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  286. auto­Unfold
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
  287. auto­Unfold
    1. 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.chain­Task
  9. BaseIO.map­Task
  10. BaseIO.map­Tasks
  11. BaseIO.to­EIO
  12. BaseIO.to­IO
  13. Bind
  14. Bind.bind­Left
  15. Bind.kleisli­Left
  16. Bind.kleisli­Right
  17. Bind.mk
    1. Instance constructor of Bind
  18. Bit­Vec
  19. BitVec.abs
  20. BitVec.adc
  21. BitVec.adcb
  22. BitVec.add
  23. BitVec.all­Ones
  24. BitVec.and
  25. BitVec.append
  26. BitVec.carry
  27. BitVec.cast
  28. BitVec.concat
  29. BitVec.cons
  30. BitVec.dec­Eq
  31. BitVec.div­Rec
  32. BitVec.div­Subtract­Shift
  33. BitVec.extract­Lsb
  34. BitVec.extract­Lsb'
  35. BitVec.fill
  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.iunfoldr_replace
  47. BitVec.msb
  48. BitVec.mul
  49. BitVec.mul­Rec
  50. BitVec.neg
  51. BitVec.nil
  52. BitVec.not
  53. BitVec.of­Bool
  54. BitVec.of­Bool­List­BE
  55. BitVec.of­Bool­List­LE
  56. BitVec.of­Fin
    1. Constructor of Bit­Vec
  57. BitVec.of­Int
  58. BitVec.of­Nat
  59. BitVec.of­Nat­LT
  60. BitVec.or
  61. BitVec.replicate
  62. BitVec.reverse
  63. BitVec.rotate­Left
  64. BitVec.rotate­Right
  65. BitVec.sadd­Overflow
  66. BitVec.sdiv
  67. BitVec.set­Width
  68. BitVec.set­Width'
  69. BitVec.shift­Concat
  70. BitVec.shift­Left
  71. BitVec.shift­Left­Rec
  72. BitVec.shift­Left­Zero­Extend
  73. BitVec.sign­Extend
  74. BitVec.sle
  75. BitVec.slt
  76. BitVec.smod
  77. BitVec.smt­SDiv
  78. BitVec.smt­UDiv
  79. BitVec.srem
  80. BitVec.sshift­Right
  81. BitVec.sshift­Right'
  82. BitVec.sshift­Right­Rec
  83. BitVec.ssub­Overflow
  84. BitVec.sub
  85. BitVec.to­Hex
  86. BitVec.to­Int
  87. BitVec.to­Nat
  88. BitVec.truncate
  89. BitVec.two­Pow
  90. BitVec.uadd­Overflow
  91. BitVec.udiv
  92. BitVec.ule
  93. BitVec.ult
  94. BitVec.umod
  95. BitVec.ushift­Right
  96. BitVec.ushift­Right­Rec
  97. BitVec.usub­Overflow
  98. BitVec.xor
  99. BitVec.zero
  100. BitVec.zero­Extend
  101. Bool
  102. Bool.and
  103. Bool.dcond
  104. Bool.dec­Eq
  105. Bool.false
    1. Constructor of Bool
  106. Bool.not
  107. Bool.or
  108. Bool.to­ISize
  109. Bool.to­Int
  110. Bool.to­Int16
  111. Bool.to­Int32
  112. Bool.to­Int64
  113. Bool.to­Int8
  114. Bool.to­Nat
  115. Bool.to­UInt16
  116. Bool.to­UInt32
  117. Bool.to­UInt64
  118. Bool.to­UInt8
  119. Bool.to­USize
  120. Bool.true
    1. Constructor of Bool
  121. Bool.xor
  122. Buffer
    1. IO.FS.Stream.Buffer
  123. Build­Type
    1. Lake.Build­Type
  124. back!
    1. Array.back!
  125. back
    1. Array.back
  126. back
    1. String.back
  127. back?
    1. Array.back?
  128. backward.synthInstance.canon­Instances
  129. bdiv
    1. Int.bdiv
  130. beq
    1. BEq.beq (class method)
  131. beq
    1. Float.beq
  132. beq
    1. Float32.beq
  133. beq
    1. List.beq
  134. beq
    1. Nat.beq
  135. beq
    1. Substring.beq
  136. beta
    1. Lean.Meta.DSimp.Config.beta (structure field)
  137. beta
    1. Lean.Meta.Simp.Config.beta (structure field)
  138. bin­Insert
    1. Array.bin­Insert
  139. bin­Insert­M
    1. Array.bin­Insert­M
  140. bin­Search
    1. Array.bin­Search
  141. bin­Search­Contains
    1. Array.bin­Search­Contains
  142. bind
    1. Bind.bind (class method)
  143. bind
    1. EStateM.bind
  144. bind
    1. Except.bind
  145. bind
    1. ExceptT.bind
  146. bind
    1. Option.bind
  147. bind
    1. OptionT.bind
  148. bind
    1. ReaderT.bind
  149. bind
    1. StateT.bind
  150. bind
    1. Task.bind
  151. bind
    1. Thunk.bind
  152. bind­Cont
    1. ExceptT.bind­Cont
  153. bind­Left
    1. Bind.bind­Left
  154. bind­M
    1. Option.bind­M
  155. bind­Task
    1. BaseIO.bind­Task
  156. bind­Task
    1. EIO.bind­Task
  157. bind­Task
    1. IO.bind­Task
  158. bind_assoc
    1. [anonymous] (class method)
  159. bind_map
    1. [anonymous] (class method)
  160. bind_pure_comp
    1. [anonymous] (class method)
  161. binder­Name­Hint
  162. bitwise
    1. Nat.bitwise
  163. ble
    1. Nat.ble
  164. blt
    1. Nat.blt
  165. bmod
    1. Int.bmod
  166. bootstrap.inductive­Check­Resulting­Universe
  167. bsize
    1. Substring.bsize
  168. build (Lake command)
  169. bv_check
  170. bv_decide
  171. bv_decide?
  172. bv_normalize
  173. bv_omega
  174. by­Cases
    1. Decidable.by­Cases
  175. by_cases
  176. by_cases'
    1. Or.by_cases'
  177. by_cases
    1. Or.by_cases
  178. byte­Idx
    1. String.Pos.byte­Idx (structure field)
  179. byte­Size
    1. IO.FS.Metadata.byte­Size (structure field)

C

  1. CC (environment variable)
  2. CCPO
    1. Lean.Order.CCPO
  3. Channel
    1. Std.Channel
  4. Char
  5. Char.is­Alpha
  6. Char.is­Alphanum
  7. Char.is­Digit
  8. Char.is­Lower
  9. Char.is­Upper
  10. Char.is­Valid­Char­Nat
  11. Char.is­Whitespace
  12. Char.le
  13. Char.lt
  14. Char.mk
    1. Constructor of Char
  15. Char.of­Nat
  16. Char.of­UInt8
  17. Char.quote
  18. Char.to­Lower
  19. Char.to­Nat
  20. Char.to­String
  21. Char.to­UInt8
  22. Char.to­Upper
  23. Char.utf16Size
  24. Char.utf8Size
  25. Char­Lit
    1. Lean.Syntax.Char­Lit
  26. Child
    1. IO.Process.Child
  27. Closeable­Channel
    1. Std.Closeable­Channel
  28. Coe
  29. Coe.mk
    1. Instance constructor of Coe
  30. Coe­Dep
  31. CoeDep.mk
    1. Instance constructor of Coe­Dep
  32. Coe­Fun
  33. CoeFun.mk
    1. Instance constructor of Coe­Fun
  34. Coe­HTC
  35. CoeHTC.mk
    1. Instance constructor of Coe­HTC
  36. Coe­HTCT
  37. CoeHTCT.mk
    1. Instance constructor of Coe­HTCT
  38. Coe­Head
  39. CoeHead.mk
    1. Instance constructor of Coe­Head
  40. Coe­OTC
  41. CoeOTC.mk
    1. Instance constructor of Coe­OTC
  42. Coe­Out
  43. CoeOut.mk
    1. Instance constructor of Coe­Out
  44. Coe­Sort
  45. CoeSort.mk
    1. Instance constructor of Coe­Sort
  46. Coe­T
  47. CoeT.mk
    1. Instance constructor of Coe­T
  48. Coe­TC
  49. CoeTC.mk
    1. Instance constructor of Coe­TC
  50. Coe­Tail
  51. CoeTail.mk
    1. Instance constructor of Coe­Tail
  52. Command
    1. Lean.Syntax.Command
  53. Condvar
    1. Std.Condvar
  54. Config
    1. Lean.Meta.DSimp.Config
  55. Config
    1. Lean.Meta.Rewrite.Config
  56. Config
    1. Lean.Meta.Simp.Config
  57. calc
  58. call-by-need
  59. cancel
    1. IO.cancel
  60. canon­Instances
    1. backward.synthInstance.canon­Instances
  61. capitalize
    1. String.capitalize
  62. carry
    1. BitVec.carry
  63. case
  64. case ... => ...
  65. case'
  66. case' ... => ...
  67. case­Strong­Rec­On
    1. Nat.case­Strong­Rec­On
  68. cases
  69. cases
    1. Fin.cases
  70. cases­Aux­On
    1. Nat.cases­Aux­On
  71. cast
  72. cast
    1. BitVec.cast
  73. cast
    1. Fin.cast
  74. cast
    1. Int.cast
  75. cast
    1. Nat.cast
  76. cast­Add
    1. Fin.cast­Add
  77. cast­LE
    1. Fin.cast­LE
  78. cast­LT
    1. Fin.cast­LT
  79. cast­Succ
    1. Fin.cast­Succ
  80. cast_heq
  81. catch­Exceptions
    1. EIO.catch­Exceptions
  82. cbrt
    1. Float.cbrt
  83. cbrt
    1. Float32.cbrt
  84. ceil
    1. Float.ceil
  85. ceil
    1. Float32.ceil
  86. chain
    1. of coercions
  87. chain­Task
    1. BaseIO.chain­Task
  88. chain­Task
    1. EIO.chain­Task
  89. chain­Task
    1. IO.chain­Task
  90. change (0) (1)
  91. change ... with ...
  92. char­Lit­Kind
    1. Lean.char­Lit­Kind
  93. check-build (Lake command)
  94. check-lint (Lake command)
  95. check-test (Lake command)
  96. check­Canceled
    1. IO.check­Canceled
  97. choice
    1. Option.choice
  98. choice­Kind
    1. Lean.choice­Kind
  99. choose
    1. Exists.choose
  100. classical
  101. clean (Lake command)
  102. clear
  103. cmd
    1. [anonymous] (structure field)
  104. coe
    1. Coe.coe (class method)
  105. coe
    1. CoeDep.coe (class method)
  106. coe
    1. CoeFun.coe (class method)
  107. coe
    1. CoeHTC.coe (class method)
  108. coe
    1. CoeHTCT.coe (class method)
  109. coe
    1. CoeHead.coe (class method)
  110. coe
    1. CoeOTC.coe (class method)
  111. coe
    1. CoeOut.coe (class method)
  112. coe
    1. CoeSort.coe (class method)
  113. coe
    1. CoeT.coe (class method)
  114. coe
    1. CoeTC.coe (class method)
  115. coe
    1. CoeTail.coe (class method)
  116. col­Eq
  117. col­Ge
  118. col­Gt
  119. comment
    1. block
  120. comment
    1. line
  121. common­Prefix
    1. Substring.common­Prefix
  122. common­Suffix
    1. Substring.common­Suffix
  123. comp
    1. Function.comp
  124. comp_map
    1. LawfulFunctor.comp_map (class method)
  125. compare
    1. Ord.compare (class method)
  126. compare­Lex
  127. compare­Of­Less­And­BEq
  128. compare­Of­Less­And­Eq
  129. compare­On
  130. complement
    1. ISize.complement
  131. complement
    1. Int16.complement
  132. complement
    1. Int32.complement
  133. complement
    1. Int64.complement
  134. complement
    1. Int8.complement
  135. complement
    1. UInt16.complement
  136. complement
    1. UInt32.complement
  137. complement
    1. UInt64.complement
  138. complement
    1. UInt8.complement
  139. complement
    1. USize.complement
  140. completions (Elan command)
  141. components
    1. System.FilePath.components
  142. concat
    1. BitVec.concat
  143. concat
    1. List.concat
  144. cond
  145. configuration
    1. of tactics
  146. congr (0) (1) (2)
  147. congr­Arg
  148. congr­Fun
  149. cons
    1. BitVec.cons
  150. const
    1. Function.const
  151. constructor (0) (1)
  152. contains
    1. Array.contains
  153. contains
    1. List.contains
  154. contains
    1. String.contains
  155. contains
    1. Substring.contains
  156. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  157. contradiction
  158. control
  159. control­At
  160. conv
  161. conv => ...
  162. conv' (0) (1)
  163. cos
    1. Float.cos
  164. cos
    1. Float32.cos
  165. cosh
    1. Float.cosh
  166. cosh
    1. Float32.cosh
  167. count
    1. Array.count
  168. count
    1. List.count
  169. count­P
    1. Array.count­P
  170. count­P
    1. List.count­P
  171. create­Dir
    1. IO.FS.create­Dir
  172. create­Dir­All
    1. IO.FS.create­Dir­All
  173. create­Temp­Dir
    1. IO.FS.create­Temp­Dir
  174. create­Temp­File
    1. IO.FS.create­Temp­File
  175. crlf­To­Lf
    1. String.crlf­To­Lf
  176. csup
    1. [anonymous] (class method)
  177. csup_spec
    1. [anonymous] (class method)
  178. cumulativity
  179. curr
    1. String.Iterator.curr
  180. current­Dir
    1. IO.current­Dir
  181. curry
    1. Function.curry
  182. custom­Eliminators
    1. tactic.custom­Eliminators
  183. 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­LE
  8. Decidable­LT
  9. Decidable­Pred
  10. Decidable­Rel
  11. Dir­Entry
    1. IO.FS.Dir­Entry
  12. Div
  13. Div.mk
    1. Instance constructor of Div
  14. Dvd
  15. Dvd.mk
    1. Instance constructor of Dvd
  16. data
    1. IO.FS.Stream.Buffer.data (structure field)
  17. data
    1. String.data (structure field)
  18. dbg­Trace­If­Shared
  19. dbg_trace
  20. dcond
    1. Bool.dcond
  21. dec­Eq
    1. BitVec.dec­Eq
  22. dec­Eq
    1. Bool.dec­Eq
  23. dec­Eq
    1. ISize.dec­Eq
  24. dec­Eq
    1. Int.dec­Eq
  25. dec­Eq
    1. Int16.dec­Eq
  26. dec­Eq
    1. Int32.dec­Eq
  27. dec­Eq
    1. Int64.dec­Eq
  28. dec­Eq
    1. Int8.dec­Eq
  29. dec­Eq
    1. Nat.dec­Eq
  30. dec­Eq
    1. String.dec­Eq
  31. dec­Eq
    1. UInt16.dec­Eq
  32. dec­Eq
    1. UInt32.dec­Eq
  33. dec­Eq
    1. UInt64.dec­Eq
  34. dec­Eq
    1. UInt8.dec­Eq
  35. dec­Eq
    1. USize.dec­Eq
  36. dec­Le
    1. Float.dec­Le
  37. dec­Le
    1. Float32.dec­Le
  38. dec­Le
    1. ISize.dec­Le
  39. dec­Le
    1. Int16.dec­Le
  40. dec­Le
    1. Int32.dec­Le
  41. dec­Le
    1. Int64.dec­Le
  42. dec­Le
    1. Int8.dec­Le
  43. dec­Le
    1. Nat.dec­Le
  44. dec­Le
    1. UInt16.dec­Le
  45. dec­Le
    1. UInt32.dec­Le
  46. dec­Le
    1. UInt64.dec­Le
  47. dec­Le
    1. UInt8.dec­Le
  48. dec­Le
    1. USize.dec­Le
  49. dec­Lt
    1. Float.dec­Lt
  50. dec­Lt
    1. Float32.dec­Lt
  51. dec­Lt
    1. ISize.dec­Lt
  52. dec­Lt
    1. Int16.dec­Lt
  53. dec­Lt
    1. Int32.dec­Lt
  54. dec­Lt
    1. Int64.dec­Lt
  55. dec­Lt
    1. Int8.dec­Lt
  56. dec­Lt
    1. Nat.dec­Lt
  57. dec­Lt
    1. UInt16.dec­Lt
  58. dec­Lt
    1. UInt32.dec­Lt
  59. dec­Lt
    1. UInt64.dec­Lt
  60. dec­Lt
    1. UInt8.dec­Lt
  61. dec­Lt
    1. USize.dec­Lt
  62. decapitalize
    1. String.decapitalize
  63. decidable
  64. decidable­Eq­None
    1. Option.decidable­Eq­None
  65. decide
  66. decide
    1. Decidable.decide
  67. decide
    1. Lean.Meta.DSimp.Config.decide (structure field)
  68. decide
    1. Lean.Meta.Simp.Config.decide (structure field)
  69. decreasing_tactic
  70. decreasing_trivial
  71. decreasing_with
  72. dedicated
    1. Task.Priority.dedicated
  73. deep­Terms
    1. pp.deep­Terms
  74. default (Elan command)
  75. default
    1. Inhabited.default (class method)
  76. default
    1. Task.Priority.default
  77. default­Facets
    1. [anonymous] (structure field)
  78. delta (0) (1)
  79. diff
    1. guard_msgs.diff
  80. digit­Char
    1. Nat.digit­Char
  81. discard
    1. Functor.discard
  82. discharge
    1. trace.Meta.Tactic.simp.discharge
  83. div
    1. Div.div (class method)
  84. div
    1. Fin.div
  85. div
    1. Float.div
  86. div
    1. Float32.div
  87. div
    1. ISize.div
  88. div
    1. Int16.div
  89. div
    1. Int32.div
  90. div
    1. Int64.div
  91. div
    1. Int8.div
  92. div
    1. Nat.div
  93. div
    1. UInt16.div
  94. div
    1. UInt32.div
  95. div
    1. UInt64.div
  96. div
    1. UInt8.div
  97. div
    1. USize.div
  98. div2Induction
    1. Nat.div2Induction
  99. div­Rec
    1. BitVec.div­Rec
  100. div­Subtract­Shift
    1. BitVec.div­Subtract­Shift
  101. done (0) (1)
  102. down
    1. PLift.down (structure field)
  103. down
    1. ULift.down (structure field)
  104. drop
    1. Array.drop
  105. drop
    1. List.drop
  106. drop
    1. String.drop
  107. drop
    1. Subarray.drop
  108. drop
    1. Substring.drop
  109. drop­Last
    1. List.drop­Last
  110. drop­Last­TR
    1. List.drop­Last­TR
  111. drop­Prefix?
    1. String.drop­Prefix?
  112. drop­Prefix?
    1. Substring.drop­Prefix?
  113. drop­Right
    1. String.drop­Right
  114. drop­Right
    1. Substring.drop­Right
  115. drop­Right­While
    1. String.drop­Right­While
  116. drop­Right­While
    1. Substring.drop­Right­While
  117. drop­Suffix?
    1. String.drop­Suffix?
  118. drop­Suffix?
    1. Substring.drop­Suffix?
  119. drop­While
    1. List.drop­While
  120. drop­While
    1. String.drop­While
  121. drop­While
    1. Substring.drop­While
  122. dsimp (0) (1)
  123. dsimp!
  124. dsimp
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  125. dsimp?
  126. dsimp?!
  127. dvd
    1. Dvd.dvd (class method)

E

  1. EIO
  2. EIO.as­Task
  3. EIO.bind­Task
  4. EIO.catch­Exceptions
  5. EIO.chain­Task
  6. EIO.map­Task
  7. EIO.map­Tasks
  8. EIO.to­Base­IO
  9. EIO.to­IO
  10. EIO.to­IO'
  11. ELAN (environment variable)
  12. ELAN_HOME (environment variable) (0) (1)
  13. EST
  14. EState­M
  15. EStateM.Backtrackable
  16. EStateM.Backtrackable.mk
    1. Instance constructor of EStateM.Backtrackable
  17. EStateM.Result
  18. EStateM.Result.error
    1. Constructor of EStateM.Result
  19. EStateM.Result.ok
    1. Constructor of EStateM.Result
  20. EStateM.adapt­Except
  21. EStateM.bind
  22. EStateM.from­State­M
  23. EStateM.get
  24. EStateM.map
  25. EStateM.modify­Get
  26. EStateM.non­Backtrackable
  27. EStateM.or­Else
  28. EStateM.or­Else'
  29. EStateM.pure
  30. EStateM.run
  31. EStateM.run'
  32. EStateM.seq­Right
  33. EStateM.set
  34. EStateM.throw
  35. EStateM.try­Catch
  36. Empty
  37. Empty.elim
  38. Eq
  39. Eq.mp
  40. Eq.mpr
  41. Eq.refl
    1. Constructor of Eq
  42. Eq.subst
  43. Eq.symm
  44. Eq.trans
  45. Equiv
    1. HasEquiv.Equiv (class method)
  46. Equivalence
  47. Equivalence.mk
    1. Constructor of Equivalence
  48. Error
    1. IO.Error
  49. Even
  50. Even.plus­Two
    1. Constructor of Even
  51. Even.zero
    1. Constructor of Even
  52. Except
  53. Except.bind
  54. Except.error
    1. Constructor of Except
  55. Except.is­Ok
  56. Except.map
  57. Except.map­Error
  58. Except.ok
    1. Constructor of Except
  59. Except.or­Else­Lazy
  60. Except.pure
  61. Except.to­Bool
  62. Except.to­Option
  63. Except.try­Catch
  64. Except­Cps­T
  65. Except­CpsT.lift
  66. Except­CpsT.run
  67. Except­CpsT.run­Catch
  68. Except­CpsT.run­K
  69. Except­T
  70. ExceptT.adapt
  71. ExceptT.bind
  72. ExceptT.bind­Cont
  73. ExceptT.lift
  74. ExceptT.map
  75. ExceptT.mk
  76. ExceptT.pure
  77. ExceptT.run
  78. ExceptT.try­Catch
  79. Exists
  80. Exists.choose
  81. Exists.intro
    1. Constructor of Exists
  82. ediv
    1. Int.ediv
  83. elem
    1. Array.elem
  84. elem
    1. List.elem
  85. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  86. elim
    1. And.elim
  87. elim
    1. Empty.elim
  88. elim
    1. False.elim
  89. elim
    1. HEq.elim
  90. elim
    1. Iff.elim
  91. elim
    1. Not.elim
  92. elim
    1. Option.elim
  93. elim
    1. PEmpty.elim
  94. elim
    1. Subsingleton.elim
  95. elim
    1. Sum.elim
  96. elim0
    1. Fin.elim0
  97. elim­M
    1. Option.elim­M
  98. emod
    1. Int.emod
  99. empty
    1. Array.empty
  100. empty
    1. Subarray.empty
  101. empty­With­Capacity
    1. Array.empty­With­Capacity
  102. end­Pos
    1. String.end­Pos
  103. ends­With
    1. String.ends­With
  104. enter
  105. env (Lake command)
  106. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  107. environment variables
  108. eprint
    1. IO.eprint
  109. eprintln
    1. IO.eprintln
  110. eq­Rec_heq
  111. eq_of_beq
    1. [anonymous] (class method)
  112. eq_of_heq
  113. eq_refl
  114. erase
    1. Array.erase
  115. erase
    1. List.erase
  116. erase­Dups
    1. List.erase­Dups
  117. erase­Idx!
    1. Array.erase­Idx!
  118. erase­Idx
    1. Array.erase­Idx
  119. erase­Idx
    1. List.erase­Idx
  120. erase­Idx­If­In­Bounds
    1. Array.erase­Idx­If­In­Bounds
  121. erase­Idx­TR
    1. List.erase­Idx­TR
  122. erase­P
    1. Array.erase­P
  123. erase­P
    1. List.erase­P
  124. erase­PTR
    1. List.erase­PTR
  125. erase­Reps
    1. Array.erase­Reps
  126. erase­Reps
    1. List.erase­Reps
  127. erase­TR
    1. List.erase­TR
  128. erw (0) (1)
  129. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
  130. eta
    1. Lean.Meta.Simp.Config.eta (structure field)
  131. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
  132. eta­Struct
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  133. eval.derive.repr
  134. eval.pp
  135. eval.type
  136. exact
  137. exact
    1. Quotient.exact
  138. exact?
  139. exact_mod_cast
  140. exe (Lake command)
  141. exe­Extension
    1. System.FilePath.exe­Extension
  142. exe­Name
    1. [anonymous] (structure field)
  143. execution
    1. IO.AccessRight.execution (structure field)
  144. exfalso
  145. exists
  146. exit
    1. IO.Process.exit
  147. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  148. exp
    1. Float.exp
  149. exp
    1. Float32.exp
  150. exp2
    1. Float.exp2
  151. exp2
    1. Float32.exp2
  152. expand­Macro?
    1. Lean.Macro.expand­Macro?
  153. expose_names
  154. ext (0) (1)
  155. ext1
  156. ext­Separator
    1. System.FilePath.ext­Separator
  157. extension
    1. System.FilePath.extension
  158. extensionality
    1. of propositions
  159. extra­Dep­Targets
    1. [anonymous] (structure field) (0) (1)
  160. extract
    1. Array.extract
  161. extract
    1. List.extract
  162. extract
    1. String.Iterator.extract
  163. extract
    1. String.extract
  164. extract
    1. Substring.extract
  165. extract­Lsb'
    1. BitVec.extract­Lsb'
  166. 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.h­Iterate
  22. Fin.h­Iterate­From
  23. Fin.induction
  24. Fin.induction­On
  25. Fin.land
  26. Fin.last
  27. Fin.last­Cases
  28. Fin.log2
  29. Fin.lor
  30. Fin.mk
    1. Constructor of Fin
  31. Fin.mod
  32. Fin.modn
  33. Fin.mul
  34. Fin.nat­Add
  35. Fin.of­Nat'
  36. Fin.pred
  37. Fin.rev
  38. Fin.reverse­Induction
  39. Fin.shift­Left
  40. Fin.shift­Right
  41. Fin.sub
  42. Fin.sub­Nat
  43. Fin.succ
  44. Fin.succ­Rec
  45. Fin.succ­Rec­On
  46. Fin.to­Nat
  47. Fin.xor
  48. Float
  49. Float.abs
  50. Float.acos
  51. Float.acosh
  52. Float.add
  53. Float.asin
  54. Float.asinh
  55. Float.atan
  56. Float.atan2
  57. Float.atanh
  58. Float.beq
  59. Float.cbrt
  60. Float.ceil
  61. Float.cos
  62. Float.cosh
  63. Float.dec­Le
  64. Float.dec­Lt
  65. Float.div
  66. Float.exp
  67. Float.exp2
  68. Float.floor
  69. Float.fr­Exp
  70. Float.is­Finite
  71. Float.is­Inf
  72. Float.is­Na­N
  73. Float.le
  74. Float.log
  75. Float.log10
  76. Float.log2
  77. Float.lt
  78. Float.mul
  79. Float.neg
  80. Float.of­Binary­Scientific
  81. Float.of­Bits
  82. Float.of­Int
  83. Float.of­Nat
  84. Float.of­Scientific
  85. Float.pow
  86. Float.round
  87. Float.scale­B
  88. Float.sin
  89. Float.sinh
  90. Float.sqrt
  91. Float.sub
  92. Float.tan
  93. Float.tanh
  94. Float.to­Bits
  95. Float.to­Float32
  96. Float.to­ISize
  97. Float.to­Int16
  98. Float.to­Int32
  99. Float.to­Int64
  100. Float.to­Int8
  101. Float.to­String
  102. Float.to­UInt16
  103. Float.to­UInt32
  104. Float.to­UInt64
  105. Float.to­UInt8
  106. Float.to­USize
  107. Float32
  108. Float32.abs
  109. Float32.acos
  110. Float32.acosh
  111. Float32.add
  112. Float32.asin
  113. Float32.asinh
  114. Float32.atan
  115. Float32.atan2
  116. Float32.atanh
  117. Float32.beq
  118. Float32.cbrt
  119. Float32.ceil
  120. Float32.cos
  121. Float32.cosh
  122. Float32.dec­Le
  123. Float32.dec­Lt
  124. Float32.div
  125. Float32.exp
  126. Float32.exp2
  127. Float32.floor
  128. Float32.fr­Exp
  129. Float32.is­Finite
  130. Float32.is­Inf
  131. Float32.is­Na­N
  132. Float32.le
  133. Float32.log
  134. Float32.log10
  135. Float32.log2
  136. Float32.lt
  137. Float32.mul
  138. Float32.neg
  139. Float32.of­Binary­Scientific
  140. Float32.of­Bits
  141. Float32.of­Int
  142. Float32.of­Nat
  143. Float32.of­Scientific
  144. Float32.pow
  145. Float32.round
  146. Float32.scale­B
  147. Float32.sin
  148. Float32.sinh
  149. Float32.sqrt
  150. Float32.sub
  151. Float32.tan
  152. Float32.tanh
  153. Float32.to­Bits
  154. Float32.to­Float
  155. Float32.to­ISize
  156. Float32.to­Int16
  157. Float32.to­Int32
  158. Float32.to­Int64
  159. Float32.to­Int8
  160. Float32.to­String
  161. Float32.to­UInt16
  162. Float32.to­UInt32
  163. Float32.to­UInt64
  164. Float32.to­UInt8
  165. Float32.to­USize
  166. For­In
  167. For­In'
  168. ForIn'.mk
    1. Instance constructor of For­In'
  169. ForIn.mk
    1. Instance constructor of For­In
  170. For­In­Step
  171. For­InStep.done
    1. Constructor of For­In­Step
  172. For­InStep.value
  173. For­InStep.yield
    1. Constructor of For­In­Step
  174. For­M
  175. ForM.for­In
  176. ForM.mk
    1. Instance constructor of For­M
  177. Function.comp
  178. Function.const
  179. Function.curry
  180. Function.uncurry
  181. Functor
  182. Functor.discard
  183. Functor.map­Rev
  184. Functor.mk
    1. Instance constructor of Functor
  185. fail
  186. fail
    1. OptionT.fail
  187. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
  188. fail­If­Unchanged
    1. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  189. fail_if_success (0) (1)
  190. failure
    1. ReaderT.failure
  191. failure
    1. StateT.failure
  192. failure
    1. [anonymous] (class method)
  193. false_or_by_contra
  194. fdiv
    1. Int.fdiv
  195. field­Idx­Kind
    1. Lean.field­Idx­Kind
  196. field­Notation
    1. pp.field­Notation
  197. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
  198. file­Name
    1. System.FilePath.file­Name
  199. file­Stem
    1. System.FilePath.file­Stem
  200. fill
    1. BitVec.fill
  201. filter
    1. Array.filter
  202. filter
    1. List.filter
  203. filter
    1. Option.filter
  204. filter­M
    1. Array.filter­M
  205. filter­M
    1. List.filter­M
  206. filter­Map
    1. Array.filter­Map
  207. filter­Map
    1. List.filter­Map
  208. filter­Map­M
    1. Array.filter­Map­M
  209. filter­Map­M
    1. List.filter­Map­M
  210. filter­Map­TR
    1. List.filter­Map­TR
  211. filter­Rev­M
    1. Array.filter­Rev­M
  212. filter­Rev­M
    1. List.filter­Rev­M
  213. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  214. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  215. filter­TR
    1. List.filter­TR
  216. fin­Idx­Of?
    1. Array.fin­Idx­Of?
  217. fin­Idx­Of?
    1. List.fin­Idx­Of?
  218. fin­Range
    1. Array.fin­Range
  219. fin­Range
    1. List.fin­Range
  220. find
    1. String.find
  221. find?
    1. Array.find?
  222. find?
    1. List.find?
  223. find­Extern­Lib?
    1. Lake.find­Extern­Lib?
  224. find­Fin­Idx?
    1. Array.find­Fin­Idx?
  225. find­Fin­Idx?
    1. List.find­Fin­Idx?
  226. find­Idx
    1. Array.find­Idx
  227. find­Idx
    1. List.find­Idx
  228. find­Idx?
    1. Array.find­Idx?
  229. find­Idx?
    1. List.find­Idx?
  230. find­Idx­M?
    1. Array.find­Idx­M?
  231. find­Lean­Exe?
    1. Lake.find­Lean­Exe?
  232. find­Lean­Lib?
    1. Lake.find­Lean­Lib?
  233. find­Line­Start
    1. String.find­Line­Start
  234. find­M?
    1. Array.find­M?
  235. find­M?
    1. List.find­M?
  236. find­Module?
    1. Lake.find­Module?
  237. find­Package?
    1. Lake.find­Package?
  238. find­Rev?
    1. Array.find­Rev?
  239. find­Rev?
    1. Subarray.find­Rev?
  240. find­Rev­M?
    1. Array.find­Rev­M?
  241. find­Rev­M?
    1. Subarray.find­Rev­M?
  242. find­Some!
    1. Array.find­Some!
  243. find­Some?
    1. Array.find­Some?
  244. find­Some?
    1. List.find­Some?
  245. find­Some­M?
    1. Array.find­Some­M?
  246. find­Some­M?
    1. List.find­Some­M?
  247. find­Some­Rev?
    1. Array.find­Some­Rev?
  248. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
  249. find­Some­Rev­M?
    1. Subarray.find­Some­Rev­M?
  250. first (0) (1)
  251. first­Diff­Pos
    1. String.first­Diff­Pos
  252. first­M
    1. Array.first­M
  253. first­M
    1. List.first­M
  254. fix
    1. Lean.Order.fix
  255. fix
    1. WellFounded.fix
  256. fix_eq
    1. Lean.Order.fix_eq
  257. flags
    1. IO.AccessRight.flags
  258. flags
    1. IO.FileRight.flags
  259. flat­Map
    1. Array.flat­Map
  260. flat­Map
    1. List.flat­Map
  261. flat­Map­M
    1. Array.flat­Map­M
  262. flat­Map­M
    1. List.flat­Map­M
  263. flat­Map­TR
    1. List.flat­Map­TR
  264. flatten
    1. Array.flatten
  265. flatten
    1. List.flatten
  266. flatten­TR
    1. List.flatten­TR
  267. floor
    1. Float.floor
  268. floor
    1. Float32.floor
  269. flush
    1. IO.FS.Handle.flush
  270. flush
    1. IO.FS.Stream.flush (structure field)
  271. fmod
    1. Int.fmod
  272. focus (0) (1)
  273. fold
    1. Nat.fold
  274. fold­I
    1. Prod.fold­I
  275. fold­M
    1. Nat.fold­M
  276. fold­Rev
    1. Nat.fold­Rev
  277. fold­Rev­M
    1. Nat.fold­Rev­M
  278. fold­TR
    1. Nat.fold­TR
  279. foldl
    1. Array.foldl
  280. foldl
    1. Fin.foldl
  281. foldl
    1. List.foldl
  282. foldl
    1. String.foldl
  283. foldl
    1. Subarray.foldl
  284. foldl
    1. Substring.foldl
  285. foldl­M
    1. Array.foldl­M
  286. foldl­M
    1. Fin.foldl­M
  287. foldl­M
    1. List.foldl­M
  288. foldl­M
    1. Subarray.foldl­M
  289. foldl­Rec­On
    1. List.foldl­Rec­On
  290. foldr
    1. Array.foldr
  291. foldr
    1. Fin.foldr
  292. foldr
    1. List.foldr
  293. foldr
    1. String.foldr
  294. foldr
    1. Subarray.foldr
  295. foldr
    1. Substring.foldr
  296. foldr­M
    1. Array.foldr­M
  297. foldr­M
    1. Fin.foldr­M
  298. foldr­M
    1. List.foldr­M
  299. foldr­M
    1. Subarray.foldr­M
  300. foldr­Rec­On
    1. List.foldr­Rec­On
  301. foldr­TR
    1. List.foldr­TR
  302. for­A
    1. List.for­A
  303. for­Async
    1. Std.Channel.for­Async
  304. for­In'
    1. ForIn'.for­In' (class method)
  305. for­In
    1. ForIn.for­In (class method)
  306. for­In
    1. ForM.for­In
  307. for­In
    1. Subarray.for­In
  308. for­M
    1. Array.for­M
  309. for­M
    1. ForM.for­M (class method)
  310. for­M
    1. List.for­M
  311. for­M
    1. Nat.for­M
  312. for­M
    1. Option.for­M
  313. for­M
    1. Subarray.for­M
  314. for­Rev­M
    1. Array.for­Rev­M
  315. for­Rev­M
    1. Nat.for­Rev­M
  316. for­Rev­M
    1. Subarray.for­Rev­M
  317. format
    1. Option.format
  318. forward
    1. String.Iterator.forward
  319. fr­Exp
    1. Float.fr­Exp
  320. fr­Exp
    1. Float32.fr­Exp
  321. from­State­M
    1. EStateM.from­State­M
  322. from­UTF8!
    1. String.from­UTF8!
  323. from­UTF8
    1. String.from­UTF8
  324. from­UTF8?
    1. String.from­UTF8?
  325. front
    1. String.front
  326. front
    1. Substring.front
  327. fst
    1. MProd.fst (structure field)
  328. fst
    1. PProd.fst (structure field)
  329. fst
    1. PSigma.fst (structure field)
  330. fst
    1. Prod.fst (structure field)
  331. fst
    1. Sigma.fst (structure field)
  332. fun
  333. fun_cases
  334. fun_induction
  335. 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
  7. gcd
    1. Nat.gcd
  8. generalize
  9. get!
    1. Option.get!
  10. get!
    1. String.get!
  11. get!
    1. Subarray.get!
  12. get'
    1. String.get'
  13. get
    1. EStateM.get
  14. get
    1. List.get
  15. get
    1. MonadState.get
  16. get
    1. MonadState.get (class method)
  17. get
    1. Monad­StateOf.get (class method)
  18. get
    1. Option.get
  19. get
    1. ST.Ref.get
  20. get
    1. State­RefT'.get
  21. get
    1. StateT.get
  22. get
    1. String.get
  23. get
    1. Subarray.get
  24. get
    1. Substring.get
  25. get
    1. Task.get
  26. get
    1. Thunk.get
  27. get?
    1. String.get?
  28. get­Augmented­Env
    1. Lake.get­Augmented­Env
  29. get­Augmented­Lean­Path
    1. Lake.get­Augmented­Lean­Path
  30. get­Augmented­Lean­Src­Path
    1. Lake.get­Augmented­Lean­Src­Path
  31. get­Augmented­Shared­Lib­Path
    1. Lake.get­Augmented­Shared­Lib­Path
  32. get­Char
    1. Lean.TSyntax.get­Char
  33. get­Curr­Namespace
    1. Lean.Macro.get­Curr­Namespace
  34. get­Current­Dir
    1. IO.Process.get­Current­Dir
  35. get­D
    1. Array.get­D
  36. get­D
    1. List.get­D
  37. get­D
    1. Option.get­D
  38. get­D
    1. Subarray.get­D
  39. get­DM
    1. Option.get­DM
  40. get­Elan?
    1. Lake.get­Elan?
  41. get­Elan­Home?
    1. Lake.get­Elan­Home?
  42. get­Elan­Install?
    1. Lake.get­Elan­Install?
  43. get­Elan­Toolchain
    1. Lake.get­Elan­Toolchain
  44. get­Elem!
    1. GetElem?.get­Elem? (class method)
  45. get­Elem!_def
    1. Lawful­GetElem.get­Elem!_def (class method)
  46. get­Elem
    1. GetElem.get­Elem (class method)
  47. get­Elem?
    1. [anonymous] (class method)
  48. get­Elem?_def
    1. Lawful­GetElem.get­Elem?_def (class method)
  49. get­Env
    1. IO.get­Env
  50. get­Env­Lean­Path
    1. Lake.get­Env­Lean­Path
  51. get­Env­Lean­Src­Path
    1. Lake.get­Env­Lean­Src­Path
  52. get­Env­Shared­Lib­Path
    1. Lake.get­Env­Shared­Lib­Path
  53. get­Even­Elems
    1. Array.get­Even­Elems
  54. get­Hygiene­Info
    1. Lean.TSyntax.get­Hygiene­Info
  55. get­Id
    1. Lean.TSyntax.get­Id
  56. get­Kind
    1. Lean.Syntax.get­Kind
  57. get­Lake
    1. Lake.get­Lake
  58. get­Lake­Env
    1. Lake.get­Lake­Env
  59. get­Lake­Home
    1. Lake.get­Lake­Home
  60. get­Lake­Install
    1. Lake.get­Lake­Install
  61. get­Lake­Lib­Dir
    1. Lake.get­Lake­Lib­Dir
  62. get­Lake­Src­Dir
    1. Lake.get­Lake­Src­Dir
  63. get­Last!
    1. List.get­Last!
  64. get­Last
    1. List.get­Last
  65. get­Last?
    1. List.get­Last?
  66. get­Last­D
    1. List.get­Last­D
  67. get­Lean
    1. Lake.get­Lean
  68. get­Lean­Ar
    1. Lake.get­Lean­Ar
  69. get­Lean­Cc
    1. Lake.get­Lean­Cc
  70. get­Lean­Cc?
    1. Lake.get­Lean­Cc?
  71. get­Lean­Include­Dir
    1. Lake.get­Lean­Include­Dir
  72. get­Lean­Install
    1. Lake.get­Lean­Install
  73. get­Lean­Lib­Dir
    1. Lake.get­Lean­Lib­Dir
  74. get­Lean­Path
    1. Lake.get­Lean­Path
  75. get­Lean­Shared­Lib
    1. Lake.get­Lean­Shared­Lib
  76. get­Lean­Src­Dir
    1. Lake.get­Lean­Src­Dir
  77. get­Lean­Src­Path
    1. Lake.get­Lean­Src­Path
  78. get­Lean­Sysroot
    1. Lake.get­Lean­Sysroot
  79. get­Lean­System­Lib­Dir
    1. Lake.get­Lean­System­Lib­Dir
  80. get­Leanc
    1. Lake.get­Leanc
  81. get­Left
    1. Sum.get­Left
  82. get­Left?
    1. Sum.get­Left?
  83. get­Line
    1. IO.FS.Handle.get­Line
  84. get­Line
    1. IO.FS.Stream.get­Line (structure field)
  85. get­Lsb'
    1. BitVec.get­Lsb'
  86. get­Lsb?
    1. BitVec.get­Lsb?
  87. get­Lsb­D
    1. BitVec.get­Lsb­D
  88. get­M
    1. Option.get­M
  89. get­Max?
    1. Array.get­Max?
  90. get­Modify
  91. get­Msb'
    1. BitVec.get­Msb'
  92. get­Msb?
    1. BitVec.get­Msb?
  93. get­Msb­D
    1. BitVec.get­Msb­D
  94. get­Name
    1. Lean.TSyntax.get­Name
  95. get­Nat
    1. Lean.TSyntax.get­Nat
  96. get­No­Cache
    1. Lake.get­No­Cache
  97. get­Num­Heartbeats
    1. IO.get­Num­Heartbeats
  98. get­PID
    1. IO.Process.get­PID
  99. get­Pkg­Url­Map
    1. Lake.get­Pkg­Url­Map
  100. get­Random­Bytes
    1. IO.get­Random­Bytes
  101. get­Right
    1. Sum.get­Right
  102. get­Right?
    1. Sum.get­Right?
  103. get­Root­Package
    1. Lake.get­Root­Package
  104. get­Scientific
    1. Lean.TSyntax.get­Scientific
  105. get­Shared­Lib­Path
    1. Lake.get­Shared­Lib­Path
  106. get­Stderr
    1. IO.get­Stderr
  107. get­Stdin
    1. IO.get­Stdin
  108. get­Stdout
    1. IO.get­Stdout
  109. get­String
    1. Lean.TSyntax.get­String
  110. get­TID
    1. IO.get­TID
  111. get­Task­State
    1. IO.get­Task­State
  112. get­The
  113. get­Try­Cache
    1. Lake.get­Try­Cache
  114. get­Utf8Byte
    1. String.get­Utf8Byte
  115. get­Workspace
    1. Lake.MonadWorkspace.get­Workspace (class method)
  116. get_elem_tactic
  117. get_elem_tactic_trivial
  118. globs
    1. [anonymous] (structure field)
  119. goal
    1. main
  120. ground
    1. Lean.Meta.Simp.Config.ground (structure field)
  121. group
    1. IO.FileRight.group (structure field)
  122. group­By­Key
    1. Array.group­By­Key
  123. group­By­Key
    1. List.group­By­Key
  124. group­Kind
    1. Lean.group­Kind
  125. guard
  126. guard
    1. Option.guard
  127. guard_expr
  128. guard_hyp
  129. guard_msgs.diff
  130. 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­Add
    1. HAdd.h­Add (class method)
  41. h­And
    1. HAnd.h­And (class method)
  42. h­Append
    1. HAppend.h­Append (class method)
  43. h­Div
    1. HDiv.h­Div (class method)
  44. h­Iterate
    1. Fin.h­Iterate
  45. h­Iterate­From
    1. Fin.h­Iterate­From
  46. h­Mod
    1. HMod.h­Mod (class method)
  47. h­Mul
    1. HMul.h­Mul (class method)
  48. h­Or
    1. HOr.h­Or (class method)
  49. h­Pow
    1. HPow.h­Pow (class method)
  50. h­Shift­Left
    1. HShiftLeft.h­Shift­Left (class method)
  51. h­Shift­Right
    1. HShiftRight.h­Shift­Right (class method)
  52. h­Sub
    1. HSub.h­Sub (class method)
  53. h­Xor
    1. HXor.h­Xor (class method)
  54. has­Decl
    1. Lean.Macro.has­Decl
  55. has­Finished
    1. IO.has­Finished
  56. has­Next
    1. String.Iterator.has­Next
  57. has­Prev
    1. String.Iterator.has­Prev
  58. hash
    1. BitVec.hash
  59. hash
    1. Hashable.hash (class method)
  60. hash
    1. String.hash
  61. hash_eq
  62. hash_eq
    1. LawfulHashable.hash_eq (class method)
  63. have
  64. have'
  65. have­I
  66. head!
    1. List.head!
  67. head
    1. List.head
  68. head?
    1. List.head?
  69. head­D
    1. List.head­D
  70. helim
    1. Subsingleton.helim
  71. heq_of_eq
  72. heq_of_eq­Rec_eq
  73. heq_of_heq_of_eq
  74. hrec­On
    1. Quot.hrec­On
  75. hrec­On
    1. Quotient.hrec­On
  76. hygiene
    1. in tactics
  77. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  78. hygienic
    1. tactic.hygienic

I

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

J

  1. join
    1. Option.join
  2. join
    1. String.join
  3. join
    1. 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_NUM_THREADS (environment variable)
  11. LEAN_SYSROOT (environment variable)
  12. LT
  13. LT.mk
    1. Instance constructor of LT
  14. Lake.Backend
  15. Lake.Backend.c
    1. Constructor of Lake.Backend
  16. Lake.Backend.default
    1. Constructor of Lake.Backend
  17. Lake.Backend.llvm
    1. Constructor of Lake.Backend
  18. Lake.Build­Type
  19. Lake.BuildType.debug
    1. Constructor of Lake.Build­Type
  20. Lake.BuildType.min­Size­Rel
    1. Constructor of Lake.Build­Type
  21. Lake.BuildType.rel­With­Deb­Info
    1. Constructor of Lake.Build­Type
  22. Lake.BuildType.release
    1. Constructor of Lake.Build­Type
  23. Lake.Glob
  24. Lake.Glob.and­Submodules
    1. Constructor of Lake.Glob
  25. Lake.Glob.one
    1. Constructor of Lake.Glob
  26. Lake.Glob.submodules
    1. Constructor of Lake.Glob
  27. Lake.Lean­Exe­Config
  28. Lake.Lean­ExeConfig.mk
    1. Constructor of Lake.Lean­Exe­Config
  29. Lake.Lean­Lib­Config
  30. Lake.Lean­LibConfig.mk
    1. Constructor of Lake.Lean­Lib­Config
  31. Lake.Lean­Option
  32. Lake.LeanOption.mk
    1. Constructor of Lake.Lean­Option
  33. Lake.Monad­Lake­Env
  34. Lake.Monad­Workspace
  35. Lake.MonadWorkspace.mk
    1. Instance constructor of Lake.Monad­Workspace
  36. Lake.Script­M (0) (1)
  37. Lake.find­Extern­Lib?
  38. Lake.find­Lean­Exe?
  39. Lake.find­Lean­Lib?
  40. Lake.find­Module?
  41. Lake.find­Package?
  42. Lake.get­Augmented­Env
  43. Lake.get­Augmented­Lean­Path
  44. Lake.get­Augmented­Lean­Src­Path
  45. Lake.get­Augmented­Shared­Lib­Path
  46. Lake.get­Elan?
  47. Lake.get­Elan­Home?
  48. Lake.get­Elan­Install?
  49. Lake.get­Elan­Toolchain
  50. Lake.get­Env­Lean­Path
  51. Lake.get­Env­Lean­Src­Path
  52. Lake.get­Env­Shared­Lib­Path
  53. Lake.get­Lake
  54. Lake.get­Lake­Env
  55. Lake.get­Lake­Home
  56. Lake.get­Lake­Install
  57. Lake.get­Lake­Lib­Dir
  58. Lake.get­Lake­Src­Dir
  59. Lake.get­Lean
  60. Lake.get­Lean­Ar
  61. Lake.get­Lean­Cc
  62. Lake.get­Lean­Cc?
  63. Lake.get­Lean­Include­Dir
  64. Lake.get­Lean­Install
  65. Lake.get­Lean­Lib­Dir
  66. Lake.get­Lean­Path
  67. Lake.get­Lean­Shared­Lib
  68. Lake.get­Lean­Src­Dir
  69. Lake.get­Lean­Src­Path
  70. Lake.get­Lean­Sysroot
  71. Lake.get­Lean­System­Lib­Dir
  72. Lake.get­Leanc
  73. Lake.get­No­Cache
  74. Lake.get­Pkg­Url­Map
  75. Lake.get­Root­Package
  76. Lake.get­Shared­Lib­Path
  77. Lake.get­Try­Cache
  78. Lawful­Applicative
  79. LawfulApplicative.mk
    1. Instance constructor of Lawful­Applicative
  80. Lawful­BEq
  81. LawfulBEq.mk
    1. Instance constructor of Lawful­BEq
  82. Lawful­Functor
  83. LawfulFunctor.mk
    1. Instance constructor of Lawful­Functor
  84. Lawful­Get­Elem
  85. Lawful­GetElem.mk
    1. Instance constructor of Lawful­Get­Elem
  86. Lawful­Hashable
  87. LawfulHashable.mk
    1. Instance constructor of Lawful­Hashable
  88. Lawful­Monad
  89. LawfulMonad.mk'
  90. LawfulMonad.mk
    1. Instance constructor of Lawful­Monad
  91. Leading­Ident­Behavior
    1. Lean.Parser.Leading­Ident­Behavior
  92. Lean.Elab.register­Deriving­Handler
  93. Lean.Macro.Exception.unsupported­Syntax
  94. Lean.Macro.add­Macro­Scope
  95. Lean.Macro.expand­Macro?
  96. Lean.Macro.get­Curr­Namespace
  97. Lean.Macro.has­Decl
  98. Lean.Macro.resolve­Global­Name
  99. Lean.Macro.resolve­Namespace
  100. Lean.Macro.throw­Error
  101. Lean.Macro.throw­Error­At
  102. Lean.Macro.throw­Unsupported
  103. Lean.Macro.trace
  104. Lean.Macro.with­Fresh­Macro­Scope
  105. Lean.Macro­M
  106. Lean.Meta.DSimp.Config
  107. Lean.Meta.DSimp.Config.mk
    1. Constructor of Lean.Meta.DSimp.Config
  108. Lean.Meta.Occurrences
  109. Lean.Meta.Occurrences.all
    1. Constructor of Lean.Meta.Occurrences
  110. Lean.Meta.Occurrences.neg
    1. Constructor of Lean.Meta.Occurrences
  111. Lean.Meta.Occurrences.pos
    1. Constructor of Lean.Meta.Occurrences
  112. Lean.Meta.Rewrite.Config
  113. Lean.Meta.Rewrite.Config.mk
    1. Constructor of Lean.Meta.Rewrite.Config
  114. Lean.Meta.Rewrite.New­Goals
  115. Lean.Meta.Simp.Config
  116. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  117. Lean.Meta.Simp.neutral­Config
  118. Lean.Meta.Simp­Extension
  119. Lean.Meta.Transparency­Mode
  120. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.Transparency­Mode
  121. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.Transparency­Mode
  122. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.Transparency­Mode
  123. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.Transparency­Mode
  124. Lean.Meta.register­Simp­Attr
  125. Lean.Order.CCPO
  126. Lean.Order.CCPO.mk
    1. Instance constructor of Lean.Order.CCPO
  127. Lean.Order.Partial­Order
  128. Lean.Order.PartialOrder.mk
    1. Instance constructor of Lean.Order.Partial­Order
  129. Lean.Order.fix
  130. Lean.Order.fix_eq
  131. Lean.Order.monotone
  132. Lean.Parser.Leading­Ident­Behavior
  133. Lean.Parser.Leading­IdentBehavior.both
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  134. Lean.Parser.Leading­IdentBehavior.default
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  135. Lean.Parser.Leading­IdentBehavior.symbol
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  136. Lean.PrettyPrinter.Unexpand­M
  137. Lean.PrettyPrinter.Unexpander
  138. Lean.Source­Info
  139. Lean.SourceInfo.none
    1. Constructor of Lean.Source­Info
  140. Lean.SourceInfo.original
    1. Constructor of Lean.Source­Info
  141. Lean.SourceInfo.synthetic
    1. Constructor of Lean.Source­Info
  142. Lean.Syntax
  143. Lean.Syntax.Char­Lit
  144. Lean.Syntax.Command
  145. Lean.Syntax.Hygiene­Info
  146. Lean.Syntax.Ident
  147. Lean.Syntax.Level
  148. Lean.Syntax.Name­Lit
  149. Lean.Syntax.Num­Lit
  150. Lean.Syntax.Prec
  151. Lean.Syntax.Preresolved
  152. Lean.Syntax.Preresolved.decl
    1. Constructor of Lean.Syntax.Preresolved
  153. Lean.Syntax.Preresolved.namespace
    1. Constructor of Lean.Syntax.Preresolved
  154. Lean.Syntax.Prio
  155. Lean.Syntax.Scientific­Lit
  156. Lean.Syntax.Str­Lit
  157. Lean.Syntax.TSep­Array
  158. Lean.Syntax.TSepArray.mk
    1. Constructor of Lean.Syntax.TSep­Array
  159. Lean.Syntax.Tactic
  160. Lean.Syntax.Term
  161. Lean.Syntax.atom
    1. Constructor of Lean.Syntax
  162. Lean.Syntax.get­Kind
  163. Lean.Syntax.ident
    1. Constructor of Lean.Syntax
  164. Lean.Syntax.is­Of­Kind
  165. Lean.Syntax.missing
    1. Constructor of Lean.Syntax
  166. Lean.Syntax.node
    1. Constructor of Lean.Syntax
  167. Lean.Syntax.set­Kind
  168. Lean.Syntax­Node­Kind
  169. Lean.Syntax­Node­Kinds
  170. Lean.TSyntax
  171. Lean.TSyntax.get­Char
  172. Lean.TSyntax.get­Hygiene­Info
  173. Lean.TSyntax.get­Id
  174. Lean.TSyntax.get­Name
  175. Lean.TSyntax.get­Nat
  176. Lean.TSyntax.get­Scientific
  177. Lean.TSyntax.get­String
  178. Lean.TSyntax.mk
    1. Constructor of Lean.TSyntax
  179. Lean.TSyntax­Array
  180. Lean.char­Lit­Kind
  181. Lean.choice­Kind
  182. Lean.field­Idx­Kind
  183. Lean.group­Kind
  184. Lean.hygiene­Info­Kind
  185. Lean.ident­Kind
  186. Lean.interpolated­Str­Kind
  187. Lean.interpolated­Str­Lit­Kind
  188. Lean.name­Lit­Kind
  189. Lean.null­Kind
  190. Lean.num­Lit­Kind
  191. Lean.scientific­Lit­Kind
  192. Lean.str­Lit­Kind
  193. Lean­Exe­Config
    1. Lake.Lean­Exe­Config
  194. Lean­Lib­Config
    1. Lake.Lean­Lib­Config
  195. Lean­Option
    1. Lake.Lean­Option
  196. Level
    1. Lean.Syntax.Level
  197. Lex
    1. List.Lex
  198. List
  199. List.Is­Infix
  200. List.Is­Prefix
  201. List.Is­Suffix
  202. List.Lex
  203. List.Lex.cons
    1. Constructor of List.Lex
  204. List.Lex.nil
    1. Constructor of List.Lex
  205. List.Lex.rel
    1. Constructor of List.Lex
  206. List.Mem
  207. List.Mem.head
    1. Constructor of List.Mem
  208. List.Mem.tail
    1. Constructor of List.Mem
  209. List.Nodup
  210. List.Pairwise
  211. List.Pairwise.cons
    1. Constructor of List.Pairwise
  212. List.Pairwise.nil
    1. Constructor of List.Pairwise
  213. List.Perm
  214. List.Perm.cons
    1. Constructor of List.Perm
  215. List.Perm.nil
    1. Constructor of List.Perm
  216. List.Perm.swap
    1. Constructor of List.Perm
  217. List.Perm.trans
    1. Constructor of List.Perm
  218. List.Sublist
  219. List.Sublist.cons
    1. Constructor of List.Sublist
  220. List.Sublist.cons₂
    1. Constructor of List.Sublist
  221. List.Sublist.slnil
    1. Constructor of List.Sublist
  222. List.all
  223. List.all­M
  224. List.and
  225. List.any
  226. List.any­M
  227. List.append
  228. List.append­TR
  229. List.as­String
  230. List.attach
  231. List.attach­With
  232. List.beq
  233. List.concat
  234. List.cons
    1. Constructor of List
  235. List.contains
  236. List.count
  237. List.count­P
  238. List.drop
  239. List.drop­Last
  240. List.drop­Last­TR
  241. List.drop­While
  242. List.elem
  243. List.erase
  244. List.erase­Dups
  245. List.erase­Idx
  246. List.erase­Idx­TR
  247. List.erase­P
  248. List.erase­PTR
  249. List.erase­Reps
  250. List.erase­TR
  251. List.extract
  252. List.filter
  253. List.filter­M
  254. List.filter­Map
  255. List.filter­Map­M
  256. List.filter­Map­TR
  257. List.filter­Rev­M
  258. List.filter­TR
  259. List.fin­Idx­Of?
  260. List.fin­Range
  261. List.find?
  262. List.find­Fin­Idx?
  263. List.find­Idx
  264. List.find­Idx?
  265. List.find­M?
  266. List.find­Some?
  267. List.find­Some­M?
  268. List.first­M
  269. List.flat­Map
  270. List.flat­Map­M
  271. List.flat­Map­TR
  272. List.flatten
  273. List.flatten­TR
  274. List.foldl
  275. List.foldl­M
  276. List.foldl­Rec­On
  277. List.foldr
  278. List.foldr­M
  279. List.foldr­Rec­On
  280. List.foldr­TR
  281. List.for­A
  282. List.for­M
  283. List.get
  284. List.get­D
  285. List.get­Last
  286. List.get­Last!
  287. List.get­Last?
  288. List.get­Last­D
  289. List.group­By­Key
  290. List.head
  291. List.head!
  292. List.head?
  293. List.head­D
  294. List.idx­Of
  295. List.idx­Of?
  296. List.insert
  297. List.insert­Idx
  298. List.insert­Idx­TR
  299. List.intercalate
  300. List.intercalate­TR
  301. List.intersperse
  302. List.intersperse­TR
  303. List.is­Empty
  304. List.is­Eqv
  305. List.is­Perm
  306. List.is­Prefix­Of
  307. List.is­Prefix­Of?
  308. List.is­Sublist
  309. List.is­Suffix­Of
  310. List.is­Suffix­Of?
  311. List.le
  312. List.leftpad
  313. List.leftpad­TR
  314. List.length
  315. List.length­TR
  316. List.lex
  317. List.lookup
  318. List.lt
  319. List.map
  320. List.map­A
  321. List.map­Fin­Idx
  322. List.map­Fin­Idx­M
  323. List.map­Idx
  324. List.map­Idx­M
  325. List.map­M
  326. List.map­M'
  327. List.map­Mono
  328. List.map­Mono­M
  329. List.map­TR
  330. List.max?
  331. List.merge
  332. List.merge­Sort
  333. List.min?
  334. List.modify
  335. List.modify­Head
  336. List.modify­TR
  337. List.modify­Tail­Idx
  338. List.nil
    1. Constructor of List
  339. List.of­Fn
  340. List.or
  341. List.partition
  342. List.partition­M
  343. List.partition­Map
  344. List.pmap
  345. List.range
  346. List.range'
  347. List.range'TR
  348. List.remove­All
  349. List.replace
  350. List.replace­TR
  351. List.replicate
  352. List.replicate­TR
  353. List.reverse
  354. List.rightpad
  355. List.rotate­Left
  356. List.rotate­Right
  357. List.set
  358. List.set­TR
  359. List.singleton
  360. List.span
  361. List.split­At
  362. List.split­By
  363. List.sum
  364. List.tail
  365. List.tail!
  366. List.tail?
  367. List.tail­D
  368. List.take
  369. List.take­TR
  370. List.take­While
  371. List.take­While­TR
  372. List.to­Array
  373. List.to­Array­Impl
  374. List.to­Byte­Array
  375. List.to­Float­Array
  376. List.to­String
  377. List.unattach
  378. List.unzip
  379. List.unzip­TR
  380. List.zip
  381. List.zip­Idx
  382. List.zip­Idx­TR
  383. List.zip­With
  384. List.zip­With­All
  385. List.zip­With­TR
  386. land
    1. Fin.land
  387. land
    1. ISize.land
  388. land
    1. Int16.land
  389. land
    1. Int32.land
  390. land
    1. Int64.land
  391. land
    1. Int8.land
  392. land
    1. Nat.land
  393. land
    1. UInt16.land
  394. land
    1. UInt32.land
  395. land
    1. UInt64.land
  396. land
    1. UInt8.land
  397. land
    1. USize.land
  398. last
    1. Fin.last
  399. last­Cases
    1. Fin.last­Cases
  400. lazy­Pure
    1. IO.lazy­Pure
  401. lcm
    1. Int.lcm
  402. lcm
    1. Nat.lcm
  403. le
    1. Char.le
  404. le
    1. Float.le
  405. le
    1. Float32.le
  406. le
    1. ISize.le
  407. le
    1. Int.le
  408. le
    1. Int16.le
  409. le
    1. Int32.le
  410. le
    1. Int64.le
  411. le
    1. Int8.le
  412. le
    1. LE.le (class method)
  413. le
    1. List.le
  414. le
    1. Nat.le
  415. le
    1. String.le
  416. le
    1. UInt16.le
  417. le
    1. UInt32.le
  418. le
    1. UInt64.le
  419. le
    1. UInt8.le
  420. le
    1. USize.le
  421. le­Of­Ord
  422. lean (Lake command)
  423. lean_is_array
  424. lean_is_string
  425. lean_string_object (0) (1)
  426. lean_to_array
  427. lean_to_string
  428. left (0) (1)
  429. left
    1. And.left (structure field)
  430. leftpad
    1. Array.leftpad
  431. leftpad
    1. List.leftpad
  432. leftpad­TR
    1. List.leftpad­TR
  433. length
    1. List.length
  434. length
    1. String.length
  435. length­TR
    1. List.length­TR
  436. let
  437. let rec
  438. let'
  439. let­I
  440. level
    1. of universe
  441. lex'
    1. Ord.lex'
  442. lex
    1. Array.lex
  443. lex
    1. List.lex
  444. lex
    1. Ord.lex
  445. lex­Lt
    1. Prod.lex­Lt
  446. lhs
  447. lib­Name
    1. [anonymous] (structure field)
  448. lift
    1. Except­CpsT.lift
  449. lift
    1. ExceptT.lift
  450. lift
    1. OptionT.lift
  451. lift
    1. Quot.lift
  452. lift
    1. Quotient.lift
  453. lift
    1. Squash.lift
  454. lift
    1. State­CpsT.lift
  455. lift
    1. State­RefT'.lift
  456. lift
    1. StateT.lift
  457. lift­On
    1. Quot.lift­On
  458. lift­On
    1. Quotient.lift­On
  459. lift­On₂
    1. Quotient.lift­On₂
  460. lift­With
    1. MonadControl.lift­With (class method)
  461. lift­With
    1. Monad­ControlT.lift­With (class method)
  462. lift₂
    1. Quotient.lift₂
  463. line­Eq
  464. lines
    1. IO.FS.lines
  465. lint (Lake command)
  466. linter.unnecessary­Simpa
  467. literal
    1. raw string
  468. literal
    1. string
  469. lock
    1. IO.FS.Handle.lock
  470. log
    1. Float.log
  471. log
    1. Float32.log
  472. log10
    1. Float.log10
  473. log10
    1. Float32.log10
  474. log2
    1. Fin.log2
  475. log2
    1. Float.log2
  476. log2
    1. Float32.log2
  477. log2
    1. Nat.log2
  478. log2
    1. UInt16.log2
  479. log2
    1. UInt32.log2
  480. log2
    1. UInt64.log2
  481. log2
    1. UInt8.log2
  482. log2
    1. USize.log2
  483. lookup
    1. List.lookup
  484. lor
    1. Fin.lor
  485. lor
    1. ISize.lor
  486. lor
    1. Int16.lor
  487. lor
    1. Int32.lor
  488. lor
    1. Int64.lor
  489. lor
    1. Int8.lor
  490. lor
    1. Nat.lor
  491. lor
    1. UInt16.lor
  492. lor
    1. UInt32.lor
  493. lor
    1. UInt64.lor
  494. lor
    1. UInt8.lor
  495. lor
    1. USize.lor
  496. lt
    1. Char.lt
  497. lt
    1. Float.lt
  498. lt
    1. Float32.lt
  499. lt
    1. ISize.lt
  500. lt
    1. Int.lt
  501. lt
    1. Int16.lt
  502. lt
    1. Int32.lt
  503. lt
    1. Int64.lt
  504. lt
    1. Int8.lt
  505. lt
    1. LT.lt (class method)
  506. lt
    1. List.lt
  507. lt
    1. Nat.lt
  508. lt
    1. Option.lt
  509. lt
    1. UInt16.lt
  510. lt
    1. UInt32.lt
  511. lt
    1. UInt64.lt
  512. lt
    1. UInt8.lt
  513. lt
    1. USize.lt
  514. lt­Of­Ord

M

  1. MProd
  2. MProd.mk
    1. Constructor of MProd
  3. Macro­M
    1. Lean.Macro­M
  4. Max
  5. Max.mk
    1. Instance constructor of Max
  6. Mem
    1. List.Mem
  7. Metadata
    1. IO.FS.Metadata
  8. Min
  9. Min.mk
    1. Instance constructor of Min
  10. Mod
  11. Mod.mk
    1. Instance constructor of Mod
  12. Mode
    1. IO.FS.Mode
  13. Monad
  14. Monad.mk
    1. Instance constructor of Monad
  15. Monad­Control
  16. MonadControl.mk
    1. Instance constructor of Monad­Control
  17. Monad­Control­T
  18. Monad­ControlT.mk
    1. Instance constructor of Monad­Control­T
  19. Monad­Eval
  20. MonadEval.mk
    1. Instance constructor of Monad­Eval
  21. Monad­Eval­T
  22. Monad­EvalT.mk
    1. Instance constructor of Monad­Eval­T
  23. Monad­Except
  24. MonadExcept.mk
    1. Instance constructor of Monad­Except
  25. MonadExcept.of­Except
  26. MonadExcept.or­Else
  27. MonadExcept.orelse'
  28. Monad­Except­Of
  29. Monad­ExceptOf.mk
    1. Instance constructor of Monad­Except­Of
  30. Monad­Finally
  31. MonadFinally.mk
    1. Instance constructor of Monad­Finally
  32. Monad­Functor
  33. MonadFunctor.mk
    1. Instance constructor of Monad­Functor
  34. Monad­Functor­T
  35. Monad­FunctorT.mk
    1. Instance constructor of Monad­Functor­T
  36. Monad­Lake­Env
    1. Lake.Monad­Lake­Env
  37. Monad­Lift
  38. MonadLift.mk
    1. Instance constructor of Monad­Lift
  39. Monad­Lift­T
  40. Monad­LiftT.mk
    1. Instance constructor of Monad­Lift­T
  41. Monad­Reader
  42. MonadReader.mk
    1. Instance constructor of Monad­Reader
  43. Monad­Reader­Of
  44. Monad­ReaderOf.mk
    1. Instance constructor of Monad­Reader­Of
  45. Monad­State
  46. MonadState.get
  47. MonadState.mk
    1. Instance constructor of Monad­State
  48. MonadState.modify­Get
  49. Monad­State­Of
  50. Monad­StateOf.mk
    1. Instance constructor of Monad­State­Of
  51. Monad­With­Reader
  52. Monad­WithReader.mk
    1. Instance constructor of Monad­With­Reader
  53. Monad­With­Reader­Of
  54. Monad­With­ReaderOf.mk
    1. Instance constructor of Monad­With­Reader­Of
  55. Monad­Workspace
    1. Lake.Monad­Workspace
  56. Mul
  57. Mul.mk
    1. Instance constructor of Mul
  58. Mutex
    1. Std.Mutex
  59. main goal
  60. map
    1. Array.map
  61. map
    1. EStateM.map
  62. map
    1. Except.map
  63. map
    1. ExceptT.map
  64. map
    1. Functor.map (class method)
  65. map
    1. List.map
  66. map
    1. Option.map
  67. map
    1. Prod.map
  68. map
    1. StateT.map
  69. map
    1. String.map
  70. map
    1. Sum.map
  71. map
    1. Task.map
  72. map
    1. Thunk.map
  73. map­A
    1. List.map­A
  74. map­A
    1. Option.map­A
  75. map­Const
    1. Functor.map­Const (class method)
  76. map­Error
    1. Except.map­Error
  77. map­Fin­Idx
    1. Array.map­Fin­Idx
  78. map­Fin­Idx
    1. List.map­Fin­Idx
  79. map­Fin­Idx­M
    1. Array.map­Fin­Idx­M
  80. map­Fin­Idx­M
    1. List.map­Fin­Idx­M
  81. map­Idx
    1. Array.map­Idx
  82. map­Idx
    1. List.map­Idx
  83. map­Idx­M
    1. Array.map­Idx­M
  84. map­Idx­M
    1. List.map­Idx­M
  85. map­List
    1. Task.map­List
  86. map­M'
    1. Array.map­M'
  87. map­M'
    1. List.map­M'
  88. map­M
    1. Array.map­M
  89. map­M
    1. List.map­M
  90. map­M
    1. Option.map­M
  91. map­Mono
    1. Array.map­Mono
  92. map­Mono
    1. List.map­Mono
  93. map­Mono­M
    1. Array.map­Mono­M
  94. map­Mono­M
    1. List.map­Mono­M
  95. map­Rev
    1. Functor.map­Rev
  96. map­TR
    1. List.map­TR
  97. map­Task
    1. BaseIO.map­Task
  98. map­Task
    1. EIO.map­Task
  99. map­Task
    1. IO.map­Task
  100. map­Tasks
    1. BaseIO.map­Tasks
  101. map­Tasks
    1. EIO.map­Tasks
  102. map­Tasks
    1. IO.map­Tasks
  103. map_const
    1. LawfulFunctor.map_const (class method)
  104. map_pure
    1. LawfulApplicative.seq­Left_eq (class method)
  105. match
  106. match
    1. pp.match
  107. max
    1. Max.max (class method)
  108. max
    1. Nat.max
  109. max
    1. Option.max
  110. max
    1. Task.Priority.max
  111. max?
    1. List.max?
  112. max­Discharge­Depth
    1. Lean.Meta.Simp.Config.max­Discharge­Depth (structure field)
  113. max­Heartbeats
    1. synthInstance.max­Heartbeats
  114. max­Of­Le
  115. max­Size
    1. synthInstance.max­Size
  116. max­Steps
    1. Lean.Meta.Simp.Config.max­Steps (structure field)
  117. max­Steps
    1. pp.max­Steps
  118. max­Value
    1. ISize.max­Value
  119. max­Value
    1. Int16.max­Value
  120. max­Value
    1. Int32.max­Value
  121. max­Value
    1. Int64.max­Value
  122. max­Value
    1. Int8.max­Value
  123. memoize
    1. Lean.Meta.Simp.Config.memoize (structure field)
  124. merge
    1. List.merge
  125. merge
    1. Option.merge
  126. merge­Sort
    1. List.merge­Sort
  127. metadata
    1. System.FilePath.metadata
  128. min
    1. Min.min (class method)
  129. min
    1. Nat.min
  130. min
    1. Option.min
  131. min
    1. String.Pos.min
  132. min?
    1. List.min?
  133. min­Of­Le
  134. min­Value
    1. ISize.min­Value
  135. min­Value
    1. Int16.min­Value
  136. min­Value
    1. Int32.min­Value
  137. min­Value
    1. Int64.min­Value
  138. min­Value
    1. Int8.min­Value
  139. mix­Hash
  140. mk'
    1. LawfulMonad.mk'
  141. mk'
    1. Quotient.mk'
  142. mk
    1. ExceptT.mk
  143. mk
    1. IO.FS.Handle.mk
  144. mk
    1. OptionT.mk
  145. mk
    1. Quot.mk
  146. mk
    1. Quotient.mk
  147. mk
    1. Squash.mk
  148. mk­File­Path
    1. System.mk­File­Path
  149. mk­Iterator
    1. String.mk­Iterator
  150. mk­Ref
    1. IO.mk­Ref
  151. mk­Ref
    1. ST.mk­Ref
  152. mk­Std­Gen
  153. mod
    1. Fin.mod
  154. mod
    1. ISize.mod
  155. mod
    1. Int16.mod
  156. mod
    1. Int32.mod
  157. mod
    1. Int64.mod
  158. mod
    1. Int8.mod
  159. mod
    1. Mod.mod (class method)
  160. mod
    1. Nat.mod
  161. mod
    1. UInt16.mod
  162. mod
    1. UInt32.mod
  163. mod
    1. UInt64.mod
  164. mod
    1. UInt8.mod
  165. mod
    1. USize.mod
  166. mod­Core
    1. Nat.mod­Core
  167. modified
    1. IO.FS.Metadata.modified (structure field)
  168. modify
  169. modify
    1. Array.modify
  170. modify
    1. List.modify
  171. modify
    1. ST.Ref.modify
  172. modify
    1. String.modify
  173. modify­Get
    1. EStateM.modify­Get
  174. modify­Get
    1. MonadState.modify­Get
  175. modify­Get
    1. MonadState.modify­Get (class method)
  176. modify­Get
    1. Monad­StateOf.modify­Get (class method)
  177. modify­Get
    1. ST.Ref.modify­Get
  178. modify­Get
    1. State­RefT'.modify­Get
  179. modify­Get
    1. StateT.modify­Get
  180. modify­Get­The
  181. modify­Head
    1. List.modify­Head
  182. modify­M
    1. Array.modify­M
  183. modify­Op
    1. Array.modify­Op
  184. modify­TR
    1. List.modify­TR
  185. modify­Tail­Idx
    1. List.modify­Tail­Idx
  186. modify­The
  187. modn
    1. Fin.modn
  188. monad­Eval
    1. MonadEval.monad­Eval (class method)
  189. monad­Eval
    1. Monad­EvalT.monad­Eval (class method)
  190. monad­Lift
    1. MonadLift.monad­Lift (class method)
  191. monad­Lift
    1. Monad­LiftT.monad­Lift (class method)
  192. monad­Map
    1. MonadFunctor.monad­Map (class method)
  193. monad­Map
    1. Monad­FunctorT.monad­Map (class method)
  194. mono­Ms­Now
    1. IO.mono­Ms­Now
  195. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  196. monotone
    1. Lean.Order.monotone
  197. mp
    1. Eq.mp
  198. mp
    1. Iff.mp (structure field)
  199. mpr
    1. Eq.mpr
  200. mpr
    1. Iff.mpr (structure field)
  201. msb
    1. BitVec.msb
  202. mul
    1. BitVec.mul
  203. mul
    1. Fin.mul
  204. mul
    1. Float.mul
  205. mul
    1. Float32.mul
  206. mul
    1. ISize.mul
  207. mul
    1. Int.mul
  208. mul
    1. Int16.mul
  209. mul
    1. Int32.mul
  210. mul
    1. Int64.mul
  211. mul
    1. Int8.mul
  212. mul
    1. Mul.mul (class method)
  213. mul
    1. Nat.mul
  214. mul
    1. UInt16.mul
  215. mul
    1. UInt32.mul
  216. mul
    1. UInt64.mul
  217. mul
    1. UInt8.mul
  218. mul
    1. USize.mul
  219. mul­Rec
    1. BitVec.mul­Rec
  220. 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.beq
  11. Nat.bitwise
  12. Nat.ble
  13. Nat.blt
  14. Nat.case­Strong­Rec­On
  15. Nat.cases­Aux­On
  16. Nat.cast
  17. Nat.dec­Eq
  18. Nat.dec­Le
  19. Nat.dec­Lt
  20. Nat.digit­Char
  21. Nat.div
  22. Nat.div.induction­On
  23. Nat.div2Induction
  24. Nat.fold
  25. Nat.fold­M
  26. Nat.fold­Rev
  27. Nat.fold­Rev­M
  28. Nat.fold­TR
  29. Nat.for­M
  30. Nat.for­Rev­M
  31. Nat.gcd
  32. Nat.is­Power­Of­Two
  33. Nat.is­Valid­Char
  34. Nat.land
  35. Nat.lcm
  36. Nat.le
  37. Nat.le.refl
    1. Constructor of Nat.le
  38. Nat.le.step
    1. Constructor of Nat.le
  39. Nat.log2
  40. Nat.lor
  41. Nat.lt
  42. Nat.max
  43. Nat.min
  44. Nat.mod
  45. Nat.mod.induction­On
  46. Nat.mod­Core
  47. Nat.mul
  48. Nat.next­Power­Of­Two
  49. Nat.pow
  50. Nat.pred
  51. Nat.rec­Aux
  52. Nat.repeat
  53. Nat.repeat­TR
  54. Nat.repr
  55. Nat.shift­Left
  56. Nat.shift­Right
  57. Nat.strong­Rec­On
  58. Nat.sub
  59. Nat.sub­Digit­Char
  60. Nat.succ
    1. Constructor of Nat
  61. Nat.super­Digit­Char
  62. Nat.test­Bit
  63. Nat.to­Digits
  64. Nat.to­Float
  65. Nat.to­Float32
  66. Nat.to­ISize
  67. Nat.to­Int16
  68. Nat.to­Int32
  69. Nat.to­Int64
  70. Nat.to­Int8
  71. Nat.to­Sub­Digits
  72. Nat.to­Subscript­String
  73. Nat.to­Super­Digits
  74. Nat.to­Superscript­String
  75. Nat.to­UInt16
  76. Nat.to­UInt32
  77. Nat.to­UInt64
  78. Nat.to­UInt8
  79. Nat.to­USize
  80. Nat.xor
  81. Nat.zero
    1. Constructor of Nat
  82. Nat­Cast
  83. NatCast.mk
    1. Instance constructor of Nat­Cast
  84. Nat­Pow
  85. NatPow.mk
    1. Instance constructor of Nat­Pow
  86. Ne­Zero
  87. NeZero.mk
    1. Instance constructor of Ne­Zero
  88. Neg
  89. Neg.mk
    1. Instance constructor of Neg
  90. New­Goals
    1. Lean.Meta.Rewrite.New­Goals
  91. Nodup
    1. List.Nodup
  92. Nonempty
  93. Nonempty.intro
    1. Constructor of Nonempty
  94. Not
  95. Not.elim
  96. Num­Lit
    1. Lean.Syntax.Num­Lit
  97. name
    1. Lake.LeanOption.name (structure field)
  98. name­Lit­Kind
    1. Lean.name­Lit­Kind
  99. namespace
    1. of inductive type
  100. nat­Abs
    1. Int.nat­Abs
  101. nat­Add
    1. Fin.nat­Add
  102. nat­Cast
    1. NatCast.nat­Cast (class method)
  103. native­Facets
    1. [anonymous] (structure field) (0) (1)
  104. native_decide
  105. ndrec
    1. HEq.ndrec
  106. ndrec­On
    1. HEq.ndrec­On
  107. needs
    1. [anonymous] (structure field) (0) (1)
  108. neg
    1. BitVec.neg
  109. neg
    1. Float.neg
  110. neg
    1. Float32.neg
  111. neg
    1. ISize.neg
  112. neg
    1. Int.neg
  113. neg
    1. Int16.neg
  114. neg
    1. Int32.neg
  115. neg
    1. Int64.neg
  116. neg
    1. Int8.neg
  117. neg
    1. Neg.neg (class method)
  118. neg
    1. UInt16.neg
  119. neg
    1. UInt32.neg
  120. neg
    1. UInt64.neg
  121. neg
    1. UInt8.neg
  122. neg
    1. USize.neg
  123. neg­Of­Nat
    1. Int.neg­Of­Nat
  124. neutral­Config
    1. Lean.Meta.Simp.neutral­Config
  125. new (Lake command)
  126. new
    1. IO.Promise.new
  127. new
    1. Std.Channel.new
  128. new
    1. Std.CloseableChannel.new
  129. new
    1. Std.Condvar.new
  130. new
    1. Std.Mutex.new
  131. new­Goals
    1. Lean.Meta.Rewrite.Config.new­Goals (structure field)
  132. next
  133. next ... => ...
  134. next'
    1. String.next'
  135. next
    1. RandomGen.next (class method)
  136. next
    1. String.Iterator.next
  137. next
    1. String.next
  138. next
    1. Substring.next
  139. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  140. next­Until
    1. String.next­Until
  141. next­While
    1. String.next­While
  142. nextn
    1. String.Iterator.nextn
  143. nextn
    1. Substring.nextn
  144. nil
    1. BitVec.nil
  145. nofun
  146. nomatch
  147. non­Backtrackable
    1. EStateM.non­Backtrackable
  148. norm_cast (0) (1)
  149. normalize
    1. System.FilePath.normalize
  150. not
    1. BitVec.not
  151. not
    1. Bool.not
  152. not
    1. Int.not
  153. not­M
  154. notify­All
    1. Std.Condvar.notify­All
  155. notify­One
    1. Std.Condvar.notify­One
  156. null­Kind
    1. Lean.null­Kind
  157. num­Bits
    1. System.Platform.num­Bits
  158. 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.lt
  31. Option.map
  32. Option.map­A
  33. Option.map­M
  34. Option.max
  35. Option.merge
  36. Option.min
  37. Option.none
    1. Constructor of Option
  38. Option.or
  39. Option.or­Else
  40. Option.pbind
  41. Option.pelim
  42. Option.pmap
  43. Option.repr
  44. Option.sequence
  45. Option.some
    1. Constructor of Option
  46. Option.to­Array
  47. Option.to­List
  48. Option.try­Catch
  49. Option.unattach
  50. Option­T
  51. OptionT.bind
  52. OptionT.fail
  53. OptionT.lift
  54. OptionT.mk
  55. OptionT.or­Else
  56. OptionT.pure
  57. OptionT.run
  58. OptionT.try­Catch
  59. Or
  60. Or.by_cases
  61. Or.by_cases'
  62. Or.inl
    1. Constructor of Or
  63. Or.inr
    1. Constructor of Or
  64. Ord
  65. Ord.lex
  66. Ord.lex'
  67. Ord.mk
    1. Instance constructor of Ord
  68. Ord.on
  69. Ord.opposite
  70. Ord.to­BEq
  71. Ord.to­LE
  72. Ord.to­LT
  73. Ordering
  74. Ordering.eq
    1. Constructor of Ordering
  75. Ordering.gt
    1. Constructor of Ordering
  76. Ordering.is­Eq
  77. Ordering.is­GE
  78. Ordering.is­GT
  79. Ordering.is­LE
  80. Ordering.is­LT
  81. Ordering.is­Ne
  82. Ordering.lt
    1. Constructor of Ordering
  83. Ordering.swap
  84. Ordering.then
  85. Output
    1. IO.Process.Output
  86. obtain
  87. occs
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  88. of­Binary­Scientific
    1. Float.of­Binary­Scientific
  89. of­Binary­Scientific
    1. Float32.of­Binary­Scientific
  90. of­Bit­Vec
    1. ISize.of­Bit­Vec
  91. of­Bit­Vec
    1. Int16.of­Bit­Vec
  92. of­Bit­Vec
    1. Int32.of­Bit­Vec
  93. of­Bit­Vec
    1. Int64.of­Bit­Vec
  94. of­Bit­Vec
    1. Int8.of­Bit­Vec
  95. of­Bits
    1. Float.of­Bits
  96. of­Bits
    1. Float32.of­Bits
  97. of­Bool
    1. BitVec.of­Bool
  98. of­Bool­List­BE
    1. BitVec.of­Bool­List­BE
  99. of­Bool­List­LE
    1. BitVec.of­Bool­List­LE
  100. of­Buffer
    1. IO.FS.Stream.of­Buffer
  101. of­Except
    1. IO.of­Except
  102. of­Except
    1. MonadExcept.of­Except
  103. of­Fin
    1. UInt16.of­Fin
  104. of­Fin
    1. UInt32.of­Fin
  105. of­Fin
    1. UInt64.of­Fin
  106. of­Fin
    1. UInt8.of­Fin
  107. of­Fin
    1. USize.of­Fin
  108. of­Fn
    1. Array.of­Fn
  109. of­Fn
    1. List.of­Fn
  110. of­Handle
    1. IO.FS.Stream.of­Handle
  111. of­Int
    1. BitVec.of­Int
  112. of­Int
    1. Float.of­Int
  113. of­Int
    1. Float32.of­Int
  114. of­Int
    1. ISize.of­Int
  115. of­Int
    1. Int16.of­Int
  116. of­Int
    1. Int32.of­Int
  117. of­Int
    1. Int64.of­Int
  118. of­Int
    1. Int8.of­Int
  119. of­Int­LE
    1. ISize.of­Int­LE
  120. of­Int­LE
    1. Int16.of­Int­LE
  121. of­Int­LE
    1. Int32.of­Int­LE
  122. of­Int­LE
    1. Int64.of­Int­LE
  123. of­Int­LE
    1. Int8.of­Int­LE
  124. of­Int­Truncate
    1. ISize.of­Int­Truncate
  125. of­Int­Truncate
    1. Int16.of­Int­Truncate
  126. of­Int­Truncate
    1. Int32.of­Int­Truncate
  127. of­Int­Truncate
    1. Int64.of­Int­Truncate
  128. of­Int­Truncate
    1. Int8.of­Int­Truncate
  129. of­Nat'
    1. Fin.of­Nat'
  130. of­Nat
    1. BitVec.of­Nat
  131. of­Nat
    1. Char.of­Nat
  132. of­Nat
    1. Float.of­Nat
  133. of­Nat
    1. Float32.of­Nat
  134. of­Nat
    1. ISize.of­Nat
  135. of­Nat
    1. Int16.of­Nat
  136. of­Nat
    1. Int32.of­Nat
  137. of­Nat
    1. Int64.of­Nat
  138. of­Nat
    1. Int8.of­Nat
  139. of­Nat
    1. OfNat.of­Nat (class method)
  140. of­Nat
    1. UInt16.of­Nat
  141. of­Nat
    1. UInt32.of­Nat
  142. of­Nat
    1. UInt64.of­Nat
  143. of­Nat
    1. UInt8.of­Nat
  144. of­Nat
    1. USize.of­Nat
  145. of­Nat32
    1. USize.of­Nat32
  146. of­Nat­LT
    1. BitVec.of­Nat­LT
  147. of­Nat­LT
    1. UInt16.of­Nat­LT
  148. of­Nat­LT
    1. UInt32.of­Nat­LT
  149. of­Nat­LT
    1. UInt64.of­Nat­LT
  150. of­Nat­LT
    1. UInt8.of­Nat­LT
  151. of­Nat­LT
    1. USize.of­Nat­LT
  152. of­Nat­Truncate
    1. UInt16.of­Nat­Truncate
  153. of­Nat­Truncate
    1. UInt32.of­Nat­Truncate
  154. of­Nat­Truncate
    1. UInt64.of­Nat­Truncate
  155. of­Nat­Truncate
    1. UInt8.of­Nat­Truncate
  156. of­Nat­Truncate
    1. USize.of­Nat­Truncate
  157. of­Scientific
    1. Float.of­Scientific
  158. of­Scientific
    1. Float32.of­Scientific
  159. of­Scientific
    1. OfScientific.of­Scientific (class method)
  160. of­Subarray
    1. Array.of­Subarray
  161. of­UInt8
    1. Char.of­UInt8
  162. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  163. offset­Of­Pos
    1. String.offset­Of­Pos
  164. omega
  165. on
    1. Ord.on
  166. open
  167. opposite
    1. Ord.opposite
  168. opt­Param
  169. optional
  170. or
    1. BitVec.or
  171. or
    1. Bool.or
  172. or
    1. List.or
  173. or
    1. Option.or
  174. or­Else'
    1. EStateM.or­Else'
  175. or­Else
    1. EStateM.or­Else
  176. or­Else
    1. MonadExcept.or­Else
  177. or­Else
    1. Option.or­Else
  178. or­Else
    1. OptionT.or­Else
  179. or­Else
    1. ReaderT.or­Else
  180. or­Else
    1. StateT.or­Else
  181. or­Else
    1. [anonymous] (class method)
  182. or­Else­Lazy
    1. Except.or­Else­Lazy
  183. or­M
  184. orelse'
    1. MonadExcept.orelse'
  185. other
    1. IO.FileRight.other (structure field)
  186. out
    1. NeZero.out (class method)
  187. out­Param
  188. output
    1. IO.Process.output
  189. override list (Elan command)
  190. override set (Elan command)
  191. override unset (Elan command)

P

  1. PEmpty
  2. PEmpty.elim
  3. PLift
  4. PLift.up
    1. Constructor of PLift
  5. PProd
  6. PProd.mk
    1. Constructor of PProd
  7. PSigma
  8. PSigma.mk
    1. Constructor of PSigma
  9. PSum
  10. PSum.inhabited­Left
  11. PSum.inhabited­Right
  12. PSum.inl
    1. Constructor of PSum
  13. PSum.inr
    1. Constructor of PSum
  14. PUnit
  15. PUnit.unit
    1. Constructor of PUnit
  16. Pairwise
    1. List.Pairwise
  17. Partial­Order
    1. Lean.Order.Partial­Order
  18. Perm
    1. List.Perm
  19. Pos
    1. String.Pos
  20. Pow
  21. Pow.mk
    1. Instance constructor of Pow
  22. Prec
    1. Lean.Syntax.Prec
  23. Preresolved
    1. Lean.Syntax.Preresolved
  24. Prio
    1. Lean.Syntax.Prio
  25. Priority
    1. Task.Priority
  26. Prod
  27. Prod.all­I
  28. Prod.any­I
  29. Prod.fold­I
  30. Prod.lex­Lt
  31. Prod.map
  32. Prod.mk
    1. Constructor of Prod
  33. Prod.swap
  34. Promise
    1. IO.Promise
  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
  43. partition
    1. List.partition
  44. partition­M
    1. List.partition­M
  45. partition­Map
    1. List.partition­Map
  46. path
    1. IO.FS.DirEntry.path
  47. path­Exists
    1. System.FilePath.path­Exists
  48. path­Separator
    1. System.FilePath.path­Separator
  49. path­Separators
    1. System.FilePath.path­Separators
  50. pattern
  51. pbind
    1. Option.pbind
  52. pelim
    1. Option.pelim
  53. placeholder term
  54. pmap
    1. Array.pmap
  55. pmap
    1. List.pmap
  56. pmap
    1. Option.pmap
  57. polymorphism
    1. universe
  58. pop
    1. Array.pop
  59. pop­Front
    1. Subarray.pop­Front
  60. pop­While
    1. Array.pop­While
  61. pos
    1. IO.FS.Stream.Buffer.pos (structure field)
  62. pos
    1. String.Iterator.pos
  63. pos­Of
    1. String.pos­Of
  64. pos­Of
    1. Substring.pos­Of
  65. pow
    1. Float.pow
  66. pow
    1. Float32.pow
  67. pow
    1. HomogeneousPow.pow (class method)
  68. pow
    1. Int.pow
  69. pow
    1. Nat.pow
  70. pow
    1. NatPow.pow (class method)
  71. pow
    1. Pow.pow (class method)
  72. pp
    1. eval.pp
  73. pp.deep­Terms
  74. pp.deepTerms.threshold
  75. pp.field­Notation
  76. pp.match
  77. pp.max­Steps
  78. pp.mvars
  79. pp.proofs
  80. pp.proofs.threshold
  81. precompile­Modules
    1. [anonymous] (structure field)
  82. pred
    1. Fin.pred
  83. pred
    1. Nat.pred
  84. predicative
  85. prev
    1. String.Iterator.prev
  86. prev
    1. String.prev
  87. prev
    1. Substring.prev
  88. prevn
    1. String.Iterator.prevn
  89. prevn
    1. Substring.prevn
  90. print
    1. IO.print
  91. println
    1. IO.println
  92. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
  93. proj
    1. Lean.Meta.Simp.Config.proj (structure field)
  94. proof state
  95. proofs
    1. pp.proofs
  96. property
    1. Subtype.property (structure field)
  97. propext
  98. proposition
  99. proposition
    1. decidable
  100. ptr­Addr­Unsafe
  101. ptr­Eq
  102. ptr­Eq
    1. ST.Ref.ptr­Eq
  103. ptr­Eq­List
  104. pure
    1. EStateM.pure
  105. pure
    1. Except.pure
  106. pure
    1. ExceptT.pure
  107. pure
    1. OptionT.pure
  108. pure
    1. Pure.pure (class method)
  109. pure
    1. ReaderT.pure
  110. pure
    1. StateT.pure
  111. pure
    1. Task.pure
  112. pure
    1. Thunk.pure
  113. pure_bind
    1. [anonymous] (class method)
  114. pure_seq
    1. [anonymous] (class method)
  115. push
    1. Array.push
  116. push
    1. String.push
  117. push_cast
  118. pushn
    1. String.pushn
  119. put­Str
    1. IO.FS.Handle.put­Str
  120. put­Str
    1. IO.FS.Stream.put­Str (structure field)
  121. put­Str­Ln
    1. IO.FS.Handle.put­Str­Ln
  122. put­Str­Ln
    1. 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
  29. quantification
    1. predicative
  30. query (Lake command)
  31. quote
    1. Char.quote
  32. 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
  13. Ref
    1. ST.Ref
  14. Result
    1. EStateM.Result
  15. r
    1. Setoid.r (class method)
  16. rand
    1. IO.rand
  17. rand­Bool
  18. rand­Nat
  19. range'
    1. Array.range'
  20. range'
    1. List.range'
  21. range'TR
    1. List.range'TR
  22. range
    1. Array.range
  23. range
    1. List.range
  24. range
    1. RandomGen.range (class method)
  25. raw
    1. Lean.TSyntax.raw (structure field)
  26. rcases
  27. read
    1. IO.AccessRight.read (structure field)
  28. read
    1. IO.FS.Handle.read
  29. read
    1. IO.FS.Stream.read (structure field)
  30. read
    1. MonadReader.read (class method)
  31. read
    1. Monad­ReaderOf.read (class method)
  32. read
    1. ReaderT.read
  33. read­Bin­File
    1. IO.FS.read­Bin­File
  34. read­Bin­To­End
    1. IO.FS.Handle.read­Bin­To­End
  35. read­Bin­To­End­Into
    1. IO.FS.Handle.read­Bin­To­End­Into
  36. read­Dir
    1. System.FilePath.read­Dir
  37. read­File
    1. IO.FS.read­File
  38. read­The
  39. read­To­End
    1. IO.FS.Handle.read­To­End
  40. real­Path
    1. IO.FS.real­Path
  41. rec
    1. Quot.rec
  42. rec
    1. Quotient.rec
  43. rec­Aux
    1. Nat.rec­Aux
  44. rec­On
    1. Quot.rec­On
  45. rec­On
    1. Quotient.rec­On
  46. rec­On­Subsingleton
    1. Quot.rec­On­Subsingleton
  47. rec­On­Subsingleton
    1. Quotient.rec­On­Subsingleton
  48. rec­On­Subsingleton₂
    1. Quotient.rec­On­Subsingleton₂
  49. recursor
  50. recv
    1. Std.Channel.recv
  51. reduce
  52. reduction
    1. ι (iota)
  53. refine
  54. refine'
  55. refl
    1. Equivalence.refl (structure field)
  56. refl
    1. Setoid.refl
  57. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  58. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  59. rel
    1. Lean.Order.PartialOrder.rel (class method)
  60. rel
    1. Well­FoundedRelation.rel (class method)
  61. rel_antisymm
    1. Lean.Order.PartialOrder.rel_antisymm (class method)
  62. rel_refl
    1. Lean.Order.PartialOrder.rel_refl (class method)
  63. rel_trans
    1. Lean.Order.PartialOrder.rel_trans (class method)
  64. relaxed­Auto­Implicit
  65. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  66. remaining­To­String
    1. String.Iterator.remaining­To­String
  67. remove­All
    1. List.remove­All
  68. remove­Dir
    1. IO.FS.remove­Dir
  69. remove­Dir­All
    1. IO.FS.remove­Dir­All
  70. remove­File
    1. IO.FS.remove­File
  71. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  72. rename
  73. rename
    1. IO.FS.rename
  74. rename_i
  75. repeat (0) (1)
  76. repeat'
  77. repeat
    1. Nat.repeat
  78. repeat1'
  79. repeat­TR
    1. Nat.repeat­TR
  80. replace
  81. replace
    1. Array.replace
  82. replace
    1. List.replace
  83. replace
    1. String.replace
  84. replace­TR
    1. List.replace­TR
  85. replicate
    1. Array.replicate
  86. replicate
    1. BitVec.replicate
  87. replicate
    1. List.replicate
  88. replicate­TR
    1. List.replicate­TR
  89. repr
    1. Int.repr
  90. repr
    1. Nat.repr
  91. repr
    1. Option.repr
  92. repr
    1. USize.repr
  93. repr
    1. eval.derive.repr
  94. resolve
    1. IO.Promise.resolve
  95. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  96. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  97. restore
    1. EStateM.Backtrackable.restore (class method)
  98. restore­M
    1. MonadControl.restore­M (class method)
  99. restore­M
    1. Monad­ControlT.restore­M (class method)
  100. result!
    1. IO.Promise.result!
  101. result
    1. trace.compiler.ir.result
  102. result?
    1. IO.Promise.result?
  103. result­D
    1. IO.Promise.result­D
  104. rev
    1. Fin.rev
  105. rev­Find
    1. String.rev­Find
  106. rev­Pos­Of
    1. String.rev­Pos­Of
  107. reverse
    1. Array.reverse
  108. reverse
    1. BitVec.reverse
  109. reverse
    1. List.reverse
  110. reverse­Induction
    1. Fin.reverse­Induction
  111. revert
  112. rewind
    1. IO.FS.Handle.rewind
  113. rewrite (0) (1)
  114. rewrite
    1. trace.Meta.Tactic.simp.rewrite
  115. rfl (0) (1) (2)
  116. rfl'
  117. rfl
    1. HEq.rfl
  118. rhs
  119. right (0) (1)
  120. right
    1. And.right (structure field)
  121. rightpad
    1. Array.rightpad
  122. rightpad
    1. List.rightpad
  123. rintro
  124. root
    1. IO.FS.DirEntry.root (structure field)
  125. root
    1. [anonymous] (structure field)
  126. roots
    1. [anonymous] (structure field)
  127. rotate­Left
    1. BitVec.rotate­Left
  128. rotate­Left
    1. List.rotate­Left
  129. rotate­Right
    1. BitVec.rotate­Right
  130. rotate­Right
    1. List.rotate­Right
  131. rotate_left
  132. rotate_right
  133. round
    1. Float.round
  134. round
    1. Float32.round
  135. run (Elan command)
  136. run'
    1. EStateM.run'
  137. run'
    1. State­CpsT.run'
  138. run'
    1. State­RefT'.run'
  139. run'
    1. StateT.run'
  140. run
    1. EStateM.run
  141. run
    1. Except­CpsT.run
  142. run
    1. ExceptT.run
  143. run
    1. IO.Process.run
  144. run
    1. Id.run
  145. run
    1. OptionT.run
  146. run
    1. ReaderT.run
  147. run
    1. State­CpsT.run
  148. run
    1. State­RefT'.run
  149. run
    1. StateT.run
  150. run­Catch
    1. Except­CpsT.run­Catch
  151. run­EST
  152. run­K
    1. Except­CpsT.run­K
  153. run­K
    1. State­CpsT.run­K
  154. run­ST
  155. run_tac
  156. rw (0) (1)
  157. rw?
  158. rw_mod_cast
  159. 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. Setoid.refl
  26. Setoid.symm
  27. Setoid.trans
  28. Shift­Left
  29. ShiftLeft.mk
    1. Instance constructor of Shift­Left
  30. Shift­Right
  31. ShiftRight.mk
    1. Instance constructor of Shift­Right
  32. Sigma
  33. Sigma.mk
    1. Constructor of Sigma
  34. Simp­Extension
    1. Lean.Meta.Simp­Extension
  35. Size­Of
  36. SizeOf.mk
    1. Instance constructor of Size­Of
  37. Sort
  38. Source­Info
    1. Lean.Source­Info
  39. Spawn­Args
    1. IO.Process.Spawn­Args
  40. Squash
  41. Squash.ind
  42. Squash.lift
  43. Squash.mk
  44. State­Cps­T
  45. State­CpsT.lift
  46. State­CpsT.run
  47. State­CpsT.run'
  48. State­CpsT.run­K
  49. State­M
  50. State­Ref­T'
  51. State­RefT'.get
  52. State­RefT'.lift
  53. State­RefT'.modify­Get
  54. State­RefT'.run
  55. State­RefT'.run'
  56. State­RefT'.set
  57. State­T
  58. StateT.bind
  59. StateT.failure
  60. StateT.get
  61. StateT.lift
  62. StateT.map
  63. StateT.modify­Get
  64. StateT.or­Else
  65. StateT.pure
  66. StateT.run
  67. StateT.run'
  68. StateT.set
  69. Std.Atomic­T
  70. Std.Channel
  71. Std.Channel.Sync
  72. Std.Channel.for­Async
  73. Std.Channel.new
  74. Std.Channel.recv
  75. Std.Channel.send
  76. Std.Channel.sync
  77. Std.Closeable­Channel
  78. Std.CloseableChannel.new
  79. Std.Condvar
  80. Std.Condvar.new
  81. Std.Condvar.notify­All
  82. Std.Condvar.notify­One
  83. Std.Condvar.wait
  84. Std.Condvar.wait­Until
  85. Std.Mutex
  86. Std.Mutex.atomically
  87. Std.Mutex.atomically­Once
  88. Std.Mutex.new
  89. Std­Gen
  90. Stdio
    1. IO.Process.Stdio
  91. Stdio­Config
    1. IO.Process.Stdio­Config
  92. Str­Lit
    1. Lean.Syntax.Str­Lit
  93. Stream
    1. IO.FS.Stream
  94. String
  95. String.Iterator
  96. String.Iterator.at­End
  97. String.Iterator.curr
  98. String.Iterator.extract
  99. String.Iterator.forward
  100. String.Iterator.has­Next
  101. String.Iterator.has­Prev
  102. String.Iterator.mk
    1. Constructor of String.Iterator
  103. String.Iterator.next
  104. String.Iterator.nextn
  105. String.Iterator.pos
  106. String.Iterator.prev
  107. String.Iterator.prevn
  108. String.Iterator.remaining­Bytes
  109. String.Iterator.remaining­To­String
  110. String.Iterator.set­Curr
  111. String.Iterator.to­End
  112. String.Pos
  113. String.Pos.is­Valid
  114. String.Pos.min
  115. String.Pos.mk
    1. Constructor of String.Pos
  116. String.all
  117. String.any
  118. String.append
  119. String.at­End
  120. String.back
  121. String.capitalize
  122. String.contains
  123. String.crlf­To­Lf
  124. String.dec­Eq
  125. String.decapitalize
  126. String.drop
  127. String.drop­Prefix?
  128. String.drop­Right
  129. String.drop­Right­While
  130. String.drop­Suffix?
  131. String.drop­While
  132. String.end­Pos
  133. String.ends­With
  134. String.extract
  135. String.find
  136. String.find­Line­Start
  137. String.first­Diff­Pos
  138. String.foldl
  139. String.foldr
  140. String.from­UTF8
  141. String.from­UTF8!
  142. String.from­UTF8?
  143. String.front
  144. String.get
  145. String.get!
  146. String.get'
  147. String.get?
  148. String.get­Utf8Byte
  149. String.hash
  150. String.intercalate
  151. String.is­Empty
  152. String.is­Int
  153. String.is­Nat
  154. String.is­Prefix­Of
  155. String.iter
  156. String.join
  157. String.le
  158. String.length
  159. String.map
  160. String.mk
    1. Constructor of String
  161. String.mk­Iterator
  162. String.modify
  163. String.next
  164. String.next'
  165. String.next­Until
  166. String.next­While
  167. String.offset­Of­Pos
  168. String.pos­Of
  169. String.prev
  170. String.push
  171. String.pushn
  172. String.quote
  173. String.remove­Leading­Spaces
  174. String.replace
  175. String.rev­Find
  176. String.rev­Pos­Of
  177. String.set
  178. String.singleton
  179. String.split
  180. String.split­On
  181. String.starts­With
  182. String.strip­Prefix
  183. String.strip­Suffix
  184. String.substr­Eq
  185. String.take
  186. String.take­Right
  187. String.take­Right­While
  188. String.take­While
  189. String.to­Format
  190. String.to­Int!
  191. String.to­Int?
  192. String.to­List
  193. String.to­Lower
  194. String.to­Name
  195. String.to­Nat!
  196. String.to­Nat?
  197. String.to­Substring
  198. String.to­Substring'
  199. String.to­UTF8
  200. String.to­Upper
  201. String.trim
  202. String.trim­Left
  203. String.trim­Right
  204. String.utf8Byte­Size
  205. String.utf8Decode­Char?
  206. String.utf8Encode­Char
  207. String.validate­UTF8
  208. Sub
  209. Sub.mk
    1. Instance constructor of Sub
  210. Subarray
  211. Subarray.all
  212. Subarray.all­M
  213. Subarray.any
  214. Subarray.any­M
  215. Subarray.drop
  216. Subarray.empty
  217. Subarray.find­Rev?
  218. Subarray.find­Rev­M?
  219. Subarray.find­Some­Rev­M?
  220. Subarray.foldl
  221. Subarray.foldl­M
  222. Subarray.foldr
  223. Subarray.foldr­M
  224. Subarray.for­In
  225. Subarray.for­M
  226. Subarray.for­Rev­M
  227. Subarray.get
  228. Subarray.get!
  229. Subarray.get­D
  230. Subarray.mk
    1. Constructor of Subarray
  231. Subarray.pop­Front
  232. Subarray.size
  233. Subarray.split
  234. Subarray.take
  235. Subarray.to­Array
  236. Sublist
    1. List.Sublist
  237. Subsingleton
  238. Subsingleton.elim
  239. Subsingleton.helim
  240. Subsingleton.intro
    1. Instance constructor of Subsingleton
  241. Substring
  242. Substring.all
  243. Substring.any
  244. Substring.at­End
  245. Substring.beq
  246. Substring.bsize
  247. Substring.common­Prefix
  248. Substring.common­Suffix
  249. Substring.contains
  250. Substring.drop
  251. Substring.drop­Prefix?
  252. Substring.drop­Right
  253. Substring.drop­Right­While
  254. Substring.drop­Suffix?
  255. Substring.drop­While
  256. Substring.extract
  257. Substring.foldl
  258. Substring.foldr
  259. Substring.front
  260. Substring.get
  261. Substring.is­Empty
  262. Substring.is­Nat
  263. Substring.mk
    1. Constructor of Substring
  264. Substring.next
  265. Substring.nextn
  266. Substring.pos­Of
  267. Substring.prev
  268. Substring.prevn
  269. Substring.same­As
  270. Substring.split­On
  271. Substring.take
  272. Substring.take­Right
  273. Substring.take­Right­While
  274. Substring.take­While
  275. Substring.to­Iterator
  276. Substring.to­Name
  277. Substring.to­Nat?
  278. Substring.to­String
  279. Substring.trim
  280. Substring.trim­Left
  281. Substring.trim­Right
  282. Subtype
  283. Subtype.mk
    1. Constructor of Subtype
  284. Sum
  285. Sum.elim
  286. Sum.get­Left
  287. Sum.get­Left?
  288. Sum.get­Right
  289. Sum.get­Right?
  290. Sum.inhabited­Left
  291. Sum.inhabited­Right
  292. Sum.inl
    1. Constructor of Sum
  293. Sum.inr
    1. Constructor of Sum
  294. Sum.is­Left
  295. Sum.is­Right
  296. Sum.map
  297. Sum.swap
  298. Sync
    1. Std.Channel.Sync
  299. Syntax
    1. Lean.Syntax
  300. Syntax­Node­Kind
    1. Lean.Syntax­Node­Kind
  301. Syntax­Node­Kinds
    1. Lean.Syntax­Node­Kinds
  302. System.File­Path
  303. System.FilePath.add­Extension
  304. System.FilePath.components
  305. System.FilePath.exe­Extension
  306. System.FilePath.ext­Separator
  307. System.FilePath.extension
  308. System.FilePath.file­Name
  309. System.FilePath.file­Stem
  310. System.FilePath.is­Absolute
  311. System.FilePath.is­Dir
  312. System.FilePath.is­Relative
  313. System.FilePath.join
  314. System.FilePath.metadata
  315. System.FilePath.mk
    1. Constructor of System.File­Path
  316. System.FilePath.normalize
  317. System.FilePath.parent
  318. System.FilePath.path­Exists
  319. System.FilePath.path­Separator
  320. System.FilePath.path­Separators
  321. System.FilePath.read­Dir
  322. System.FilePath.walk­Dir
  323. System.FilePath.with­Extension
  324. System.FilePath.with­File­Name
  325. System.Platform.is­Emscripten
  326. System.Platform.is­OSX
  327. System.Platform.is­Windows
  328. System.Platform.num­Bits
  329. System.Platform.target
  330. System.mk­File­Path
  331. s
    1. String.Iterator.s (structure field)
  332. sadd­Overflow
    1. BitVec.sadd­Overflow
  333. same­As
    1. Substring.same­As
  334. save
    1. EStateM.Backtrackable.save (class method)
  335. scale­B
    1. Float.scale­B
  336. scale­B
    1. Float32.scale­B
  337. scientific­Lit­Kind
    1. Lean.scientific­Lit­Kind
  338. script doc (Lake command)
  339. script list (Lake command)
  340. script run (Lake command)
  341. sdiv
    1. BitVec.sdiv
  342. self uninstall (Elan command)
  343. self update (Elan command)
  344. semi­Out­Param
  345. send
    1. Std.Channel.send
  346. seq
    1. Seq.seq (class method)
  347. seq­Left
    1. SeqLeft.seq­Left (class method)
  348. seq­Left_eq
    1. [anonymous] (class method)
  349. seq­Right
    1. EStateM.seq­Right
  350. seq­Right
    1. SeqRight.seq­Right (class method)
  351. seq­Right_eq
    1. [anonymous] (class method)
  352. seq_assoc
    1. LawfulApplicative.pure_seq (class method)
  353. seq_pure
    1. LawfulApplicative.seq­Right_eq (class method)
  354. sequence
    1. Option.sequence
  355. serve (Lake command)
  356. set!
    1. Array.set!
  357. set
    1. Array.set
  358. set
    1. EStateM.set
  359. set
    1. List.set
  360. set
    1. MonadState.set (class method)
  361. set
    1. Monad­StateOf.set (class method)
  362. set
    1. ST.Ref.set
  363. set
    1. State­RefT'.set
  364. set
    1. StateT.set
  365. set
    1. String.set
  366. set­Access­Rights
    1. IO.set­Access­Rights
  367. set­Curr
    1. String.Iterator.set­Curr
  368. set­Current­Dir
    1. IO.Process.set­Current­Dir
  369. set­If­In­Bounds
    1. Array.set­If­In­Bounds
  370. set­Kind
    1. Lean.Syntax.set­Kind
  371. set­Rand­Seed
    1. IO.set­Rand­Seed
  372. set­Stderr
    1. IO.set­Stderr
  373. set­Stdin
    1. IO.set­Stdin
  374. set­Stdout
    1. IO.set­Stdout
  375. set­TR
    1. List.set­TR
  376. set­Width'
    1. BitVec.set­Width'
  377. set­Width
    1. BitVec.set­Width
  378. set_option
  379. setsid
    1. IO.Process.SpawnArgs.cwd (structure field)
  380. shift­Concat
    1. BitVec.shift­Concat
  381. shift­Left
    1. BitVec.shift­Left
  382. shift­Left
    1. Fin.shift­Left
  383. shift­Left
    1. ISize.shift­Left
  384. shift­Left
    1. Int16.shift­Left
  385. shift­Left
    1. Int32.shift­Left
  386. shift­Left
    1. Int64.shift­Left
  387. shift­Left
    1. Int8.shift­Left
  388. shift­Left
    1. Nat.shift­Left
  389. shift­Left
    1. ShiftLeft.shift­Left (class method)
  390. shift­Left
    1. UInt16.shift­Left
  391. shift­Left
    1. UInt32.shift­Left
  392. shift­Left
    1. UInt64.shift­Left
  393. shift­Left
    1. UInt8.shift­Left
  394. shift­Left
    1. USize.shift­Left
  395. shift­Left­Rec
    1. BitVec.shift­Left­Rec
  396. shift­Left­Zero­Extend
    1. BitVec.shift­Left­Zero­Extend
  397. shift­Right
    1. Fin.shift­Right
  398. shift­Right
    1. ISize.shift­Right
  399. shift­Right
    1. Int.shift­Right
  400. shift­Right
    1. Int16.shift­Right
  401. shift­Right
    1. Int32.shift­Right
  402. shift­Right
    1. Int64.shift­Right
  403. shift­Right
    1. Int8.shift­Right
  404. shift­Right
    1. Nat.shift­Right
  405. shift­Right
    1. ShiftRight.shift­Right (class method)
  406. shift­Right
    1. UInt16.shift­Right
  407. shift­Right
    1. UInt32.shift­Right
  408. shift­Right
    1. UInt64.shift­Right
  409. shift­Right
    1. UInt8.shift­Right
  410. shift­Right
    1. USize.shift­Right
  411. show
  412. show (Elan command)
  413. show_term
  414. shrink
    1. Array.shrink
  415. sign
    1. Int.sign
  416. sign­Extend
    1. BitVec.sign­Extend
  417. simp (0) (1)
  418. simp!
  419. simp?
  420. simp?!
  421. simp_all
  422. simp_all!
  423. simp_all?
  424. simp_all?!
  425. simp_all_arith
  426. simp_all_arith!
  427. simp_arith
  428. simp_arith!
  429. simp_match
  430. simp_wf
  431. simpa
  432. simpa!
  433. simpa?
  434. simpa?!
  435. simprocs
  436. sin
    1. Float.sin
  437. sin
    1. Float32.sin
  438. single­Pass
    1. Lean.Meta.Simp.Config.single­Pass (structure field)
  439. singleton
    1. Array.singleton
  440. singleton
    1. List.singleton
  441. singleton
    1. String.singleton
  442. sinh
    1. Float.sinh
  443. sinh
    1. Float32.sinh
  444. size
    1. Array.size
  445. size
    1. ISize.size
  446. size
    1. Int16.size
  447. size
    1. Int32.size
  448. size
    1. Int64.size
  449. size
    1. Int8.size
  450. size
    1. Subarray.size
  451. size
    1. UInt16.size
  452. size
    1. UInt32.size
  453. size
    1. UInt64.size
  454. size
    1. UInt8.size
  455. size
    1. USize.size
  456. size­Of
    1. SizeOf.size­Of (class method)
  457. skip (0) (1)
  458. skip­Assigned­Instances
    1. tactic.skip­Assigned­Instances
  459. sle
    1. BitVec.sle
  460. sleep
  461. sleep
    1. IO.sleep
  462. slt
    1. BitVec.slt
  463. smod
    1. BitVec.smod
  464. smt­SDiv
    1. BitVec.smt­SDiv
  465. smt­UDiv
    1. BitVec.smt­UDiv
  466. snd
    1. MProd.snd (structure field)
  467. snd
    1. PProd.snd (structure field)
  468. snd
    1. PSigma.snd (structure field)
  469. snd
    1. Prod.snd (structure field)
  470. snd
    1. Sigma.snd (structure field)
  471. solve
  472. solve_by_elim
  473. sorry
  474. sound
    1. Quot.sound
  475. sound
    1. Quotient.sound
  476. span
    1. List.span
  477. spawn
    1. IO.Process.spawn
  478. spawn
    1. Task.spawn
  479. specialize
  480. split
  481. split
    1. RandomGen.split (class method)
  482. split
    1. String.split
  483. split
    1. Subarray.split
  484. split­At
    1. List.split­At
  485. split­By
    1. List.split­By
  486. split­On
    1. String.split­On
  487. split­On
    1. Substring.split­On
  488. sqrt
    1. Float.sqrt
  489. sqrt
    1. Float32.sqrt
  490. src­Dir
    1. [anonymous] (structure field) (0) (1)
  491. srem
    1. BitVec.srem
  492. sshift­Right'
    1. BitVec.sshift­Right'
  493. sshift­Right
    1. BitVec.sshift­Right
  494. sshift­Right­Rec
    1. BitVec.sshift­Right­Rec
  495. ssub­Overflow
    1. BitVec.ssub­Overflow
  496. st­M
    1. MonadControl.st­M (class method)
  497. st­M
    1. Monad­ControlT.st­M (class method)
  498. start
    1. Subarray.start (structure field)
  499. start­Pos
    1. Substring.start­Pos (structure field)
  500. start_le_stop
    1. Subarray.start_le_stop (structure field)
  501. starts­With
    1. String.starts­With
  502. std­Next
  503. std­Range
  504. std­Split
  505. stderr
    1. IO.Process.Child.stderr (structure field)
  506. stderr
    1. IO.Process.Output.stderr (structure field)
  507. stderr
    1. IO.Process.StdioConfig.stderr (structure field)
  508. stdin
    1. IO.Process.Child.stdin (structure field)
  509. stdin
    1. IO.Process.StdioConfig.stdin (structure field)
  510. stdout
    1. IO.Process.Child.stdout (structure field)
  511. stdout
    1. IO.Process.Output.stdout (structure field)
  512. stdout
    1. IO.Process.StdioConfig.stdout (structure field)
  513. stop
  514. stop
    1. Subarray.stop (structure field)
  515. stop­Pos
    1. Substring.stop­Pos (structure field)
  516. stop_le_array_size
    1. Subarray.stop_le_array_size (structure field)
  517. str
    1. Substring.str (structure field)
  518. str­Lit­Kind
    1. Lean.str­Lit­Kind
  519. strip­Prefix
    1. String.strip­Prefix
  520. strip­Suffix
    1. String.strip­Suffix
  521. strong­Rec­On
    1. Nat.strong­Rec­On
  522. sub
    1. BitVec.sub
  523. sub
    1. Fin.sub
  524. sub
    1. Float.sub
  525. sub
    1. Float32.sub
  526. sub
    1. ISize.sub
  527. sub
    1. Int.sub
  528. sub
    1. Int16.sub
  529. sub
    1. Int32.sub
  530. sub
    1. Int64.sub
  531. sub
    1. Int8.sub
  532. sub
    1. Nat.sub
  533. sub
    1. Sub.sub (class method)
  534. sub
    1. UInt16.sub
  535. sub
    1. UInt32.sub
  536. sub
    1. UInt64.sub
  537. sub
    1. UInt8.sub
  538. sub
    1. USize.sub
  539. sub­Digit­Char
    1. Nat.sub­Digit­Char
  540. sub­Nat
    1. Fin.sub­Nat
  541. sub­Nat­Nat
    1. Int.sub­Nat­Nat
  542. subst
  543. subst
    1. Eq.subst
  544. subst
    1. HEq.subst
  545. subst_eqs
  546. subst_vars
  547. substr­Eq
    1. String.substr­Eq
  548. succ
    1. Fin.succ
  549. succ­Rec
    1. Fin.succ­Rec
  550. succ­Rec­On
    1. Fin.succ­Rec­On
  551. suffices
  552. sum
    1. Array.sum
  553. sum
    1. List.sum
  554. super­Digit­Char
    1. Nat.super­Digit­Char
  555. support­Interpreter
    1. [anonymous] (structure field)
  556. swap
    1. Array.swap
  557. swap
    1. Ordering.swap
  558. swap
    1. Prod.swap
  559. swap
    1. ST.Ref.swap
  560. swap
    1. Sum.swap
  561. swap­At!
    1. Array.swap­At!
  562. swap­At
    1. Array.swap­At
  563. swap­If­In­Bounds
    1. Array.swap­If­In­Bounds
  564. symm
  565. symm
    1. Eq.symm
  566. symm
    1. Equivalence.symm (structure field)
  567. symm
    1. Setoid.symm
  568. symm_saturate
  569. sync
    1. Std.Channel.sync
  570. synthInstance.max­Heartbeats
  571. synthInstance.max­Size
  572. 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.Syntax.Tactic
  5. Task
  6. Task.Priority
  7. Task.Priority.dedicated
  8. Task.Priority.default
  9. Task.Priority.max
  10. Task.bind
  11. Task.get
  12. Task.map
  13. Task.map­List
  14. Task.pure
  15. Task.spawn
  16. Task­State
    1. IO.Task­State
  17. Term
    1. Lean.Syntax.Term
  18. Thunk
  19. Thunk.bind
  20. Thunk.get
  21. Thunk.map
  22. Thunk.mk
    1. Constructor of Thunk
  23. Thunk.pure
  24. Trans
  25. Trans.mk
    1. Instance constructor of Trans
  26. Transparency­Mode
    1. Lean.Meta.Transparency­Mode
  27. True
  28. True.intro
    1. Constructor of True
  29. Type
  30. tactic
  31. tactic'
  32. tactic.custom­Eliminators
  33. tactic.hygienic
  34. tactic.simp.trace (0) (1)
  35. tactic.skip­Assigned­Instances
  36. tail!
    1. List.tail!
  37. tail
    1. List.tail
  38. tail?
    1. List.tail?
  39. tail­D
    1. List.tail­D
  40. take
    1. Array.take
  41. take
    1. List.take
  42. take
    1. ST.Ref.take
  43. take
    1. String.take
  44. take
    1. Subarray.take
  45. take
    1. Substring.take
  46. take­Right
    1. String.take­Right
  47. take­Right
    1. Substring.take­Right
  48. take­Right­While
    1. String.take­Right­While
  49. take­Right­While
    1. Substring.take­Right­While
  50. take­Stdin
    1. IO.Process.Child.take­Stdin
  51. take­TR
    1. List.take­TR
  52. take­While
    1. Array.take­While
  53. take­While
    1. List.take­While
  54. take­While
    1. String.take­While
  55. take­While
    1. Substring.take­While
  56. take­While­TR
    1. List.take­While­TR
  57. tan
    1. Float.tan
  58. tan
    1. Float32.tan
  59. tanh
    1. Float.tanh
  60. tanh
    1. Float32.tanh
  61. target
    1. System.Platform.target
  62. tdiv
    1. Int.tdiv
  63. term
    1. placeholder
  64. test (Lake command)
  65. test­Bit
    1. Nat.test­Bit
  66. then
    1. Ordering.then
  67. threshold
    1. pp.deepTerms.threshold
  68. threshold
    1. pp.proofs.threshold
  69. throw
    1. EStateM.throw
  70. throw
    1. MonadExcept.throw (class method)
  71. throw
    1. Monad­ExceptOf.throw (class method)
  72. throw­Error
    1. Lean.Macro.throw­Error
  73. throw­Error­At
    1. Lean.Macro.throw­Error­At
  74. throw­The
  75. throw­Unsupported
    1. Lean.Macro.throw­Unsupported
  76. tmod
    1. Int.tmod
  77. to­Applicative
    1. Alternative.to­Applicative (class method)
  78. to­Applicative
    1. Monad.to­Applicative (class method)
  79. to­Array
    1. List.to­Array
  80. to­Array
    1. Option.to­Array
  81. to­Array
    1. Subarray.to­Array
  82. to­Array­Impl
    1. List.to­Array­Impl
  83. to­BEq
    1. Ord.to­BEq
  84. to­Base­IO
    1. EIO.to­Base­IO
  85. to­Bind
    1. [anonymous] (class method)
  86. to­Bit­Vec
    1. ISize.to­Bit­Vec
  87. to­Bit­Vec
    1. Int16.to­Bit­Vec
  88. to­Bit­Vec
    1. Int32.to­Bit­Vec
  89. to­Bit­Vec
    1. Int64.to­Bit­Vec
  90. to­Bit­Vec
    1. Int8.to­Bit­Vec
  91. to­Bit­Vec
    1. UInt16.to­Bit­Vec (structure field)
  92. to­Bit­Vec
    1. UInt32.to­Bit­Vec (structure field)
  93. to­Bit­Vec
    1. UInt64.to­Bit­Vec (structure field)
  94. to­Bit­Vec
    1. UInt8.to­Bit­Vec (structure field)
  95. to­Bit­Vec
    1. USize.to­Bit­Vec (structure field)
  96. to­Bits
    1. Float.to­Bits
  97. to­Bits
    1. Float32.to­Bits
  98. to­Bool
    1. Except.to­Bool
  99. to­Byte­Array
    1. List.to­Byte­Array
  100. to­Digits
    1. Nat.to­Digits
  101. to­EIO
    1. BaseIO.to­EIO
  102. to­EIO
    1. IO.to­EIO
  103. to­End
    1. String.Iterator.to­End
  104. to­Fin
    1. BitVec.to­Fin (structure field)
  105. to­Fin
    1. UInt16.to­Fin
  106. to­Fin
    1. UInt32.to­Fin
  107. to­Fin
    1. UInt64.to­Fin
  108. to­Fin
    1. UInt8.to­Fin
  109. to­Fin
    1. USize.to­Fin
  110. to­Float
    1. Float32.to­Float
  111. to­Float
    1. ISize.to­Float
  112. to­Float
    1. Int16.to­Float
  113. to­Float
    1. Int32.to­Float
  114. to­Float
    1. Int64.to­Float
  115. to­Float
    1. Int8.to­Float
  116. to­Float
    1. Nat.to­Float
  117. to­Float
    1. UInt16.to­Float
  118. to­Float
    1. UInt32.to­Float
  119. to­Float
    1. UInt64.to­Float
  120. to­Float
    1. UInt8.to­Float
  121. to­Float
    1. USize.to­Float
  122. to­Float32
    1. Float.to­Float32
  123. to­Float32
    1. ISize.to­Float32
  124. to­Float32
    1. Int16.to­Float32
  125. to­Float32
    1. Int32.to­Float32
  126. to­Float32
    1. Int64.to­Float32
  127. to­Float32
    1. Int8.to­Float32
  128. to­Float32
    1. Nat.to­Float32
  129. to­Float32
    1. UInt16.to­Float32
  130. to­Float32
    1. UInt32.to­Float32
  131. to­Float32
    1. UInt64.to­Float32
  132. to­Float32
    1. UInt8.to­Float32
  133. to­Float32
    1. USize.to­Float32
  134. to­Float­Array
    1. List.to­Float­Array
  135. to­Format
    1. String.to­Format
  136. to­Functor
    1. Applicative.to­Functor (class method)
  137. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  138. to­Handle­Type
    1. IO.Process.Stdio.to­Handle­Type
  139. to­Hex
    1. BitVec.to­Hex
  140. to­IO'
    1. EIO.to­IO'
  141. to­IO
    1. BaseIO.to­IO
  142. to­IO
    1. EIO.to­IO
  143. to­ISize
    1. Bool.to­ISize
  144. to­ISize
    1. Float.to­ISize
  145. to­ISize
    1. Float32.to­ISize
  146. to­ISize
    1. Int.to­ISize
  147. to­ISize
    1. Int16.to­ISize
  148. to­ISize
    1. Int32.to­ISize
  149. to­ISize
    1. Int64.to­ISize
  150. to­ISize
    1. Int8.to­ISize
  151. to­ISize
    1. Nat.to­ISize
  152. to­ISize
    1. USize.to­ISize
  153. to­Int!
    1. String.to­Int!
  154. to­Int
    1. BitVec.to­Int
  155. to­Int
    1. Bool.to­Int
  156. to­Int
    1. ISize.to­Int
  157. to­Int
    1. Int16.to­Int
  158. to­Int
    1. Int32.to­Int
  159. to­Int
    1. Int64.to­Int
  160. to­Int
    1. Int8.to­Int
  161. to­Int16
    1. Bool.to­Int16
  162. to­Int16
    1. Float.to­Int16
  163. to­Int16
    1. Float32.to­Int16
  164. to­Int16
    1. ISize.to­Int16
  165. to­Int16
    1. Int.to­Int16
  166. to­Int16
    1. Int32.to­Int16
  167. to­Int16
    1. Int64.to­Int16
  168. to­Int16
    1. Int8.to­Int16
  169. to­Int16
    1. Nat.to­Int16
  170. to­Int16
    1. UInt16.to­Int16
  171. to­Int32
    1. Bool.to­Int32
  172. to­Int32
    1. Float.to­Int32
  173. to­Int32
    1. Float32.to­Int32
  174. to­Int32
    1. ISize.to­Int32
  175. to­Int32
    1. Int.to­Int32
  176. to­Int32
    1. Int16.to­Int32
  177. to­Int32
    1. Int64.to­Int32
  178. to­Int32
    1. Int8.to­Int32
  179. to­Int32
    1. Nat.to­Int32
  180. to­Int32
    1. UInt32.to­Int32
  181. to­Int64
    1. Bool.to­Int64
  182. to­Int64
    1. Float.to­Int64
  183. to­Int64
    1. Float32.to­Int64
  184. to­Int64
    1. ISize.to­Int64
  185. to­Int64
    1. Int.to­Int64
  186. to­Int64
    1. Int16.to­Int64
  187. to­Int64
    1. Int32.to­Int64
  188. to­Int64
    1. Int8.to­Int64
  189. to­Int64
    1. Nat.to­Int64
  190. to­Int64
    1. UInt64.to­Int64
  191. to­Int8
    1. Bool.to­Int8
  192. to­Int8
    1. Float.to­Int8
  193. to­Int8
    1. Float32.to­Int8
  194. to­Int8
    1. ISize.to­Int8
  195. to­Int8
    1. Int.to­Int8
  196. to­Int8
    1. Int16.to­Int8
  197. to­Int8
    1. Int32.to­Int8
  198. to­Int8
    1. Int64.to­Int8
  199. to­Int8
    1. Nat.to­Int8
  200. to­Int8
    1. UInt8.to­Int8
  201. to­Int?
    1. String.to­Int?
  202. to­Iterator
    1. Substring.to­Iterator
  203. to­LE
    1. Ord.to­LE
  204. to­LT
    1. Ord.to­LT
  205. to­Lawful­Applicative
    1. LawfulMonad.to­Lawful­Applicative (class method)
  206. to­Lawful­Functor
    1. LawfulApplicative.to­Lawful­Functor (class method)
  207. to­Lean­Config
    1. Lake.Lean­ExeConfig.to­Lean­Config (structure field)
  208. to­Lean­Config
    1. Lake.Lean­LibConfig.to­Lean­Config (structure field)
  209. to­List
    1. Array.to­List
  210. to­List
    1. Array.to­List (structure field)
  211. to­List
    1. Option.to­List
  212. to­List
    1. String.to­List
  213. to­List­Append
    1. Array.to­List­Append
  214. to­List­Rev
    1. Array.to­List­Rev
  215. to­Lower
    1. Char.to­Lower
  216. to­Lower
    1. String.to­Lower
  217. to­Monad­State­Of
    1. ST.Ref.to­Monad­State­Of
  218. to­Name
    1. String.to­Name
  219. to­Name
    1. Substring.to­Name
  220. to­Nat!
    1. String.to­Nat!
  221. to­Nat
    1. BitVec.to­Nat
  222. to­Nat
    1. Bool.to­Nat
  223. to­Nat
    1. Char.to­Nat
  224. to­Nat
    1. Fin.to­Nat
  225. to­Nat
    1. Int.to­Nat
  226. to­Nat
    1. UInt16.to­Nat
  227. to­Nat
    1. UInt32.to­Nat
  228. to­Nat
    1. UInt64.to­Nat
  229. to­Nat
    1. UInt8.to­Nat
  230. to­Nat
    1. USize.to­Nat
  231. to­Nat?
    1. Int.to­Nat?
  232. to­Nat?
    1. String.to­Nat?
  233. to­Nat?
    1. Substring.to­Nat?
  234. to­Nat­Clamp­Neg
    1. ISize.to­Nat­Clamp­Neg
  235. to­Nat­Clamp­Neg
    1. Int16.to­Nat­Clamp­Neg
  236. to­Nat­Clamp­Neg
    1. Int32.to­Nat­Clamp­Neg
  237. to­Nat­Clamp­Neg
    1. Int64.to­Nat­Clamp­Neg
  238. to­Nat­Clamp­Neg
    1. Int8.to­Nat­Clamp­Neg
  239. to­Option
    1. Except.to­Option
  240. to­Partial­Order
    1. Lean.Order.CCPO.to­Partial­Order (class method)
  241. to­Pure
    1. [anonymous] (class method)
  242. to­Refl­BEq
    1. LawfulBEq.to­Refl­BEq (class method)
  243. to­Seq
    1. [anonymous] (class method)
  244. to­Seq­Left
    1. Applicative.to­Pure (class method)
  245. to­Seq­Right
    1. [anonymous] (class method)
  246. to­Stdio­Config
    1. IO.Process.SpawnArgs.to­Stdio­Config (structure field)
  247. to­String
    1. Char.to­String
  248. to­String
    1. Float.to­String
  249. to­String
    1. Float32.to­String
  250. to­String
    1. IO.Error.to­String
  251. to­String
    1. List.to­String
  252. to­String
    1. Substring.to­String
  253. to­String
    1. System.FilePath.to­String (structure field)
  254. to­Sub­Digits
    1. Nat.to­Sub­Digits
  255. to­Subarray
    1. Array.to­Subarray
  256. to­Subscript­String
    1. Nat.to­Subscript­String
  257. to­Substring'
    1. String.to­Substring'
  258. to­Substring
    1. String.to­Substring
  259. to­Super­Digits
    1. Nat.to­Super­Digits
  260. to­Superscript­String
    1. Nat.to­Superscript­String
  261. to­UInt16
    1. Bool.to­UInt16
  262. to­UInt16
    1. Float.to­UInt16
  263. to­UInt16
    1. Float32.to­UInt16
  264. to­UInt16
    1. Int16.to­UInt16 (structure field)
  265. to­UInt16
    1. Nat.to­UInt16
  266. to­UInt16
    1. UInt32.to­UInt16
  267. to­UInt16
    1. UInt64.to­UInt16
  268. to­UInt16
    1. UInt8.to­UInt16
  269. to­UInt16
    1. USize.to­UInt16
  270. to­UInt32
    1. Bool.to­UInt32
  271. to­UInt32
    1. Float.to­UInt32
  272. to­UInt32
    1. Float32.to­UInt32
  273. to­UInt32
    1. Int32.to­UInt32 (structure field)
  274. to­UInt32
    1. Nat.to­UInt32
  275. to­UInt32
    1. UInt16.to­UInt32
  276. to­UInt32
    1. UInt64.to­UInt32
  277. to­UInt32
    1. UInt8.to­UInt32
  278. to­UInt32
    1. USize.to­UInt32
  279. to­UInt64
    1. Bool.to­UInt64
  280. to­UInt64
    1. Float.to­UInt64
  281. to­UInt64
    1. Float32.to­UInt64
  282. to­UInt64
    1. Int64.to­UInt64 (structure field)
  283. to­UInt64
    1. Nat.to­UInt64
  284. to­UInt64
    1. UInt16.to­UInt64
  285. to­UInt64
    1. UInt32.to­UInt64
  286. to­UInt64
    1. UInt8.to­UInt64
  287. to­UInt64
    1. USize.to­UInt64
  288. to­UInt8
    1. Bool.to­UInt8
  289. to­UInt8
    1. Char.to­UInt8
  290. to­UInt8
    1. Float.to­UInt8
  291. to­UInt8
    1. Float32.to­UInt8
  292. to­UInt8
    1. Int8.to­UInt8 (structure field)
  293. to­UInt8
    1. Nat.to­UInt8
  294. to­UInt8
    1. UInt16.to­UInt8
  295. to­UInt8
    1. UInt32.to­UInt8
  296. to­UInt8
    1. UInt64.to­UInt8
  297. to­UInt8
    1. USize.to­UInt8
  298. to­USize
    1. Bool.to­USize
  299. to­USize
    1. Float.to­USize
  300. to­USize
    1. Float32.to­USize
  301. to­USize
    1. ISize.to­USize (structure field)
  302. to­USize
    1. Nat.to­USize
  303. to­USize
    1. UInt16.to­USize
  304. to­USize
    1. UInt32.to­USize
  305. to­USize
    1. UInt64.to­USize
  306. to­USize
    1. UInt8.to­USize
  307. to­UTF8
    1. String.to­UTF8
  308. to­Upper
    1. Char.to­Upper
  309. to­Upper
    1. String.to­Upper
  310. to­Vector
    1. Array.to­Vector
  311. toolchain gc (Elan command)
  312. toolchain install (Elan command)
  313. toolchain link (Elan command)
  314. toolchain list (Elan command)
  315. toolchain uninstall (Elan command)
  316. trace
  317. trace
    1. Lean.Macro.trace
  318. trace
    1. tactic.simp.trace (0) (1)
  319. trace.Elab.definition.wf
  320. trace.Meta.Tactic.simp.discharge
  321. trace.Meta.Tactic.simp.rewrite
  322. trace.compiler.ir.result
  323. trace_state (0) (1)
  324. trans
    1. Eq.trans
  325. trans
    1. Equivalence.trans (structure field)
  326. trans
    1. Setoid.trans
  327. trans
    1. Trans.trans (class method)
  328. translate-config (Lake command)
  329. transparency
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  330. trim
    1. String.trim
  331. trim
    1. Substring.trim
  332. trim­Left
    1. String.trim­Left
  333. trim­Left
    1. Substring.trim­Left
  334. trim­Right
    1. String.trim­Right
  335. trim­Right
    1. Substring.trim­Right
  336. trivial
  337. truncate
    1. BitVec.truncate
  338. truncate
    1. IO.FS.Handle.truncate
  339. try (0) (1)
  340. try­Catch
    1. EStateM.try­Catch
  341. try­Catch
    1. Except.try­Catch
  342. try­Catch
    1. ExceptT.try­Catch
  343. try­Catch
    1. MonadExcept.try­Catch (class method)
  344. try­Catch
    1. Monad­ExceptOf.try­Catch (class method)
  345. try­Catch
    1. Option.try­Catch
  346. try­Catch
    1. OptionT.try­Catch
  347. try­Catch­The
  348. try­Finally'
    1. MonadFinally.try­Finally' (class method)
  349. try­Lock
    1. IO.FS.Handle.try­Lock
  350. try­Wait
    1. IO.Process.Child.try­Wait
  351. two­Pow
    1. BitVec.two­Pow
  352. type constructor
  353. type
    1. IO.FS.Metadata.type (structure field)
  354. type
    1. eval.type
  355. 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.land
  9. UInt16.le
  10. UInt16.log2
  11. UInt16.lor
  12. UInt16.lt
  13. UInt16.mod
  14. UInt16.mul
  15. UInt16.neg
  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.shift­Left
  22. UInt16.shift­Right
  23. UInt16.size
  24. UInt16.sub
  25. UInt16.to­Fin
  26. UInt16.to­Float
  27. UInt16.to­Float32
  28. UInt16.to­Int16
  29. UInt16.to­Nat
  30. UInt16.to­UInt32
  31. UInt16.to­UInt64
  32. UInt16.to­UInt8
  33. UInt16.to­USize
  34. UInt16.xor
  35. UInt32
  36. UInt32.add
  37. UInt32.complement
  38. UInt32.dec­Eq
  39. UInt32.dec­Le
  40. UInt32.dec­Lt
  41. UInt32.div
  42. UInt32.is­Valid­Char
  43. UInt32.land
  44. UInt32.le
  45. UInt32.log2
  46. UInt32.lor
  47. UInt32.lt
  48. UInt32.mod
  49. UInt32.mul
  50. UInt32.neg
  51. UInt32.of­Bit­Vec
    1. Constructor of UInt32
  52. UInt32.of­Fin
  53. UInt32.of­Nat
  54. UInt32.of­Nat­LT
  55. UInt32.of­Nat­Truncate
  56. UInt32.shift­Left
  57. UInt32.shift­Right
  58. UInt32.size
  59. UInt32.sub
  60. UInt32.to­Fin
  61. UInt32.to­Float
  62. UInt32.to­Float32
  63. UInt32.to­Int32
  64. UInt32.to­Nat
  65. UInt32.to­UInt16
  66. UInt32.to­UInt64
  67. UInt32.to­UInt8
  68. UInt32.to­USize
  69. UInt32.xor
  70. UInt64
  71. UInt64.add
  72. UInt64.complement
  73. UInt64.dec­Eq
  74. UInt64.dec­Le
  75. UInt64.dec­Lt
  76. UInt64.div
  77. UInt64.land
  78. UInt64.le
  79. UInt64.log2
  80. UInt64.lor
  81. UInt64.lt
  82. UInt64.mod
  83. UInt64.mul
  84. UInt64.neg
  85. UInt64.of­Bit­Vec
    1. Constructor of UInt64
  86. UInt64.of­Fin
  87. UInt64.of­Nat
  88. UInt64.of­Nat­LT
  89. UInt64.of­Nat­Truncate
  90. UInt64.shift­Left
  91. UInt64.shift­Right
  92. UInt64.size
  93. UInt64.sub
  94. UInt64.to­Fin
  95. UInt64.to­Float
  96. UInt64.to­Float32
  97. UInt64.to­Int64
  98. UInt64.to­Nat
  99. UInt64.to­UInt16
  100. UInt64.to­UInt32
  101. UInt64.to­UInt8
  102. UInt64.to­USize
  103. UInt64.xor
  104. UInt8
  105. UInt8.add
  106. UInt8.complement
  107. UInt8.dec­Eq
  108. UInt8.dec­Le
  109. UInt8.dec­Lt
  110. UInt8.div
  111. UInt8.land
  112. UInt8.le
  113. UInt8.log2
  114. UInt8.lor
  115. UInt8.lt
  116. UInt8.mod
  117. UInt8.mul
  118. UInt8.neg
  119. UInt8.of­Bit­Vec
    1. Constructor of UInt8
  120. UInt8.of­Fin
  121. UInt8.of­Nat
  122. UInt8.of­Nat­LT
  123. UInt8.of­Nat­Truncate
  124. UInt8.shift­Left
  125. UInt8.shift­Right
  126. UInt8.size
  127. UInt8.sub
  128. UInt8.to­Fin
  129. UInt8.to­Float
  130. UInt8.to­Float32
  131. UInt8.to­Int8
  132. UInt8.to­Nat
  133. UInt8.to­UInt16
  134. UInt8.to­UInt32
  135. UInt8.to­UInt64
  136. UInt8.to­USize
  137. UInt8.xor
  138. ULift
  139. ULift.up
    1. Constructor of ULift
  140. USize
  141. USize.add
  142. USize.complement
  143. USize.dec­Eq
  144. USize.dec­Le
  145. USize.dec­Lt
  146. USize.div
  147. USize.land
  148. USize.le
  149. USize.log2
  150. USize.lor
  151. USize.lt
  152. USize.mod
  153. USize.mul
  154. USize.neg
  155. USize.of­Bit­Vec
    1. Constructor of USize
  156. USize.of­Fin
  157. USize.of­Nat
  158. USize.of­Nat32
  159. USize.of­Nat­LT
  160. USize.of­Nat­Truncate
  161. USize.repr
  162. USize.shift­Left
  163. USize.shift­Right
  164. USize.size
  165. USize.sub
  166. USize.to­Fin
  167. USize.to­Float
  168. USize.to­Float32
  169. USize.to­ISize
  170. USize.to­Nat
  171. USize.to­UInt16
  172. USize.to­UInt32
  173. USize.to­UInt64
  174. USize.to­UInt8
  175. USize.xor
  176. Unexpand­M
    1. Lean.PrettyPrinter.Unexpand­M
  177. Unexpander
    1. Lean.PrettyPrinter.Unexpander
  178. Unit
  179. Unit.unit
  180. uadd­Overflow
    1. BitVec.uadd­Overflow
  181. udiv
    1. BitVec.udiv
  182. uget
    1. Array.uget
  183. ule
    1. BitVec.ule
  184. ult
    1. BitVec.ult
  185. umod
    1. BitVec.umod
  186. unattach
    1. Array.unattach
  187. unattach
    1. List.unattach
  188. unattach
    1. Option.unattach
  189. uncurry
    1. Function.uncurry
  190. unfold (0) (1)
  191. unfold­Partial­App
    1. Lean.Meta.DSimp.Config.unfold­Partial­App (structure field)
  192. unfold­Partial­App
    1. Lean.Meta.Simp.Config.unfold­Partial­App (structure field)
  193. unhygienic
  194. unit
    1. Unit.unit
  195. universe
  196. universe polymorphism
  197. unlock
    1. IO.FS.Handle.unlock
  198. unnecessary­Simpa
    1. linter.unnecessary­Simpa
  199. unpack (Lake command)
  200. unsafe­Base­IO
  201. unsafe­Cast
  202. unsafe­EIO
  203. unsafe­IO
  204. unsupported­Syntax
    1. Lean.Macro.Exception.unsupported­Syntax
  205. unzip
    1. Array.unzip
  206. unzip
    1. List.unzip
  207. unzip­TR
    1. List.unzip­TR
  208. update (Lake command)
  209. upload (Lake command)
  210. user
    1. IO.FileRight.user (structure field)
  211. user­Error
    1. IO.user­Error
  212. uset
    1. Array.uset
  213. ushift­Right
    1. BitVec.ushift­Right
  214. ushift­Right­Rec
    1. BitVec.ushift­Right­Rec
  215. usize
    1. Array.usize
  216. usub­Overflow
    1. BitVec.usub­Overflow
  217. utf16Size
    1. Char.utf16Size
  218. utf8Byte­Size
    1. String.utf8Byte­Size
  219. utf8Decode­Char?
    1. String.utf8Decode­Char?
  220. utf8Encode­Char
    1. String.utf8Encode­Char
  221. utf8Size
    1. Char.utf8Size

V

  1. val
    1. Char.val (structure field)
  2. val
    1. Fin.val (structure field)
  3. val
    1. Subtype.val (structure field)
  4. valid
    1. Char.valid (structure field)
  5. validate­UTF8
    1. String.validate­UTF8
  6. value
    1. For­InStep.value
  7. 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
  7. wait
    1. IO.wait
  8. wait
    1. Std.Condvar.wait
  9. wait­Any
    1. IO.wait­Any
  10. wait­Until
    1. Std.Condvar.wait­Until
  11. walk­Dir
    1. System.FilePath.walk­Dir
  12. wf
    1. Well­FoundedRelation.wf (class method)
  13. wf
    1. trace.Elab.definition.wf
  14. wf­Param
  15. which (Elan command)
  16. whnf
  17. with­Extension
    1. System.FilePath.with­Extension
  18. with­File
    1. IO.FS.with­File
  19. with­File­Name
    1. System.FilePath.with­File­Name
  20. with­Fresh­Macro­Scope
    1. Lean.Macro.with­Fresh­Macro­Scope
  21. with­Isolated­Streams
    1. IO.FS.with­Isolated­Streams
  22. with­Position
  23. with­Position­After­Linebreak
  24. with­Reader
    1. Monad­WithReader.with­Reader (class method)
  25. with­Reader
    1. Monad­With­ReaderOf.with­Reader (class method)
  26. with­Stderr
    1. IO.with­Stderr
  27. with­Stdin
    1. IO.with­Stdin
  28. with­Stdout
    1. IO.with­Stdout
  29. with­Temp­Dir
    1. IO.FS.with­Temp­Dir
  30. with­Temp­File
    1. IO.FS.with­Temp­File
  31. with­The­Reader
  32. with_reducible (0) (1)
  33. with_reducible_and_instances (0) (1)
  34. with_unfolding_all (0) (1)
  35. without­Position
  36. write
    1. IO.AccessRight.write (structure field)
  37. write
    1. IO.FS.Handle.write
  38. write
    1. IO.FS.Stream.write (structure field)
  39. write­Bin­File
    1. IO.FS.write­Bin­File
  40. write­File
    1. IO.FS.write­File

X

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

Z

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