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. Add­Right­Cancel
    1. Lean.Grind.Add­Right­Cancel
  8. Alternative
  9. Alternative.mk
    1. Instance constructor of Alternative
  10. And
  11. And.elim
  12. And.intro
    1. Constructor of And
  13. And­Op
  14. AndOp.mk
    1. Instance constructor of And­Op
  15. Append
  16. Append.mk
    1. Instance constructor of Append
  17. Applicative
  18. Applicative.mk
    1. Instance constructor of Applicative
  19. Array
  20. Array.all
  21. Array.all­Diff
  22. Array.all­M
  23. Array.any
  24. Array.any­M
  25. Array.append
  26. Array.append­List
  27. Array.attach
  28. Array.attach­With
  29. Array.back
  30. Array.back!
  31. Array.back?
  32. Array.bin­Insert
  33. Array.bin­Insert­M
  34. Array.bin­Search
  35. Array.bin­Search­Contains
  36. Array.contains
  37. Array.count
  38. Array.count­P
  39. Array.drop
  40. Array.elem
  41. Array.empty
  42. Array.empty­With­Capacity
  43. Array.erase
  44. Array.erase­Idx
  45. Array.erase­Idx!
  46. Array.erase­Idx­If­In­Bounds
  47. Array.erase­P
  48. Array.erase­Reps
  49. Array.extract
  50. Array.filter
  51. Array.filter­M
  52. Array.filter­Map
  53. Array.filter­Map­M
  54. Array.filter­Rev­M
  55. Array.filter­Sep­Elems
  56. Array.filter­Sep­Elems­M
  57. Array.fin­Idx­Of?
  58. Array.fin­Range
  59. Array.find?
  60. Array.find­Fin­Idx?
  61. Array.find­Idx
  62. Array.find­Idx?
  63. Array.find­Idx­M?
  64. Array.find­M?
  65. Array.find­Rev?
  66. Array.find­Rev­M?
  67. Array.find­Some!
  68. Array.find­Some?
  69. Array.find­Some­M?
  70. Array.find­Some­Rev?
  71. Array.find­Some­Rev­M?
  72. Array.first­M
  73. Array.flat­Map
  74. Array.flat­Map­M
  75. Array.flatten
  76. Array.foldl
  77. Array.foldl­M
  78. Array.foldr
  79. Array.foldr­M
  80. Array.for­M
  81. Array.for­Rev­M
  82. Array.get­D
  83. Array.get­Even­Elems
  84. Array.get­Max?
  85. Array.group­By­Key
  86. Array.idx­Of
  87. Array.idx­Of?
  88. Array.insert­Idx
  89. Array.insert­Idx!
  90. Array.insert­Idx­If­In­Bounds
  91. Array.insertion­Sort
  92. Array.is­Empty
  93. Array.is­Eqv
  94. Array.is­Prefix­Of
  95. Array.leftpad
  96. Array.lex
  97. Array.map
  98. Array.map­Fin­Idx
  99. Array.map­Fin­Idx­M
  100. Array.map­Idx
  101. Array.map­Idx­M
  102. Array.map­M
  103. Array.map­M'
  104. Array.map­Mono
  105. Array.map­Mono­M
  106. Array.mk
    1. Constructor of Array
  107. Array.modify
  108. Array.modify­M
  109. Array.modify­Op
  110. Array.of­Fn
  111. Array.of­Subarray
  112. Array.partition
  113. Array.pmap
  114. Array.pop
  115. Array.pop­While
  116. Array.push
  117. Array.qsort
  118. Array.qsort­Ord
  119. Array.range
  120. Array.range'
  121. Array.replace
  122. Array.replicate
  123. Array.reverse
  124. Array.rightpad
  125. Array.set
  126. Array.set!
  127. Array.set­If­In­Bounds
  128. Array.shrink
  129. Array.singleton
  130. Array.size
  131. Array.sum
  132. Array.swap
  133. Array.swap­At
  134. Array.swap­At!
  135. Array.swap­If­In­Bounds
  136. Array.take
  137. Array.take­While
  138. Array.to­List
  139. Array.to­List­Append
  140. Array.to­List­Rev
  141. Array.to­Subarray
  142. Array.to­Vector
  143. Array.uget
  144. Array.unattach
  145. Array.unzip
  146. Array.uset
  147. Array.usize
  148. Array.zip
  149. Array.zip­Idx
  150. Array.zip­With
  151. Array.zip­With­All
  152. Atomic­T
    1. Std.Atomic­T
  153. abs
    1. BitVec.abs
  154. abs
    1. Float.abs
  155. abs
    1. Float32.abs
  156. abs
    1. ISize.abs
  157. abs
    1. Int16.abs
  158. abs
    1. Int32.abs
  159. abs
    1. Int64.abs
  160. abs
    1. Int8.abs
  161. absurd
  162. ac_nf
  163. ac_nf0
  164. ac_rfl
  165. accessed
    1. IO.FS.Metadata.accessed (structure field)
  166. acos
    1. Float.acos
  167. acos
    1. Float32.acos
  168. acosh
    1. Float.acosh
  169. acosh
    1. Float32.acosh
  170. adapt
    1. ExceptT.adapt
  171. adapt
    1. ReaderT.adapt
  172. adapt­Except
    1. EStateM.adapt­Except
  173. adc
    1. BitVec.adc
  174. adcb
    1. BitVec.adcb
  175. add
    1. Add.add (class method)
  176. add
    1. BitVec.add
  177. add
    1. Fin.add
  178. add
    1. Float.add
  179. add
    1. Float32.add
  180. add
    1. ISize.add
  181. add
    1. Int.add
  182. add
    1. Int16.add
  183. add
    1. Int32.add
  184. add
    1. Int64.add
  185. add
    1. Int8.add
  186. add
    1. Nat.add
  187. add
    1. UInt16.add
  188. add
    1. UInt32.add
  189. add
    1. UInt64.add
  190. add
    1. UInt8.add
  191. add
    1. USize.add
  192. add­App­Paren
    1. Repr.add­App­Paren
  193. add­Cases
    1. Fin.add­Cases
  194. add­Extension
    1. System.FilePath.add­Extension
  195. add­Heartbeats
    1. IO.add­Heartbeats
  196. add­Macro­Scope
    1. Lean.Macro.add­Macro­Scope
  197. add­Nat
    1. Fin.add­Nat
  198. add_assoc
    1. Lean.Grind.Semiring.add_zero (class method)
  199. add_comm
    1. Lean.Grind.Semiring.npow (class method)
  200. add_le_left_iff
    1. Lean.Grind.OrderedAdd.add_le_left_iff (class method)
  201. add_one_nsmul
    1. [anonymous] (class method)
  202. add_right_cancel
    1. Lean.Grind.Add­RightCancel.add_right_cancel (class method)
  203. add_zero
    1. Lean.Grind.Semiring.nsmul (class method)
  204. add_zsmul
    1. [anonymous] (class method)
  205. admit
  206. all
    1. Array.all
  207. all
    1. List.all
  208. all
    1. Nat.all
  209. all
    1. Option.all
  210. all
    1. Std.HashSet.all
  211. all
    1. Std.TreeMap.all
  212. all
    1. Std.TreeSet.all
  213. all
    1. String.Slice.all
  214. all
    1. String.all
  215. all
    1. Subarray.all
  216. all
    1. Substring.Raw.all
  217. all­Diff
    1. Array.all­Diff
  218. all­Eq
    1. Subsingleton.all­Eq (class method)
  219. all­I
    1. Prod.all­I
  220. all­M
    1. Array.all­M
  221. all­M
    1. List.all­M
  222. all­M
    1. Nat.all­M
  223. all­M
    1. Subarray.all­M
  224. all­Ones
    1. BitVec.all­Ones
  225. all­TR
    1. Nat.all­TR
  226. all_goals (0) (1)
  227. allow­Import­All
    1. [anonymous] (structure field)
  228. allow­Unsafe­Reducibility
  229. alter
    1. Std.DHashMap.alter
  230. alter
    1. Std.DTreeMap.alter
  231. alter
    1. Std.Ext­DHashMap.alter
  232. alter
    1. Std.Ext­HashMap.alter
  233. alter
    1. Std.HashMap.alter
  234. alter
    1. Std.TreeMap.alter
  235. and
    1. AndOp.and (class method)
  236. and
    1. BitVec.and
  237. and
    1. Bool.and
  238. and
    1. List.and
  239. and­M
  240. and_intros
  241. any
    1. Array.any
  242. any
    1. List.any
  243. any
    1. Nat.any
  244. any
    1. Option.any
  245. any
    1. Std.HashSet.any
  246. any
    1. Std.TreeMap.any
  247. any
    1. Std.TreeSet.any
  248. any
    1. String.any
  249. any
    1. Subarray.any
  250. any
    1. Substring.Raw.any
  251. any­I
    1. Prod.any­I
  252. any­M
    1. Array.any­M
  253. any­M
    1. List.any­M
  254. any­M
    1. Nat.any­M
  255. any­M
    1. Subarray.any­M
  256. any­TR
    1. Nat.any­TR
  257. any_goals (0) (1)
  258. app­Dir
    1. IO.app­Dir
  259. app­Path
    1. IO.app­Path
  260. append
    1. Append.append (class method)
  261. append
    1. Array.append
  262. append
    1. BitVec.append
  263. append
    1. ByteArray.append
  264. append
    1. List.append
  265. append
    1. String.append
  266. append­List
    1. Array.append­List
  267. append­TR
    1. List.append­TR
  268. apply (0) (1)
  269. apply
    1. Std.Do.PredTrans.apply (structure field)
  270. apply?
  271. apply_assumption
  272. apply_ext_theorem
  273. apply_mod_cast
  274. apply_rfl
  275. apply_rules
  276. arg [@]i
  277. args
  278. args
    1. [anonymous] (structure field)
  279. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  280. array
    1. ByteArray.Iterator.array (structure field)
  281. array
    1. Subarray.array
  282. as­Task
    1. BaseIO.as­Task
  283. as­Task
    1. EIO.as­Task
  284. as­Task
    1. IO.as­Task
  285. as_aux_lemma
  286. asin
    1. Float.asin
  287. asin
    1. Float32.asin
  288. asinh
    1. Float.asinh
  289. asinh
    1. Float32.asinh
  290. assumption
  291. assumption
    1. inaccessible
  292. assumption_mod_cast
  293. at­End
    1. ByteArray.Iterator.at­End
  294. at­End
    1. String.Legacy.Iterator.at­End
  295. at­End
    1. String.Pos.Raw.at­End
  296. at­End
    1. Substring.Raw.at­End
  297. at­Idx!
    1. Std.TreeSet.at­Idx!
  298. at­Idx
    1. Std.TreeSet.at­Idx
  299. at­Idx?
    1. Std.TreeSet.at­Idx?
  300. at­Idx­D
    1. Std.TreeSet.at­Idx­D
  301. atan
    1. Float.atan
  302. atan
    1. Float32.atan
  303. atan2
    1. Float.atan2
  304. atan2
    1. Float32.atan2
  305. atanh
    1. Float.atanh
  306. atanh
    1. Float32.atanh
  307. atomically
    1. Std.Mutex.atomically
  308. atomically­Once
    1. Std.Mutex.atomically­Once
  309. attach
    1. Array.attach
  310. attach
    1. List.attach
  311. attach
    1. Option.attach
  312. attach­With
    1. Array.attach­With
  313. attach­With
    1. List.attach­With
  314. attach­With
    1. Option.attach­With
  315. auto­Implicit
  316. auto­Lift
  317. auto­Param
  318. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  319. auto­Unfold
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
  320. 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. Backward­Pattern
    1. String.Slice.Pattern.Backward­Pattern
  6. Base­IO
  7. BaseIO.as­Task
  8. BaseIO.bind­Task
  9. BaseIO.chain­Task
  10. BaseIO.map­Task
  11. BaseIO.map­Tasks
  12. BaseIO.to­EIO
  13. BaseIO.to­IO
  14. Bind
  15. Bind.bind­Left
  16. Bind.kleisli­Left
  17. Bind.kleisli­Right
  18. Bind.mk
    1. Instance constructor of Bind
  19. Bit­Vec
  20. BitVec.abs
  21. BitVec.adc
  22. BitVec.adcb
  23. BitVec.add
  24. BitVec.all­Ones
  25. BitVec.and
  26. BitVec.append
  27. BitVec.carry
  28. BitVec.cast
  29. BitVec.concat
  30. BitVec.cons
  31. BitVec.dec­Eq
  32. BitVec.div­Rec
  33. BitVec.div­Subtract­Shift
  34. BitVec.extract­Lsb
  35. BitVec.extract­Lsb'
  36. BitVec.fill
  37. BitVec.get­Lsb
  38. BitVec.get­Lsb?
  39. BitVec.get­Lsb­D
  40. BitVec.get­Msb
  41. BitVec.get­Msb?
  42. BitVec.get­Msb­D
  43. BitVec.hash
  44. BitVec.int­Max
  45. BitVec.int­Min
  46. BitVec.iunfoldr
  47. BitVec.iunfoldr_replace
  48. BitVec.msb
  49. BitVec.mul
  50. BitVec.mul­Rec
  51. BitVec.neg
  52. BitVec.nil
  53. BitVec.not
  54. BitVec.of­Bool
  55. BitVec.of­Bool­List­BE
  56. BitVec.of­Bool­List­LE
  57. BitVec.of­Fin
    1. Constructor of Bit­Vec
  58. BitVec.of­Int
  59. BitVec.of­Nat
  60. BitVec.of­Nat­LT
  61. BitVec.or
  62. BitVec.replicate
  63. BitVec.reverse
  64. BitVec.rotate­Left
  65. BitVec.rotate­Right
  66. BitVec.sadd­Overflow
  67. BitVec.sdiv
  68. BitVec.set­Width
  69. BitVec.set­Width'
  70. BitVec.shift­Concat
  71. BitVec.shift­Left
  72. BitVec.shift­Left­Rec
  73. BitVec.shift­Left­Zero­Extend
  74. BitVec.sign­Extend
  75. BitVec.sle
  76. BitVec.slt
  77. BitVec.smod
  78. BitVec.smt­SDiv
  79. BitVec.smt­UDiv
  80. BitVec.srem
  81. BitVec.sshift­Right
  82. BitVec.sshift­Right'
  83. BitVec.sshift­Right­Rec
  84. BitVec.ssub­Overflow
  85. BitVec.sub
  86. BitVec.to­Hex
  87. BitVec.to­Int
  88. BitVec.to­Nat
  89. BitVec.truncate
  90. BitVec.two­Pow
  91. BitVec.uadd­Overflow
  92. BitVec.udiv
  93. BitVec.ule
  94. BitVec.ult
  95. BitVec.umod
  96. BitVec.ushift­Right
  97. BitVec.ushift­Right­Rec
  98. BitVec.usub­Overflow
  99. BitVec.xor
  100. BitVec.zero
  101. BitVec.zero­Extend
  102. Bool
  103. Bool.and
  104. Bool.dcond
  105. Bool.dec­Eq
  106. Bool.false
    1. Constructor of Bool
  107. Bool.not
  108. Bool.or
  109. Bool.to­ISize
  110. Bool.to­Int
  111. Bool.to­Int16
  112. Bool.to­Int32
  113. Bool.to­Int64
  114. Bool.to­Int8
  115. Bool.to­Nat
  116. Bool.to­UInt16
  117. Bool.to­UInt32
  118. Bool.to­UInt64
  119. Bool.to­UInt8
  120. Bool.to­USize
  121. Bool.true
    1. Constructor of Bool
  122. Bool.xor
  123. Buffer
    1. IO.FS.Stream.Buffer
  124. Build­Type
    1. Lake.Build­Type
  125. Byte­Array
  126. ByteArray.Iterator
  127. ByteArray.Iterator.at­End
  128. ByteArray.Iterator.curr
  129. ByteArray.Iterator.curr'
  130. ByteArray.Iterator.forward
  131. ByteArray.Iterator.has­Next
  132. ByteArray.Iterator.has­Prev
  133. ByteArray.Iterator.mk
    1. Constructor of ByteArray.Iterator
  134. ByteArray.Iterator.next
  135. ByteArray.Iterator.next'
  136. ByteArray.Iterator.nextn
  137. ByteArray.Iterator.pos
  138. ByteArray.Iterator.prev
  139. ByteArray.Iterator.prevn
  140. ByteArray.Iterator.remaining­Bytes
  141. ByteArray.Iterator.to­End
  142. ByteArray.append
  143. ByteArray.copy­Slice
  144. ByteArray.empty
  145. ByteArray.empty­With­Capacity
  146. ByteArray.extract
  147. ByteArray.fast­Append
  148. ByteArray.find­Fin­Idx?
  149. ByteArray.find­Idx?
  150. ByteArray.foldl
  151. ByteArray.foldl­M
  152. ByteArray.for­In
  153. ByteArray.get
  154. ByteArray.get!
  155. ByteArray.is­Empty
  156. ByteArray.iter
  157. ByteArray.mk
    1. Constructor of Byte­Array
  158. ByteArray.push
  159. ByteArray.set
  160. ByteArray.set!
  161. ByteArray.size
  162. ByteArray.to­Byte­Slice
  163. ByteArray.to­List
  164. ByteArray.to­UInt64BE!
  165. ByteArray.to­UInt64LE!
  166. ByteArray.uget
  167. ByteArray.uset
  168. ByteArray.usize
  169. ByteArray.utf8Decode?
  170. ByteArray.utf8Decode­Char
  171. ByteArray.utf8Decode­Char?
  172. Byte­Slice
  173. ByteSlice.beq
  174. ByteSlice.byte­Array
  175. ByteSlice.contains
  176. ByteSlice.empty
  177. ByteSlice.foldr
  178. ByteSlice.foldr­M
  179. ByteSlice.for­M
  180. ByteSlice.get
  181. ByteSlice.get!
  182. ByteSlice.get­D
  183. ByteSlice.of­Byte­Array
  184. ByteSlice.size
  185. ByteSlice.slice
  186. ByteSlice.start
  187. ByteSlice.stop
  188. ByteSlice.to­Byte­Array
  189. back!
    1. Array.back!
  190. back
    1. Array.back
  191. back
    1. String.Slice.back
  192. back
    1. String.back
  193. back?
    1. Array.back?
  194. back?
    1. String.Slice.back?
  195. backward.synthInstance.canon­Instances
  196. bdiv
    1. Int.bdiv
  197. beq
    1. BEq.beq (class method)
  198. beq
    1. ByteSlice.beq
  199. beq
    1. Float.beq
  200. beq
    1. Float32.beq
  201. beq
    1. List.beq
  202. beq
    1. Nat.beq
  203. beq
    1. String.Slice.beq
  204. beq
    1. Substring.Raw.beq
  205. beta
    1. Lean.Meta.DSimp.Config.beta (structure field)
  206. beta
    1. Lean.Meta.Simp.Config.beta (structure field)
  207. bin­Insert
    1. Array.bin­Insert
  208. bin­Insert­M
    1. Array.bin­Insert­M
  209. bin­Search
    1. Array.bin­Search
  210. bin­Search­Contains
    1. Array.bin­Search­Contains
  211. bind
    1. Bind.bind (class method)
  212. bind
    1. EStateM.bind
  213. bind
    1. Except.bind
  214. bind
    1. ExceptT.bind
  215. bind
    1. Option.bind
  216. bind
    1. OptionT.bind
  217. bind
    1. ReaderT.bind
  218. bind
    1. StateT.bind
  219. bind
    1. Task.bind
  220. bind
    1. Thunk.bind
  221. bind­Cont
    1. ExceptT.bind­Cont
  222. bind­Left
    1. Bind.bind­Left
  223. bind­M
    1. Option.bind­M
  224. bind­Task
    1. BaseIO.bind­Task
  225. bind­Task
    1. EIO.bind­Task
  226. bind­Task
    1. IO.bind­Task
  227. bind_assoc
    1. [anonymous] (class method)
  228. bind_map
    1. [anonymous] (class method)
  229. bind_pure_comp
    1. [anonymous] (class method)
  230. binder­Name­Hint
  231. bit­Vec­Of­Nat
    1. Lean.Meta.Simp.Config.bit­Vec­Of­Nat (structure field)
  232. bitwise
    1. Nat.bitwise
  233. ble
    1. Nat.ble
  234. blt
    1. Nat.blt
  235. bmod
    1. Int.bmod
  236. bootstrap.inductive­Check­Resulting­Universe
  237. bracket
    1. Std.Format.bracket
  238. bracket­Fill
    1. Std.Format.bracket­Fill
  239. bsize
    1. Substring.Raw.bsize
  240. buckets
    1. Std.DHashMap.Raw.buckets (structure field)
  241. build (Lake command)
  242. bv_check
  243. bv_decide
  244. bv_decide?
  245. bv_normalize
  246. bv_omega
  247. by­Cases
    1. Decidable.by­Cases
  248. by_cases
  249. by_cases'
    1. Or.by_cases'
  250. by_cases
    1. Or.by_cases
  251. byte
    1. String.Slice.Pos.byte
  252. byte
    1. String.ValidPos.byte
  253. byte­Array
    1. ByteSlice.byte­Array
  254. byte­Distance
    1. String.Pos.Raw.byte­Distance
  255. byte­Idx
    1. String.Pos.Raw.byte­Idx (structure field)
  256. byte­Size
    1. IO.FS.Metadata.byte­Size (structure field)
  257. bytes
    1. String.Slice.bytes
  258. bytes
    1. String.bytes (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. Comm­Ring
    1. Lean.Grind.Comm­Ring
  53. Comm­Semiring
    1. Lean.Grind.Comm­Semiring
  54. Command
    1. Lean.Syntax.Command
  55. Condvar
    1. Std.Condvar
  56. Config
    1. Lean.Meta.DSimp.Config
  57. Config
    1. Lean.Meta.Rewrite.Config
  58. Config
    1. Lean.Meta.Simp.Config
  59. cache get (Lake command)
  60. cache put (Lake command)
  61. calc
  62. call-by-need
  63. cancel
    1. IO.cancel
  64. canon­Instances
    1. backward.synthInstance.canon­Instances
  65. capitalize
    1. String.capitalize
  66. carry
    1. BitVec.carry
  67. case
  68. case ... => ...
  69. case'
  70. case' ... => ...
  71. case­Strong­Rec­On
    1. Nat.case­Strong­Rec­On
  72. cases
  73. cases
    1. Fin.cases
  74. cases­Aux­On
    1. Nat.cases­Aux­On
  75. cast
  76. cast
    1. BitVec.cast
  77. cast
    1. Fin.cast
  78. cast
    1. Int.cast
  79. cast
    1. Nat.cast
  80. cast
    1. String.Slice.Pos.cast
  81. cast
    1. String.ValidPos.cast
  82. cast­Add
    1. Fin.cast­Add
  83. cast­LE
    1. Fin.cast­LE
  84. cast­LT
    1. Fin.cast­LT
  85. cast­Succ
    1. Fin.cast­Succ
  86. cast_heq
  87. catch­Exceptions
    1. EIO.catch­Exceptions
  88. catch­Runtime
    1. Lean.Meta.Simp.Config.catch­Runtime (structure field)
  89. cbrt
    1. Float.cbrt
  90. cbrt
    1. Float32.cbrt
  91. ceil
    1. Float.ceil
  92. ceil
    1. Float32.ceil
  93. chain
    1. of coercions
  94. chain­Task
    1. BaseIO.chain­Task
  95. chain­Task
    1. EIO.chain­Task
  96. chain­Task
    1. IO.chain­Task
  97. change (0) (1)
  98. change ... with ...
  99. char­Lit­Kind
    1. Lean.char­Lit­Kind
  100. chars
    1. String.Slice.chars
  101. check-build (Lake command)
  102. check-lint (Lake command)
  103. check-test (Lake command)
  104. check­Canceled
    1. IO.check­Canceled
  105. choice
    1. Option.choice
  106. choice­Kind
    1. Lean.choice­Kind
  107. choose
    1. Exists.choose
  108. classical
  109. clean (Lake command)
  110. clear
  111. cmd
    1. [anonymous] (structure field)
  112. coe
    1. Coe.coe (class method)
  113. coe
    1. CoeDep.coe (class method)
  114. coe
    1. CoeFun.coe (class method)
  115. coe
    1. CoeHTC.coe (class method)
  116. coe
    1. CoeHTCT.coe (class method)
  117. coe
    1. CoeHead.coe (class method)
  118. coe
    1. CoeOTC.coe (class method)
  119. coe
    1. CoeOut.coe (class method)
  120. coe
    1. CoeSort.coe (class method)
  121. coe
    1. CoeT.coe (class method)
  122. coe
    1. CoeTC.coe (class method)
  123. coe
    1. CoeTail.coe (class method)
  124. col­Eq
  125. col­Ge
  126. col­Gt
  127. comment
    1. block
  128. comment
    1. line
  129. common­Prefix
    1. Substring.Raw.common­Prefix
  130. common­Suffix
    1. Substring.Raw.common­Suffix
  131. comp
    1. Function.comp
  132. comp_map
    1. LawfulFunctor.comp_map (class method)
  133. compare
    1. Ord.compare (class method)
  134. compare­Lex
  135. compare­Of­Less­And­BEq
  136. compare­Of­Less­And­Eq
  137. compare­On
  138. complement
    1. ISize.complement
  139. complement
    1. Int16.complement
  140. complement
    1. Int32.complement
  141. complement
    1. Int64.complement
  142. complement
    1. Int8.complement
  143. complement
    1. UInt16.complement
  144. complement
    1. UInt32.complement
  145. complement
    1. UInt64.complement
  146. complement
    1. UInt8.complement
  147. complement
    1. USize.complement
  148. completions (Elan command)
  149. components
    1. System.FilePath.components
  150. concat
    1. BitVec.concat
  151. concat
    1. List.concat
  152. cond
  153. configuration
    1. of tactics
  154. congr (0) (1) (2)
  155. congr­Arg
  156. congr­Consts
    1. Lean.Meta.Simp.Config.congr­Consts (structure field)
  157. congr­Fun
  158. conjunctive
    1. Std.Do.PredTrans.conjunctive (structure field)
  159. cons
    1. BitVec.cons
  160. const
    1. Function.const
  161. constructor (0) (1)
  162. contains
    1. Array.contains
  163. contains
    1. ByteSlice.contains
  164. contains
    1. List.contains
  165. contains
    1. Std.DHashMap.contains
  166. contains
    1. Std.DTreeMap.contains
  167. contains
    1. Std.Ext­DHashMap.contains
  168. contains
    1. Std.Ext­HashMap.contains
  169. contains
    1. Std.Ext­HashSet.contains
  170. contains
    1. Std.HashMap.contains
  171. contains
    1. Std.HashSet.contains
  172. contains
    1. Std.TreeMap.contains
  173. contains
    1. Std.TreeSet.contains
  174. contains
    1. String.Slice.contains
  175. contains
    1. String.contains
  176. contains
    1. Substring.Raw.contains
  177. contains­Then­Insert
    1. Std.DHashMap.contains­Then­Insert
  178. contains­Then­Insert
    1. Std.DTreeMap.contains­Then­Insert
  179. contains­Then­Insert
    1. Std.Ext­DHashMap.contains­Then­Insert
  180. contains­Then­Insert
    1. Std.Ext­HashMap.contains­Then­Insert
  181. contains­Then­Insert
    1. Std.Ext­HashSet.contains­Then­Insert
  182. contains­Then­Insert
    1. Std.HashMap.contains­Then­Insert
  183. contains­Then­Insert
    1. Std.HashSet.contains­Then­Insert
  184. contains­Then­Insert
    1. Std.TreeMap.contains­Then­Insert
  185. contains­Then­Insert
    1. Std.TreeSet.contains­Then­Insert
  186. contains­Then­Insert­If­New
    1. Std.DHashMap.contains­Then­Insert­If­New
  187. contains­Then­Insert­If­New
    1. Std.DTreeMap.contains­Then­Insert­If­New
  188. contains­Then­Insert­If­New
    1. Std.Ext­DHashMap.contains­Then­Insert­If­New
  189. contains­Then­Insert­If­New
    1. Std.Ext­HashMap.contains­Then­Insert­If­New
  190. contains­Then­Insert­If­New
    1. Std.HashMap.contains­Then­Insert­If­New
  191. contains­Then­Insert­If­New
    1. Std.TreeMap.contains­Then­Insert­If­New
  192. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  193. contradiction
  194. control
  195. control­At
  196. conv
  197. conv => ...
  198. conv' (0) (1)
  199. copy
    1. String.Slice.copy
  200. copy­Slice
    1. ByteArray.copy­Slice
  201. cos
    1. Float.cos
  202. cos
    1. Float32.cos
  203. cosh
    1. Float.cosh
  204. cosh
    1. Float32.cosh
  205. count
    1. Array.count
  206. count
    1. List.count
  207. count­P
    1. Array.count­P
  208. count­P
    1. List.count­P
  209. create­Dir
    1. IO.FS.create­Dir
  210. create­Dir­All
    1. IO.FS.create­Dir­All
  211. create­Temp­Dir
    1. IO.FS.create­Temp­Dir
  212. create­Temp­File
    1. IO.FS.create­Temp­File
  213. crlf­To­Lf
    1. String.crlf­To­Lf
  214. csup
    1. [anonymous] (class method)
  215. csup_spec
    1. [anonymous] (class method)
  216. cumulativity
  217. curr'
    1. ByteArray.Iterator.curr'
  218. curr'
    1. String.Legacy.Iterator.curr'
  219. curr
    1. ByteArray.Iterator.curr
  220. curr
    1. String.Legacy.Iterator.curr
  221. curr­Column
    1. Std.Format.Monad­PrettyFormat.curr­Column (class method)
  222. current­Dir
    1. IO.current­Dir
  223. curry
    1. Function.curry
  224. custom­Eliminators
    1. tactic.custom­Eliminators
  225. cwd
    1. [anonymous] (structure field)

D

  1. DHash­Map
    1. Std.DHash­Map
  2. DTree­Map
    1. Std.DTree­Map
  3. Decidable
  4. Decidable.by­Cases
  5. Decidable.decide
  6. Decidable.is­False
    1. Constructor of Decidable
  7. Decidable.is­True
    1. Constructor of Decidable
  8. Decidable­Eq
  9. Decidable­LE
  10. Decidable­LT
  11. Decidable­Pred
  12. Decidable­Rel
  13. Dir­Entry
    1. IO.FS.Dir­Entry
  14. Div
  15. Div.mk
    1. Instance constructor of Div
  16. Dvd
  17. Dvd.mk
    1. Instance constructor of Dvd
  18. data
    1. ByteArray.data (structure field)
  19. data
    1. IO.FS.Stream.Buffer.data (structure field)
  20. dbg­Trace­If­Shared
  21. dbg_trace
  22. dcond
    1. Bool.dcond
  23. dec
    1. String.Pos.Raw.dec
  24. dec­Eq
    1. BitVec.dec­Eq
  25. dec­Eq
    1. Bool.dec­Eq
  26. dec­Eq
    1. ISize.dec­Eq
  27. dec­Eq
    1. Int.dec­Eq
  28. dec­Eq
    1. Int16.dec­Eq
  29. dec­Eq
    1. Int32.dec­Eq
  30. dec­Eq
    1. Int64.dec­Eq
  31. dec­Eq
    1. Int8.dec­Eq
  32. dec­Eq
    1. Nat.dec­Eq
  33. dec­Eq
    1. String.dec­Eq
  34. dec­Eq
    1. UInt16.dec­Eq
  35. dec­Eq
    1. UInt32.dec­Eq
  36. dec­Eq
    1. UInt64.dec­Eq
  37. dec­Eq
    1. UInt8.dec­Eq
  38. dec­Eq
    1. USize.dec­Eq
  39. dec­Le
    1. Float.dec­Le
  40. dec­Le
    1. Float32.dec­Le
  41. dec­Le
    1. ISize.dec­Le
  42. dec­Le
    1. Int16.dec­Le
  43. dec­Le
    1. Int32.dec­Le
  44. dec­Le
    1. Int64.dec­Le
  45. dec­Le
    1. Int8.dec­Le
  46. dec­Le
    1. Nat.dec­Le
  47. dec­Le
    1. UInt16.dec­Le
  48. dec­Le
    1. UInt32.dec­Le
  49. dec­Le
    1. UInt64.dec­Le
  50. dec­Le
    1. UInt8.dec­Le
  51. dec­Le
    1. USize.dec­Le
  52. dec­Lt
    1. Float.dec­Lt
  53. dec­Lt
    1. Float32.dec­Lt
  54. dec­Lt
    1. ISize.dec­Lt
  55. dec­Lt
    1. Int16.dec­Lt
  56. dec­Lt
    1. Int32.dec­Lt
  57. dec­Lt
    1. Int64.dec­Lt
  58. dec­Lt
    1. Int8.dec­Lt
  59. dec­Lt
    1. Nat.dec­Lt
  60. dec­Lt
    1. UInt16.dec­Lt
  61. dec­Lt
    1. UInt32.dec­Lt
  62. dec­Lt
    1. UInt64.dec­Lt
  63. dec­Lt
    1. UInt8.dec­Lt
  64. dec­Lt
    1. USize.dec­Lt
  65. decapitalize
    1. String.decapitalize
  66. decidable
  67. decidable­Eq­None
    1. Option.decidable­Eq­None
  68. decide
  69. decide
    1. Decidable.decide
  70. decide
    1. Lean.Meta.DSimp.Config.decide (structure field)
  71. decide
    1. Lean.Meta.Simp.Config.decide (structure field)
  72. decrease­By
    1. String.Pos.Raw.decrease­By
  73. decreasing_tactic
  74. decreasing_trivial
  75. decreasing_with
  76. dedicated
    1. Task.Priority.dedicated
  77. deep­Terms
    1. pp.deep­Terms
  78. def­Indent
    1. Std.Format.def­Indent
  79. def­Width
    1. Std.Format.def­Width
  80. default (Elan command)
  81. default
    1. Inhabited.default (class method)
  82. default
    1. Task.Priority.default
  83. default­Facets
    1. [anonymous] (structure field)
  84. delta (0) (1)
  85. diff
    1. guard_msgs.diff
  86. digit­Char
    1. Nat.digit­Char
  87. discard
    1. Functor.discard
  88. discharge
    1. trace.Meta.Tactic.simp.discharge
  89. div
    1. Div.div (class method)
  90. div
    1. Fin.div
  91. div
    1. Float.div
  92. div
    1. Float32.div
  93. div
    1. ISize.div
  94. div
    1. Int16.div
  95. div
    1. Int32.div
  96. div
    1. Int64.div
  97. div
    1. Int8.div
  98. div
    1. Nat.div
  99. div
    1. UInt16.div
  100. div
    1. UInt32.div
  101. div
    1. UInt64.div
  102. div
    1. UInt8.div
  103. div
    1. USize.div
  104. div2Induction
    1. Nat.div2Induction
  105. div­Rec
    1. BitVec.div­Rec
  106. div­Subtract­Shift
    1. BitVec.div­Subtract­Shift
  107. div_eq_mul_inv
    1. [anonymous] (class method)
  108. done (0) (1)
  109. down
    1. PLift.down (structure field)
  110. down
    1. ULift.down (structure field)
  111. drop
    1. Array.drop
  112. drop
    1. List.drop
  113. drop
    1. String.Slice.drop
  114. drop
    1. String.drop
  115. drop
    1. Subarray.drop
  116. drop
    1. Substring.Raw.drop
  117. drop­End
    1. String.Slice.drop­End
  118. drop­End
    1. String.drop­End
  119. drop­End­While
    1. String.Slice.drop­End­While
  120. drop­End­While
    1. String.drop­End­While
  121. drop­Last
    1. List.drop­Last
  122. drop­Last­TR
    1. List.drop­Last­TR
  123. drop­Prefix
    1. String.Slice.drop­Prefix
  124. drop­Prefix
    1. String.drop­Prefix
  125. drop­Prefix?
    1. String.Slice.Pattern.ForwardPattern.drop­Prefix? (class method)
  126. drop­Prefix?
    1. String.Slice.drop­Prefix?
  127. drop­Prefix?
    1. String.drop­Prefix?
  128. drop­Prefix?
    1. Substring.Raw.drop­Prefix?
  129. drop­Right
    1. Substring.Raw.drop­Right
  130. drop­Right­While
    1. Substring.Raw.drop­Right­While
  131. drop­Suffix
    1. String.Slice.drop­Suffix
  132. drop­Suffix
    1. String.drop­Suffix
  133. drop­Suffix?
    1. String.Slice.Pattern.BackwardPattern.drop­Suffix? (class method)
  134. drop­Suffix?
    1. String.Slice.drop­Suffix?
  135. drop­Suffix?
    1. String.drop­Suffix?
  136. drop­Suffix?
    1. Substring.Raw.drop­Suffix?
  137. drop­While
    1. List.drop­While
  138. drop­While
    1. String.Slice.drop­While
  139. drop­While
    1. String.drop­While
  140. drop­While
    1. Substring.Raw.drop­While
  141. dsimp (0) (1)
  142. dsimp!
  143. dsimp
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  144. dsimp?
  145. dsimp?!
  146. 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. Equiv
    1. Std.DHashMap.Equiv
  47. Equiv
    1. Std.HashMap.Equiv
  48. Equiv
    1. Std.HashSet.Equiv
  49. Equiv­BEq
  50. EquivBEq.mk
    1. Instance constructor of Equiv­BEq
  51. Equivalence
  52. Equivalence.mk
    1. Constructor of Equivalence
  53. Error
    1. IO.Error
  54. Even
  55. Even.plus­Two
    1. Constructor of Even
  56. Even.zero
    1. Constructor of Even
  57. Except
  58. Except.bind
  59. Except.error
    1. Constructor of Except
  60. Except.is­Ok
  61. Except.map
  62. Except.map­Error
  63. Except.ok
    1. Constructor of Except
  64. Except.or­Else­Lazy
  65. Except.pure
  66. Except.to­Bool
  67. Except.to­Option
  68. Except.try­Catch
  69. Except­Cps­T
  70. Except­CpsT.lift
  71. Except­CpsT.run
  72. Except­CpsT.run­Catch
  73. Except­CpsT.run­K
  74. Except­T
  75. ExceptT.adapt
  76. ExceptT.bind
  77. ExceptT.bind­Cont
  78. ExceptT.lift
  79. ExceptT.map
  80. ExceptT.mk
  81. ExceptT.pure
  82. ExceptT.run
  83. ExceptT.try­Catch
  84. Exists
  85. Exists.choose
  86. Exists.intro
    1. Constructor of Exists
  87. Ext­DHash­Map
    1. Std.Ext­DHash­Map
  88. Ext­Hash­Map
    1. Std.Ext­Hash­Map
  89. Ext­Hash­Set
    1. Std.Ext­Hash­Set
  90. ediv
    1. Int.ediv
  91. elem
    1. Array.elem
  92. elem
    1. List.elem
  93. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  94. elim
    1. And.elim
  95. elim
    1. Empty.elim
  96. elim
    1. False.elim
  97. elim
    1. HEq.elim
  98. elim
    1. Iff.elim
  99. elim
    1. Not.elim
  100. elim
    1. Option.elim
  101. elim
    1. PEmpty.elim
  102. elim
    1. Subsingleton.elim
  103. elim
    1. Sum.elim
  104. elim0
    1. Fin.elim0
  105. elim­M
    1. Option.elim­M
  106. emod
    1. Int.emod
  107. empty
    1. Array.empty
  108. empty
    1. ByteArray.empty
  109. empty
    1. ByteSlice.empty
  110. empty
    1. Std.DTreeMap.empty
  111. empty
    1. Std.TreeMap.empty
  112. empty
    1. Std.TreeSet.empty
  113. empty
    1. Subarray.empty
  114. empty­With­Capacity
    1. Array.empty­With­Capacity
  115. empty­With­Capacity
    1. ByteArray.empty­With­Capacity
  116. empty­With­Capacity
    1. Std.DHashMap.empty­With­Capacity
  117. empty­With­Capacity
    1. Std.Ext­DHashMap.empty­With­Capacity
  118. empty­With­Capacity
    1. Std.Ext­HashMap.empty­With­Capacity
  119. empty­With­Capacity
    1. Std.Ext­HashSet.empty­With­Capacity
  120. empty­With­Capacity
    1. Std.HashMap.empty­With­Capacity
  121. empty­With­Capacity
    1. Std.HashSet.empty­With­Capacity
  122. end­Exclusive
    1. String.Slice.end­Exclusive (structure field)
  123. end­Pos
    1. String.Slice.end­Pos
  124. end­Tags
    1. Std.Format.Monad­PrettyFormat.end­Tags (class method)
  125. end­Valid­Pos
    1. String.end­Valid­Pos
  126. ends­With
    1. String.Slice.Pattern.BackwardPattern.ends­With (class method)
  127. ends­With
    1. String.Slice.ends­With
  128. ends­With
    1. String.ends­With
  129. entails
    1. Std.Do.SPred.entails
  130. enter
  131. entry­At­Idx!
    1. Std.TreeMap.entry­At­Idx!
  132. entry­At­Idx
    1. Std.TreeMap.entry­At­Idx
  133. entry­At­Idx?
    1. Std.TreeMap.entry­At­Idx?
  134. entry­At­Idx­D
    1. Std.TreeMap.entry­At­Idx­D
  135. env (Lake command)
  136. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  137. environment variables
  138. eprint
    1. IO.eprint
  139. eprintln
    1. IO.eprintln
  140. eq­Ignore­Ascii­Case
    1. String.Slice.eq­Ignore­Ascii­Case
  141. eq­Rec_heq
  142. eq_of_beq
    1. [anonymous] (class method)
  143. eq_of_heq
  144. eq_refl
  145. erase
    1. Array.erase
  146. erase
    1. List.erase
  147. erase
    1. Std.DHashMap.erase
  148. erase
    1. Std.DTreeMap.erase
  149. erase
    1. Std.Ext­DHashMap.erase
  150. erase
    1. Std.Ext­HashMap.erase
  151. erase
    1. Std.Ext­HashSet.erase
  152. erase
    1. Std.HashMap.erase
  153. erase
    1. Std.HashSet.erase
  154. erase
    1. Std.TreeMap.erase
  155. erase
    1. Std.TreeSet.erase
  156. erase­Dups
    1. List.erase­Dups
  157. erase­Idx!
    1. Array.erase­Idx!
  158. erase­Idx
    1. Array.erase­Idx
  159. erase­Idx
    1. List.erase­Idx
  160. erase­Idx­If­In­Bounds
    1. Array.erase­Idx­If­In­Bounds
  161. erase­Idx­TR
    1. List.erase­Idx­TR
  162. erase­Many
    1. Std.TreeMap.erase­Many
  163. erase­Many
    1. Std.TreeSet.erase­Many
  164. erase­P
    1. Array.erase­P
  165. erase­P
    1. List.erase­P
  166. erase­PTR
    1. List.erase­PTR
  167. erase­Reps
    1. Array.erase­Reps
  168. erase­Reps
    1. List.erase­Reps
  169. erase­TR
    1. List.erase­TR
  170. erw (0) (1)
  171. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
  172. eta
    1. Lean.Meta.Simp.Config.eta (structure field)
  173. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
  174. eta­Struct
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  175. eval.derive.repr
  176. eval.pp
  177. eval.type
  178. exact
  179. exact
    1. Quotient.exact
  180. exact?
  181. exact_mod_cast
  182. exe (Lake command)
  183. exe­Extension
    1. System.FilePath.exe­Extension
  184. exe­Name
    1. [anonymous] (structure field)
  185. execution
    1. IO.AccessRight.execution (structure field)
  186. exfalso
  187. exists
  188. exit
    1. IO.Process.exit
  189. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  190. exp
    1. Float.exp
  191. exp
    1. Float32.exp
  192. exp2
    1. Float.exp2
  193. exp2
    1. Float32.exp2
  194. expand­Macro?
    1. Lean.Macro.expand­Macro?
  195. expose_names
  196. ext (0) (1)
  197. ext1
  198. ext­Separator
    1. System.FilePath.ext­Separator
  199. extension
    1. System.FilePath.extension
  200. extensionality
    1. of propositions
  201. extra­Dep­Targets
    1. [anonymous] (structure field) (0) (1)
  202. extract
    1. Array.extract
  203. extract
    1. ByteArray.extract
  204. extract
    1. List.extract
  205. extract
    1. String.Legacy.Iterator.extract
  206. extract
    1. String.Pos.Raw.extract
  207. extract
    1. String.ValidPos.extract
  208. extract
    1. Substring.Raw.extract
  209. extract­Lsb'
    1. BitVec.extract­Lsb'
  210. extract­Lsb
    1. BitVec.extract­Lsb

F

  1. False
  2. False.elim
  3. Field
    1. Lean.Grind.Field
  4. File­Path
    1. System.File­Path
  5. File­Right
    1. IO.File­Right
  6. Fin
  7. Fin.add
  8. Fin.add­Cases
  9. Fin.add­Nat
  10. Fin.cases
  11. Fin.cast
  12. Fin.cast­Add
  13. Fin.cast­LE
  14. Fin.cast­LT
  15. Fin.cast­Succ
  16. Fin.div
  17. Fin.elim0
  18. Fin.foldl
  19. Fin.foldl­M
  20. Fin.foldr
  21. Fin.foldr­M
  22. Fin.h­Iterate
  23. Fin.h­Iterate­From
  24. Fin.induction
  25. Fin.induction­On
  26. Fin.land
  27. Fin.last
  28. Fin.last­Cases
  29. Fin.log2
  30. Fin.lor
  31. Fin.mk
    1. Constructor of Fin
  32. Fin.mod
  33. Fin.modn
  34. Fin.mul
  35. Fin.nat­Add
  36. Fin.of­Nat
  37. Fin.pred
  38. Fin.rev
  39. Fin.reverse­Induction
  40. Fin.shift­Left
  41. Fin.shift­Right
  42. Fin.sub
  43. Fin.sub­Nat
  44. Fin.succ
  45. Fin.succ­Rec
  46. Fin.succ­Rec­On
  47. Fin.to­Nat
  48. Fin.xor
  49. Flatten­Behavior
    1. Std.Format.Flatten­Behavior
  50. Float
  51. Float.abs
  52. Float.acos
  53. Float.acosh
  54. Float.add
  55. Float.asin
  56. Float.asinh
  57. Float.atan
  58. Float.atan2
  59. Float.atanh
  60. Float.beq
  61. Float.cbrt
  62. Float.ceil
  63. Float.cos
  64. Float.cosh
  65. Float.dec­Le
  66. Float.dec­Lt
  67. Float.div
  68. Float.exp
  69. Float.exp2
  70. Float.floor
  71. Float.fr­Exp
  72. Float.is­Finite
  73. Float.is­Inf
  74. Float.is­Na­N
  75. Float.le
  76. Float.log
  77. Float.log10
  78. Float.log2
  79. Float.lt
  80. Float.mul
  81. Float.neg
  82. Float.of­Binary­Scientific
  83. Float.of­Bits
  84. Float.of­Int
  85. Float.of­Nat
  86. Float.of­Scientific
  87. Float.pow
  88. Float.round
  89. Float.scale­B
  90. Float.sin
  91. Float.sinh
  92. Float.sqrt
  93. Float.sub
  94. Float.tan
  95. Float.tanh
  96. Float.to­Bits
  97. Float.to­Float32
  98. Float.to­ISize
  99. Float.to­Int16
  100. Float.to­Int32
  101. Float.to­Int64
  102. Float.to­Int8
  103. Float.to­String
  104. Float.to­UInt16
  105. Float.to­UInt32
  106. Float.to­UInt64
  107. Float.to­UInt8
  108. Float.to­USize
  109. Float32
  110. Float32.abs
  111. Float32.acos
  112. Float32.acosh
  113. Float32.add
  114. Float32.asin
  115. Float32.asinh
  116. Float32.atan
  117. Float32.atan2
  118. Float32.atanh
  119. Float32.beq
  120. Float32.cbrt
  121. Float32.ceil
  122. Float32.cos
  123. Float32.cosh
  124. Float32.dec­Le
  125. Float32.dec­Lt
  126. Float32.div
  127. Float32.exp
  128. Float32.exp2
  129. Float32.floor
  130. Float32.fr­Exp
  131. Float32.is­Finite
  132. Float32.is­Inf
  133. Float32.is­Na­N
  134. Float32.le
  135. Float32.log
  136. Float32.log10
  137. Float32.log2
  138. Float32.lt
  139. Float32.mul
  140. Float32.neg
  141. Float32.of­Binary­Scientific
  142. Float32.of­Bits
  143. Float32.of­Int
  144. Float32.of­Nat
  145. Float32.of­Scientific
  146. Float32.pow
  147. Float32.round
  148. Float32.scale­B
  149. Float32.sin
  150. Float32.sinh
  151. Float32.sqrt
  152. Float32.sub
  153. Float32.tan
  154. Float32.tanh
  155. Float32.to­Bits
  156. Float32.to­Float
  157. Float32.to­ISize
  158. Float32.to­Int16
  159. Float32.to­Int32
  160. Float32.to­Int64
  161. Float32.to­Int8
  162. Float32.to­String
  163. Float32.to­UInt16
  164. Float32.to­UInt32
  165. Float32.to­UInt64
  166. Float32.to­UInt8
  167. Float32.to­USize
  168. For­In
  169. For­In'
  170. ForIn'.mk
    1. Instance constructor of For­In'
  171. ForIn.mk
    1. Instance constructor of For­In
  172. For­In­Step
  173. For­InStep.done
    1. Constructor of For­In­Step
  174. For­InStep.value
  175. For­InStep.yield
    1. Constructor of For­In­Step
  176. For­M
  177. ForM.for­In
  178. ForM.mk
    1. Instance constructor of For­M
  179. Format
    1. Std.Format
  180. Forward­Pattern
    1. String.Slice.Pattern.Forward­Pattern
  181. Function.Has­Left­Inverse
  182. Function.Has­Right­Inverse
  183. Function.Injective
  184. Function.Left­Inverse
  185. Function.Right­Inverse
  186. Function.Surjective
  187. Function.comp
  188. Function.const
  189. Function.curry
  190. Function.uncurry
  191. Functor
  192. Functor.discard
  193. Functor.map­Rev
  194. Functor.mk
    1. Instance constructor of Functor
  195. fail
  196. fail
    1. OptionT.fail
  197. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
  198. fail­If­Unchanged
    1. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  199. fail_if_success (0) (1)
  200. failure
    1. ReaderT.failure
  201. failure
    1. StateT.failure
  202. failure
    1. [anonymous] (class method)
  203. false_or_by_contra
  204. fast­Append
    1. ByteArray.fast­Append
  205. fdiv
    1. Int.fdiv
  206. field­Idx­Kind
    1. Lean.field­Idx­Kind
  207. field­Notation
    1. pp.field­Notation
  208. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
  209. file­Name
    1. System.FilePath.file­Name
  210. file­Stem
    1. System.FilePath.file­Stem
  211. fill
    1. BitVec.fill
  212. fill
    1. Std.Format.fill
  213. filter
    1. Array.filter
  214. filter
    1. List.filter
  215. filter
    1. Option.filter
  216. filter
    1. Std.DHashMap.filter
  217. filter
    1. Std.DTreeMap.filter
  218. filter
    1. Std.Ext­DHashMap.filter
  219. filter
    1. Std.Ext­HashMap.filter
  220. filter
    1. Std.Ext­HashSet.filter
  221. filter
    1. Std.HashMap.filter
  222. filter
    1. Std.HashSet.filter
  223. filter
    1. Std.TreeMap.filter
  224. filter
    1. Std.TreeSet.filter
  225. filter­M
    1. Array.filter­M
  226. filter­M
    1. List.filter­M
  227. filter­M
    1. Option.filter­M
  228. filter­Map
    1. Array.filter­Map
  229. filter­Map
    1. List.filter­Map
  230. filter­Map
    1. Std.DHashMap.filter­Map
  231. filter­Map
    1. Std.DTreeMap.filter­Map
  232. filter­Map
    1. Std.Ext­DHashMap.filter­Map
  233. filter­Map
    1. Std.Ext­HashMap.filter­Map
  234. filter­Map
    1. Std.HashMap.filter­Map
  235. filter­Map
    1. Std.TreeMap.filter­Map
  236. filter­Map­M
    1. Array.filter­Map­M
  237. filter­Map­M
    1. List.filter­Map­M
  238. filter­Map­TR
    1. List.filter­Map­TR
  239. filter­Rev­M
    1. Array.filter­Rev­M
  240. filter­Rev­M
    1. List.filter­Rev­M
  241. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  242. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  243. filter­TR
    1. List.filter­TR
  244. fin­Idx­Of?
    1. Array.fin­Idx­Of?
  245. fin­Idx­Of?
    1. List.fin­Idx­Of?
  246. fin­Range
    1. Array.fin­Range
  247. fin­Range
    1. List.fin­Range
  248. find
    1. String.Legacy.Iterator.find
  249. find
    1. String.find
  250. find?
    1. Array.find?
  251. find?
    1. List.find?
  252. find?
    1. String.Slice.find?
  253. find­Extern­Lib?
    1. Lake.find­Extern­Lib?
  254. find­Fin­Idx?
    1. Array.find­Fin­Idx?
  255. find­Fin­Idx?
    1. ByteArray.find­Fin­Idx?
  256. find­Fin­Idx?
    1. List.find­Fin­Idx?
  257. find­Idx
    1. Array.find­Idx
  258. find­Idx
    1. List.find­Idx
  259. find­Idx?
    1. Array.find­Idx?
  260. find­Idx?
    1. ByteArray.find­Idx?
  261. find­Idx?
    1. List.find­Idx?
  262. find­Idx­M?
    1. Array.find­Idx­M?
  263. find­Lean­Exe?
    1. Lake.find­Lean­Exe?
  264. find­Lean­Lib?
    1. Lake.find­Lean­Lib?
  265. find­Line­Start
    1. String.find­Line­Start
  266. find­M?
    1. Array.find­M?
  267. find­M?
    1. List.find­M?
  268. find­Module?
    1. Lake.find­Module?
  269. find­Next­Pos
    1. String.Slice.find­Next­Pos
  270. find­Package?
    1. Lake.find­Package?
  271. find­Rev?
    1. Array.find­Rev?
  272. find­Rev?
    1. Subarray.find­Rev?
  273. find­Rev­M?
    1. Array.find­Rev­M?
  274. find­Rev­M?
    1. Subarray.find­Rev­M?
  275. find­Some!
    1. Array.find­Some!
  276. find­Some?
    1. Array.find­Some?
  277. find­Some?
    1. List.find­Some?
  278. find­Some­M?
    1. Array.find­Some­M?
  279. find­Some­M?
    1. List.find­Some­M?
  280. find­Some­Rev?
    1. Array.find­Some­Rev?
  281. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
  282. find­Some­Rev­M?
    1. Subarray.find­Some­Rev­M?
  283. first (0) (1)
  284. first­Diff­Pos
    1. String.first­Diff­Pos
  285. first­M
    1. Array.first­M
  286. first­M
    1. List.first­M
  287. fix
    1. Lean.Order.fix
  288. fix
    1. WellFounded.fix
  289. fix_eq
    1. Lean.Order.fix_eq
  290. flags
    1. IO.AccessRight.flags
  291. flags
    1. IO.FileRight.flags
  292. flat­Map
    1. Array.flat­Map
  293. flat­Map
    1. List.flat­Map
  294. flat­Map­M
    1. Array.flat­Map­M
  295. flat­Map­M
    1. List.flat­Map­M
  296. flat­Map­TR
    1. List.flat­Map­TR
  297. flatten
    1. Array.flatten
  298. flatten
    1. List.flatten
  299. flatten­TR
    1. List.flatten­TR
  300. floor
    1. Float.floor
  301. floor
    1. Float32.floor
  302. flush
    1. IO.FS.Handle.flush
  303. flush
    1. IO.FS.Stream.flush (structure field)
  304. fmod
    1. Int.fmod
  305. fn
    1. Thunk.fn (structure field)
  306. focus (0) (1)
  307. fold
    1. Nat.fold
  308. fold
    1. Std.DHashMap.fold
  309. fold
    1. Std.HashMap.fold
  310. fold
    1. Std.HashSet.fold
  311. fold­I
    1. Prod.fold­I
  312. fold­M
    1. Nat.fold­M
  313. fold­M
    1. Std.DHashMap.fold­M
  314. fold­M
    1. Std.HashMap.fold­M
  315. fold­M
    1. Std.HashSet.fold­M
  316. fold­Rev
    1. Nat.fold­Rev
  317. fold­Rev­M
    1. Nat.fold­Rev­M
  318. fold­TR
    1. Nat.fold­TR
  319. fold­Until
    1. String.Legacy.Iterator.fold­Until
  320. foldl
    1. Array.foldl
  321. foldl
    1. ByteArray.foldl
  322. foldl
    1. Fin.foldl
  323. foldl
    1. List.foldl
  324. foldl
    1. Std.DTreeMap.foldl
  325. foldl
    1. Std.TreeMap.foldl
  326. foldl
    1. Std.TreeSet.foldl
  327. foldl
    1. String.Slice.foldl
  328. foldl
    1. String.foldl
  329. foldl
    1. Subarray.foldl
  330. foldl
    1. Substring.Raw.foldl
  331. foldl­M
    1. Array.foldl­M
  332. foldl­M
    1. ByteArray.foldl­M
  333. foldl­M
    1. Fin.foldl­M
  334. foldl­M
    1. List.foldl­M
  335. foldl­M
    1. Std.DTreeMap.foldl­M
  336. foldl­M
    1. Std.TreeMap.foldl­M
  337. foldl­M
    1. Std.TreeSet.foldl­M
  338. foldl­M
    1. Subarray.foldl­M
  339. foldl­Rec­On
    1. List.foldl­Rec­On
  340. foldr
    1. Array.foldr
  341. foldr
    1. ByteSlice.foldr
  342. foldr
    1. Fin.foldr
  343. foldr
    1. List.foldr
  344. foldr
    1. Std.TreeMap.foldr
  345. foldr
    1. Std.TreeSet.foldr
  346. foldr
    1. String.Slice.foldr
  347. foldr
    1. String.foldr
  348. foldr
    1. Subarray.foldr
  349. foldr
    1. Substring.Raw.foldr
  350. foldr­M
    1. Array.foldr­M
  351. foldr­M
    1. ByteSlice.foldr­M
  352. foldr­M
    1. Fin.foldr­M
  353. foldr­M
    1. List.foldr­M
  354. foldr­M
    1. Std.TreeMap.foldr­M
  355. foldr­M
    1. Std.TreeSet.foldr­M
  356. foldr­M
    1. Subarray.foldr­M
  357. foldr­Rec­On
    1. List.foldr­Rec­On
  358. foldr­TR
    1. List.foldr­TR
  359. for­A
    1. List.for­A
  360. for­Async
    1. Std.Channel.for­Async
  361. for­In'
    1. ForIn'.for­In' (class method)
  362. for­In
    1. ByteArray.for­In
  363. for­In
    1. ForIn.for­In (class method)
  364. for­In
    1. ForM.for­In
  365. for­In
    1. Std.DHashMap.for­In
  366. for­In
    1. Std.DTreeMap.for­In
  367. for­In
    1. Std.HashMap.for­In
  368. for­In
    1. Std.HashSet.for­In
  369. for­In
    1. Std.TreeMap.for­In
  370. for­In
    1. Std.TreeSet.for­In
  371. for­In
    1. Subarray.for­In
  372. for­M
    1. Array.for­M
  373. for­M
    1. ByteSlice.for­M
  374. for­M
    1. ForM.for­M (class method)
  375. for­M
    1. List.for­M
  376. for­M
    1. Nat.for­M
  377. for­M
    1. Option.for­M
  378. for­M
    1. Std.DHashMap.for­M
  379. for­M
    1. Std.DTreeMap.for­M
  380. for­M
    1. Std.HashMap.for­M
  381. for­M
    1. Std.HashSet.for­M
  382. for­M
    1. Std.TreeMap.for­M
  383. for­M
    1. Std.TreeSet.for­M
  384. for­M
    1. Subarray.for­M
  385. for­Rev­M
    1. Array.for­Rev­M
  386. for­Rev­M
    1. Nat.for­Rev­M
  387. for­Rev­M
    1. Subarray.for­Rev­M
  388. format
    1. Option.format
  389. format
    1. Std.ToFormat.format (class method)
  390. forward
    1. ByteArray.Iterator.forward
  391. forward
    1. String.Legacy.Iterator.forward
  392. fr­Exp
    1. Float.fr­Exp
  393. fr­Exp
    1. Float32.fr­Exp
  394. from­State­M
    1. EStateM.from­State­M
  395. from­UTF8!
    1. String.from­UTF8!
  396. from­UTF8
    1. String.from­UTF8
  397. from­UTF8?
    1. String.from­UTF8?
  398. front
    1. String.Slice.front
  399. front
    1. String.front
  400. front
    1. Substring.Raw.front
  401. front?
    1. String.Slice.front?
  402. fst
    1. MProd.fst (structure field)
  403. fst
    1. PProd.fst (structure field)
  404. fst
    1. PSigma.fst (structure field)
  405. fst
    1. Prod.fst (structure field)
  406. fst
    1. Sigma.fst (structure field)
  407. fun
  408. fun_cases
  409. fun_induction
  410. 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. ByteArray.get!
  10. get!
    1. ByteSlice.get!
  11. get!
    1. Option.get!
  12. get!
    1. Std.DHashMap.get!
  13. get!
    1. Std.DTreeMap.get!
  14. get!
    1. Std.Ext­DHashMap.get!
  15. get!
    1. Std.Ext­HashMap.get!
  16. get!
    1. Std.Ext­HashSet.get!
  17. get!
    1. Std.HashMap.get!
  18. get!
    1. Std.HashSet.get!
  19. get!
    1. Std.TreeMap.get!
  20. get!
    1. Std.TreeSet.get!
  21. get!
    1. String.Pos.Raw.get!
  22. get!
    1. String.Slice.Pos.get!
  23. get!
    1. String.ValidPos.get!
  24. get!
    1. Subarray.get!
  25. get'
    1. String.Pos.Raw.get'
  26. get
    1. ByteArray.get
  27. get
    1. ByteSlice.get
  28. get
    1. EStateM.get
  29. get
    1. List.get
  30. get
    1. MonadState.get
  31. get
    1. MonadState.get (class method)
  32. get
    1. Monad­StateOf.get (class method)
  33. get
    1. Option.get
  34. get
    1. ST.Ref.get
  35. get
    1. State­RefT'.get
  36. get
    1. StateT.get
  37. get
    1. Std.DHashMap.get
  38. get
    1. Std.DTreeMap.get
  39. get
    1. Std.Ext­DHashMap.get
  40. get
    1. Std.Ext­HashMap.get
  41. get
    1. Std.Ext­HashSet.get
  42. get
    1. Std.HashMap.get
  43. get
    1. Std.HashSet.get
  44. get
    1. Std.TreeMap.get
  45. get
    1. Std.TreeSet.get
  46. get
    1. String.Pos.Raw.get
  47. get
    1. String.Slice.Pos.get
  48. get
    1. String.ValidPos.get
  49. get
    1. Subarray.get
  50. get
    1. Substring.Raw.get
  51. get
    1. Task.get
  52. get
    1. Thunk.get
  53. get?
    1. Std.DHashMap.get?
  54. get?
    1. Std.DTreeMap.get?
  55. get?
    1. Std.Ext­DHashMap.get?
  56. get?
    1. Std.Ext­HashMap.get?
  57. get?
    1. Std.Ext­HashSet.get?
  58. get?
    1. Std.HashMap.get?
  59. get?
    1. Std.HashSet.get?
  60. get?
    1. Std.TreeMap.get?
  61. get?
    1. Std.TreeSet.get?
  62. get?
    1. String.Pos.Raw.get?
  63. get?
    1. String.Slice.Pos.get?
  64. get?
    1. String.ValidPos.get?
  65. get­Augmented­Env
    1. Lake.get­Augmented­Env
  66. get­Augmented­Lean­Path
    1. Lake.get­Augmented­Lean­Path
  67. get­Augmented­Lean­Src­Path
    1. Lake.get­Augmented­Lean­Src­Path
  68. get­Augmented­Shared­Lib­Path
    1. Lake.get­Augmented­Shared­Lib­Path
  69. get­Char
    1. Lean.TSyntax.get­Char
  70. get­Curr­Namespace
    1. Lean.Macro.get­Curr­Namespace
  71. get­Current­Dir
    1. IO.Process.get­Current­Dir
  72. get­D
    1. Array.get­D
  73. get­D
    1. ByteSlice.get­D
  74. get­D
    1. List.get­D
  75. get­D
    1. Option.get­D
  76. get­D
    1. Std.DHashMap.get­D
  77. get­D
    1. Std.DTreeMap.get­D
  78. get­D
    1. Std.Ext­DHashMap.get­D
  79. get­D
    1. Std.Ext­HashMap.get­D
  80. get­D
    1. Std.Ext­HashSet.get­D
  81. get­D
    1. Std.HashMap.get­D
  82. get­D
    1. Std.HashSet.get­D
  83. get­D
    1. Std.TreeMap.get­D
  84. get­D
    1. Std.TreeSet.get­D
  85. get­D
    1. Subarray.get­D
  86. get­DM
    1. Option.get­DM
  87. get­Elan?
    1. Lake.get­Elan?
  88. get­Elan­Home?
    1. Lake.get­Elan­Home?
  89. get­Elan­Install?
    1. Lake.get­Elan­Install?
  90. get­Elan­Toolchain
    1. Lake.get­Elan­Toolchain
  91. get­Elem!
    1. GetElem?.get­Elem? (class method)
  92. get­Elem!_def
    1. Lawful­GetElem.get­Elem!_def (class method)
  93. get­Elem
    1. GetElem.get­Elem (class method)
  94. get­Elem?
    1. [anonymous] (class method)
  95. get­Elem?_def
    1. Lawful­GetElem.get­Elem?_def (class method)
  96. get­Entry­GE!
    1. Std.TreeMap.get­Entry­GE!
  97. get­Entry­GE
    1. Std.TreeMap.get­Entry­GE
  98. get­Entry­GE?
    1. Std.TreeMap.get­Entry­GE?
  99. get­Entry­GED
    1. Std.TreeMap.get­Entry­GED
  100. get­Entry­GT!
    1. Std.TreeMap.get­Entry­GT!
  101. get­Entry­GT
    1. Std.TreeMap.get­Entry­GT
  102. get­Entry­GT?
    1. Std.TreeMap.get­Entry­GT?
  103. get­Entry­GTD
    1. Std.TreeMap.get­Entry­GTD
  104. get­Entry­LE!
    1. Std.TreeMap.get­Entry­LE!
  105. get­Entry­LE
    1. Std.TreeMap.get­Entry­LE
  106. get­Entry­LE?
    1. Std.TreeMap.get­Entry­LE?
  107. get­Entry­LED
    1. Std.TreeMap.get­Entry­LED
  108. get­Entry­LT!
    1. Std.TreeMap.get­Entry­LT!
  109. get­Entry­LT
    1. Std.TreeMap.get­Entry­LT
  110. get­Entry­LT?
    1. Std.TreeMap.get­Entry­LT?
  111. get­Entry­LTD
    1. Std.TreeMap.get­Entry­LTD
  112. get­Env
    1. IO.get­Env
  113. get­Env­Lean­Path
    1. Lake.get­Env­Lean­Path
  114. get­Env­Lean­Src­Path
    1. Lake.get­Env­Lean­Src­Path
  115. get­Env­Shared­Lib­Path
    1. Lake.get­Env­Shared­Lib­Path
  116. get­Even­Elems
    1. Array.get­Even­Elems
  117. get­GE!
    1. Std.TreeSet.get­GE!
  118. get­GE
    1. Std.TreeSet.get­GE
  119. get­GE?
    1. Std.TreeSet.get­GE?
  120. get­GED
    1. Std.TreeSet.get­GED
  121. get­GT!
    1. Std.TreeSet.get­GT!
  122. get­GT
    1. Std.TreeSet.get­GT
  123. get­GT?
    1. Std.TreeSet.get­GT?
  124. get­GTD
    1. Std.TreeSet.get­GTD
  125. get­Hygiene­Info
    1. Lean.TSyntax.get­Hygiene­Info
  126. get­Id
    1. Lean.TSyntax.get­Id
  127. get­Key!
    1. Std.DHashMap.get­Key!
  128. get­Key!
    1. Std.DTreeMap.get­Key!
  129. get­Key!
    1. Std.Ext­DHashMap.get­Key!
  130. get­Key!
    1. Std.Ext­HashMap.get­Key!
  131. get­Key!
    1. Std.HashMap.get­Key!
  132. get­Key!
    1. Std.TreeMap.get­Key!
  133. get­Key
    1. Std.DHashMap.get­Key
  134. get­Key
    1. Std.DTreeMap.get­Key
  135. get­Key
    1. Std.Ext­DHashMap.get­Key
  136. get­Key
    1. Std.Ext­HashMap.get­Key
  137. get­Key
    1. Std.HashMap.get­Key
  138. get­Key
    1. Std.TreeMap.get­Key
  139. get­Key?
    1. Std.DHashMap.get­Key?
  140. get­Key?
    1. Std.DTreeMap.get­Key?
  141. get­Key?
    1. Std.Ext­DHashMap.get­Key?
  142. get­Key?
    1. Std.Ext­HashMap.get­Key?
  143. get­Key?
    1. Std.HashMap.get­Key?
  144. get­Key?
    1. Std.TreeMap.get­Key?
  145. get­Key­D
    1. Std.DHashMap.get­Key­D
  146. get­Key­D
    1. Std.DTreeMap.get­Key­D
  147. get­Key­D
    1. Std.Ext­DHashMap.get­Key­D
  148. get­Key­D
    1. Std.Ext­HashMap.get­Key­D
  149. get­Key­D
    1. Std.HashMap.get­Key­D
  150. get­Key­D
    1. Std.TreeMap.get­Key­D
  151. get­Key­GE!
    1. Std.TreeMap.get­Key­GE!
  152. get­Key­GE
    1. Std.TreeMap.get­Key­GE
  153. get­Key­GE?
    1. Std.TreeMap.get­Key­GE?
  154. get­Key­GED
    1. Std.TreeMap.get­Key­GED
  155. get­Key­GT!
    1. Std.TreeMap.get­Key­GT!
  156. get­Key­GT
    1. Std.TreeMap.get­Key­GT
  157. get­Key­GT?
    1. Std.TreeMap.get­Key­GT?
  158. get­Key­GTD
    1. Std.TreeMap.get­Key­GTD
  159. get­Key­LE!
    1. Std.TreeMap.get­Key­LE!
  160. get­Key­LE
    1. Std.TreeMap.get­Key­LE
  161. get­Key­LE?
    1. Std.TreeMap.get­Key­LE?
  162. get­Key­LED
    1. Std.TreeMap.get­Key­LED
  163. get­Key­LT!
    1. Std.TreeMap.get­Key­LT!
  164. get­Key­LT
    1. Std.TreeMap.get­Key­LT
  165. get­Key­LT?
    1. Std.TreeMap.get­Key­LT?
  166. get­Key­LTD
    1. Std.TreeMap.get­Key­LTD
  167. get­Kind
    1. Lean.Syntax.get­Kind
  168. get­LE!
    1. Std.TreeSet.get­LE!
  169. get­LE
    1. Std.TreeSet.get­LE
  170. get­LE?
    1. Std.TreeSet.get­LE?
  171. get­LED
    1. Std.TreeSet.get­LED
  172. get­LT!
    1. Std.TreeSet.get­LT!
  173. get­LT
    1. Std.TreeSet.get­LT
  174. get­LT?
    1. Std.TreeSet.get­LT?
  175. get­LTD
    1. Std.TreeSet.get­LTD
  176. get­Lake
    1. Lake.get­Lake
  177. get­Lake­Env
    1. Lake.get­Lake­Env
  178. get­Lake­Home
    1. Lake.get­Lake­Home
  179. get­Lake­Install
    1. Lake.get­Lake­Install
  180. get­Lake­Lib­Dir
    1. Lake.get­Lake­Lib­Dir
  181. get­Lake­Src­Dir
    1. Lake.get­Lake­Src­Dir
  182. get­Last!
    1. List.get­Last!
  183. get­Last
    1. List.get­Last
  184. get­Last?
    1. List.get­Last?
  185. get­Last­D
    1. List.get­Last­D
  186. get­Lean
    1. Lake.get­Lean
  187. get­Lean­Ar
    1. Lake.get­Lean­Ar
  188. get­Lean­Cc
    1. Lake.get­Lean­Cc
  189. get­Lean­Cc?
    1. Lake.get­Lean­Cc?
  190. get­Lean­Include­Dir
    1. Lake.get­Lean­Include­Dir
  191. get­Lean­Install
    1. Lake.get­Lean­Install
  192. get­Lean­Lib­Dir
    1. Lake.get­Lean­Lib­Dir
  193. get­Lean­Path
    1. Lake.get­Lean­Path
  194. get­Lean­Shared­Lib
    1. Lake.get­Lean­Shared­Lib
  195. get­Lean­Src­Dir
    1. Lake.get­Lean­Src­Dir
  196. get­Lean­Src­Path
    1. Lake.get­Lean­Src­Path
  197. get­Lean­Sysroot
    1. Lake.get­Lean­Sysroot
  198. get­Lean­System­Lib­Dir
    1. Lake.get­Lean­System­Lib­Dir
  199. get­Leanc
    1. Lake.get­Leanc
  200. get­Left
    1. Sum.get­Left
  201. get­Left?
    1. Sum.get­Left?
  202. get­Line
    1. IO.FS.Handle.get­Line
  203. get­Line
    1. IO.FS.Stream.get­Line (structure field)
  204. get­Lsb
    1. BitVec.get­Lsb
  205. get­Lsb?
    1. BitVec.get­Lsb?
  206. get­Lsb­D
    1. BitVec.get­Lsb­D
  207. get­M
    1. Option.get­M
  208. get­Max?
    1. Array.get­Max?
  209. get­Modify
  210. get­Msb
    1. BitVec.get­Msb
  211. get­Msb?
    1. BitVec.get­Msb?
  212. get­Msb­D
    1. BitVec.get­Msb­D
  213. get­Name
    1. Lean.TSyntax.get­Name
  214. get­Nat
    1. Lean.TSyntax.get­Nat
  215. get­No­Cache
    1. Lake.get­No­Cache
  216. get­Num­Heartbeats
    1. IO.get­Num­Heartbeats
  217. get­PID
    1. IO.Process.get­PID
  218. get­Pkg­Url­Map
    1. Lake.get­Pkg­Url­Map
  219. get­Random­Bytes
    1. IO.get­Random­Bytes
  220. get­Right
    1. Sum.get­Right
  221. get­Right?
    1. Sum.get­Right?
  222. get­Root­Package
    1. Lake.get­Root­Package
  223. get­Scientific
    1. Lean.TSyntax.get­Scientific
  224. get­Shared­Lib­Path
    1. Lake.get­Shared­Lib­Path
  225. get­Stderr
    1. IO.get­Stderr
  226. get­Stdin
    1. IO.get­Stdin
  227. get­Stdout
    1. IO.get­Stdout
  228. get­String
    1. Lean.TSyntax.get­String
  229. get­TID
    1. IO.get­TID
  230. get­Task­State
    1. IO.get­Task­State
  231. get­The
  232. get­Then­Insert­If­New?
    1. Std.DHashMap.get­Then­Insert­If­New?
  233. get­Then­Insert­If­New?
    1. Std.DTreeMap.get­Then­Insert­If­New?
  234. get­Then­Insert­If­New?
    1. Std.Ext­DHashMap.get­Then­Insert­If­New?
  235. get­Then­Insert­If­New?
    1. Std.Ext­HashMap.get­Then­Insert­If­New?
  236. get­Then­Insert­If­New?
    1. Std.HashMap.get­Then­Insert­If­New?
  237. get­Then­Insert­If­New?
    1. Std.TreeMap.get­Then­Insert­If­New?
  238. get­Try­Cache
    1. Lake.get­Try­Cache
  239. get­UTF8Byte!
    1. String.Slice.get­UTF8Byte!
  240. get­UTF8Byte
    1. String.Slice.get­UTF8Byte
  241. get­UTF8Byte
    1. String.get­UTF8Byte
  242. get­Workspace
    1. Lake.MonadWorkspace.get­Workspace (class method)
  243. get_elem_tactic
  244. get_elem_tactic_trivial
  245. globs
    1. [anonymous] (structure field)
  246. goal
    1. main
  247. grind
  248. ground
    1. Lean.Meta.Simp.Config.ground (structure field)
  249. group
    1. IO.FileRight.group (structure field)
  250. group­By­Key
    1. Array.group­By­Key
  251. group­By­Key
    1. List.group­By­Key
  252. group­Kind
    1. Lean.group­Kind
  253. guard
  254. guard
    1. Option.guard
  255. guard_expr
  256. guard_hyp
  257. guard_msgs.diff
  258. 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. Has­Left­Inverse
    1. Function.Has­Left­Inverse
  36. Has­Right­Inverse
    1. Function.Has­Right­Inverse
  37. Hash­Map
    1. Std.Hash­Map
  38. Hash­Set
    1. Std.Hash­Set
  39. Hashable
  40. Hashable.mk
    1. Instance constructor of Hashable
  41. Homogeneous­Pow
  42. HomogeneousPow.mk
    1. Instance constructor of Homogeneous­Pow
  43. Hygiene­Info
    1. Lean.Syntax.Hygiene­Info
  44. h­Add
    1. HAdd.h­Add (class method)
  45. h­And
    1. HAnd.h­And (class method)
  46. h­Append
    1. HAppend.h­Append (class method)
  47. h­Div
    1. HDiv.h­Div (class method)
  48. h­Iterate
    1. Fin.h­Iterate
  49. h­Iterate­From
    1. Fin.h­Iterate­From
  50. h­Mod
    1. HMod.h­Mod (class method)
  51. h­Mul
    1. HMul.h­Mul (class method)
  52. h­Or
    1. HOr.h­Or (class method)
  53. h­Pow
    1. HPow.h­Pow (class method)
  54. h­Shift­Left
    1. HShiftLeft.h­Shift­Left (class method)
  55. h­Shift­Right
    1. HShiftRight.h­Shift­Right (class method)
  56. h­Sub
    1. HSub.h­Sub (class method)
  57. h­Xor
    1. HXor.h­Xor (class method)
  58. has­Decl
    1. Lean.Macro.has­Decl
  59. has­Finished
    1. IO.has­Finished
  60. has­Next
    1. ByteArray.Iterator.has­Next
  61. has­Next
    1. String.Legacy.Iterator.has­Next
  62. has­Prev
    1. ByteArray.Iterator.has­Prev
  63. has­Prev
    1. String.Legacy.Iterator.has­Prev
  64. hash
    1. BitVec.hash
  65. hash
    1. Hashable.hash (class method)
  66. hash
    1. String.hash
  67. hash_eq
  68. hash_eq
    1. LawfulHashable.hash_eq (class method)
  69. have (0) (1)
  70. have'
  71. head!
    1. List.head!
  72. head
    1. List.head
  73. head?
    1. List.head?
  74. head­D
    1. List.head­D
  75. helim
    1. Subsingleton.helim
  76. heq_of_eq
  77. heq_of_eq­Rec_eq
  78. heq_of_heq_of_eq
  79. hrec­On
    1. Quot.hrec­On
  80. hrec­On
    1. Quotient.hrec­On
  81. hygiene
    1. in tactics
  82. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  83. 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.of­USize
    1. Constructor of ISize
  184. ISize.shift­Left
  185. ISize.shift­Right
  186. ISize.size
  187. ISize.sub
  188. ISize.to­Bit­Vec
  189. ISize.to­Float
  190. ISize.to­Float32
  191. ISize.to­Int
  192. ISize.to­Int16
  193. ISize.to­Int32
  194. ISize.to­Int64
  195. ISize.to­Int8
  196. ISize.to­Nat­Clamp­Neg
  197. ISize.xor
  198. Id
  199. Id.run
  200. Ident
    1. Lean.Syntax.Ident
  201. Iff
  202. Iff.elim
  203. Iff.intro
    1. Constructor of Iff
  204. Inhabited
  205. Inhabited.mk
    1. Instance constructor of Inhabited
  206. Injective
    1. Function.Injective
  207. Int
  208. Int.add
  209. Int.bdiv
  210. Int.bmod
  211. Int.cast
  212. Int.dec­Eq
  213. Int.ediv
  214. Int.emod
  215. Int.fdiv
  216. Int.fmod
  217. Int.gcd
  218. Int.lcm
  219. Int.le
  220. Int.lt
  221. Int.mul
  222. Int.nat­Abs
  223. Int.neg
  224. Int.neg­Of­Nat
  225. Int.neg­Succ
    1. Constructor of Int
  226. Int.not
  227. Int.of­Nat
    1. Constructor of Int
  228. Int.pow
  229. Int.repr
  230. Int.shift­Right
  231. Int.sign
  232. Int.sub
  233. Int.sub­Nat­Nat
  234. Int.tdiv
  235. Int.tmod
  236. Int.to­ISize
  237. Int.to­Int16
  238. Int.to­Int32
  239. Int.to­Int64
  240. Int.to­Int8
  241. Int.to­Nat
  242. Int.to­Nat?
  243. Int16
  244. Int16.abs
  245. Int16.add
  246. Int16.complement
  247. Int16.dec­Eq
  248. Int16.dec­Le
  249. Int16.dec­Lt
  250. Int16.div
  251. Int16.land
  252. Int16.le
  253. Int16.lor
  254. Int16.lt
  255. Int16.max­Value
  256. Int16.min­Value
  257. Int16.mod
  258. Int16.mul
  259. Int16.neg
  260. Int16.of­Bit­Vec
  261. Int16.of­Int
  262. Int16.of­Int­LE
  263. Int16.of­Int­Truncate
  264. Int16.of­Nat
  265. Int16.of­UInt16
    1. Constructor of Int16
  266. Int16.shift­Left
  267. Int16.shift­Right
  268. Int16.size
  269. Int16.sub
  270. Int16.to­Bit­Vec
  271. Int16.to­Float
  272. Int16.to­Float32
  273. Int16.to­ISize
  274. Int16.to­Int
  275. Int16.to­Int32
  276. Int16.to­Int64
  277. Int16.to­Int8
  278. Int16.to­Nat­Clamp­Neg
  279. Int16.xor
  280. Int32
  281. Int32.abs
  282. Int32.add
  283. Int32.complement
  284. Int32.dec­Eq
  285. Int32.dec­Le
  286. Int32.dec­Lt
  287. Int32.div
  288. Int32.land
  289. Int32.le
  290. Int32.lor
  291. Int32.lt
  292. Int32.max­Value
  293. Int32.min­Value
  294. Int32.mod
  295. Int32.mul
  296. Int32.neg
  297. Int32.of­Bit­Vec
  298. Int32.of­Int
  299. Int32.of­Int­LE
  300. Int32.of­Int­Truncate
  301. Int32.of­Nat
  302. Int32.of­UInt32
    1. Constructor of Int32
  303. Int32.shift­Left
  304. Int32.shift­Right
  305. Int32.size
  306. Int32.sub
  307. Int32.to­Bit­Vec
  308. Int32.to­Float
  309. Int32.to­Float32
  310. Int32.to­ISize
  311. Int32.to­Int
  312. Int32.to­Int16
  313. Int32.to­Int64
  314. Int32.to­Int8
  315. Int32.to­Nat­Clamp­Neg
  316. Int32.xor
  317. Int64
  318. Int64.abs
  319. Int64.add
  320. Int64.complement
  321. Int64.dec­Eq
  322. Int64.dec­Le
  323. Int64.dec­Lt
  324. Int64.div
  325. Int64.land
  326. Int64.le
  327. Int64.lor
  328. Int64.lt
  329. Int64.max­Value
  330. Int64.min­Value
  331. Int64.mod
  332. Int64.mul
  333. Int64.neg
  334. Int64.of­Bit­Vec
  335. Int64.of­Int
  336. Int64.of­Int­LE
  337. Int64.of­Int­Truncate
  338. Int64.of­Nat
  339. Int64.of­UInt64
    1. Constructor of Int64
  340. Int64.shift­Left
  341. Int64.shift­Right
  342. Int64.size
  343. Int64.sub
  344. Int64.to­Bit­Vec
  345. Int64.to­Float
  346. Int64.to­Float32
  347. Int64.to­ISize
  348. Int64.to­Int
  349. Int64.to­Int16
  350. Int64.to­Int32
  351. Int64.to­Int8
  352. Int64.to­Nat­Clamp­Neg
  353. Int64.xor
  354. Int8
  355. Int8.abs
  356. Int8.add
  357. Int8.complement
  358. Int8.dec­Eq
  359. Int8.dec­Le
  360. Int8.dec­Lt
  361. Int8.div
  362. Int8.land
  363. Int8.le
  364. Int8.lor
  365. Int8.lt
  366. Int8.max­Value
  367. Int8.min­Value
  368. Int8.mod
  369. Int8.mul
  370. Int8.neg
  371. Int8.of­Bit­Vec
  372. Int8.of­Int
  373. Int8.of­Int­LE
  374. Int8.of­Int­Truncate
  375. Int8.of­Nat
  376. Int8.of­UInt8
    1. Constructor of Int8
  377. Int8.shift­Left
  378. Int8.shift­Right
  379. Int8.size
  380. Int8.sub
  381. Int8.to­Bit­Vec
  382. Int8.to­Float
  383. Int8.to­Float32
  384. Int8.to­ISize
  385. Int8.to­Int
  386. Int8.to­Int16
  387. Int8.to­Int32
  388. Int8.to­Int64
  389. Int8.to­Nat­Clamp­Neg
  390. Int8.xor
  391. Int­Cast
  392. IntCast.mk
    1. Instance constructor of Int­Cast
  393. Int­Interval
    1. Lean.Grind.Int­Interval
  394. Int­Module
    1. Lean.Grind.Int­Module
  395. Is­Char­P
    1. Lean.Grind.Is­Char­P
  396. Is­Infix
    1. List.Is­Infix
  397. Is­Prefix
    1. List.Is­Prefix
  398. Is­Suffix
    1. List.Is­Suffix
  399. Iterator
    1. ByteArray.Iterator
  400. Iterator
    1. String.Legacy.Iterator
  401. i
    1. String.Legacy.Iterator.i (structure field)
  402. id_map
    1. LawfulFunctor.id_map (class method)
  403. ident­Kind
    1. Lean.ident­Kind
  404. identifier
  405. identifier
    1. raw
  406. idx
    1. ByteArray.Iterator.idx (structure field)
  407. idx­Of
    1. Array.idx­Of
  408. idx­Of
    1. List.idx­Of
  409. idx­Of?
    1. Array.idx­Of?
  410. idx­Of?
    1. List.idx­Of?
  411. if ... then ... else ...
  412. if h : ... then ... else ...
  413. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  414. impredicative
  415. inaccessible
  416. inc
    1. String.Pos.Raw.inc
  417. increase­By
    1. String.Pos.Raw.increase­By
  418. ind
    1. Quot.ind
  419. ind
    1. Quotient.ind
  420. ind
    1. Squash.ind
  421. indent­D
    1. Std.Format.indent­D
  422. index
    1. Lean.Meta.DSimp.Config.index (structure field)
  423. index
    1. Lean.Meta.Simp.Config.index (structure field)
  424. index
    1. of inductive type
  425. indexed family
    1. of types
  426. induction
  427. induction
    1. Fin.induction
  428. induction­On
    1. Fin.induction­On
  429. induction­On
    1. Nat.div.induction­On
  430. induction­On
    1. Nat.mod.induction­On
  431. inductive.auto­Promote­Indices
  432. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  433. infer­Instance
  434. infer­Instance­As
  435. infer_instance
  436. inhabited­Left
    1. PSum.inhabited­Left
  437. inhabited­Left
    1. Sum.inhabited­Left
  438. inhabited­Right
    1. PSum.inhabited­Right
  439. inhabited­Right
    1. Sum.inhabited­Right
  440. inherit­Env
    1. IO.Process.SpawnArgs.args (structure field)
  441. init (Lake command)
  442. injection
  443. injections
  444. inner
    1. Std.DHashMap.Equiv.inner (structure field)
  445. inner
    1. Std.DTreeMap.Raw.inner (structure field)
  446. inner
    1. Std.Ext­HashSet.inner (structure field)
  447. inner
    1. Std.HashMap.Equiv.inner (structure field)
  448. inner
    1. Std.HashMap.Raw.inner (structure field)
  449. inner
    1. Std.HashSet.Equiv.inner (structure field)
  450. inner
    1. Std.HashSet.Raw.inner (structure field)
  451. inner
    1. Std.HashSet.inner (structure field)
  452. inner
    1. Std.TreeMap.Raw.inner (structure field)
  453. inner
    1. Std.TreeSet.Raw.inner (structure field)
  454. insert
    1. List.insert
  455. insert
    1. Std.DHashMap.insert
  456. insert
    1. Std.DTreeMap.insert
  457. insert
    1. Std.Ext­DHashMap.insert
  458. insert
    1. Std.Ext­HashMap.insert
  459. insert
    1. Std.Ext­HashSet.insert
  460. insert
    1. Std.HashMap.insert
  461. insert
    1. Std.HashSet.insert
  462. insert
    1. Std.TreeMap.insert
  463. insert
    1. Std.TreeSet.insert
  464. insert­Idx!
    1. Array.insert­Idx!
  465. insert­Idx
    1. Array.insert­Idx
  466. insert­Idx
    1. List.insert­Idx
  467. insert­Idx­If­In­Bounds
    1. Array.insert­Idx­If­In­Bounds
  468. insert­Idx­TR
    1. List.insert­Idx­TR
  469. insert­If­New
    1. Std.DHashMap.insert­If­New
  470. insert­If­New
    1. Std.DTreeMap.insert­If­New
  471. insert­If­New
    1. Std.Ext­DHashMap.insert­If­New
  472. insert­If­New
    1. Std.Ext­HashMap.insert­If­New
  473. insert­If­New
    1. Std.HashMap.insert­If­New
  474. insert­If­New
    1. Std.TreeMap.insert­If­New
  475. insert­Many
    1. Std.DHashMap.insert­Many
  476. insert­Many
    1. Std.DTreeMap.insert­Many
  477. insert­Many
    1. Std.Ext­DHashMap.insert­Many
  478. insert­Many
    1. Std.Ext­HashMap.insert­Many
  479. insert­Many
    1. Std.Ext­HashSet.insert­Many
  480. insert­Many
    1. Std.HashMap.insert­Many
  481. insert­Many
    1. Std.HashSet.insert­Many
  482. insert­Many
    1. Std.TreeMap.insert­Many
  483. insert­Many
    1. Std.TreeSet.insert­Many
  484. insert­Many­If­New­Unit
    1. Std.Ext­HashMap.insert­Many­If­New­Unit
  485. insert­Many­If­New­Unit
    1. Std.HashMap.insert­Many­If­New­Unit
  486. insert­Many­If­New­Unit
    1. Std.TreeMap.insert­Many­If­New­Unit
  487. insertion­Sort
    1. Array.insertion­Sort
  488. instance synthesis
  489. instance
    1. trace.grind.ematch.instance
  490. int­Cast
    1. IntCast.int­Cast (class method)
  491. int­Cast
    1. [anonymous] (class method)
  492. int­Cast_neg
    1. [anonymous] (class method)
  493. int­Cast_of­Nat
    1. [anonymous] (class method)
  494. int­Max
    1. BitVec.int­Max
  495. int­Min
    1. BitVec.int­Min
  496. intercalate
    1. List.intercalate
  497. intercalate
    1. String.intercalate
  498. intercalate­TR
    1. List.intercalate­TR
  499. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  500. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  501. intersperse
    1. List.intersperse
  502. intersperse­TR
    1. List.intersperse­TR
  503. intro (0) (1)
  504. intro | ... => ... | ... => ...
  505. intros
  506. inv­Image
  507. inv_zero
    1. [anonymous] (class method)
  508. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
  509. iota
    1. Lean.Meta.Simp.Config.iota (structure field)
  510. is­Absolute
    1. System.FilePath.is­Absolute
  511. is­Alpha
    1. Char.is­Alpha
  512. is­Alphanum
    1. Char.is­Alphanum
  513. is­Digit
    1. Char.is­Digit
  514. is­Dir
    1. System.FilePath.is­Dir
  515. is­Empty
    1. Array.is­Empty
  516. is­Empty
    1. ByteArray.is­Empty
  517. is­Empty
    1. List.is­Empty
  518. is­Empty
    1. Std.DHashMap.is­Empty
  519. is­Empty
    1. Std.DTreeMap.is­Empty
  520. is­Empty
    1. Std.Ext­DHashMap.is­Empty
  521. is­Empty
    1. Std.Ext­HashMap.is­Empty
  522. is­Empty
    1. Std.Ext­HashSet.is­Empty
  523. is­Empty
    1. Std.Format.is­Empty
  524. is­Empty
    1. Std.HashMap.is­Empty
  525. is­Empty
    1. Std.HashSet.is­Empty
  526. is­Empty
    1. Std.TreeMap.is­Empty
  527. is­Empty
    1. Std.TreeSet.is­Empty
  528. is­Empty
    1. String.Slice.is­Empty
  529. is­Empty
    1. String.is­Empty
  530. is­Empty
    1. Substring.Raw.is­Empty
  531. is­Emscripten
    1. System.Platform.is­Emscripten
  532. is­Eq
    1. Ordering.is­Eq
  533. is­Eq­Some
    1. Option.is­Eq­Some
  534. is­Eqv
    1. Array.is­Eqv
  535. is­Eqv
    1. List.is­Eqv
  536. is­Exclusive­Unsafe
  537. is­Finite
    1. Float.is­Finite
  538. is­Finite
    1. Float32.is­Finite
  539. is­GE
    1. Ordering.is­GE
  540. is­GT
    1. Ordering.is­GT
  541. is­Inf
    1. Float.is­Inf
  542. is­Inf
    1. Float32.is­Inf
  543. is­Int
    1. String.is­Int
  544. is­LE
    1. Ordering.is­LE
  545. is­LT
    1. Ordering.is­LT
  546. is­Left
    1. Sum.is­Left
  547. is­Lower
    1. Char.is­Lower
  548. is­Lt
    1. Fin.is­Lt (structure field)
  549. is­Na­N
    1. Float.is­Na­N
  550. is­Na­N
    1. Float32.is­Na­N
  551. is­Nat
    1. String.Slice.is­Nat
  552. is­Nat
    1. String.is­Nat
  553. is­Nat
    1. Substring.Raw.is­Nat
  554. is­Ne
    1. Ordering.is­Ne
  555. is­Nil
    1. Std.Format.is­Nil
  556. is­None
    1. Option.is­None
  557. is­OSX
    1. System.Platform.is­OSX
  558. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  559. is­Ok
    1. Except.is­Ok
  560. is­Perm
    1. List.is­Perm
  561. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  562. is­Prefix­Of
    1. Array.is­Prefix­Of
  563. is­Prefix­Of
    1. List.is­Prefix­Of
  564. is­Prefix­Of
    1. String.is­Prefix­Of
  565. is­Prefix­Of?
    1. List.is­Prefix­Of?
  566. is­Relative
    1. System.FilePath.is­Relative
  567. is­Resolved
    1. IO.Promise.is­Resolved
  568. is­Right
    1. Sum.is­Right
  569. is­Some
    1. Option.is­Some
  570. is­Sublist
    1. List.is­Sublist
  571. is­Suffix­Of
    1. List.is­Suffix­Of
  572. is­Suffix­Of?
    1. List.is­Suffix­Of?
  573. is­Tty
    1. IO.FS.Handle.is­Tty
  574. is­Tty
    1. IO.FS.Stream.is­Tty (structure field)
  575. is­Upper
    1. Char.is­Upper
  576. is­Valid
    1. String.Pos.Raw.is­Valid
  577. is­Valid
    1. String.ValidPos.is­Valid (structure field)
  578. is­Valid­Char
    1. Nat.is­Valid­Char
  579. is­Valid­Char
    1. UInt32.is­Valid­Char
  580. is­Valid­Char­Nat
    1. Char.is­Valid­Char­Nat
  581. is­Valid­For­Slice
    1. String.Pos.Raw.is­Valid­For­Slice
  582. is­Valid­For­Slice
    1. String.Slice.Pos.is­Valid­For­Slice (structure field)
  583. is­Valid­UTF8
    1. String.is­Valid­UTF8 (structure field)
  584. is­Whitespace
    1. Char.is­Whitespace
  585. is­Windows
    1. System.Platform.is­Windows
  586. iseqv
    1. Setoid.iseqv (class method)
  587. iter
    1. ByteArray.iter
  588. iter
    1. String.Legacy.iter
  589. iterate
  590. iterate
    1. IO.iterate
  591. iunfoldr
    1. BitVec.iunfoldr
  592. iunfoldr_replace
    1. BitVec.iunfoldr_replace

J

  1. join
    1. Option.join
  2. join
    1. Std.Format.join
  3. join
    1. String.join
  4. join
    1. System.FilePath.join
  5. join­Sep
    1. Std.Format.join­Sep
  6. join­Suffix
    1. Std.Format.join­Suffix

K

  1. key­At­Idx!
    1. Std.TreeMap.key­At­Idx!
  2. key­At­Idx
    1. Std.TreeMap.key­At­Idx
  3. key­At­Idx?
    1. Std.TreeMap.key­At­Idx?
  4. key­At­Idx­D
    1. Std.TreeMap.key­At­Idx­D
  5. keys
    1. Std.DHashMap.keys
  6. keys
    1. Std.DTreeMap.keys
  7. keys
    1. Std.HashMap.keys
  8. keys
    1. Std.TreeMap.keys
  9. keys­Array
    1. Std.DHashMap.keys­Array
  10. keys­Array
    1. Std.DTreeMap.keys­Array
  11. keys­Array
    1. Std.HashMap.keys­Array
  12. keys­Array
    1. Std.TreeMap.keys­Array
  13. kill
    1. IO.Process.Child.kill
  14. kleisli­Left
    1. Bind.kleisli­Left
  15. kleisli­Right
    1. Bind.kleisli­Right

L

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

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­Module
    1. Lean.Grind.Nat­Module
  85. Nat­Pow
  86. NatPow.mk
    1. Instance constructor of Nat­Pow
  87. Ne­Zero
  88. NeZero.mk
    1. Instance constructor of Ne­Zero
  89. Neg
  90. Neg.mk
    1. Instance constructor of Neg
  91. New­Goals
    1. Lean.Meta.Rewrite.New­Goals
  92. No­Nat­Zero­Divisors
    1. Lean.Grind.No­Nat­Zero­Divisors
  93. Nodup
    1. List.Nodup
  94. Nonempty
  95. Nonempty.intro
    1. Constructor of Nonempty
  96. Not
  97. Not.elim
  98. Num­Lit
    1. Lean.Syntax.Num­Lit
  99. name
    1. Lean.LeanOption.name (structure field)
  100. name­Lit­Kind
    1. Lean.name­Lit­Kind
  101. namespace
    1. of inductive type
  102. nat­Abs
    1. Int.nat­Abs
  103. nat­Add
    1. Fin.nat­Add
  104. nat­Cast
    1. Lean.Grind.Semiring.to­Mul (class method)
  105. nat­Cast
    1. NatCast.nat­Cast (class method)
  106. native­Facets
    1. [anonymous] (structure field) (0) (1)
  107. native_decide
  108. ndrec
    1. HEq.ndrec
  109. ndrec­On
    1. HEq.ndrec­On
  110. needs
    1. [anonymous] (structure field) (0) (1)
  111. neg
    1. BitVec.neg
  112. neg
    1. Float.neg
  113. neg
    1. Float32.neg
  114. neg
    1. ISize.neg
  115. neg
    1. Int.neg
  116. neg
    1. Int16.neg
  117. neg
    1. Int32.neg
  118. neg
    1. Int64.neg
  119. neg
    1. Int8.neg
  120. neg
    1. Neg.neg (class method)
  121. neg
    1. UInt16.neg
  122. neg
    1. UInt32.neg
  123. neg
    1. UInt64.neg
  124. neg
    1. UInt8.neg
  125. neg
    1. USize.neg
  126. neg­Of­Nat
    1. Int.neg­Of­Nat
  127. neg_add_cancel
    1. [anonymous] (class method)
  128. neg_zsmul
    1. [anonymous] (class method)
  129. nest­D
    1. Std.Format.nest­D
  130. neutral­Config
    1. Lean.Meta.Simp.neutral­Config
  131. new (Lake command)
  132. new
    1. IO.Promise.new
  133. new
    1. Std.Channel.new
  134. new
    1. Std.CloseableChannel.new
  135. new
    1. Std.Condvar.new
  136. new
    1. Std.Mutex.new
  137. new­Goals
    1. Lean.Meta.Rewrite.Config.new­Goals (structure field)
  138. next
  139. next ... => ...
  140. next!
    1. String.Slice.Pos.next!
  141. next!
    1. String.ValidPos.next!
  142. next'
    1. ByteArray.Iterator.next'
  143. next'
    1. String.Legacy.Iterator.next'
  144. next'
    1. String.Pos.Raw.next'
  145. next
    1. ByteArray.Iterator.next
  146. next
    1. RandomGen.next (class method)
  147. next
    1. String.Legacy.Iterator.next
  148. next
    1. String.Pos.Raw.next
  149. next
    1. String.Slice.Pos.next
  150. next
    1. String.ValidPos.next
  151. next
    1. Substring.Raw.next
  152. next?
    1. String.Slice.Pos.next?
  153. next?
    1. String.ValidPos.next?
  154. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  155. next­Until
    1. String.Pos.Raw.next­Until
  156. next­While
    1. String.Pos.Raw.next­While
  157. nextn
    1. ByteArray.Iterator.nextn
  158. nextn
    1. String.Legacy.Iterator.nextn
  159. nextn
    1. String.Slice.Pos.nextn
  160. nextn
    1. Substring.Raw.nextn
  161. nil
    1. BitVec.nil
  162. no_nat_zero_divisors
    1. Lean.Grind.No­Nat­ZeroDivisors.no_nat_zero_divisors (class method)
  163. nofun
  164. nomatch
  165. non­Backtrackable
    1. EStateM.non­Backtrackable
  166. norm_cast (0) (1)
  167. normalize
    1. System.FilePath.normalize
  168. not
    1. BitVec.not
  169. not
    1. Bool.not
  170. not
    1. Int.not
  171. not­M
  172. notify­All
    1. Std.Condvar.notify­All
  173. notify­One
    1. Std.Condvar.notify­One
  174. npow
    1. Lean.Grind.Semiring.of­Nat (class method)
  175. nsmul
    1. Lean.Grind.Semiring.nat­Cast (class method)
  176. nsmul
    1. [anonymous] (class method) (0) (1)
  177. nsmul_eq_nat­Cast_mul
    1. Lean.Grind.Semiring.of­Nat_succ (class method)
  178. null­Kind
    1. Lean.null­Kind
  179. num­Bits
    1. System.Platform.num­Bits
  180. 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.filter­M
  19. Option.for­M
  20. Option.format
  21. Option.get
  22. Option.get!
  23. Option.get­D
  24. Option.get­DM
  25. Option.get­M
  26. Option.guard
  27. Option.is­Eq­Some
  28. Option.is­None
  29. Option.is­Some
  30. Option.join
  31. Option.lt
  32. Option.map
  33. Option.map­A
  34. Option.map­M
  35. Option.max
  36. Option.merge
  37. Option.min
  38. Option.none
    1. Constructor of Option
  39. Option.or
  40. Option.or­Else
  41. Option.pbind
  42. Option.pelim
  43. Option.pmap
  44. Option.repr
  45. Option.sequence
  46. Option.some
    1. Constructor of Option
  47. Option.to­Array
  48. Option.to­List
  49. Option.try­Catch
  50. Option.unattach
  51. Option­T
  52. OptionT.bind
  53. OptionT.fail
  54. OptionT.lift
  55. OptionT.mk
  56. OptionT.or­Else
  57. OptionT.pure
  58. OptionT.run
  59. OptionT.try­Catch
  60. Or
  61. Or.by_cases
  62. Or.by_cases'
  63. Or.inl
    1. Constructor of Or
  64. Or.inr
    1. Constructor of Or
  65. Or­Op
  66. OrOp.mk
    1. Instance constructor of Or­Op
  67. Ord
  68. Ord.lex
  69. Ord.lex'
  70. Ord.mk
    1. Instance constructor of Ord
  71. Ord.on
  72. Ord.opposite
  73. Ord.to­BEq
  74. Ord.to­LE
  75. Ord.to­LT
  76. Ordered­Add
    1. Lean.Grind.Ordered­Add
  77. Ordered­Ring
    1. Lean.Grind.Ordered­Ring
  78. Ordering
  79. Ordering.eq
    1. Constructor of Ordering
  80. Ordering.gt
    1. Constructor of Ordering
  81. Ordering.is­Eq
  82. Ordering.is­GE
  83. Ordering.is­GT
  84. Ordering.is­LE
  85. Ordering.is­LT
  86. Ordering.is­Ne
  87. Ordering.lt
    1. Constructor of Ordering
  88. Ordering.swap
  89. Ordering.then
  90. Output
    1. IO.Process.Output
  91. obtain
  92. occs
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  93. of­Array
    1. Std.Ext­HashSet.of­Array
  94. of­Array
    1. Std.HashSet.of­Array
  95. of­Array
    1. Std.TreeMap.of­Array
  96. of­Array
    1. Std.TreeSet.of­Array
  97. of­Binary­Scientific
    1. Float.of­Binary­Scientific
  98. of­Binary­Scientific
    1. Float32.of­Binary­Scientific
  99. of­Bit­Vec
    1. ISize.of­Bit­Vec
  100. of­Bit­Vec
    1. Int16.of­Bit­Vec
  101. of­Bit­Vec
    1. Int32.of­Bit­Vec
  102. of­Bit­Vec
    1. Int64.of­Bit­Vec
  103. of­Bit­Vec
    1. Int8.of­Bit­Vec
  104. of­Bits
    1. Float.of­Bits
  105. of­Bits
    1. Float32.of­Bits
  106. of­Bool
    1. BitVec.of­Bool
  107. of­Bool­List­BE
    1. BitVec.of­Bool­List­BE
  108. of­Bool­List­LE
    1. BitVec.of­Bool­List­LE
  109. of­Buffer
    1. IO.FS.Stream.of­Buffer
  110. of­Byte­Array
    1. ByteSlice.of­Byte­Array
  111. of­Copy
    1. String.ValidPos.of­Copy
  112. of­Except
    1. IO.of­Except
  113. of­Except
    1. MonadExcept.of­Except
  114. of­Fin
    1. UInt16.of­Fin
  115. of­Fin
    1. UInt32.of­Fin
  116. of­Fin
    1. UInt64.of­Fin
  117. of­Fin
    1. UInt8.of­Fin
  118. of­Fin
    1. USize.of­Fin
  119. of­Fn
    1. Array.of­Fn
  120. of­Fn
    1. List.of­Fn
  121. of­Handle
    1. IO.FS.Stream.of­Handle
  122. of­Int
    1. BitVec.of­Int
  123. of­Int
    1. Float.of­Int
  124. of­Int
    1. Float32.of­Int
  125. of­Int
    1. ISize.of­Int
  126. of­Int
    1. Int16.of­Int
  127. of­Int
    1. Int32.of­Int
  128. of­Int
    1. Int64.of­Int
  129. of­Int
    1. Int8.of­Int
  130. of­Int­LE
    1. ISize.of­Int­LE
  131. of­Int­LE
    1. Int16.of­Int­LE
  132. of­Int­LE
    1. Int32.of­Int­LE
  133. of­Int­LE
    1. Int64.of­Int­LE
  134. of­Int­LE
    1. Int8.of­Int­LE
  135. of­Int­Truncate
    1. ISize.of­Int­Truncate
  136. of­Int­Truncate
    1. Int16.of­Int­Truncate
  137. of­Int­Truncate
    1. Int32.of­Int­Truncate
  138. of­Int­Truncate
    1. Int64.of­Int­Truncate
  139. of­Int­Truncate
    1. Int8.of­Int­Truncate
  140. of­List
    1. Std.DHashMap.of­List
  141. of­List
    1. Std.DTreeMap.of­List
  142. of­List
    1. Std.Ext­DHashMap.of­List
  143. of­List
    1. Std.Ext­HashMap.of­List
  144. of­List
    1. Std.Ext­HashSet.of­List
  145. of­List
    1. Std.HashMap.of­List
  146. of­List
    1. Std.HashSet.of­List
  147. of­List
    1. Std.TreeMap.of­List
  148. of­List
    1. Std.TreeSet.of­List
  149. of­List
    1. String.of­List
  150. of­Nat
    1. BitVec.of­Nat
  151. of­Nat
    1. Char.of­Nat
  152. of­Nat
    1. Fin.of­Nat
  153. of­Nat
    1. Float.of­Nat
  154. of­Nat
    1. Float32.of­Nat
  155. of­Nat
    1. ISize.of­Nat
  156. of­Nat
    1. Int16.of­Nat
  157. of­Nat
    1. Int32.of­Nat
  158. of­Nat
    1. Int64.of­Nat
  159. of­Nat
    1. Int8.of­Nat
  160. of­Nat
    1. OfNat.of­Nat (class method)
  161. of­Nat
    1. UInt16.of­Nat
  162. of­Nat
    1. UInt32.of­Nat
  163. of­Nat
    1. UInt64.of­Nat
  164. of­Nat
    1. UInt8.of­Nat
  165. of­Nat
    1. USize.of­Nat
  166. of­Nat
    1. [anonymous] (class method)
  167. of­Nat32
    1. USize.of­Nat32
  168. of­Nat­LT
    1. BitVec.of­Nat­LT
  169. of­Nat­LT
    1. UInt16.of­Nat­LT
  170. of­Nat­LT
    1. UInt32.of­Nat­LT
  171. of­Nat­LT
    1. UInt64.of­Nat­LT
  172. of­Nat­LT
    1. UInt8.of­Nat­LT
  173. of­Nat­LT
    1. USize.of­Nat­LT
  174. of­Nat­Truncate
    1. UInt16.of­Nat­Truncate
  175. of­Nat­Truncate
    1. UInt32.of­Nat­Truncate
  176. of­Nat­Truncate
    1. UInt64.of­Nat­Truncate
  177. of­Nat­Truncate
    1. UInt8.of­Nat­Truncate
  178. of­Nat­Truncate
    1. USize.of­Nat­Truncate
  179. of­Nat_eq_nat­Cast
    1. Lean.Grind.Semiring.pow_succ (class method)
  180. of­Nat_ext_iff
    1. Lean.Grind.Is­CharP.of­Nat_ext_iff (class method)
  181. of­Nat_succ
    1. Lean.Grind.Semiring.pow_zero (class method)
  182. of­Replace­Start
    1. String.Slice.Pos.of­Replace­Start
  183. of­Scientific
    1. Float.of­Scientific
  184. of­Scientific
    1. Float32.of­Scientific
  185. of­Scientific
    1. OfScientific.of­Scientific (class method)
  186. of­Slice
    1. String.Slice.Pos.of­Slice
  187. of­Subarray
    1. Array.of­Subarray
  188. of­UInt8
    1. Char.of­UInt8
  189. offset
    1. String.Slice.Pos.offset (structure field)
  190. offset
    1. String.ValidPos.offset (structure field)
  191. offset­By
    1. String.Pos.Raw.offset­By
  192. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  193. offset­Of­Pos
    1. String.Pos.Raw.offset­Of­Pos
  194. omega
  195. on
    1. Ord.on
  196. one_mul
    1. Lean.Grind.Semiring.mul_assoc (class method)
  197. one_zsmul
    1. [anonymous] (class method)
  198. open
  199. opposite
    1. Ord.opposite
  200. opt­Param
  201. optional
  202. or
    1. BitVec.or
  203. or
    1. Bool.or
  204. or
    1. List.or
  205. or
    1. Option.or
  206. or
    1. OrOp.or (class method)
  207. or­Else'
    1. EStateM.or­Else'
  208. or­Else
    1. EStateM.or­Else
  209. or­Else
    1. MonadExcept.or­Else
  210. or­Else
    1. Option.or­Else
  211. or­Else
    1. OptionT.or­Else
  212. or­Else
    1. ReaderT.or­Else
  213. or­Else
    1. StateT.or­Else
  214. or­Else
    1. [anonymous] (class method)
  215. or­Else­Lazy
    1. Except.or­Else­Lazy
  216. or­M
  217. orelse'
    1. MonadExcept.orelse'
  218. other
    1. IO.FileRight.other (structure field)
  219. out
    1. NeZero.out (class method)
  220. out
    1. Std.DTreeMap.Raw.WF.out (structure field)
  221. out
    1. Std.HashMap.Raw.WF.out (structure field)
  222. out
    1. Std.HashSet.Raw.WF.out (structure field)
  223. out
    1. Std.TreeMap.Raw.WF.out (structure field)
  224. out
    1. Std.TreeSet.Raw.WF.out (structure field)
  225. out­Param
  226. output
    1. IO.Process.output
  227. override list (Elan command)
  228. override set (Elan command)
  229. 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.Slice.Pos
  20. Pow
  21. Pow.mk
    1. Instance constructor of Pow
  22. Prec
    1. Lean.Syntax.Prec
  23. Pred­Trans
    1. Std.Do.Pred­Trans
  24. Preresolved
    1. Lean.Syntax.Preresolved
  25. Prio
    1. Lean.Syntax.Prio
  26. Priority
    1. Task.Priority
  27. Prod
  28. Prod.all­I
  29. Prod.any­I
  30. Prod.fold­I
  31. Prod.lex­Lt
  32. Prod.map
  33. Prod.mk
    1. Constructor of Prod
  34. Prod.swap
  35. Promise
    1. IO.Promise
  36. Prop
  37. Pure
  38. Pure.mk
    1. Instance constructor of Pure
  39. pack (Lake command)
  40. parameter
    1. of inductive type
  41. paren
    1. Std.Format.paren
  42. parent
    1. System.FilePath.parent
  43. parser
  44. partition
    1. Array.partition
  45. partition
    1. List.partition
  46. partition
    1. Std.DHashMap.partition
  47. partition
    1. Std.DTreeMap.partition
  48. partition
    1. Std.HashMap.partition
  49. partition
    1. Std.HashSet.partition
  50. partition
    1. Std.TreeMap.partition
  51. partition
    1. Std.TreeSet.partition
  52. partition­M
    1. List.partition­M
  53. partition­Map
    1. List.partition­Map
  54. path
    1. IO.FS.DirEntry.path
  55. path­Exists
    1. System.FilePath.path­Exists
  56. path­Separator
    1. System.FilePath.path­Separator
  57. path­Separators
    1. System.FilePath.path­Separators
  58. pattern
  59. pbind
    1. Option.pbind
  60. pelim
    1. Option.pelim
  61. placeholder term
  62. pmap
    1. Array.pmap
  63. pmap
    1. List.pmap
  64. pmap
    1. Option.pmap
  65. polymorphism
    1. universe
  66. pop
    1. Array.pop
  67. pop­Front
    1. Subarray.pop­Front
  68. pop­While
    1. Array.pop­While
  69. pos!
    1. String.Slice.pos!
  70. pos!
    1. String.pos!
  71. pos
    1. ByteArray.Iterator.pos
  72. pos
    1. IO.FS.Stream.Buffer.pos (structure field)
  73. pos
    1. String.Legacy.Iterator.pos
  74. pos
    1. String.Slice.pos
  75. pos
    1. String.pos
  76. pos?
    1. String.Slice.pos?
  77. pos?
    1. String.pos?
  78. pos­Of
    1. String.pos­Of
  79. pos­Of
    1. Substring.Raw.pos­Of
  80. positions
    1. String.Slice.positions
  81. pow
    1. Float.pow
  82. pow
    1. Float32.pow
  83. pow
    1. HomogeneousPow.pow (class method)
  84. pow
    1. Int.pow
  85. pow
    1. Nat.pow
  86. pow
    1. NatPow.pow (class method)
  87. pow
    1. Pow.pow (class method)
  88. pow_succ
    1. Lean.Grind.Semiring.mul_zero (class method)
  89. pow_zero
    1. Lean.Grind.Semiring.zero_mul (class method)
  90. pp
    1. eval.pp
  91. pp.deep­Terms
  92. pp.deepTerms.threshold
  93. pp.field­Notation
  94. pp.match
  95. pp.max­Steps
  96. pp.mvars
  97. pp.proofs
  98. pp.proofs.threshold
  99. precompile­Modules
    1. [anonymous] (structure field)
  100. pred
    1. Fin.pred
  101. pred
    1. Nat.pred
  102. predicative
  103. prefix­Join
    1. Std.Format.prefix­Join
  104. pretty
    1. Std.Format.pretty
  105. pretty­M
    1. Std.Format.pretty­M
  106. prev!
    1. String.Slice.Pos.prev!
  107. prev!
    1. String.ValidPos.prev!
  108. prev
    1. ByteArray.Iterator.prev
  109. prev
    1. String.Legacy.Iterator.prev
  110. prev
    1. String.Pos.Raw.prev
  111. prev
    1. String.Slice.Pos.prev
  112. prev
    1. String.ValidPos.prev
  113. prev
    1. Substring.Raw.prev
  114. prev?
    1. String.Slice.Pos.prev?
  115. prev?
    1. String.ValidPos.prev?
  116. prevn
    1. ByteArray.Iterator.prevn
  117. prevn
    1. String.Legacy.Iterator.prevn
  118. prevn
    1. String.Slice.Pos.prevn
  119. prevn
    1. Substring.Raw.prevn
  120. print
    1. IO.print
  121. println
    1. IO.println
  122. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
  123. proj
    1. Lean.Meta.Simp.Config.proj (structure field)
  124. proof state
  125. proofs
    1. pp.proofs
  126. property
    1. Subtype.property (structure field)
  127. propext
  128. proposition
  129. proposition
    1. decidable
  130. ptr­Addr­Unsafe
  131. ptr­Eq
  132. ptr­Eq
    1. ST.Ref.ptr­Eq
  133. ptr­Eq­List
  134. pure
    1. EStateM.pure
  135. pure
    1. Except.pure
  136. pure
    1. ExceptT.pure
  137. pure
    1. OptionT.pure
  138. pure
    1. Pure.pure (class method)
  139. pure
    1. ReaderT.pure
  140. pure
    1. StateT.pure
  141. pure
    1. Task.pure
  142. pure
    1. Thunk.pure
  143. pure_bind
    1. [anonymous] (class method)
  144. pure_seq
    1. [anonymous] (class method)
  145. push
    1. Array.push
  146. push
    1. ByteArray.push
  147. push
    1. String.push
  148. push­Newline
    1. Std.Format.Monad­PrettyFormat.push­Newline (class method)
  149. push­Output
    1. Std.Format.Monad­PrettyFormat.push­Output (class method)
  150. push_cast
  151. pushn
    1. String.pushn
  152. put­Str
    1. IO.FS.Handle.put­Str
  153. put­Str
    1. IO.FS.Stream.put­Str (structure field)
  154. put­Str­Ln
    1. IO.FS.Handle.put­Str­Ln
  155. 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. Raw
    1. Std.DHashMap.Raw
  4. Raw
    1. Std.DTreeMap.Raw
  5. Raw
    1. Std.HashMap.Raw
  6. Raw
    1. Std.HashSet.Raw
  7. Raw
    1. Std.TreeMap.Raw
  8. Raw
    1. Std.TreeSet.Raw
  9. Raw
    1. String.Pos.Raw
  10. Raw
    1. Substring.Raw
  11. Reader­M
  12. Reader­T
  13. ReaderT.adapt
  14. ReaderT.bind
  15. ReaderT.failure
  16. ReaderT.or­Else
  17. ReaderT.pure
  18. ReaderT.read
  19. ReaderT.run
  20. Ref
    1. IO.Ref
  21. Ref
    1. ST.Ref
  22. Refl­BEq
  23. ReflBEq.mk
    1. Instance constructor of Refl­BEq
  24. Repr
  25. Repr.add­App­Paren
  26. Repr.mk
    1. Instance constructor of Repr
  27. Repr­Atom
  28. ReprAtom.mk
    1. Instance constructor of Repr­Atom
  29. Result
    1. EStateM.Result
  30. Right­Inverse
    1. Function.Right­Inverse
  31. Ring
    1. Lean.Grind.Ring
  32. r
    1. Setoid.r (class method)
  33. rand
    1. IO.rand
  34. rand­Bool
  35. rand­Nat
  36. range'
    1. Array.range'
  37. range'
    1. List.range'
  38. range'TR
    1. List.range'TR
  39. range
    1. Array.range
  40. range
    1. List.range
  41. range
    1. RandomGen.range (class method)
  42. raw
    1. Lean.TSyntax.raw (structure field)
  43. raw­End­Pos
    1. String.Slice.raw­End­Pos
  44. raw­End­Pos
    1. String.raw­End­Pos
  45. rcases
  46. read
    1. IO.AccessRight.read (structure field)
  47. read
    1. IO.FS.Handle.read
  48. read
    1. IO.FS.Stream.read (structure field)
  49. read
    1. MonadReader.read (class method)
  50. read
    1. Monad­ReaderOf.read (class method)
  51. read
    1. ReaderT.read
  52. read­Bin­File
    1. IO.FS.read­Bin­File
  53. read­Bin­To­End
    1. IO.FS.Handle.read­Bin­To­End
  54. read­Bin­To­End­Into
    1. IO.FS.Handle.read­Bin­To­End­Into
  55. read­Dir
    1. System.FilePath.read­Dir
  56. read­File
    1. IO.FS.read­File
  57. read­The
  58. read­To­End
    1. IO.FS.Handle.read­To­End
  59. real­Path
    1. IO.FS.real­Path
  60. rec
    1. Quot.rec
  61. rec
    1. Quotient.rec
  62. rec­Aux
    1. Nat.rec­Aux
  63. rec­On
    1. Quot.rec­On
  64. rec­On
    1. Quotient.rec­On
  65. rec­On­Subsingleton
    1. Quot.rec­On­Subsingleton
  66. rec­On­Subsingleton
    1. Quotient.rec­On­Subsingleton
  67. rec­On­Subsingleton₂
    1. Quotient.rec­On­Subsingleton₂
  68. recursor
  69. recv
    1. Std.Channel.recv
  70. reduce
  71. reduction
    1. ι (iota)
  72. refine
  73. refine'
  74. refl
    1. Equivalence.refl (structure field)
  75. refl
    1. Setoid.refl
  76. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  77. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  78. rel
    1. Lean.Order.PartialOrder.rel (class method)
  79. rel
    1. Well­FoundedRelation.rel (class method)
  80. rel_antisymm
    1. Lean.Order.PartialOrder.rel_antisymm (class method)
  81. rel_refl
    1. Lean.Order.PartialOrder.rel_refl (class method)
  82. rel_trans
    1. Lean.Order.PartialOrder.rel_trans (class method)
  83. relaxed­Auto­Implicit
  84. remaining­Bytes
    1. ByteArray.Iterator.remaining­Bytes
  85. remaining­Bytes
    1. String.Legacy.Iterator.remaining­Bytes
  86. remaining­To­String
    1. String.Legacy.Iterator.remaining­To­String
  87. remove­All
    1. List.remove­All
  88. remove­Dir
    1. IO.FS.remove­Dir
  89. remove­Dir­All
    1. IO.FS.remove­Dir­All
  90. remove­File
    1. IO.FS.remove­File
  91. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  92. rename
  93. rename
    1. IO.FS.rename
  94. rename_i
  95. repair
    1. Substring.Raw.repair
  96. repeat (0) (1)
  97. repeat'
  98. repeat
    1. Nat.repeat
  99. repeat1'
  100. repeat­TR
    1. Nat.repeat­TR
  101. replace
  102. replace
    1. Array.replace
  103. replace
    1. List.replace
  104. replace
    1. String.replace
  105. replace­End
    1. String.Slice.replace­End
  106. replace­End
    1. String.replace­End
  107. replace­Start
    1. String.Slice.replace­Start
  108. replace­Start
    1. String.replace­Start
  109. replace­Start­End!
    1. String.Slice.replace­Start­End!
  110. replace­Start­End
    1. String.Slice.replace­Start­End
  111. replace­TR
    1. List.replace­TR
  112. replicate
    1. Array.replicate
  113. replicate
    1. BitVec.replicate
  114. replicate
    1. List.replicate
  115. replicate­TR
    1. List.replicate­TR
  116. repr
  117. repr
    1. Int.repr
  118. repr
    1. Nat.repr
  119. repr
    1. Option.repr
  120. repr
    1. USize.repr
  121. repr
    1. eval.derive.repr
  122. repr­Arg
  123. repr­Prec
    1. Repr.repr­Prec (class method)
  124. repr­Str
  125. resolve
    1. IO.Promise.resolve
  126. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  127. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  128. restore
    1. EStateM.Backtrackable.restore (class method)
  129. restore­M
    1. MonadControl.restore­M (class method)
  130. restore­M
    1. Monad­ControlT.restore­M (class method)
  131. result!
    1. IO.Promise.result!
  132. result
    1. trace.compiler.ir.result
  133. result?
    1. IO.Promise.result?
  134. result­D
    1. IO.Promise.result­D
  135. rev
    1. Fin.rev
  136. rev­Bytes
    1. String.Slice.rev­Bytes
  137. rev­Chars
    1. String.Slice.rev­Chars
  138. rev­Find
    1. String.rev­Find
  139. rev­Find?
    1. String.Slice.rev­Find?
  140. rev­Pos­Of
    1. String.rev­Pos­Of
  141. rev­Positions
    1. String.Slice.rev­Positions
  142. rev­Split
    1. String.Slice.rev­Split
  143. reverse
    1. Array.reverse
  144. reverse
    1. BitVec.reverse
  145. reverse
    1. List.reverse
  146. reverse­Induction
    1. Fin.reverse­Induction
  147. revert
  148. rewind
    1. IO.FS.Handle.rewind
  149. rewrite (0) (1)
  150. rewrite
    1. trace.Meta.Tactic.simp.rewrite
  151. rfl (0) (1) (2)
  152. rfl'
  153. rfl
    1. HEq.rfl
  154. rfl
    1. ReflBEq.rfl (class method)
  155. rhs
  156. right (0) (1)
  157. right
    1. And.right (structure field)
  158. right_distrib
    1. Lean.Grind.Semiring.one_mul (class method)
  159. rightpad
    1. Array.rightpad
  160. rightpad
    1. List.rightpad
  161. rintro
  162. root
    1. IO.FS.DirEntry.root (structure field)
  163. root
    1. [anonymous] (structure field)
  164. roots
    1. [anonymous] (structure field)
  165. rotate­Left
    1. BitVec.rotate­Left
  166. rotate­Left
    1. List.rotate­Left
  167. rotate­Right
    1. BitVec.rotate­Right
  168. rotate­Right
    1. List.rotate­Right
  169. rotate_left
  170. rotate_right
  171. round
    1. Float.round
  172. round
    1. Float32.round
  173. run (Elan command)
  174. run'
    1. EStateM.run'
  175. run'
    1. State­CpsT.run'
  176. run'
    1. State­RefT'.run'
  177. run'
    1. StateT.run'
  178. run
    1. EStateM.run
  179. run
    1. Except­CpsT.run
  180. run
    1. ExceptT.run
  181. run
    1. IO.Process.run
  182. run
    1. Id.run
  183. run
    1. OptionT.run
  184. run
    1. ReaderT.run
  185. run
    1. State­CpsT.run
  186. run
    1. State­RefT'.run
  187. run
    1. StateT.run
  188. run­Catch
    1. Except­CpsT.run­Catch
  189. run­EST
  190. run­K
    1. Except­CpsT.run­K
  191. run­K
    1. State­CpsT.run­K
  192. run­ST
  193. run_tac
  194. rw (0) (1)
  195. rw?
  196. rw_mod_cast
  197. rwa

S

  1. SMul
  2. SMul.mk
    1. Instance constructor of SMul
  3. SPred
    1. Std.Do.SPred
  4. ST
  5. ST.Ref
  6. ST.Ref.get
  7. ST.Ref.mk
    1. Constructor of ST.Ref
  8. ST.Ref.modify
  9. ST.Ref.modify­Get
  10. ST.Ref.ptr­Eq
  11. ST.Ref.set
  12. ST.Ref.swap
  13. ST.Ref.take
  14. ST.Ref.to­Monad­State­Of
  15. ST.mk­Ref
  16. STWorld
  17. STWorld.mk
    1. Instance constructor of STWorld
  18. Scientific­Lit
    1. Lean.Syntax.Scientific­Lit
  19. Script­M
    1. Lake.Script­M (0) (1)
  20. Semiring
    1. Lean.Grind.Semiring
  21. Seq
  22. Seq.mk
    1. Instance constructor of Seq
  23. Seq­Left
  24. SeqLeft.mk
    1. Instance constructor of Seq­Left
  25. Seq­Right
  26. SeqRight.mk
    1. Instance constructor of Seq­Right
  27. Setoid
  28. Setoid.mk
    1. Instance constructor of Setoid
  29. Setoid.refl
  30. Setoid.symm
  31. Setoid.trans
  32. Shift­Left
  33. ShiftLeft.mk
    1. Instance constructor of Shift­Left
  34. Shift­Right
  35. ShiftRight.mk
    1. Instance constructor of Shift­Right
  36. Sigma
  37. Sigma.mk
    1. Constructor of Sigma
  38. Simp­Extension
    1. Lean.Meta.Simp­Extension
  39. Size­Of
  40. SizeOf.mk
    1. Instance constructor of Size­Of
  41. Slice
    1. String.Slice
  42. Sort
  43. Source­Info
    1. Lean.Source­Info
  44. Spawn­Args
    1. IO.Process.Spawn­Args
  45. Squash
  46. Squash.ind
  47. Squash.lift
  48. Squash.mk
  49. State­Cps­T
  50. State­CpsT.lift
  51. State­CpsT.run
  52. State­CpsT.run'
  53. State­CpsT.run­K
  54. State­M
  55. State­Ref­T'
  56. State­RefT'.get
  57. State­RefT'.lift
  58. State­RefT'.modify­Get
  59. State­RefT'.run
  60. State­RefT'.run'
  61. State­RefT'.set
  62. State­T
  63. StateT.bind
  64. StateT.failure
  65. StateT.get
  66. StateT.lift
  67. StateT.map
  68. StateT.modify­Get
  69. StateT.or­Else
  70. StateT.pure
  71. StateT.run
  72. StateT.run'
  73. StateT.set
  74. Std.Atomic­T
  75. Std.Channel
  76. Std.Channel.Sync
  77. Std.Channel.for­Async
  78. Std.Channel.new
  79. Std.Channel.recv
  80. Std.Channel.send
  81. Std.Channel.sync
  82. Std.Closeable­Channel
  83. Std.CloseableChannel.new
  84. Std.Condvar
  85. Std.Condvar.new
  86. Std.Condvar.notify­All
  87. Std.Condvar.notify­One
  88. Std.Condvar.wait
  89. Std.Condvar.wait­Until
  90. Std.DHash­Map
  91. Std.DHashMap.Equiv
  92. Std.DHashMap.Equiv.mk
    1. Constructor of Std.DHashMap.Equiv
  93. Std.DHashMap.Raw
  94. Std.DHashMap.Raw.WF
  95. Std.DHashMap.Raw.WF.alter₀
    1. Constructor of Std.DHashMap.Raw.WF
  96. Std.DHashMap.Raw.WF.const­Alter₀
    1. Constructor of Std.DHashMap.Raw.WF
  97. Std.DHashMap.Raw.WF.const­Get­Then­Insert­If­New?₀
    1. Constructor of Std.DHashMap.Raw.WF
  98. Std.DHashMap.Raw.WF.const­Modify₀
    1. Constructor of Std.DHashMap.Raw.WF
  99. Std.DHashMap.Raw.WF.contains­Then­Insert­If­New₀
    1. Constructor of Std.DHashMap.Raw.WF
  100. Std.DHashMap.Raw.WF.contains­Then­Insert₀
    1. Constructor of Std.DHashMap.Raw.WF
  101. Std.DHashMap.Raw.WF.empty­With­Capacity₀
    1. Constructor of Std.DHashMap.Raw.WF
  102. Std.DHashMap.Raw.WF.erase₀
    1. Constructor of Std.DHashMap.Raw.WF
  103. Std.DHashMap.Raw.WF.filter₀
    1. Constructor of Std.DHashMap.Raw.WF
  104. Std.DHashMap.Raw.WF.get­Then­Insert­If­New?₀
    1. Constructor of Std.DHashMap.Raw.WF
  105. Std.DHashMap.Raw.WF.insert­If­New₀
    1. Constructor of Std.DHashMap.Raw.WF
  106. Std.DHashMap.Raw.WF.insert₀
    1. Constructor of Std.DHashMap.Raw.WF
  107. Std.DHashMap.Raw.WF.inter₀
    1. Constructor of Std.DHashMap.Raw.WF
  108. Std.DHashMap.Raw.WF.modify₀
    1. Constructor of Std.DHashMap.Raw.WF
  109. Std.DHashMap.Raw.WF.wf
    1. Constructor of Std.DHashMap.Raw.WF
  110. Std.DHashMap.Raw.mk
    1. Constructor of Std.DHashMap.Raw
  111. Std.DHashMap.alter
  112. Std.DHashMap.contains
  113. Std.DHashMap.contains­Then­Insert
  114. Std.DHashMap.contains­Then­Insert­If­New
  115. Std.DHashMap.empty­With­Capacity
  116. Std.DHashMap.erase
  117. Std.DHashMap.filter
  118. Std.DHashMap.filter­Map
  119. Std.DHashMap.fold
  120. Std.DHashMap.fold­M
  121. Std.DHashMap.for­In
  122. Std.DHashMap.for­M
  123. Std.DHashMap.get
  124. Std.DHashMap.get!
  125. Std.DHashMap.get?
  126. Std.DHashMap.get­D
  127. Std.DHashMap.get­Key
  128. Std.DHashMap.get­Key!
  129. Std.DHashMap.get­Key?
  130. Std.DHashMap.get­Key­D
  131. Std.DHashMap.get­Then­Insert­If­New?
  132. Std.DHashMap.insert
  133. Std.DHashMap.insert­If­New
  134. Std.DHashMap.insert­Many
  135. Std.DHashMap.is­Empty
  136. Std.DHashMap.keys
  137. Std.DHashMap.keys­Array
  138. Std.DHashMap.map
  139. Std.DHashMap.modify
  140. Std.DHashMap.of­List
  141. Std.DHashMap.partition
  142. Std.DHashMap.size
  143. Std.DHashMap.to­Array
  144. Std.DHashMap.to­List
  145. Std.DHashMap.union
  146. Std.DHashMap.values
  147. Std.DHashMap.values­Array
  148. Std.DTree­Map
  149. Std.DTreeMap.Raw
  150. Std.DTreeMap.Raw.WF
  151. Std.DTreeMap.Raw.WF.mk
    1. Constructor of Std.DTreeMap.Raw.WF
  152. Std.DTreeMap.Raw.mk
    1. Constructor of Std.DTreeMap.Raw
  153. Std.DTreeMap.alter
  154. Std.DTreeMap.contains
  155. Std.DTreeMap.contains­Then­Insert
  156. Std.DTreeMap.contains­Then­Insert­If­New
  157. Std.DTreeMap.empty
  158. Std.DTreeMap.erase
  159. Std.DTreeMap.filter
  160. Std.DTreeMap.filter­Map
  161. Std.DTreeMap.foldl
  162. Std.DTreeMap.foldl­M
  163. Std.DTreeMap.for­In
  164. Std.DTreeMap.for­M
  165. Std.DTreeMap.get
  166. Std.DTreeMap.get!
  167. Std.DTreeMap.get?
  168. Std.DTreeMap.get­D
  169. Std.DTreeMap.get­Key
  170. Std.DTreeMap.get­Key!
  171. Std.DTreeMap.get­Key?
  172. Std.DTreeMap.get­Key­D
  173. Std.DTreeMap.get­Then­Insert­If­New?
  174. Std.DTreeMap.insert
  175. Std.DTreeMap.insert­If­New
  176. Std.DTreeMap.insert­Many
  177. Std.DTreeMap.is­Empty
  178. Std.DTreeMap.keys
  179. Std.DTreeMap.keys­Array
  180. Std.DTreeMap.map
  181. Std.DTreeMap.modify
  182. Std.DTreeMap.of­List
  183. Std.DTreeMap.partition
  184. Std.DTreeMap.size
  185. Std.DTreeMap.to­Array
  186. Std.DTreeMap.to­List
  187. Std.DTreeMap.values
  188. Std.DTreeMap.values­Array
  189. Std.Do.Pred­Trans
  190. Std.Do.PredTrans.mk
    1. Constructor of Std.Do.Pred­Trans
  191. Std.Do.SPred
  192. Std.Do.SPred.entails
  193. Std.Do.WP
  194. Std.Do.WP.mk
    1. Instance constructor of Std.Do.WP
  195. Std.Do.WPMonad
  196. Std.Do.WPMonad.mk
    1. Instance constructor of Std.Do.WPMonad
  197. Std.Ext­DHash­Map
  198. Std.Ext­DHashMap.alter
  199. Std.Ext­DHashMap.contains
  200. Std.Ext­DHashMap.contains­Then­Insert
  201. Std.Ext­DHashMap.contains­Then­Insert­If­New
  202. Std.Ext­DHashMap.empty­With­Capacity
  203. Std.Ext­DHashMap.erase
  204. Std.Ext­DHashMap.filter
  205. Std.Ext­DHashMap.filter­Map
  206. Std.Ext­DHashMap.get
  207. Std.Ext­DHashMap.get!
  208. Std.Ext­DHashMap.get?
  209. Std.Ext­DHashMap.get­D
  210. Std.Ext­DHashMap.get­Key
  211. Std.Ext­DHashMap.get­Key!
  212. Std.Ext­DHashMap.get­Key?
  213. Std.Ext­DHashMap.get­Key­D
  214. Std.Ext­DHashMap.get­Then­Insert­If­New?
  215. Std.Ext­DHashMap.insert
  216. Std.Ext­DHashMap.insert­If­New
  217. Std.Ext­DHashMap.insert­Many
  218. Std.Ext­DHashMap.is­Empty
  219. Std.Ext­DHashMap.map
  220. Std.Ext­DHashMap.modify
  221. Std.Ext­DHashMap.of­List
  222. Std.Ext­DHashMap.size
  223. Std.Ext­Hash­Map
  224. Std.Ext­HashMap.alter
  225. Std.Ext­HashMap.contains
  226. Std.Ext­HashMap.contains­Then­Insert
  227. Std.Ext­HashMap.contains­Then­Insert­If­New
  228. Std.Ext­HashMap.empty­With­Capacity
  229. Std.Ext­HashMap.erase
  230. Std.Ext­HashMap.filter
  231. Std.Ext­HashMap.filter­Map
  232. Std.Ext­HashMap.get
  233. Std.Ext­HashMap.get!
  234. Std.Ext­HashMap.get?
  235. Std.Ext­HashMap.get­D
  236. Std.Ext­HashMap.get­Key
  237. Std.Ext­HashMap.get­Key!
  238. Std.Ext­HashMap.get­Key?
  239. Std.Ext­HashMap.get­Key­D
  240. Std.Ext­HashMap.get­Then­Insert­If­New?
  241. Std.Ext­HashMap.insert
  242. Std.Ext­HashMap.insert­If­New
  243. Std.Ext­HashMap.insert­Many
  244. Std.Ext­HashMap.insert­Many­If­New­Unit
  245. Std.Ext­HashMap.is­Empty
  246. Std.Ext­HashMap.map
  247. Std.Ext­HashMap.modify
  248. Std.Ext­HashMap.of­List
  249. Std.Ext­HashMap.size
  250. Std.Ext­HashMap.unit­Of­Array
  251. Std.Ext­HashMap.unit­Of­List
  252. Std.Ext­Hash­Set
  253. Std.Ext­HashSet.contains
  254. Std.Ext­HashSet.contains­Then­Insert
  255. Std.Ext­HashSet.empty­With­Capacity
  256. Std.Ext­HashSet.erase
  257. Std.Ext­HashSet.filter
  258. Std.Ext­HashSet.get
  259. Std.Ext­HashSet.get!
  260. Std.Ext­HashSet.get?
  261. Std.Ext­HashSet.get­D
  262. Std.Ext­HashSet.insert
  263. Std.Ext­HashSet.insert­Many
  264. Std.Ext­HashSet.is­Empty
  265. Std.Ext­HashSet.mk
    1. Constructor of Std.Ext­Hash­Set
  266. Std.Ext­HashSet.of­Array
  267. Std.Ext­HashSet.of­List
  268. Std.Ext­HashSet.size
  269. Std.Format
  270. Std.Format.Flatten­Behavior
  271. Std.Format.FlattenBehavior.all­Or­None
    1. Constructor of Std.Format.Flatten­Behavior
  272. Std.Format.FlattenBehavior.fill
    1. Constructor of Std.Format.Flatten­Behavior
  273. Std.Format.Monad­Pretty­Format
  274. Std.Format.Monad­PrettyFormat.mk
    1. Instance constructor of Std.Format.Monad­Pretty­Format
  275. Std.Format.align
    1. Constructor of Std.Format
  276. Std.Format.append
    1. Constructor of Std.Format
  277. Std.Format.bracket
  278. Std.Format.bracket­Fill
  279. Std.Format.def­Indent
  280. Std.Format.def­Width
  281. Std.Format.fill
  282. Std.Format.group
    1. Constructor of Std.Format
  283. Std.Format.indent­D
  284. Std.Format.is­Empty
  285. Std.Format.is­Nil
  286. Std.Format.join
  287. Std.Format.join­Sep
  288. Std.Format.join­Suffix
  289. Std.Format.line
    1. Constructor of Std.Format
  290. Std.Format.nest
    1. Constructor of Std.Format
  291. Std.Format.nest­D
  292. Std.Format.nil
    1. Constructor of Std.Format
  293. Std.Format.paren
  294. Std.Format.prefix­Join
  295. Std.Format.pretty
  296. Std.Format.pretty­M
  297. Std.Format.sbracket
  298. Std.Format.tag
    1. Constructor of Std.Format
  299. Std.Format.text
    1. Constructor of Std.Format
  300. Std.Hash­Map
  301. Std.HashMap.Equiv
  302. Std.HashMap.Equiv.mk
    1. Constructor of Std.HashMap.Equiv
  303. Std.HashMap.Raw
  304. Std.HashMap.Raw.WF
  305. Std.HashMap.Raw.WF.mk
    1. Constructor of Std.HashMap.Raw.WF
  306. Std.HashMap.Raw.mk
    1. Constructor of Std.HashMap.Raw
  307. Std.HashMap.alter
  308. Std.HashMap.contains
  309. Std.HashMap.contains­Then­Insert
  310. Std.HashMap.contains­Then­Insert­If­New
  311. Std.HashMap.empty­With­Capacity
  312. Std.HashMap.erase
  313. Std.HashMap.filter
  314. Std.HashMap.filter­Map
  315. Std.HashMap.fold
  316. Std.HashMap.fold­M
  317. Std.HashMap.for­In
  318. Std.HashMap.for­M
  319. Std.HashMap.get
  320. Std.HashMap.get!
  321. Std.HashMap.get?
  322. Std.HashMap.get­D
  323. Std.HashMap.get­Key
  324. Std.HashMap.get­Key!
  325. Std.HashMap.get­Key?
  326. Std.HashMap.get­Key­D
  327. Std.HashMap.get­Then­Insert­If­New?
  328. Std.HashMap.insert
  329. Std.HashMap.insert­If­New
  330. Std.HashMap.insert­Many
  331. Std.HashMap.insert­Many­If­New­Unit
  332. Std.HashMap.is­Empty
  333. Std.HashMap.keys
  334. Std.HashMap.keys­Array
  335. Std.HashMap.map
  336. Std.HashMap.modify
  337. Std.HashMap.of­List
  338. Std.HashMap.partition
  339. Std.HashMap.size
  340. Std.HashMap.to­Array
  341. Std.HashMap.to­List
  342. Std.HashMap.union
  343. Std.HashMap.unit­Of­Array
  344. Std.HashMap.unit­Of­List
  345. Std.HashMap.values
  346. Std.HashMap.values­Array
  347. Std.Hash­Set
  348. Std.HashSet.Equiv
  349. Std.HashSet.Equiv.mk
    1. Constructor of Std.HashSet.Equiv
  350. Std.HashSet.Raw
  351. Std.HashSet.Raw.WF
  352. Std.HashSet.Raw.WF.mk
    1. Constructor of Std.HashSet.Raw.WF
  353. Std.HashSet.Raw.mk
    1. Constructor of Std.HashSet.Raw
  354. Std.HashSet.all
  355. Std.HashSet.any
  356. Std.HashSet.contains
  357. Std.HashSet.contains­Then­Insert
  358. Std.HashSet.empty­With­Capacity
  359. Std.HashSet.erase
  360. Std.HashSet.filter
  361. Std.HashSet.fold
  362. Std.HashSet.fold­M
  363. Std.HashSet.for­In
  364. Std.HashSet.for­M
  365. Std.HashSet.get
  366. Std.HashSet.get!
  367. Std.HashSet.get?
  368. Std.HashSet.get­D
  369. Std.HashSet.insert
  370. Std.HashSet.insert­Many
  371. Std.HashSet.is­Empty
  372. Std.HashSet.mk
    1. Constructor of Std.Hash­Set
  373. Std.HashSet.of­Array
  374. Std.HashSet.of­List
  375. Std.HashSet.partition
  376. Std.HashSet.size
  377. Std.HashSet.to­Array
  378. Std.HashSet.to­List
  379. Std.HashSet.union
  380. Std.Mutex
  381. Std.Mutex.atomically
  382. Std.Mutex.atomically­Once
  383. Std.Mutex.new
  384. Std.To­Format
  385. Std.ToFormat.mk
    1. Instance constructor of Std.To­Format
  386. Std.Tree­Map
  387. Std.TreeMap.Raw
  388. Std.TreeMap.Raw.WF
  389. Std.TreeMap.Raw.WF.mk
    1. Constructor of Std.TreeMap.Raw.WF
  390. Std.TreeMap.Raw.mk
    1. Constructor of Std.TreeMap.Raw
  391. Std.TreeMap.all
  392. Std.TreeMap.alter
  393. Std.TreeMap.any
  394. Std.TreeMap.contains
  395. Std.TreeMap.contains­Then­Insert
  396. Std.TreeMap.contains­Then­Insert­If­New
  397. Std.TreeMap.empty
  398. Std.TreeMap.entry­At­Idx
  399. Std.TreeMap.entry­At­Idx!
  400. Std.TreeMap.entry­At­Idx?
  401. Std.TreeMap.entry­At­Idx­D
  402. Std.TreeMap.erase
  403. Std.TreeMap.erase­Many
  404. Std.TreeMap.filter
  405. Std.TreeMap.filter­Map
  406. Std.TreeMap.foldl
  407. Std.TreeMap.foldl­M
  408. Std.TreeMap.foldr
  409. Std.TreeMap.foldr­M
  410. Std.TreeMap.for­In
  411. Std.TreeMap.for­M
  412. Std.TreeMap.get
  413. Std.TreeMap.get!
  414. Std.TreeMap.get?
  415. Std.TreeMap.get­D
  416. Std.TreeMap.get­Entry­GE
  417. Std.TreeMap.get­Entry­GE!
  418. Std.TreeMap.get­Entry­GE?
  419. Std.TreeMap.get­Entry­GED
  420. Std.TreeMap.get­Entry­GT
  421. Std.TreeMap.get­Entry­GT!
  422. Std.TreeMap.get­Entry­GT?
  423. Std.TreeMap.get­Entry­GTD
  424. Std.TreeMap.get­Entry­LE
  425. Std.TreeMap.get­Entry­LE!
  426. Std.TreeMap.get­Entry­LE?
  427. Std.TreeMap.get­Entry­LED
  428. Std.TreeMap.get­Entry­LT
  429. Std.TreeMap.get­Entry­LT!
  430. Std.TreeMap.get­Entry­LT?
  431. Std.TreeMap.get­Entry­LTD
  432. Std.TreeMap.get­Key
  433. Std.TreeMap.get­Key!
  434. Std.TreeMap.get­Key?
  435. Std.TreeMap.get­Key­D
  436. Std.TreeMap.get­Key­GE
  437. Std.TreeMap.get­Key­GE!
  438. Std.TreeMap.get­Key­GE?
  439. Std.TreeMap.get­Key­GED
  440. Std.TreeMap.get­Key­GT
  441. Std.TreeMap.get­Key­GT!
  442. Std.TreeMap.get­Key­GT?
  443. Std.TreeMap.get­Key­GTD
  444. Std.TreeMap.get­Key­LE
  445. Std.TreeMap.get­Key­LE!
  446. Std.TreeMap.get­Key­LE?
  447. Std.TreeMap.get­Key­LED
  448. Std.TreeMap.get­Key­LT
  449. Std.TreeMap.get­Key­LT!
  450. Std.TreeMap.get­Key­LT?
  451. Std.TreeMap.get­Key­LTD
  452. Std.TreeMap.get­Then­Insert­If­New?
  453. Std.TreeMap.insert
  454. Std.TreeMap.insert­If­New
  455. Std.TreeMap.insert­Many
  456. Std.TreeMap.insert­Many­If­New­Unit
  457. Std.TreeMap.is­Empty
  458. Std.TreeMap.key­At­Idx
  459. Std.TreeMap.key­At­Idx!
  460. Std.TreeMap.key­At­Idx?
  461. Std.TreeMap.key­At­Idx­D
  462. Std.TreeMap.keys
  463. Std.TreeMap.keys­Array
  464. Std.TreeMap.map
  465. Std.TreeMap.max­Entry
  466. Std.TreeMap.max­Entry!
  467. Std.TreeMap.max­Entry?
  468. Std.TreeMap.max­Entry­D
  469. Std.TreeMap.max­Key
  470. Std.TreeMap.max­Key!
  471. Std.TreeMap.max­Key?
  472. Std.TreeMap.max­Key­D
  473. Std.TreeMap.merge­With
  474. Std.TreeMap.min­Entry
  475. Std.TreeMap.min­Entry!
  476. Std.TreeMap.min­Entry?
  477. Std.TreeMap.min­Entry­D
  478. Std.TreeMap.min­Key
  479. Std.TreeMap.min­Key!
  480. Std.TreeMap.min­Key?
  481. Std.TreeMap.min­Key­D
  482. Std.TreeMap.modify
  483. Std.TreeMap.of­Array
  484. Std.TreeMap.of­List
  485. Std.TreeMap.partition
  486. Std.TreeMap.size
  487. Std.TreeMap.to­Array
  488. Std.TreeMap.to­List
  489. Std.TreeMap.unit­Of­Array
  490. Std.TreeMap.unit­Of­List
  491. Std.TreeMap.values
  492. Std.TreeMap.values­Array
  493. Std.Tree­Set
  494. Std.TreeSet.Raw
  495. Std.TreeSet.Raw.WF
  496. Std.TreeSet.Raw.WF.mk
    1. Constructor of Std.TreeSet.Raw.WF
  497. Std.TreeSet.Raw.mk
    1. Constructor of Std.TreeSet.Raw
  498. Std.TreeSet.all
  499. Std.TreeSet.any
  500. Std.TreeSet.at­Idx
  501. Std.TreeSet.at­Idx!
  502. Std.TreeSet.at­Idx?
  503. Std.TreeSet.at­Idx­D
  504. Std.TreeSet.contains
  505. Std.TreeSet.contains­Then­Insert
  506. Std.TreeSet.empty
  507. Std.TreeSet.erase
  508. Std.TreeSet.erase­Many
  509. Std.TreeSet.filter
  510. Std.TreeSet.foldl
  511. Std.TreeSet.foldl­M
  512. Std.TreeSet.foldr
  513. Std.TreeSet.foldr­M
  514. Std.TreeSet.for­In
  515. Std.TreeSet.for­M
  516. Std.TreeSet.get
  517. Std.TreeSet.get!
  518. Std.TreeSet.get?
  519. Std.TreeSet.get­D
  520. Std.TreeSet.get­GE
  521. Std.TreeSet.get­GE!
  522. Std.TreeSet.get­GE?
  523. Std.TreeSet.get­GED
  524. Std.TreeSet.get­GT
  525. Std.TreeSet.get­GT!
  526. Std.TreeSet.get­GT?
  527. Std.TreeSet.get­GTD
  528. Std.TreeSet.get­LE
  529. Std.TreeSet.get­LE!
  530. Std.TreeSet.get­LE?
  531. Std.TreeSet.get­LED
  532. Std.TreeSet.get­LT
  533. Std.TreeSet.get­LT!
  534. Std.TreeSet.get­LT?
  535. Std.TreeSet.get­LTD
  536. Std.TreeSet.insert
  537. Std.TreeSet.insert­Many
  538. Std.TreeSet.is­Empty
  539. Std.TreeSet.max
  540. Std.TreeSet.max!
  541. Std.TreeSet.max?
  542. Std.TreeSet.max­D
  543. Std.TreeSet.merge
  544. Std.TreeSet.min
  545. Std.TreeSet.min!
  546. Std.TreeSet.min?
  547. Std.TreeSet.min­D
  548. Std.TreeSet.of­Array
  549. Std.TreeSet.of­List
  550. Std.TreeSet.partition
  551. Std.TreeSet.size
  552. Std.TreeSet.to­Array
  553. Std.TreeSet.to­List
  554. Std­Gen
  555. Stdio
    1. IO.Process.Stdio
  556. Stdio­Config
    1. IO.Process.Stdio­Config
  557. Str­Lit
    1. Lean.Syntax.Str­Lit
  558. Stream
    1. IO.FS.Stream
  559. String
  560. String.Legacy.Iterator
  561. String.Legacy.Iterator.at­End
  562. String.Legacy.Iterator.curr
  563. String.Legacy.Iterator.curr'
  564. String.Legacy.Iterator.extract
  565. String.Legacy.Iterator.find
  566. String.Legacy.Iterator.fold­Until
  567. String.Legacy.Iterator.forward
  568. String.Legacy.Iterator.has­Next
  569. String.Legacy.Iterator.has­Prev
  570. String.Legacy.Iterator.mk
    1. Constructor of String.Legacy.Iterator
  571. String.Legacy.Iterator.next
  572. String.Legacy.Iterator.next'
  573. String.Legacy.Iterator.nextn
  574. String.Legacy.Iterator.pos
  575. String.Legacy.Iterator.prev
  576. String.Legacy.Iterator.prevn
  577. String.Legacy.Iterator.remaining­Bytes
  578. String.Legacy.Iterator.remaining­To­String
  579. String.Legacy.Iterator.set­Curr
  580. String.Legacy.Iterator.to­End
  581. String.Legacy.Iterator.to­String
  582. String.Legacy.iter
  583. String.Legacy.mk­Iterator
  584. String.Pos.Raw
  585. String.Pos.Raw.at­End
  586. String.Pos.Raw.byte­Distance
  587. String.Pos.Raw.dec
  588. String.Pos.Raw.decrease­By
  589. String.Pos.Raw.extract
  590. String.Pos.Raw.get
  591. String.Pos.Raw.get!
  592. String.Pos.Raw.get'
  593. String.Pos.Raw.get?
  594. String.Pos.Raw.inc
  595. String.Pos.Raw.increase­By
  596. String.Pos.Raw.is­Valid
  597. String.Pos.Raw.is­Valid­For­Slice
  598. String.Pos.Raw.min
  599. String.Pos.Raw.mk
    1. Constructor of String.Pos.Raw
  600. String.Pos.Raw.modify
  601. String.Pos.Raw.next
  602. String.Pos.Raw.next'
  603. String.Pos.Raw.next­Until
  604. String.Pos.Raw.next­While
  605. String.Pos.Raw.offset­By
  606. String.Pos.Raw.offset­Of­Pos
  607. String.Pos.Raw.prev
  608. String.Pos.Raw.set
  609. String.Pos.Raw.substr­Eq
  610. String.Pos.Raw.unoffset­By
  611. String.Slice
  612. String.Slice.Pattern.Backward­Pattern
  613. String.Slice.Pattern.BackwardPattern.mk
    1. Instance constructor of String.Slice.Pattern.Backward­Pattern
  614. String.Slice.Pattern.Forward­Pattern
  615. String.Slice.Pattern.ForwardPattern.mk
    1. Instance constructor of String.Slice.Pattern.Forward­Pattern
  616. String.Slice.Pattern.To­Backward­Searcher
  617. String.Slice.Pattern.To­BackwardSearcher.mk
    1. Instance constructor of String.Slice.Pattern.To­Backward­Searcher
  618. String.Slice.Pattern.To­Forward­Searcher
  619. String.Slice.Pattern.To­ForwardSearcher.mk
    1. Instance constructor of String.Slice.Pattern.To­Forward­Searcher
  620. String.Slice.Pos
  621. String.Slice.Pos.byte
  622. String.Slice.Pos.cast
  623. String.Slice.Pos.get
  624. String.Slice.Pos.get!
  625. String.Slice.Pos.get?
  626. String.Slice.Pos.mk
    1. Constructor of String.Slice.Pos
  627. String.Slice.Pos.next
  628. String.Slice.Pos.next!
  629. String.Slice.Pos.next?
  630. String.Slice.Pos.nextn
  631. String.Slice.Pos.of­Replace­Start
  632. String.Slice.Pos.of­Slice
  633. String.Slice.Pos.prev
  634. String.Slice.Pos.prev!
  635. String.Slice.Pos.prev?
  636. String.Slice.Pos.prevn
  637. String.Slice.Pos.str
  638. String.Slice.Pos.to­Copy
  639. String.Slice.Pos.to­Replace­Start
  640. String.Slice.all
  641. String.Slice.back
  642. String.Slice.back?
  643. String.Slice.beq
  644. String.Slice.bytes
  645. String.Slice.chars
  646. String.Slice.contains
  647. String.Slice.copy
  648. String.Slice.drop
  649. String.Slice.drop­End
  650. String.Slice.drop­End­While
  651. String.Slice.drop­Prefix
  652. String.Slice.drop­Prefix?
  653. String.Slice.drop­Suffix
  654. String.Slice.drop­Suffix?
  655. String.Slice.drop­While
  656. String.Slice.end­Pos
  657. String.Slice.ends­With
  658. String.Slice.eq­Ignore­Ascii­Case
  659. String.Slice.find?
  660. String.Slice.find­Next­Pos
  661. String.Slice.foldl
  662. String.Slice.foldr
  663. String.Slice.front
  664. String.Slice.front?
  665. String.Slice.get­UTF8Byte
  666. String.Slice.get­UTF8Byte!
  667. String.Slice.is­Empty
  668. String.Slice.is­Nat
  669. String.Slice.lines
  670. String.Slice.mk
    1. Constructor of String.Slice
  671. String.Slice.pos
  672. String.Slice.pos!
  673. String.Slice.pos?
  674. String.Slice.positions
  675. String.Slice.raw­End­Pos
  676. String.Slice.replace­End
  677. String.Slice.replace­Start
  678. String.Slice.replace­Start­End
  679. String.Slice.replace­Start­End!
  680. String.Slice.rev­Bytes
  681. String.Slice.rev­Chars
  682. String.Slice.rev­Find?
  683. String.Slice.rev­Positions
  684. String.Slice.rev­Split
  685. String.Slice.split
  686. String.Slice.split­Inclusive
  687. String.Slice.start­Pos
  688. String.Slice.starts­With
  689. String.Slice.take
  690. String.Slice.take­End
  691. String.Slice.take­End­While
  692. String.Slice.take­While
  693. String.Slice.to­Nat!
  694. String.Slice.to­Nat?
  695. String.Slice.trim­Ascii
  696. String.Slice.trim­Ascii­End
  697. String.Slice.trim­Ascii­Start
  698. String.Slice.utf8Byte­Size
  699. String.Valid­Pos
  700. String.ValidPos.byte
  701. String.ValidPos.cast
  702. String.ValidPos.extract
  703. String.ValidPos.get
  704. String.ValidPos.get!
  705. String.ValidPos.get?
  706. String.ValidPos.mk
    1. Constructor of String.Valid­Pos
  707. String.ValidPos.modify
  708. String.ValidPos.next
  709. String.ValidPos.next!
  710. String.ValidPos.next?
  711. String.ValidPos.of­Copy
  712. String.ValidPos.prev
  713. String.ValidPos.prev!
  714. String.ValidPos.prev?
  715. String.ValidPos.set
  716. String.ValidPos.to­Modify­Of­LE
  717. String.ValidPos.to­Set­Of­LE
  718. String.ValidPos.to­Slice
  719. String.all
  720. String.any
  721. String.append
  722. String.back
  723. String.capitalize
  724. String.contains
  725. String.crlf­To­Lf
  726. String.dec­Eq
  727. String.decapitalize
  728. String.drop
  729. String.drop­End
  730. String.drop­End­While
  731. String.drop­Prefix
  732. String.drop­Prefix?
  733. String.drop­Suffix
  734. String.drop­Suffix?
  735. String.drop­While
  736. String.end­Valid­Pos
  737. String.ends­With
  738. String.find
  739. String.find­Line­Start
  740. String.first­Diff­Pos
  741. String.foldl
  742. String.foldr
  743. String.from­UTF8
  744. String.from­UTF8!
  745. String.from­UTF8?
  746. String.front
  747. String.get­UTF8Byte
  748. String.hash
  749. String.intercalate
  750. String.is­Empty
  751. String.is­Int
  752. String.is­Nat
  753. String.is­Prefix­Of
  754. String.join
  755. String.le
  756. String.length
  757. String.map
  758. String.of­Byte­Array
    1. Constructor of String
  759. String.of­List
  760. String.pos
  761. String.pos!
  762. String.pos?
  763. String.pos­Of
  764. String.push
  765. String.pushn
  766. String.quote
  767. String.raw­End­Pos
  768. String.remove­Leading­Spaces
  769. String.replace
  770. String.replace­End
  771. String.replace­Start
  772. String.rev­Find
  773. String.rev­Pos­Of
  774. String.singleton
  775. String.split­On
  776. String.split­To­List
  777. String.start­Valid­Pos
  778. String.starts­With
  779. String.take
  780. String.take­End
  781. String.take­End­While
  782. String.take­While
  783. String.to­Format
  784. String.to­Int!
  785. String.to­Int?
  786. String.to­List (0) (1)
  787. String.to­Lower
  788. String.to­Name
  789. String.to­Nat!
  790. String.to­Nat?
  791. String.to­Raw­Substring
  792. String.to­Raw­Substring'
  793. String.to­Slice
  794. String.to­UTF8
  795. String.to­Upper
  796. String.trim­Ascii
  797. String.trim­Ascii­End
  798. String.trim­Ascii­Start
  799. String.utf8Byte­Size
  800. String.utf8Encode­Char
  801. Sub
  802. Sub.mk
    1. Instance constructor of Sub
  803. Subarray
  804. Subarray.all
  805. Subarray.all­M
  806. Subarray.any
  807. Subarray.any­M
  808. Subarray.array
  809. Subarray.drop
  810. Subarray.empty
  811. Subarray.find­Rev?
  812. Subarray.find­Rev­M?
  813. Subarray.find­Some­Rev­M?
  814. Subarray.foldl
  815. Subarray.foldl­M
  816. Subarray.foldr
  817. Subarray.foldr­M
  818. Subarray.for­In
  819. Subarray.for­M
  820. Subarray.for­Rev­M
  821. Subarray.get
  822. Subarray.get!
  823. Subarray.get­D
  824. Subarray.pop­Front
  825. Subarray.size
  826. Subarray.split
  827. Subarray.start
  828. Subarray.start_le_stop
  829. Subarray.stop
  830. Subarray.stop_le_array_size
  831. Subarray.take
  832. Subarray.to­Array
  833. Sublist
    1. List.Sublist
  834. Subsingleton
  835. Subsingleton.elim
  836. Subsingleton.helim
  837. Subsingleton.intro
    1. Instance constructor of Subsingleton
  838. Substring.Raw
  839. Substring.Raw.all
  840. Substring.Raw.any
  841. Substring.Raw.at­End
  842. Substring.Raw.beq
  843. Substring.Raw.bsize
  844. Substring.Raw.common­Prefix
  845. Substring.Raw.common­Suffix
  846. Substring.Raw.contains
  847. Substring.Raw.drop
  848. Substring.Raw.drop­Prefix?
  849. Substring.Raw.drop­Right
  850. Substring.Raw.drop­Right­While
  851. Substring.Raw.drop­Suffix?
  852. Substring.Raw.drop­While
  853. Substring.Raw.extract
  854. Substring.Raw.foldl
  855. Substring.Raw.foldr
  856. Substring.Raw.front
  857. Substring.Raw.get
  858. Substring.Raw.is­Empty
  859. Substring.Raw.is­Nat
  860. Substring.Raw.mk
    1. Constructor of Substring.Raw
  861. Substring.Raw.next
  862. Substring.Raw.nextn
  863. Substring.Raw.pos­Of
  864. Substring.Raw.prev
  865. Substring.Raw.prevn
  866. Substring.Raw.repair
  867. Substring.Raw.same­As
  868. Substring.Raw.split­On
  869. Substring.Raw.take
  870. Substring.Raw.take­Right
  871. Substring.Raw.take­Right­While
  872. Substring.Raw.take­While
  873. Substring.Raw.to­Legacy­Iterator
  874. Substring.Raw.to­Name
  875. Substring.Raw.to­Nat?
  876. Substring.Raw.to­String
  877. Substring.Raw.trim
  878. Substring.Raw.trim­Left
  879. Substring.Raw.trim­Right
  880. Subtype
  881. Subtype.mk
    1. Constructor of Subtype
  882. Sum
  883. Sum.elim
  884. Sum.get­Left
  885. Sum.get­Left?
  886. Sum.get­Right
  887. Sum.get­Right?
  888. Sum.inhabited­Left
  889. Sum.inhabited­Right
  890. Sum.inl
    1. Constructor of Sum
  891. Sum.inr
    1. Constructor of Sum
  892. Sum.is­Left
  893. Sum.is­Right
  894. Sum.map
  895. Sum.swap
  896. Surjective
    1. Function.Surjective
  897. Sync
    1. Std.Channel.Sync
  898. Syntax
    1. Lean.Syntax
  899. Syntax­Node­Kind
    1. Lean.Syntax­Node­Kind
  900. Syntax­Node­Kinds
    1. Lean.Syntax­Node­Kinds
  901. System.File­Path
  902. System.FilePath.add­Extension
  903. System.FilePath.components
  904. System.FilePath.exe­Extension
  905. System.FilePath.ext­Separator
  906. System.FilePath.extension
  907. System.FilePath.file­Name
  908. System.FilePath.file­Stem
  909. System.FilePath.is­Absolute
  910. System.FilePath.is­Dir
  911. System.FilePath.is­Relative
  912. System.FilePath.join
  913. System.FilePath.metadata
  914. System.FilePath.mk
    1. Constructor of System.File­Path
  915. System.FilePath.normalize
  916. System.FilePath.parent
  917. System.FilePath.path­Exists
  918. System.FilePath.path­Separator
  919. System.FilePath.path­Separators
  920. System.FilePath.read­Dir
  921. System.FilePath.symlink­Metadata
  922. System.FilePath.walk­Dir
  923. System.FilePath.with­Extension
  924. System.FilePath.with­File­Name
  925. System.Platform.is­Emscripten
  926. System.Platform.is­OSX
  927. System.Platform.is­Windows
  928. System.Platform.num­Bits
  929. System.Platform.target
  930. System.mk­File­Path
  931. s
    1. String.Legacy.Iterator.s (structure field)
  932. sadd­Overflow
    1. BitVec.sadd­Overflow
  933. same­As
    1. Substring.Raw.same­As
  934. save
    1. EStateM.Backtrackable.save (class method)
  935. sbracket
    1. Std.Format.sbracket
  936. scale­B
    1. Float.scale­B
  937. scale­B
    1. Float32.scale­B
  938. scientific­Lit­Kind
    1. Lean.scientific­Lit­Kind
  939. script doc (Lake command)
  940. script list (Lake command)
  941. script run (Lake command)
  942. sdiv
    1. BitVec.sdiv
  943. self uninstall (Elan command)
  944. self update (Elan command)
  945. semi­Out­Param
  946. send
    1. Std.Channel.send
  947. seq
    1. Seq.seq (class method)
  948. seq­Left
    1. SeqLeft.seq­Left (class method)
  949. seq­Left_eq
    1. [anonymous] (class method)
  950. seq­Right
    1. EStateM.seq­Right
  951. seq­Right
    1. SeqRight.seq­Right (class method)
  952. seq­Right_eq
    1. [anonymous] (class method)
  953. seq_assoc
    1. LawfulApplicative.pure_seq (class method)
  954. seq_pure
    1. LawfulApplicative.seq­Right_eq (class method)
  955. sequence
    1. Option.sequence
  956. serve (Lake command)
  957. set!
    1. Array.set!
  958. set!
    1. ByteArray.set!
  959. set
    1. Array.set
  960. set
    1. ByteArray.set
  961. set
    1. EStateM.set
  962. set
    1. List.set
  963. set
    1. MonadState.set (class method)
  964. set
    1. Monad­StateOf.set (class method)
  965. set
    1. ST.Ref.set
  966. set
    1. State­RefT'.set
  967. set
    1. StateT.set
  968. set
    1. String.Pos.Raw.set
  969. set
    1. String.ValidPos.set
  970. set­Access­Rights
    1. IO.set­Access­Rights
  971. set­Curr
    1. String.Legacy.Iterator.set­Curr
  972. set­Current­Dir
    1. IO.Process.set­Current­Dir
  973. set­If­In­Bounds
    1. Array.set­If­In­Bounds
  974. set­Kind
    1. Lean.Syntax.set­Kind
  975. set­Rand­Seed
    1. IO.set­Rand­Seed
  976. set­Stderr
    1. IO.set­Stderr
  977. set­Stdin
    1. IO.set­Stdin
  978. set­Stdout
    1. IO.set­Stdout
  979. set­TR
    1. List.set­TR
  980. set­Width'
    1. BitVec.set­Width'
  981. set­Width
    1. BitVec.set­Width
  982. set_option
  983. setsid
    1. IO.Process.SpawnArgs.cwd (structure field)
  984. shift­Concat
    1. BitVec.shift­Concat
  985. shift­Left
    1. BitVec.shift­Left
  986. shift­Left
    1. Fin.shift­Left
  987. shift­Left
    1. ISize.shift­Left
  988. shift­Left
    1. Int16.shift­Left
  989. shift­Left
    1. Int32.shift­Left
  990. shift­Left
    1. Int64.shift­Left
  991. shift­Left
    1. Int8.shift­Left
  992. shift­Left
    1. Nat.shift­Left
  993. shift­Left
    1. ShiftLeft.shift­Left (class method)
  994. shift­Left
    1. UInt16.shift­Left
  995. shift­Left
    1. UInt32.shift­Left
  996. shift­Left
    1. UInt64.shift­Left
  997. shift­Left
    1. UInt8.shift­Left
  998. shift­Left
    1. USize.shift­Left
  999. shift­Left­Rec
    1. BitVec.shift­Left­Rec
  1000. shift­Left­Zero­Extend
    1. BitVec.shift­Left­Zero­Extend
  1001. shift­Right
    1. Fin.shift­Right
  1002. shift­Right
    1. ISize.shift­Right
  1003. shift­Right
    1. Int.shift­Right
  1004. shift­Right
    1. Int16.shift­Right
  1005. shift­Right
    1. Int32.shift­Right
  1006. shift­Right
    1. Int64.shift­Right
  1007. shift­Right
    1. Int8.shift­Right
  1008. shift­Right
    1. Nat.shift­Right
  1009. shift­Right
    1. ShiftRight.shift­Right (class method)
  1010. shift­Right
    1. UInt16.shift­Right
  1011. shift­Right
    1. UInt32.shift­Right
  1012. shift­Right
    1. UInt64.shift­Right
  1013. shift­Right
    1. UInt8.shift­Right
  1014. shift­Right
    1. USize.shift­Right
  1015. show
  1016. show (Elan command)
  1017. show_term
  1018. shrink
    1. Array.shrink
  1019. sign
    1. Int.sign
  1020. sign­Extend
    1. BitVec.sign­Extend
  1021. simp (0) (1)
  1022. simp!
  1023. simp?
  1024. simp?!
  1025. simp_all
  1026. simp_all!
  1027. simp_all?
  1028. simp_all?!
  1029. simp_all_arith
  1030. simp_all_arith!
  1031. simp_arith
  1032. simp_arith!
  1033. simp_match
  1034. simp_wf
  1035. simpa
  1036. simpa!
  1037. simpa?
  1038. simpa?!
  1039. simprocs
  1040. sin
    1. Float.sin
  1041. sin
    1. Float32.sin
  1042. single­Pass
    1. Lean.Meta.Simp.Config.single­Pass (structure field)
  1043. singleton
    1. Array.singleton
  1044. singleton
    1. List.singleton
  1045. singleton
    1. String.singleton
  1046. sinh
    1. Float.sinh
  1047. sinh
    1. Float32.sinh
  1048. size
    1. Array.size
  1049. size
    1. ByteArray.size
  1050. size
    1. ByteSlice.size
  1051. size
    1. ISize.size
  1052. size
    1. Int16.size
  1053. size
    1. Int32.size
  1054. size
    1. Int64.size
  1055. size
    1. Int8.size
  1056. size
    1. Std.DHashMap.Raw.size (structure field)
  1057. size
    1. Std.DHashMap.size
  1058. size
    1. Std.DTreeMap.size
  1059. size
    1. Std.Ext­DHashMap.size
  1060. size
    1. Std.Ext­HashMap.size
  1061. size
    1. Std.Ext­HashSet.size
  1062. size
    1. Std.HashMap.size
  1063. size
    1. Std.HashSet.size
  1064. size
    1. Std.TreeMap.size
  1065. size
    1. Std.TreeSet.size
  1066. size
    1. Subarray.size
  1067. size
    1. UInt16.size
  1068. size
    1. UInt32.size
  1069. size
    1. UInt64.size
  1070. size
    1. UInt8.size
  1071. size
    1. USize.size
  1072. size­Of
    1. SizeOf.size­Of (class method)
  1073. skip (0) (1)
  1074. skip­Assigned­Instances
    1. tactic.skip­Assigned­Instances
  1075. sle
    1. BitVec.sle
  1076. sleep
  1077. sleep
    1. IO.sleep
  1078. slice
    1. ByteSlice.slice
  1079. slt
    1. BitVec.slt
  1080. smod
    1. BitVec.smod
  1081. smt­SDiv
    1. BitVec.smt­SDiv
  1082. smt­UDiv
    1. BitVec.smt­UDiv
  1083. smul
    1. SMul.smul (class method)
  1084. snd
    1. MProd.snd (structure field)
  1085. snd
    1. PProd.snd (structure field)
  1086. snd
    1. PSigma.snd (structure field)
  1087. snd
    1. Prod.snd (structure field)
  1088. snd
    1. Sigma.snd (structure field)
  1089. solve
  1090. solve_by_elim
  1091. sorry
  1092. sound
    1. Quot.sound
  1093. sound
    1. Quotient.sound
  1094. span
    1. List.span
  1095. spawn
    1. IO.Process.spawn
  1096. spawn
    1. Task.spawn
  1097. specialize
  1098. split
  1099. split
    1. RandomGen.split (class method)
  1100. split
    1. String.Slice.split
  1101. split
    1. Subarray.split
  1102. split
    1. trace.grind.split
  1103. split­At
    1. List.split­At
  1104. split­By
    1. List.split­By
  1105. split­Inclusive
    1. String.Slice.split­Inclusive
  1106. split­On
    1. String.split­On
  1107. split­On
    1. Substring.Raw.split­On
  1108. split­To­List
    1. String.split­To­List
  1109. sqrt
    1. Float.sqrt
  1110. sqrt
    1. Float32.sqrt
  1111. src­Dir
    1. [anonymous] (structure field) (0) (1)
  1112. srem
    1. BitVec.srem
  1113. sshift­Right'
    1. BitVec.sshift­Right'
  1114. sshift­Right
    1. BitVec.sshift­Right
  1115. sshift­Right­Rec
    1. BitVec.sshift­Right­Rec
  1116. ssub­Overflow
    1. BitVec.ssub­Overflow
  1117. st­M
    1. MonadControl.st­M (class method)
  1118. st­M
    1. Monad­ControlT.st­M (class method)
  1119. start
    1. ByteSlice.start
  1120. start
    1. Subarray.start
  1121. start­Inclusive
    1. String.Slice.start­Inclusive (structure field)
  1122. start­Inclusive_le_end­Exclusive
    1. String.Slice.start­Inclusive_le_end­Exclusive (structure field)
  1123. start­Pos
    1. String.Slice.start­Pos
  1124. start­Pos
    1. Substring.Raw.start­Pos (structure field)
  1125. start­Tag
    1. Std.Format.Monad­PrettyFormat.start­Tag (class method)
  1126. start­Valid­Pos
    1. String.start­Valid­Pos
  1127. start_le_stop
    1. Subarray.start_le_stop
  1128. starts­With
    1. String.Slice.Pattern.ForwardPattern.starts­With (class method)
  1129. starts­With
    1. String.Slice.starts­With
  1130. starts­With
    1. String.starts­With
  1131. std­Next
  1132. std­Range
  1133. std­Split
  1134. stderr
    1. IO.Process.Child.stderr (structure field)
  1135. stderr
    1. IO.Process.Output.stderr (structure field)
  1136. stderr
    1. IO.Process.StdioConfig.stderr (structure field)
  1137. stdin
    1. IO.Process.Child.stdin (structure field)
  1138. stdin
    1. IO.Process.StdioConfig.stdin (structure field)
  1139. stdout
    1. IO.Process.Child.stdout (structure field)
  1140. stdout
    1. IO.Process.Output.stdout (structure field)
  1141. stdout
    1. IO.Process.StdioConfig.stdout (structure field)
  1142. stop
  1143. stop
    1. ByteSlice.stop
  1144. stop
    1. Subarray.stop
  1145. stop­Pos
    1. Substring.Raw.stop­Pos (structure field)
  1146. stop_le_array_size
    1. Subarray.stop_le_array_size
  1147. str
    1. String.Slice.Pos.str
  1148. str
    1. String.Slice.str (structure field)
  1149. str
    1. Substring.Raw.str (structure field)
  1150. str­Lit­Kind
    1. Lean.str­Lit­Kind
  1151. strong­Rec­On
    1. Nat.strong­Rec­On
  1152. sub
    1. BitVec.sub
  1153. sub
    1. Fin.sub
  1154. sub
    1. Float.sub
  1155. sub
    1. Float32.sub
  1156. sub
    1. ISize.sub
  1157. sub
    1. Int.sub
  1158. sub
    1. Int16.sub
  1159. sub
    1. Int32.sub
  1160. sub
    1. Int64.sub
  1161. sub
    1. Int8.sub
  1162. sub
    1. Nat.sub
  1163. sub
    1. Sub.sub (class method)
  1164. sub
    1. UInt16.sub
  1165. sub
    1. UInt32.sub
  1166. sub
    1. UInt64.sub
  1167. sub
    1. UInt8.sub
  1168. sub
    1. USize.sub
  1169. sub­Digit­Char
    1. Nat.sub­Digit­Char
  1170. sub­Nat
    1. Fin.sub­Nat
  1171. sub­Nat­Nat
    1. Int.sub­Nat­Nat
  1172. sub_eq_add_neg
    1. [anonymous] (class method)
  1173. subst
  1174. subst
    1. Eq.subst
  1175. subst
    1. HEq.subst
  1176. subst_eqs
  1177. subst_vars
  1178. substr­Eq
    1. String.Pos.Raw.substr­Eq
  1179. succ
    1. Fin.succ
  1180. succ­Rec
    1. Fin.succ­Rec
  1181. succ­Rec­On
    1. Fin.succ­Rec­On
  1182. suffices
  1183. suggestions
    1. Lean.Meta.Simp.Config.suggestions (structure field)
  1184. sum
    1. Array.sum
  1185. sum
    1. List.sum
  1186. super­Digit­Char
    1. Nat.super­Digit­Char
  1187. support­Interpreter
    1. [anonymous] (structure field)
  1188. swap
    1. Array.swap
  1189. swap
    1. Ordering.swap
  1190. swap
    1. Prod.swap
  1191. swap
    1. ST.Ref.swap
  1192. swap
    1. Sum.swap
  1193. swap­At!
    1. Array.swap­At!
  1194. swap­At
    1. Array.swap­At
  1195. swap­If­In­Bounds
    1. Array.swap­If­In­Bounds
  1196. symlink­Metadata
    1. System.FilePath.symlink­Metadata
  1197. symm
  1198. symm
    1. Eq.symm
  1199. symm
    1. Equivalence.symm (structure field)
  1200. symm
    1. Setoid.symm
  1201. symm_saturate
  1202. sync
    1. Std.Channel.sync
  1203. synthInstance.max­Heartbeats
  1204. synthInstance.max­Size
  1205. 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. To­Backward­Searcher
    1. String.Slice.Pattern.To­Backward­Searcher
  25. To­Format
    1. Std.To­Format
  26. To­Forward­Searcher
    1. String.Slice.Pattern.To­Forward­Searcher
  27. To­Int
    1. Lean.Grind.To­Int
  28. Trans
  29. Trans.mk
    1. Instance constructor of Trans
  30. Transparency­Mode
    1. Lean.Meta.Transparency­Mode
  31. Tree­Map
    1. Std.Tree­Map
  32. Tree­Set
    1. Std.Tree­Set
  33. True
  34. True.intro
    1. Constructor of True
  35. Type
  36. tactic
  37. tactic'
  38. tactic.custom­Eliminators
  39. tactic.hygienic
  40. tactic.simp.trace (0) (1)
  41. tactic.skip­Assigned­Instances
  42. tail!
    1. List.tail!
  43. tail
    1. List.tail
  44. tail?
    1. List.tail?
  45. tail­D
    1. List.tail­D
  46. take
    1. Array.take
  47. take
    1. List.take
  48. take
    1. ST.Ref.take
  49. take
    1. String.Slice.take
  50. take
    1. String.take
  51. take
    1. Subarray.take
  52. take
    1. Substring.Raw.take
  53. take­End
    1. String.Slice.take­End
  54. take­End
    1. String.take­End
  55. take­End­While
    1. String.Slice.take­End­While
  56. take­End­While
    1. String.take­End­While
  57. take­Right
    1. Substring.Raw.take­Right
  58. take­Right­While
    1. Substring.Raw.take­Right­While
  59. take­Stdin
    1. IO.Process.Child.take­Stdin
  60. take­TR
    1. List.take­TR
  61. take­While
    1. Array.take­While
  62. take­While
    1. List.take­While
  63. take­While
    1. String.Slice.take­While
  64. take­While
    1. String.take­While
  65. take­While
    1. Substring.Raw.take­While
  66. take­While­TR
    1. List.take­While­TR
  67. tan
    1. Float.tan
  68. tan
    1. Float32.tan
  69. tanh
    1. Float.tanh
  70. tanh
    1. Float32.tanh
  71. target
    1. System.Platform.target
  72. tdiv
    1. Int.tdiv
  73. term
    1. placeholder
  74. test (Lake command)
  75. test­Bit
    1. Nat.test­Bit
  76. then
    1. Ordering.then
  77. threshold
    1. pp.deepTerms.threshold
  78. threshold
    1. pp.proofs.threshold
  79. throw
    1. EStateM.throw
  80. throw
    1. MonadExcept.throw (class method)
  81. throw
    1. Monad­ExceptOf.throw (class method)
  82. throw­Error
    1. Lean.Macro.throw­Error
  83. throw­Error­At
    1. Lean.Macro.throw­Error­At
  84. throw­The
  85. throw­Unsupported
    1. Lean.Macro.throw­Unsupported
  86. tmod
    1. Int.tmod
  87. to­Add
    1. Lean.Grind.Semiring.to­Add (class method)
  88. to­Add­Comm­Group
    1. Lean.Grind.IntModule.to­Add­Comm­Group (class method)
  89. to­Add­Comm­Monoid
    1. Lean.Grind.NatModule.to­Add­Comm­Monoid (class method)
  90. to­Applicative
    1. Alternative.to­Applicative (class method)
  91. to­Applicative
    1. Monad.to­Applicative (class method)
  92. to­Array
    1. List.to­Array
  93. to­Array
    1. Option.to­Array
  94. to­Array
    1. Std.DHashMap.to­Array
  95. to­Array
    1. Std.DTreeMap.to­Array
  96. to­Array
    1. Std.HashMap.to­Array
  97. to­Array
    1. Std.HashSet.to­Array
  98. to­Array
    1. Std.TreeMap.to­Array
  99. to­Array
    1. Std.TreeSet.to­Array
  100. to­Array
    1. Subarray.to­Array
  101. to­Array­Impl
    1. List.to­Array­Impl
  102. to­BEq
    1. Ord.to­BEq
  103. to­Base­IO
    1. EIO.to­Base­IO
  104. to­Bind
    1. [anonymous] (class method)
  105. to­Bit­Vec
    1. ISize.to­Bit­Vec
  106. to­Bit­Vec
    1. Int16.to­Bit­Vec
  107. to­Bit­Vec
    1. Int32.to­Bit­Vec
  108. to­Bit­Vec
    1. Int64.to­Bit­Vec
  109. to­Bit­Vec
    1. Int8.to­Bit­Vec
  110. to­Bit­Vec
    1. UInt16.to­Bit­Vec (structure field)
  111. to­Bit­Vec
    1. UInt32.to­Bit­Vec (structure field)
  112. to­Bit­Vec
    1. UInt64.to­Bit­Vec (structure field)
  113. to­Bit­Vec
    1. UInt8.to­Bit­Vec (structure field)
  114. to­Bit­Vec
    1. USize.to­Bit­Vec (structure field)
  115. to­Bits
    1. Float.to­Bits
  116. to­Bits
    1. Float32.to­Bits
  117. to­Bool
    1. Except.to­Bool
  118. to­Byte­Array
    1. ByteSlice.to­Byte­Array
  119. to­Byte­Array
    1. List.to­Byte­Array
  120. to­Byte­Slice
    1. ByteArray.to­Byte­Slice
  121. to­Comm­Ring
    1. Lean.Grind.Field.to­Comm­Ring (class method)
  122. to­Copy
    1. String.Slice.Pos.to­Copy
  123. to­Digits
    1. Nat.to­Digits
  124. to­Div
    1. [anonymous] (class method)
  125. to­EIO
    1. BaseIO.to­EIO
  126. to­EIO
    1. IO.to­EIO
  127. to­End
    1. ByteArray.Iterator.to­End
  128. to­End
    1. String.Legacy.Iterator.to­End
  129. to­Fin
    1. BitVec.to­Fin (structure field)
  130. to­Fin
    1. UInt16.to­Fin
  131. to­Fin
    1. UInt32.to­Fin
  132. to­Fin
    1. UInt64.to­Fin
  133. to­Fin
    1. UInt8.to­Fin
  134. to­Fin
    1. USize.to­Fin
  135. to­Float
    1. Float32.to­Float
  136. to­Float
    1. ISize.to­Float
  137. to­Float
    1. Int16.to­Float
  138. to­Float
    1. Int32.to­Float
  139. to­Float
    1. Int64.to­Float
  140. to­Float
    1. Int8.to­Float
  141. to­Float
    1. Nat.to­Float
  142. to­Float
    1. UInt16.to­Float
  143. to­Float
    1. UInt32.to­Float
  144. to­Float
    1. UInt64.to­Float
  145. to­Float
    1. UInt8.to­Float
  146. to­Float
    1. USize.to­Float
  147. to­Float32
    1. Float.to­Float32
  148. to­Float32
    1. ISize.to­Float32
  149. to­Float32
    1. Int16.to­Float32
  150. to­Float32
    1. Int32.to­Float32
  151. to­Float32
    1. Int64.to­Float32
  152. to­Float32
    1. Int8.to­Float32
  153. to­Float32
    1. Nat.to­Float32
  154. to­Float32
    1. UInt16.to­Float32
  155. to­Float32
    1. UInt32.to­Float32
  156. to­Float32
    1. UInt64.to­Float32
  157. to­Float32
    1. UInt8.to­Float32
  158. to­Float32
    1. USize.to­Float32
  159. to­Float­Array
    1. List.to­Float­Array
  160. to­Format
    1. String.to­Format
  161. to­Functor
    1. Applicative.to­Functor (class method)
  162. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  163. to­Handle­Type
    1. IO.Process.Stdio.to­Handle­Type
  164. to­Hex
    1. BitVec.to­Hex
  165. to­IO'
    1. EIO.to­IO'
  166. to­IO
    1. BaseIO.to­IO
  167. to­IO
    1. EIO.to­IO
  168. to­ISize
    1. Bool.to­ISize
  169. to­ISize
    1. Float.to­ISize
  170. to­ISize
    1. Float32.to­ISize
  171. to­ISize
    1. Int.to­ISize
  172. to­ISize
    1. Int16.to­ISize
  173. to­ISize
    1. Int32.to­ISize
  174. to­ISize
    1. Int64.to­ISize
  175. to­ISize
    1. Int8.to­ISize
  176. to­ISize
    1. Nat.to­ISize
  177. to­ISize
    1. USize.to­ISize
  178. to­Int!
    1. String.to­Int!
  179. to­Int
    1. BitVec.to­Int
  180. to­Int
    1. Bool.to­Int
  181. to­Int
    1. ISize.to­Int
  182. to­Int
    1. Int16.to­Int
  183. to­Int
    1. Int32.to­Int
  184. to­Int
    1. Int64.to­Int
  185. to­Int
    1. Int8.to­Int
  186. to­Int
    1. Lean.Grind.ToInt.to­Int (class method)
  187. to­Int16
    1. Bool.to­Int16
  188. to­Int16
    1. Float.to­Int16
  189. to­Int16
    1. Float32.to­Int16
  190. to­Int16
    1. ISize.to­Int16
  191. to­Int16
    1. Int.to­Int16
  192. to­Int16
    1. Int32.to­Int16
  193. to­Int16
    1. Int64.to­Int16
  194. to­Int16
    1. Int8.to­Int16
  195. to­Int16
    1. Nat.to­Int16
  196. to­Int16
    1. UInt16.to­Int16
  197. to­Int32
    1. Bool.to­Int32
  198. to­Int32
    1. Float.to­Int32
  199. to­Int32
    1. Float32.to­Int32
  200. to­Int32
    1. ISize.to­Int32
  201. to­Int32
    1. Int.to­Int32
  202. to­Int32
    1. Int16.to­Int32
  203. to­Int32
    1. Int64.to­Int32
  204. to­Int32
    1. Int8.to­Int32
  205. to­Int32
    1. Nat.to­Int32
  206. to­Int32
    1. UInt32.to­Int32
  207. to­Int64
    1. Bool.to­Int64
  208. to­Int64
    1. Float.to­Int64
  209. to­Int64
    1. Float32.to­Int64
  210. to­Int64
    1. ISize.to­Int64
  211. to­Int64
    1. Int.to­Int64
  212. to­Int64
    1. Int16.to­Int64
  213. to­Int64
    1. Int32.to­Int64
  214. to­Int64
    1. Int8.to­Int64
  215. to­Int64
    1. Nat.to­Int64
  216. to­Int64
    1. UInt64.to­Int64
  217. to­Int8
    1. Bool.to­Int8
  218. to­Int8
    1. Float.to­Int8
  219. to­Int8
    1. Float32.to­Int8
  220. to­Int8
    1. ISize.to­Int8
  221. to­Int8
    1. Int.to­Int8
  222. to­Int8
    1. Int16.to­Int8
  223. to­Int8
    1. Int32.to­Int8
  224. to­Int8
    1. Int64.to­Int8
  225. to­Int8
    1. Nat.to­Int8
  226. to­Int8
    1. UInt8.to­Int8
  227. to­Int?
    1. String.to­Int?
  228. to­Int_inj
    1. Lean.Grind.ToInt.to­Int_inj (class method)
  229. to­Int_mem
    1. Lean.Grind.ToInt.to­Int_mem (class method)
  230. to­Inv
    1. [anonymous] (class method)
  231. to­LE
    1. Ord.to­LE
  232. to­LT
    1. Ord.to­LT
  233. to­Lawful­Applicative
    1. LawfulMonad.to­Lawful­Applicative (class method)
  234. to­Lawful­Functor
    1. LawfulApplicative.to­Lawful­Functor (class method)
  235. to­Lawful­Monad
    1. Std.Do.WPMonad.to­Lawful­Monad (class method)
  236. to­Lean­Config
    1. Lake.Lean­ExeConfig.to­Lean­Config (structure field)
  237. to­Lean­Config
    1. Lake.Lean­LibConfig.to­Lean­Config (structure field)
  238. to­Legacy­Iterator
    1. Substring.Raw.to­Legacy­Iterator
  239. to­List
    1. Array.to­List
  240. to­List
    1. Array.to­List (structure field)
  241. to­List
    1. ByteArray.to­List
  242. to­List
    1. Option.to­List
  243. to­List
    1. Std.DHashMap.to­List
  244. to­List
    1. Std.DTreeMap.to­List
  245. to­List
    1. Std.HashMap.to­List
  246. to­List
    1. Std.HashSet.to­List
  247. to­List
    1. Std.TreeMap.to­List
  248. to­List
    1. Std.TreeSet.to­List
  249. to­List
    1. String.to­List (0) (1)
  250. to­List­Append
    1. Array.to­List­Append
  251. to­List­Rev
    1. Array.to­List­Rev
  252. to­Lower
    1. Char.to­Lower
  253. to­Lower
    1. String.to­Lower
  254. to­Modify­Of­LE
    1. String.ValidPos.to­Modify­Of­LE
  255. to­Monad­State­Of
    1. ST.Ref.to­Monad­State­Of
  256. to­Mul
    1. [anonymous] (class method)
  257. to­Name
    1. String.to­Name
  258. to­Name
    1. Substring.Raw.to­Name
  259. to­Nat!
    1. String.Slice.to­Nat!
  260. to­Nat!
    1. String.to­Nat!
  261. to­Nat
    1. BitVec.to­Nat
  262. to­Nat
    1. Bool.to­Nat
  263. to­Nat
    1. Char.to­Nat
  264. to­Nat
    1. Fin.to­Nat
  265. to­Nat
    1. Int.to­Nat
  266. to­Nat
    1. UInt16.to­Nat
  267. to­Nat
    1. UInt32.to­Nat
  268. to­Nat
    1. UInt64.to­Nat
  269. to­Nat
    1. UInt8.to­Nat
  270. to­Nat
    1. USize.to­Nat
  271. to­Nat?
    1. Int.to­Nat?
  272. to­Nat?
    1. String.Slice.to­Nat?
  273. to­Nat?
    1. String.to­Nat?
  274. to­Nat?
    1. Substring.Raw.to­Nat?
  275. to­Nat­Clamp­Neg
    1. ISize.to­Nat­Clamp­Neg
  276. to­Nat­Clamp­Neg
    1. Int16.to­Nat­Clamp­Neg
  277. to­Nat­Clamp­Neg
    1. Int32.to­Nat­Clamp­Neg
  278. to­Nat­Clamp­Neg
    1. Int64.to­Nat­Clamp­Neg
  279. to­Nat­Clamp­Neg
    1. Int8.to­Nat­Clamp­Neg
  280. to­Neg
    1. [anonymous] (class method)
  281. to­Option
    1. Except.to­Option
  282. to­Ordered­Add
    1. Lean.Grind.OrderedRing.to­Ordered­Add (class method)
  283. to­Partial­Equiv­BEq
    1. EquivBEq.to­Partial­Equiv­BEq (class method)
  284. to­Partial­Order
    1. Lean.Order.CCPO.to­Partial­Order (class method)
  285. to­Pure
    1. [anonymous] (class method)
  286. to­Raw­Substring'
    1. String.to­Raw­Substring'
  287. to­Raw­Substring
    1. String.to­Raw­Substring
  288. to­Refl­BEq
    1. LawfulBEq.to­Refl­BEq (class method)
  289. to­Refl­BEq
    1. [anonymous] (class method)
  290. to­Replace­Start
    1. String.Slice.Pos.to­Replace­Start
  291. to­Ring
    1. Lean.Grind.CommRing.to­Ring (class method)
  292. to­Searcher
    1. String.Slice.Pattern.To­BackwardSearcher.to­Searcher (class method)
  293. to­Searcher
    1. String.Slice.Pattern.To­ForwardSearcher.to­Searcher (class method)
  294. to­Semiring
    1. Lean.Grind.CommSemiring.to­Semiring (class method)
  295. to­Semiring
    1. Lean.Grind.Ring.to­Semiring (class method)
  296. to­Seq
    1. [anonymous] (class method)
  297. to­Seq­Left
    1. Applicative.to­Pure (class method)
  298. to­Seq­Right
    1. [anonymous] (class method)
  299. to­Set­Of­LE
    1. String.ValidPos.to­Set­Of­LE
  300. to­Slice
    1. String.ValidPos.to­Slice
  301. to­Slice
    1. String.to­Slice
  302. to­Stdio­Config
    1. IO.Process.SpawnArgs.to­Stdio­Config (structure field)
  303. to­String
    1. Char.to­String
  304. to­String
    1. Float.to­String
  305. to­String
    1. Float32.to­String
  306. to­String
    1. IO.Error.to­String
  307. to­String
    1. List.to­String
  308. to­String
    1. String.Legacy.Iterator.to­String
  309. to­String
    1. Substring.Raw.to­String
  310. to­String
    1. System.FilePath.to­String (structure field)
  311. to­Sub
    1. [anonymous] (class method)
  312. to­Sub­Digits
    1. Nat.to­Sub­Digits
  313. to­Subarray
    1. Array.to­Subarray
  314. to­Subscript­String
    1. Nat.to­Subscript­String
  315. to­Super­Digits
    1. Nat.to­Super­Digits
  316. to­Superscript­String
    1. Nat.to­Superscript­String
  317. to­UInt16
    1. Bool.to­UInt16
  318. to­UInt16
    1. Float.to­UInt16
  319. to­UInt16
    1. Float32.to­UInt16
  320. to­UInt16
    1. Int16.to­UInt16 (structure field)
  321. to­UInt16
    1. Nat.to­UInt16
  322. to­UInt16
    1. UInt32.to­UInt16
  323. to­UInt16
    1. UInt64.to­UInt16
  324. to­UInt16
    1. UInt8.to­UInt16
  325. to­UInt16
    1. USize.to­UInt16
  326. to­UInt32
    1. Bool.to­UInt32
  327. to­UInt32
    1. Float.to­UInt32
  328. to­UInt32
    1. Float32.to­UInt32
  329. to­UInt32
    1. Int32.to­UInt32 (structure field)
  330. to­UInt32
    1. Nat.to­UInt32
  331. to­UInt32
    1. UInt16.to­UInt32
  332. to­UInt32
    1. UInt64.to­UInt32
  333. to­UInt32
    1. UInt8.to­UInt32
  334. to­UInt32
    1. USize.to­UInt32
  335. to­UInt64
    1. Bool.to­UInt64
  336. to­UInt64
    1. Float.to­UInt64
  337. to­UInt64
    1. Float32.to­UInt64
  338. to­UInt64
    1. Int64.to­UInt64 (structure field)
  339. to­UInt64
    1. Nat.to­UInt64
  340. to­UInt64
    1. UInt16.to­UInt64
  341. to­UInt64
    1. UInt32.to­UInt64
  342. to­UInt64
    1. UInt8.to­UInt64
  343. to­UInt64
    1. USize.to­UInt64
  344. to­UInt64BE!
    1. ByteArray.to­UInt64BE!
  345. to­UInt64LE!
    1. ByteArray.to­UInt64LE!
  346. to­UInt8
    1. Bool.to­UInt8
  347. to­UInt8
    1. Char.to­UInt8
  348. to­UInt8
    1. Float.to­UInt8
  349. to­UInt8
    1. Float32.to­UInt8
  350. to­UInt8
    1. Int8.to­UInt8 (structure field)
  351. to­UInt8
    1. Nat.to­UInt8
  352. to­UInt8
    1. UInt16.to­UInt8
  353. to­UInt8
    1. UInt32.to­UInt8
  354. to­UInt8
    1. UInt64.to­UInt8
  355. to­UInt8
    1. USize.to­UInt8
  356. to­USize
    1. Bool.to­USize
  357. to­USize
    1. Float.to­USize
  358. to­USize
    1. Float32.to­USize
  359. to­USize
    1. ISize.to­USize (structure field)
  360. to­USize
    1. Nat.to­USize
  361. to­USize
    1. UInt16.to­USize
  362. to­USize
    1. UInt32.to­USize
  363. to­USize
    1. UInt64.to­USize
  364. to­USize
    1. UInt8.to­USize
  365. to­UTF8
    1. String.to­UTF8
  366. to­Upper
    1. Char.to­Upper
  367. to­Upper
    1. String.to­Upper
  368. to­Vector
    1. Array.to­Vector
  369. to­WP
    1. [anonymous] (class method)
  370. toolchain gc (Elan command)
  371. toolchain install (Elan command)
  372. toolchain link (Elan command)
  373. toolchain list (Elan command)
  374. toolchain uninstall (Elan command)
  375. trace
  376. trace
    1. Lean.Macro.trace
  377. trace
    1. tactic.simp.trace (0) (1)
  378. trace.Elab.definition.wf
  379. trace.Meta.Tactic.simp.discharge
  380. trace.Meta.Tactic.simp.rewrite
  381. trace.compiler.ir.result
  382. trace.grind.ematch.instance
  383. trace.grind.split
  384. trace_state (0) (1)
  385. trans
    1. Eq.trans
  386. trans
    1. Equivalence.trans (structure field)
  387. trans
    1. Setoid.trans
  388. trans
    1. Trans.trans (class method)
  389. translate-config (Lake command)
  390. transparency
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  391. trim
    1. Substring.Raw.trim
  392. trim­Ascii
    1. String.Slice.trim­Ascii
  393. trim­Ascii
    1. String.trim­Ascii
  394. trim­Ascii­End
    1. String.Slice.trim­Ascii­End
  395. trim­Ascii­End
    1. String.trim­Ascii­End
  396. trim­Ascii­Start
    1. String.Slice.trim­Ascii­Start
  397. trim­Ascii­Start
    1. String.trim­Ascii­Start
  398. trim­Left
    1. Substring.Raw.trim­Left
  399. trim­Right
    1. Substring.Raw.trim­Right
  400. trivial
  401. truncate
    1. BitVec.truncate
  402. truncate
    1. IO.FS.Handle.truncate
  403. try (0) (1)
  404. try­Catch
    1. EStateM.try­Catch
  405. try­Catch
    1. Except.try­Catch
  406. try­Catch
    1. ExceptT.try­Catch
  407. try­Catch
    1. MonadExcept.try­Catch (class method)
  408. try­Catch
    1. Monad­ExceptOf.try­Catch (class method)
  409. try­Catch
    1. Option.try­Catch
  410. try­Catch
    1. OptionT.try­Catch
  411. try­Catch­The
  412. try­Finally'
    1. MonadFinally.try­Finally' (class method)
  413. try­Lock
    1. IO.FS.Handle.try­Lock
  414. try­Wait
    1. IO.Process.Child.try­Wait
  415. two­Pow
    1. BitVec.two­Pow
  416. type constructor
  417. type
    1. IO.FS.Metadata.type (structure field)
  418. type
    1. eval.type
  419. 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. uget
    1. ByteArray.uget
  184. ule
    1. BitVec.ule
  185. ult
    1. BitVec.ult
  186. umod
    1. BitVec.umod
  187. unattach
    1. Array.unattach
  188. unattach
    1. List.unattach
  189. unattach
    1. Option.unattach
  190. uncurry
    1. Function.uncurry
  191. unfold (0) (1)
  192. unfold­Partial­App
    1. Lean.Meta.DSimp.Config.unfold­Partial­App (structure field)
  193. unfold­Partial­App
    1. Lean.Meta.Simp.Config.unfold­Partial­App (structure field)
  194. unhygienic
  195. union
    1. Std.DHashMap.union
  196. union
    1. Std.HashMap.union
  197. union
    1. Std.HashSet.union
  198. unit
    1. Unit.unit
  199. unit­Of­Array
    1. Std.Ext­HashMap.unit­Of­Array
  200. unit­Of­Array
    1. Std.HashMap.unit­Of­Array
  201. unit­Of­Array
    1. Std.TreeMap.unit­Of­Array
  202. unit­Of­List
    1. Std.Ext­HashMap.unit­Of­List
  203. unit­Of­List
    1. Std.HashMap.unit­Of­List
  204. unit­Of­List
    1. Std.TreeMap.unit­Of­List
  205. universe
  206. universe polymorphism
  207. unlock
    1. IO.FS.Handle.unlock
  208. unnecessary­Simpa
    1. linter.unnecessary­Simpa
  209. unoffset­By
    1. String.Pos.Raw.unoffset­By
  210. unpack (Lake command)
  211. unsafe­Base­IO
  212. unsafe­Cast
  213. unsafe­EIO
  214. unsafe­IO
  215. unsupported­Syntax
    1. Lean.Macro.Exception.unsupported­Syntax
  216. unzip
    1. Array.unzip
  217. unzip
    1. List.unzip
  218. unzip­TR
    1. List.unzip­TR
  219. update (Lake command)
  220. upload (Lake command)
  221. user
    1. IO.FileRight.user (structure field)
  222. user­Error
    1. IO.user­Error
  223. uset
    1. Array.uset
  224. uset
    1. ByteArray.uset
  225. ushift­Right
    1. BitVec.ushift­Right
  226. ushift­Right­Rec
    1. BitVec.ushift­Right­Rec
  227. usize
    1. Array.usize
  228. usize
    1. ByteArray.usize
  229. usub­Overflow
    1. BitVec.usub­Overflow
  230. utf16Size
    1. Char.utf16Size
  231. utf8Byte­Size
    1. String.Slice.utf8Byte­Size
  232. utf8Byte­Size
    1. String.utf8Byte­Size
  233. utf8Decode?
    1. ByteArray.utf8Decode?
  234. utf8Decode­Char
    1. ByteArray.utf8Decode­Char
  235. utf8Decode­Char?
    1. ByteArray.utf8Decode­Char?
  236. utf8Encode­Char
    1. String.utf8Encode­Char
  237. utf8Size
    1. Char.utf8Size

V

  1. Valid­Pos
    1. String.Valid­Pos
  2. val
    1. Char.val (structure field)
  3. val
    1. Fin.val (structure field)
  4. val
    1. Subtype.val (structure field)
  5. valid
    1. Char.valid (structure field)
  6. value
    1. For­InStep.value
  7. value
    1. Lean.LeanOption.value (structure field)
  8. values
    1. Std.DHashMap.values
  9. values
    1. Std.DTreeMap.values
  10. values
    1. Std.HashMap.values
  11. values
    1. Std.TreeMap.values
  12. values­Array
    1. Std.DHashMap.values­Array
  13. values­Array
    1. Std.DTreeMap.values­Array
  14. values­Array
    1. Std.HashMap.values­Array
  15. values­Array
    1. Std.TreeMap.values­Array

W

  1. WF
    1. Std.DHashMap.Raw.WF
  2. WF
    1. Std.DTreeMap.Raw.WF
  3. WF
    1. Std.HashMap.Raw.WF
  4. WF
    1. Std.HashSet.Raw.WF
  5. WF
    1. Std.TreeMap.Raw.WF
  6. WF
    1. Std.TreeSet.Raw.WF
  7. WP
    1. Std.Do.WP
  8. WPMonad
    1. Std.Do.WPMonad
  9. Well­Founded
  10. WellFounded.fix
  11. WellFounded.intro
    1. Constructor of Well­Founded
  12. Well­Founded­Relation
  13. Well­FoundedRelation.mk
    1. Instance constructor of Well­Founded­Relation
  14. wait
    1. IO.Process.Child.wait
  15. wait
    1. IO.wait
  16. wait
    1. Std.Condvar.wait
  17. wait­Any
    1. IO.wait­Any
  18. wait­Until
    1. Std.Condvar.wait­Until
  19. walk­Dir
    1. System.FilePath.walk­Dir
  20. warn­Exponents
    1. Lean.Meta.Simp.Config.warn­Exponents (structure field)
  21. wf
    1. Well­FoundedRelation.wf (class method)
  22. wf
    1. trace.Elab.definition.wf
  23. wf­Param
  24. which (Elan command)
  25. whnf
  26. with­Extension
    1. System.FilePath.with­Extension
  27. with­File
    1. IO.FS.with­File
  28. with­File­Name
    1. System.FilePath.with­File­Name
  29. with­Fresh­Macro­Scope
    1. Lean.Macro.with­Fresh­Macro­Scope
  30. with­Isolated­Streams
    1. IO.FS.with­Isolated­Streams
  31. with­Position
  32. with­Position­After­Linebreak
  33. with­Reader
    1. Monad­WithReader.with­Reader (class method)
  34. with­Reader
    1. Monad­With­ReaderOf.with­Reader (class method)
  35. with­Stderr
    1. IO.with­Stderr
  36. with­Stdin
    1. IO.with­Stdin
  37. with­Stdout
    1. IO.with­Stdout
  38. with­Temp­Dir
    1. IO.FS.with­Temp­Dir
  39. with­Temp­File
    1. IO.FS.with­Temp­File
  40. with­The­Reader
  41. with_reducible (0) (1)
  42. with_reducible_and_instances (0) (1)
  43. with_unfolding_all (0) (1)
  44. without­Position
  45. wp
    1. Std.Do.WP.wp (class method)
  46. wp_bind
    1. [anonymous] (class method)
  47. wp_pure
    1. [anonymous] (class method)
  48. write
    1. IO.AccessRight.write (structure field)
  49. write
    1. IO.FS.Handle.write
  50. write
    1. IO.FS.Stream.write (structure field)
  51. write­Bin­File
    1. IO.FS.write­Bin­File
  52. write­File
    1. IO.FS.write­File

X

  1. Xor­Op
  2. XorOp.mk
    1. Instance constructor of Xor­Op
  3. xor
    1. BitVec.xor
  4. xor
    1. Bool.xor
  5. xor
    1. Fin.xor
  6. xor
    1. ISize.xor
  7. xor
    1. Int16.xor
  8. xor
    1. Int32.xor
  9. xor
    1. Int64.xor
  10. xor
    1. Int8.xor
  11. xor
    1. Nat.xor
  12. xor
    1. UInt16.xor
  13. xor
    1. UInt32.xor
  14. xor
    1. UInt64.xor
  15. xor
    1. UInt8.xor
  16. xor
    1. USize.xor
  17. xor
    1. XorOp.xor (class method)

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. zero_lt_one
    1. [anonymous] (class method)
  7. zero_mul
    1. Lean.Grind.Semiring.left_distrib (class method)
  8. zero_ne_one
    1. [anonymous] (class method)
  9. zero_nsmul
    1. [anonymous] (class method)
  10. zero_zsmul
    1. [anonymous] (class method)
  11. zeta
  12. zeta
    1. Lean.Meta.DSimp.Config.zeta (structure field)
  13. zeta
    1. Lean.Meta.Simp.Config.zeta (structure field)
  14. zeta­Delta
    1. Lean.Meta.DSimp.Config.zeta­Delta (structure field)
  15. zeta­Delta
    1. Lean.Meta.Simp.Config.zeta­Delta (structure field)
  16. zeta­Have
    1. Lean.Meta.DSimp.Config.zeta­Have (structure field)
  17. zeta­Have
    1. Lean.Meta.Simp.Config.zeta­Have (structure field)
  18. zeta­Unused
    1. Lean.Meta.DSimp.Config.zeta­Unused (structure field)
  19. zeta­Unused
    1. Lean.Meta.Simp.Config.zeta­Unused (structure field)
  20. zip
    1. Array.zip
  21. zip
    1. List.zip
  22. zip­Idx
    1. Array.zip­Idx
  23. zip­Idx
    1. List.zip­Idx
  24. zip­Idx­TR
    1. List.zip­Idx­TR
  25. zip­With
    1. Array.zip­With
  26. zip­With
    1. List.zip­With
  27. zip­With­All
    1. Array.zip­With­All
  28. zip­With­All
    1. List.zip­With­All
  29. zip­With­TR
    1. List.zip­With­TR
  30. zpow
    1. [anonymous] (class method)
  31. zpow_neg
    1. [anonymous] (class method)
  32. zpow_succ
    1. [anonymous] (class method)
  33. zpow_zero
    1. [anonymous] (class method)
  34. zsmul
    1. [anonymous] (class method) (0) (1)
  35. zsmul_nat­Cast_eq_nsmul
    1. [anonymous] (class method) (0) (1)