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.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.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?
  270. apply_assumption
  271. apply_ext_theorem
  272. apply_mod_cast
  273. apply_rfl
  274. apply_rules
  275. arg [@]i
  276. args
  277. args
    1. [anonymous] (structure field)
  278. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  279. array
    1. ByteArray.Iterator.array (structure field)
  280. array
    1. Subarray.array
  281. as­String
    1. List.as­String
  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.Iterator.at­End
  295. at­End
    1. String.Pos.Raw.at­End
  296. at­End
    1. Substring.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.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.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.common­Prefix
  130. common­Suffix
    1. Substring.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. cons
    1. BitVec.cons
  159. const
    1. Function.const
  160. constructor (0) (1)
  161. contains
    1. Array.contains
  162. contains
    1. ByteSlice.contains
  163. contains
    1. List.contains
  164. contains
    1. Std.DHashMap.contains
  165. contains
    1. Std.DTreeMap.contains
  166. contains
    1. Std.Ext­DHashMap.contains
  167. contains
    1. Std.Ext­HashMap.contains
  168. contains
    1. Std.Ext­HashSet.contains
  169. contains
    1. Std.HashMap.contains
  170. contains
    1. Std.HashSet.contains
  171. contains
    1. Std.TreeMap.contains
  172. contains
    1. Std.TreeSet.contains
  173. contains
    1. String.Slice.contains
  174. contains
    1. String.contains
  175. contains
    1. Substring.contains
  176. contains­Then­Insert
    1. Std.DHashMap.contains­Then­Insert
  177. contains­Then­Insert
    1. Std.DTreeMap.contains­Then­Insert
  178. contains­Then­Insert
    1. Std.Ext­DHashMap.contains­Then­Insert
  179. contains­Then­Insert
    1. Std.Ext­HashMap.contains­Then­Insert
  180. contains­Then­Insert
    1. Std.Ext­HashSet.contains­Then­Insert
  181. contains­Then­Insert
    1. Std.HashMap.contains­Then­Insert
  182. contains­Then­Insert
    1. Std.HashSet.contains­Then­Insert
  183. contains­Then­Insert
    1. Std.TreeMap.contains­Then­Insert
  184. contains­Then­Insert
    1. Std.TreeSet.contains­Then­Insert
  185. contains­Then­Insert­If­New
    1. Std.DHashMap.contains­Then­Insert­If­New
  186. contains­Then­Insert­If­New
    1. Std.DTreeMap.contains­Then­Insert­If­New
  187. contains­Then­Insert­If­New
    1. Std.Ext­DHashMap.contains­Then­Insert­If­New
  188. contains­Then­Insert­If­New
    1. Std.Ext­HashMap.contains­Then­Insert­If­New
  189. contains­Then­Insert­If­New
    1. Std.HashMap.contains­Then­Insert­If­New
  190. contains­Then­Insert­If­New
    1. Std.TreeMap.contains­Then­Insert­If­New
  191. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  192. contradiction
  193. control
  194. control­At
  195. conv
  196. conv => ...
  197. conv' (0) (1)
  198. copy
    1. String.Slice.copy
  199. copy­Slice
    1. ByteArray.copy­Slice
  200. cos
    1. Float.cos
  201. cos
    1. Float32.cos
  202. cosh
    1. Float.cosh
  203. cosh
    1. Float32.cosh
  204. count
    1. Array.count
  205. count
    1. List.count
  206. count­P
    1. Array.count­P
  207. count­P
    1. List.count­P
  208. create­Dir
    1. IO.FS.create­Dir
  209. create­Dir­All
    1. IO.FS.create­Dir­All
  210. create­Temp­Dir
    1. IO.FS.create­Temp­Dir
  211. create­Temp­File
    1. IO.FS.create­Temp­File
  212. crlf­To­Lf
    1. String.crlf­To­Lf
  213. csup
    1. [anonymous] (class method)
  214. csup_spec
    1. [anonymous] (class method)
  215. cumulativity
  216. curr'
    1. ByteArray.Iterator.curr'
  217. curr'
    1. String.Iterator.curr'
  218. curr
    1. ByteArray.Iterator.curr
  219. curr
    1. String.Iterator.curr
  220. curr­Column
    1. Std.Format.Monad­PrettyFormat.curr­Column (class method)
  221. current­Dir
    1. IO.current­Dir
  222. curry
    1. Function.curry
  223. custom­Eliminators
    1. tactic.custom­Eliminators
  224. 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. data
    1. String.data
  21. dbg­Trace­If­Shared
  22. dbg_trace
  23. dcond
    1. Bool.dcond
  24. dec
    1. String.Pos.Raw.dec
  25. dec­Eq
    1. BitVec.dec­Eq
  26. dec­Eq
    1. Bool.dec­Eq
  27. dec­Eq
    1. ISize.dec­Eq
  28. dec­Eq
    1. Int.dec­Eq
  29. dec­Eq
    1. Int16.dec­Eq
  30. dec­Eq
    1. Int32.dec­Eq
  31. dec­Eq
    1. Int64.dec­Eq
  32. dec­Eq
    1. Int8.dec­Eq
  33. dec­Eq
    1. Nat.dec­Eq
  34. dec­Eq
    1. String.dec­Eq
  35. dec­Eq
    1. UInt16.dec­Eq
  36. dec­Eq
    1. UInt32.dec­Eq
  37. dec­Eq
    1. UInt64.dec­Eq
  38. dec­Eq
    1. UInt8.dec­Eq
  39. dec­Eq
    1. USize.dec­Eq
  40. dec­Le
    1. Float.dec­Le
  41. dec­Le
    1. Float32.dec­Le
  42. dec­Le
    1. ISize.dec­Le
  43. dec­Le
    1. Int16.dec­Le
  44. dec­Le
    1. Int32.dec­Le
  45. dec­Le
    1. Int64.dec­Le
  46. dec­Le
    1. Int8.dec­Le
  47. dec­Le
    1. Nat.dec­Le
  48. dec­Le
    1. UInt16.dec­Le
  49. dec­Le
    1. UInt32.dec­Le
  50. dec­Le
    1. UInt64.dec­Le
  51. dec­Le
    1. UInt8.dec­Le
  52. dec­Le
    1. USize.dec­Le
  53. dec­Lt
    1. Float.dec­Lt
  54. dec­Lt
    1. Float32.dec­Lt
  55. dec­Lt
    1. ISize.dec­Lt
  56. dec­Lt
    1. Int16.dec­Lt
  57. dec­Lt
    1. Int32.dec­Lt
  58. dec­Lt
    1. Int64.dec­Lt
  59. dec­Lt
    1. Int8.dec­Lt
  60. dec­Lt
    1. Nat.dec­Lt
  61. dec­Lt
    1. UInt16.dec­Lt
  62. dec­Lt
    1. UInt32.dec­Lt
  63. dec­Lt
    1. UInt64.dec­Lt
  64. dec­Lt
    1. UInt8.dec­Lt
  65. dec­Lt
    1. USize.dec­Lt
  66. decapitalize
    1. String.decapitalize
  67. decidable
  68. decidable­Eq­None
    1. Option.decidable­Eq­None
  69. decide
  70. decide
    1. Decidable.decide
  71. decide
    1. Lean.Meta.DSimp.Config.decide (structure field)
  72. decide
    1. Lean.Meta.Simp.Config.decide (structure field)
  73. decrease­By
    1. String.Pos.Raw.decrease­By
  74. decreasing_tactic
  75. decreasing_trivial
  76. decreasing_with
  77. dedicated
    1. Task.Priority.dedicated
  78. deep­Terms
    1. pp.deep­Terms
  79. def­Indent
    1. Std.Format.def­Indent
  80. def­Width
    1. Std.Format.def­Width
  81. default (Elan command)
  82. default
    1. Inhabited.default (class method)
  83. default
    1. Task.Priority.default
  84. default­Facets
    1. [anonymous] (structure field)
  85. delta (0) (1)
  86. diff
    1. guard_msgs.diff
  87. digit­Char
    1. Nat.digit­Char
  88. discard
    1. Functor.discard
  89. discharge
    1. trace.Meta.Tactic.simp.discharge
  90. div
    1. Div.div (class method)
  91. div
    1. Fin.div
  92. div
    1. Float.div
  93. div
    1. Float32.div
  94. div
    1. ISize.div
  95. div
    1. Int16.div
  96. div
    1. Int32.div
  97. div
    1. Int64.div
  98. div
    1. Int8.div
  99. div
    1. Nat.div
  100. div
    1. UInt16.div
  101. div
    1. UInt32.div
  102. div
    1. UInt64.div
  103. div
    1. UInt8.div
  104. div
    1. USize.div
  105. div2Induction
    1. Nat.div2Induction
  106. div­Rec
    1. BitVec.div­Rec
  107. div­Subtract­Shift
    1. BitVec.div­Subtract­Shift
  108. div_eq_mul_inv
    1. [anonymous] (class method)
  109. done (0) (1)
  110. down
    1. PLift.down (structure field)
  111. down
    1. ULift.down (structure field)
  112. drop
    1. Array.drop
  113. drop
    1. List.drop
  114. drop
    1. String.Slice.drop
  115. drop
    1. String.drop
  116. drop
    1. Subarray.drop
  117. drop
    1. Substring.drop
  118. drop­End
    1. String.Slice.drop­End
  119. drop­End­While
    1. String.Slice.drop­End­While
  120. drop­Last
    1. List.drop­Last
  121. drop­Last­TR
    1. List.drop­Last­TR
  122. drop­Prefix
    1. String.Slice.drop­Prefix
  123. drop­Prefix?
    1. String.Slice.Pattern.ForwardPattern.drop­Prefix? (class method)
  124. drop­Prefix?
    1. String.Slice.drop­Prefix?
  125. drop­Prefix?
    1. String.drop­Prefix?
  126. drop­Prefix?
    1. Substring.drop­Prefix?
  127. drop­Right
    1. String.drop­Right
  128. drop­Right
    1. Substring.drop­Right
  129. drop­Right­While
    1. String.drop­Right­While
  130. drop­Right­While
    1. Substring.drop­Right­While
  131. drop­Suffix
    1. String.Slice.drop­Suffix
  132. drop­Suffix?
    1. String.Slice.Pattern.BackwardPattern.drop­Suffix? (class method)
  133. drop­Suffix?
    1. String.Slice.drop­Suffix?
  134. drop­Suffix?
    1. String.drop­Suffix?
  135. drop­Suffix?
    1. Substring.drop­Suffix?
  136. drop­While
    1. List.drop­While
  137. drop­While
    1. String.Slice.drop­While
  138. drop­While
    1. String.drop­While
  139. drop­While
    1. Substring.drop­While
  140. dsimp (0) (1)
  141. dsimp!
  142. dsimp
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  143. dsimp?
  144. dsimp?!
  145. 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­Pos
    1. String.end­Pos
  125. end­Tags
    1. Std.Format.Monad­PrettyFormat.end­Tags (class method)
  126. end­Valid­Pos
    1. String.end­Valid­Pos
  127. ends­With
    1. String.Slice.Pattern.BackwardPattern.ends­With (class method)
  128. ends­With
    1. String.Slice.ends­With
  129. ends­With
    1. String.ends­With
  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.Iterator.extract
  206. extract
    1. String.Pos.Raw.extract
  207. extract
    1. String.ValidPos.extract
  208. extract
    1. Substring.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.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.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.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.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.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.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.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.Iterator.has­Next
  62. has­Prev
    1. ByteArray.Iterator.has­Prev
  63. has­Prev
    1. String.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.Iterator
  401. i
    1. String.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.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.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.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.as­String
  267. List.attach
  268. List.attach­With
  269. List.beq
  270. List.concat
  271. List.cons
    1. Constructor of List
  272. List.contains
  273. List.count
  274. List.count­P
  275. List.drop
  276. List.drop­Last
  277. List.drop­Last­TR
  278. List.drop­While
  279. List.elem
  280. List.erase
  281. List.erase­Dups
  282. List.erase­Idx
  283. List.erase­Idx­TR
  284. List.erase­P
  285. List.erase­PTR
  286. List.erase­Reps
  287. List.erase­TR
  288. List.extract
  289. List.filter
  290. List.filter­M
  291. List.filter­Map
  292. List.filter­Map­M
  293. List.filter­Map­TR
  294. List.filter­Rev­M
  295. List.filter­TR
  296. List.fin­Idx­Of?
  297. List.fin­Range
  298. List.find?
  299. List.find­Fin­Idx?
  300. List.find­Idx
  301. List.find­Idx?
  302. List.find­M?
  303. List.find­Some?
  304. List.find­Some­M?
  305. List.first­M
  306. List.flat­Map
  307. List.flat­Map­M
  308. List.flat­Map­TR
  309. List.flatten
  310. List.flatten­TR
  311. List.foldl
  312. List.foldl­M
  313. List.foldl­Rec­On
  314. List.foldr
  315. List.foldr­M
  316. List.foldr­Rec­On
  317. List.foldr­TR
  318. List.for­A
  319. List.for­M
  320. List.get
  321. List.get­D
  322. List.get­Last
  323. List.get­Last!
  324. List.get­Last?
  325. List.get­Last­D
  326. List.group­By­Key
  327. List.head
  328. List.head!
  329. List.head?
  330. List.head­D
  331. List.idx­Of
  332. List.idx­Of?
  333. List.insert
  334. List.insert­Idx
  335. List.insert­Idx­TR
  336. List.intercalate
  337. List.intercalate­TR
  338. List.intersperse
  339. List.intersperse­TR
  340. List.is­Empty
  341. List.is­Eqv
  342. List.is­Perm
  343. List.is­Prefix­Of
  344. List.is­Prefix­Of?
  345. List.is­Sublist
  346. List.is­Suffix­Of
  347. List.is­Suffix­Of?
  348. List.le
  349. List.leftpad
  350. List.leftpad­TR
  351. List.length
  352. List.length­TR
  353. List.lex
  354. List.lookup
  355. List.lt
  356. List.map
  357. List.map­A
  358. List.map­Fin­Idx
  359. List.map­Fin­Idx­M
  360. List.map­Idx
  361. List.map­Idx­M
  362. List.map­M
  363. List.map­M'
  364. List.map­Mono
  365. List.map­Mono­M
  366. List.map­TR
  367. List.max?
  368. List.merge
  369. List.merge­Sort
  370. List.min?
  371. List.modify
  372. List.modify­Head
  373. List.modify­TR
  374. List.modify­Tail­Idx
  375. List.nil
    1. Constructor of List
  376. List.of­Fn
  377. List.or
  378. List.partition
  379. List.partition­M
  380. List.partition­Map
  381. List.pmap
  382. List.range
  383. List.range'
  384. List.range'TR
  385. List.remove­All
  386. List.replace
  387. List.replace­TR
  388. List.replicate
  389. List.replicate­TR
  390. List.reverse
  391. List.rightpad
  392. List.rotate­Left
  393. List.rotate­Right
  394. List.set
  395. List.set­TR
  396. List.singleton
  397. List.span
  398. List.split­At
  399. List.split­By
  400. List.sum
  401. List.tail
  402. List.tail!
  403. List.tail?
  404. List.tail­D
  405. List.take
  406. List.take­TR
  407. List.take­While
  408. List.take­While­TR
  409. List.to­Array
  410. List.to­Array­Impl
  411. List.to­Byte­Array
  412. List.to­Float­Array
  413. List.to­String
  414. List.unattach
  415. List.unzip
  416. List.unzip­TR
  417. List.zip
  418. List.zip­Idx
  419. List.zip­Idx­TR
  420. List.zip­With
  421. List.zip­With­All
  422. List.zip­With­TR
  423. land
    1. Fin.land
  424. land
    1. ISize.land
  425. land
    1. Int16.land
  426. land
    1. Int32.land
  427. land
    1. Int64.land
  428. land
    1. Int8.land
  429. land
    1. Nat.land
  430. land
    1. UInt16.land
  431. land
    1. UInt32.land
  432. land
    1. UInt64.land
  433. land
    1. UInt8.land
  434. land
    1. USize.land
  435. last
    1. Fin.last
  436. last­Cases
    1. Fin.last­Cases
  437. lazy­Pure
    1. IO.lazy­Pure
  438. lcm
    1. Int.lcm
  439. lcm
    1. Nat.lcm
  440. le
    1. Char.le
  441. le
    1. Float.le
  442. le
    1. Float32.le
  443. le
    1. ISize.le
  444. le
    1. Int.le
  445. le
    1. Int16.le
  446. le
    1. Int32.le
  447. le
    1. Int64.le
  448. le
    1. Int8.le
  449. le
    1. LE.le (class method)
  450. le
    1. List.le
  451. le
    1. Nat.le
  452. le
    1. String.le
  453. le
    1. UInt16.le
  454. le
    1. UInt32.le
  455. le
    1. UInt64.le
  456. le
    1. UInt8.le
  457. le
    1. USize.le
  458. le­Of­Ord
  459. lean (Lake command)
  460. lean_is_array
  461. lean_is_string
  462. lean_string_object (0) (1)
  463. lean_to_array
  464. lean_to_string
  465. left (0) (1)
  466. left
    1. And.left (structure field)
  467. left_distrib
    1. Lean.Grind.Semiring.mul_one (class method)
  468. leftpad
    1. Array.leftpad
  469. leftpad
    1. List.leftpad
  470. leftpad­TR
    1. List.leftpad­TR
  471. length
    1. List.length
  472. length
    1. String.length
  473. length­TR
    1. List.length­TR
  474. let
  475. let rec
  476. let'
  477. let­I
  478. let­To­Have
    1. Lean.Meta.Simp.Config.let­To­Have (structure field)
  479. level
    1. of universe
  480. lex'
    1. Ord.lex'
  481. lex
    1. Array.lex
  482. lex
    1. List.lex
  483. lex
    1. Ord.lex
  484. lex­Lt
    1. Prod.lex­Lt
  485. lhs
  486. lib­Name
    1. [anonymous] (structure field)
  487. lib­Prefix­On­Windows
    1. [anonymous] (structure field)
  488. lift
    1. Except­CpsT.lift
  489. lift
    1. ExceptT.lift
  490. lift
    1. OptionT.lift
  491. lift
    1. Quot.lift
  492. lift
    1. Quotient.lift
  493. lift
    1. Squash.lift
  494. lift
    1. State­CpsT.lift
  495. lift
    1. State­RefT'.lift
  496. lift
    1. StateT.lift
  497. lift­On
    1. Quot.lift­On
  498. lift­On
    1. Quotient.lift­On
  499. lift­On₂
    1. Quotient.lift­On₂
  500. lift­With
    1. MonadControl.lift­With (class method)
  501. lift­With
    1. Monad­ControlT.lift­With (class method)
  502. lift₂
    1. Quotient.lift₂
  503. line­Eq
  504. lines
    1. IO.FS.lines
  505. lines
    1. String.Slice.lines
  506. lint (Lake command)
  507. linter.unnecessary­Simpa
  508. literal
    1. raw string
  509. literal
    1. string
  510. lock
    1. IO.FS.Handle.lock
  511. log
    1. Float.log
  512. log
    1. Float32.log
  513. log10
    1. Float.log10
  514. log10
    1. Float32.log10
  515. log2
    1. Fin.log2
  516. log2
    1. Float.log2
  517. log2
    1. Float32.log2
  518. log2
    1. Nat.log2
  519. log2
    1. UInt16.log2
  520. log2
    1. UInt32.log2
  521. log2
    1. UInt64.log2
  522. log2
    1. UInt8.log2
  523. log2
    1. USize.log2
  524. lookup
    1. List.lookup
  525. lor
    1. Fin.lor
  526. lor
    1. ISize.lor
  527. lor
    1. Int16.lor
  528. lor
    1. Int32.lor
  529. lor
    1. Int64.lor
  530. lor
    1. Int8.lor
  531. lor
    1. Nat.lor
  532. lor
    1. UInt16.lor
  533. lor
    1. UInt32.lor
  534. lor
    1. UInt64.lor
  535. lor
    1. UInt8.lor
  536. lor
    1. USize.lor
  537. lt
    1. Char.lt
  538. lt
    1. Float.lt
  539. lt
    1. Float32.lt
  540. lt
    1. ISize.lt
  541. lt
    1. Int.lt
  542. lt
    1. Int16.lt
  543. lt
    1. Int32.lt
  544. lt
    1. Int64.lt
  545. lt
    1. Int8.lt
  546. lt
    1. LT.lt (class method)
  547. lt
    1. List.lt
  548. lt
    1. Nat.lt
  549. lt
    1. Option.lt
  550. lt
    1. UInt16.lt
  551. lt
    1. UInt32.lt
  552. lt
    1. UInt64.lt
  553. lt
    1. UInt8.lt
  554. lt
    1. USize.lt
  555. 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
    1. String.mk
  196. mk­File­Path
    1. System.mk­File­Path
  197. mk­Iterator
    1. String.mk­Iterator
  198. mk­Ref
    1. IO.mk­Ref
  199. mk­Ref
    1. ST.mk­Ref
  200. mk­Std­Gen
  201. mleave
  202. mleft
  203. mod
    1. Fin.mod
  204. mod
    1. ISize.mod
  205. mod
    1. Int16.mod
  206. mod
    1. Int32.mod
  207. mod
    1. Int64.mod
  208. mod
    1. Int8.mod
  209. mod
    1. Mod.mod (class method)
  210. mod
    1. Nat.mod
  211. mod
    1. UInt16.mod
  212. mod
    1. UInt32.mod
  213. mod
    1. UInt64.mod
  214. mod
    1. UInt8.mod
  215. mod
    1. USize.mod
  216. mod­Core
    1. Nat.mod­Core
  217. modified
    1. IO.FS.Metadata.modified (structure field)
  218. modify
  219. modify
    1. Array.modify
  220. modify
    1. List.modify
  221. modify
    1. ST.Ref.modify
  222. modify
    1. Std.DHashMap.modify
  223. modify
    1. Std.DTreeMap.modify
  224. modify
    1. Std.Ext­DHashMap.modify
  225. modify
    1. Std.Ext­HashMap.modify
  226. modify
    1. Std.HashMap.modify
  227. modify
    1. Std.TreeMap.modify
  228. modify
    1. String.Pos.Raw.modify
  229. modify
    1. String.ValidPos.modify
  230. modify­Get
    1. EStateM.modify­Get
  231. modify­Get
    1. MonadState.modify­Get
  232. modify­Get
    1. MonadState.modify­Get (class method)
  233. modify­Get
    1. Monad­StateOf.modify­Get (class method)
  234. modify­Get
    1. ST.Ref.modify­Get
  235. modify­Get
    1. State­RefT'.modify­Get
  236. modify­Get
    1. StateT.modify­Get
  237. modify­Get­The
  238. modify­Head
    1. List.modify­Head
  239. modify­M
    1. Array.modify­M
  240. modify­Of­LE
    1. String.ValidPos.modify­Of­LE
  241. modify­Op
    1. Array.modify­Op
  242. modify­TR
    1. List.modify­TR
  243. modify­Tail­Idx
    1. List.modify­Tail­Idx
  244. modify­The
  245. modn
    1. Fin.modn
  246. monad­Eval
    1. MonadEval.monad­Eval (class method)
  247. monad­Eval
    1. Monad­EvalT.monad­Eval (class method)
  248. monad­Lift
    1. MonadLift.monad­Lift (class method)
  249. monad­Lift
    1. Monad­LiftT.monad­Lift (class method)
  250. monad­Map
    1. MonadFunctor.monad­Map (class method)
  251. monad­Map
    1. Monad­FunctorT.monad­Map (class method)
  252. mono­Ms­Now
    1. IO.mono­Ms­Now
  253. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  254. monotone
    1. Lean.Order.monotone
  255. mp
    1. Eq.mp
  256. mp
    1. Iff.mp (structure field)
  257. mpr
    1. Eq.mpr
  258. mpr
    1. Iff.mpr (structure field)
  259. mpure
  260. mpure_intro
  261. mrefine
  262. mrename_i
  263. mreplace
  264. mright
  265. msb
    1. BitVec.msb
  266. mspec
  267. mspecialize
  268. mspecialize_pure
  269. mstart
  270. mstop
  271. mul
    1. BitVec.mul
  272. mul
    1. Fin.mul
  273. mul
    1. Float.mul
  274. mul
    1. Float32.mul
  275. mul
    1. ISize.mul
  276. mul
    1. Int.mul
  277. mul
    1. Int16.mul
  278. mul
    1. Int32.mul
  279. mul
    1. Int64.mul
  280. mul
    1. Int8.mul
  281. mul
    1. Mul.mul (class method)
  282. mul
    1. Nat.mul
  283. mul
    1. UInt16.mul
  284. mul
    1. UInt32.mul
  285. mul
    1. UInt64.mul
  286. mul
    1. UInt8.mul
  287. mul
    1. USize.mul
  288. mul­Rec
    1. BitVec.mul­Rec
  289. mul_assoc
    1. Lean.Grind.Semiring.add_comm (class method)
  290. mul_comm
    1. [anonymous] (class method) (0) (1)
  291. mul_inv_cancel
    1. [anonymous] (class method)
  292. mul_lt_mul_of_pos_left
    1. Lean.Grind.OrderedRing.zero_lt_one (class method)
  293. mul_lt_mul_of_pos_right
    1. Lean.Grind.OrderedRing.mul_lt_mul_of_pos_left (class method)
  294. mul_one
    1. Lean.Grind.Semiring.add_assoc (class method)
  295. mul_zero
    1. Lean.Grind.Semiring.right_distrib (class method)
  296. mvars
    1. pp.mvars
  297. 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.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.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.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.Iterator.nextn
  159. nextn
    1. String.Slice.Pos.nextn
  160. nextn
    1. Substring.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­Nat
    1. BitVec.of­Nat
  150. of­Nat
    1. Char.of­Nat
  151. of­Nat
    1. Fin.of­Nat
  152. of­Nat
    1. Float.of­Nat
  153. of­Nat
    1. Float32.of­Nat
  154. of­Nat
    1. ISize.of­Nat
  155. of­Nat
    1. Int16.of­Nat
  156. of­Nat
    1. Int32.of­Nat
  157. of­Nat
    1. Int64.of­Nat
  158. of­Nat
    1. Int8.of­Nat
  159. of­Nat
    1. OfNat.of­Nat (class method)
  160. of­Nat
    1. UInt16.of­Nat
  161. of­Nat
    1. UInt32.of­Nat
  162. of­Nat
    1. UInt64.of­Nat
  163. of­Nat
    1. UInt8.of­Nat
  164. of­Nat
    1. USize.of­Nat
  165. of­Nat
    1. [anonymous] (class method)
  166. of­Nat32
    1. USize.of­Nat32
  167. of­Nat­LT
    1. BitVec.of­Nat­LT
  168. of­Nat­LT
    1. UInt16.of­Nat­LT
  169. of­Nat­LT
    1. UInt32.of­Nat­LT
  170. of­Nat­LT
    1. UInt64.of­Nat­LT
  171. of­Nat­LT
    1. UInt8.of­Nat­LT
  172. of­Nat­LT
    1. USize.of­Nat­LT
  173. of­Nat­Truncate
    1. UInt16.of­Nat­Truncate
  174. of­Nat­Truncate
    1. UInt32.of­Nat­Truncate
  175. of­Nat­Truncate
    1. UInt64.of­Nat­Truncate
  176. of­Nat­Truncate
    1. UInt8.of­Nat­Truncate
  177. of­Nat­Truncate
    1. USize.of­Nat­Truncate
  178. of­Nat_eq_nat­Cast
    1. Lean.Grind.Semiring.pow_succ (class method)
  179. of­Nat_ext_iff
    1. Lean.Grind.Is­CharP.of­Nat_ext_iff (class method)
  180. of­Nat_succ
    1. Lean.Grind.Semiring.pow_zero (class method)
  181. of­Replace­Start
    1. String.Slice.Pos.of­Replace­Start
  182. of­Scientific
    1. Float.of­Scientific
  183. of­Scientific
    1. Float32.of­Scientific
  184. of­Scientific
    1. OfScientific.of­Scientific (class method)
  185. of­Slice
    1. String.Slice.Pos.of­Slice
  186. of­Subarray
    1. Array.of­Subarray
  187. of­UInt8
    1. Char.of­UInt8
  188. offset
    1. String.Slice.Pos.offset (structure field)
  189. offset
    1. String.ValidPos.offset (structure field)
  190. offset­By
    1. String.Pos.Raw.offset­By
  191. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  192. offset­Of­Pos
    1. String.offset­Of­Pos
  193. omega
  194. on
    1. Ord.on
  195. one_mul
    1. Lean.Grind.Semiring.mul_assoc (class method)
  196. one_zsmul
    1. [anonymous] (class method)
  197. open
  198. opposite
    1. Ord.opposite
  199. opt­Param
  200. optional
  201. or
    1. BitVec.or
  202. or
    1. Bool.or
  203. or
    1. List.or
  204. or
    1. Option.or
  205. or
    1. OrOp.or (class method)
  206. or­Else'
    1. EStateM.or­Else'
  207. or­Else
    1. EStateM.or­Else
  208. or­Else
    1. MonadExcept.or­Else
  209. or­Else
    1. Option.or­Else
  210. or­Else
    1. OptionT.or­Else
  211. or­Else
    1. ReaderT.or­Else
  212. or­Else
    1. StateT.or­Else
  213. or­Else
    1. [anonymous] (class method)
  214. or­Else­Lazy
    1. Except.or­Else­Lazy
  215. or­M
  216. orelse'
    1. MonadExcept.orelse'
  217. other
    1. IO.FileRight.other (structure field)
  218. out
    1. NeZero.out (class method)
  219. out
    1. Std.DTreeMap.Raw.WF.out (structure field)
  220. out
    1. Std.HashMap.Raw.WF.out (structure field)
  221. out
    1. Std.HashSet.Raw.WF.out (structure field)
  222. out
    1. Std.TreeMap.Raw.WF.out (structure field)
  223. out
    1. Std.TreeSet.Raw.WF.out (structure field)
  224. out­Param
  225. output
    1. IO.Process.output
  226. override list (Elan command)
  227. override set (Elan command)
  228. 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. Preresolved
    1. Lean.Syntax.Preresolved
  24. Prio
    1. Lean.Syntax.Prio
  25. Priority
    1. Task.Priority
  26. Prod
  27. Prod.all­I
  28. Prod.any­I
  29. Prod.fold­I
  30. Prod.lex­Lt
  31. Prod.map
  32. Prod.mk
    1. Constructor of Prod
  33. Prod.swap
  34. Promise
    1. IO.Promise
  35. Prop
  36. Pure
  37. Pure.mk
    1. Instance constructor of Pure
  38. pack (Lake command)
  39. parameter
    1. of inductive type
  40. paren
    1. Std.Format.paren
  41. parent
    1. System.FilePath.parent
  42. parser
  43. partition
    1. Array.partition
  44. partition
    1. List.partition
  45. partition
    1. Std.DHashMap.partition
  46. partition
    1. Std.DTreeMap.partition
  47. partition
    1. Std.HashMap.partition
  48. partition
    1. Std.HashSet.partition
  49. partition
    1. Std.TreeMap.partition
  50. partition
    1. Std.TreeSet.partition
  51. partition­M
    1. List.partition­M
  52. partition­Map
    1. List.partition­Map
  53. path
    1. IO.FS.DirEntry.path
  54. path­Exists
    1. System.FilePath.path­Exists
  55. path­Separator
    1. System.FilePath.path­Separator
  56. path­Separators
    1. System.FilePath.path­Separators
  57. pattern
  58. pbind
    1. Option.pbind
  59. pelim
    1. Option.pelim
  60. placeholder term
  61. pmap
    1. Array.pmap
  62. pmap
    1. List.pmap
  63. pmap
    1. Option.pmap
  64. polymorphism
    1. universe
  65. pop
    1. Array.pop
  66. pop­Front
    1. Subarray.pop­Front
  67. pop­While
    1. Array.pop­While
  68. pos!
    1. String.Slice.pos!
  69. pos!
    1. String.pos!
  70. pos
    1. ByteArray.Iterator.pos
  71. pos
    1. IO.FS.Stream.Buffer.pos (structure field)
  72. pos
    1. String.Iterator.pos
  73. pos
    1. String.Slice.pos
  74. pos
    1. String.pos
  75. pos?
    1. String.Slice.pos?
  76. pos?
    1. String.pos?
  77. pos­Of
    1. String.pos­Of
  78. pos­Of
    1. Substring.pos­Of
  79. positions
    1. String.Slice.positions
  80. pow
    1. Float.pow
  81. pow
    1. Float32.pow
  82. pow
    1. HomogeneousPow.pow (class method)
  83. pow
    1. Int.pow
  84. pow
    1. Nat.pow
  85. pow
    1. NatPow.pow (class method)
  86. pow
    1. Pow.pow (class method)
  87. pow_succ
    1. Lean.Grind.Semiring.mul_zero (class method)
  88. pow_zero
    1. Lean.Grind.Semiring.zero_mul (class method)
  89. pp
    1. eval.pp
  90. pp.deep­Terms
  91. pp.deepTerms.threshold
  92. pp.field­Notation
  93. pp.match
  94. pp.max­Steps
  95. pp.mvars
  96. pp.proofs
  97. pp.proofs.threshold
  98. precompile­Modules
    1. [anonymous] (structure field)
  99. pred
    1. Fin.pred
  100. pred
    1. Nat.pred
  101. predicative
  102. prefix­Join
    1. Std.Format.prefix­Join
  103. pretty
    1. Std.Format.pretty
  104. pretty­M
    1. Std.Format.pretty­M
  105. prev!
    1. String.Slice.Pos.prev!
  106. prev!
    1. String.ValidPos.prev!
  107. prev
    1. ByteArray.Iterator.prev
  108. prev
    1. String.Iterator.prev
  109. prev
    1. String.Pos.Raw.prev
  110. prev
    1. String.Slice.Pos.prev
  111. prev
    1. String.ValidPos.prev
  112. prev
    1. Substring.prev
  113. prev?
    1. String.Slice.Pos.prev?
  114. prev?
    1. String.ValidPos.prev?
  115. prevn
    1. ByteArray.Iterator.prevn
  116. prevn
    1. String.Iterator.prevn
  117. prevn
    1. String.Slice.Pos.prevn
  118. prevn
    1. Substring.prevn
  119. print
    1. IO.print
  120. println
    1. IO.println
  121. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
  122. proj
    1. Lean.Meta.Simp.Config.proj (structure field)
  123. proof state
  124. proofs
    1. pp.proofs
  125. property
    1. Subtype.property (structure field)
  126. propext
  127. proposition
  128. proposition
    1. decidable
  129. ptr­Addr­Unsafe
  130. ptr­Eq
  131. ptr­Eq
    1. ST.Ref.ptr­Eq
  132. ptr­Eq­List
  133. pure
    1. EStateM.pure
  134. pure
    1. Except.pure
  135. pure
    1. ExceptT.pure
  136. pure
    1. OptionT.pure
  137. pure
    1. Pure.pure (class method)
  138. pure
    1. ReaderT.pure
  139. pure
    1. StateT.pure
  140. pure
    1. Task.pure
  141. pure
    1. Thunk.pure
  142. pure_bind
    1. [anonymous] (class method)
  143. pure_seq
    1. [anonymous] (class method)
  144. push
    1. Array.push
  145. push
    1. ByteArray.push
  146. push
    1. String.push
  147. push­Newline
    1. Std.Format.Monad­PrettyFormat.push­Newline (class method)
  148. push­Output
    1. Std.Format.Monad­PrettyFormat.push­Output (class method)
  149. push_cast
  150. pushn
    1. String.pushn
  151. put­Str
    1. IO.FS.Handle.put­Str
  152. put­Str
    1. IO.FS.Stream.put­Str (structure field)
  153. put­Str­Ln
    1. IO.FS.Handle.put­Str­Ln
  154. 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. Reader­M
  11. Reader­T
  12. ReaderT.adapt
  13. ReaderT.bind
  14. ReaderT.failure
  15. ReaderT.or­Else
  16. ReaderT.pure
  17. ReaderT.read
  18. ReaderT.run
  19. Ref
    1. IO.Ref
  20. Ref
    1. ST.Ref
  21. Refl­BEq
  22. ReflBEq.mk
    1. Instance constructor of Refl­BEq
  23. Repr
  24. Repr.add­App­Paren
  25. Repr.mk
    1. Instance constructor of Repr
  26. Repr­Atom
  27. ReprAtom.mk
    1. Instance constructor of Repr­Atom
  28. Result
    1. EStateM.Result
  29. Right­Inverse
    1. Function.Right­Inverse
  30. Ring
    1. Lean.Grind.Ring
  31. r
    1. Setoid.r (class method)
  32. rand
    1. IO.rand
  33. rand­Bool
  34. rand­Nat
  35. range'
    1. Array.range'
  36. range'
    1. List.range'
  37. range'TR
    1. List.range'TR
  38. range
    1. Array.range
  39. range
    1. List.range
  40. range
    1. RandomGen.range (class method)
  41. raw
    1. Lean.TSyntax.raw (structure field)
  42. raw­End­Pos
    1. String.Slice.raw­End­Pos
  43. rcases
  44. read
    1. IO.AccessRight.read (structure field)
  45. read
    1. IO.FS.Handle.read
  46. read
    1. IO.FS.Stream.read (structure field)
  47. read
    1. MonadReader.read (class method)
  48. read
    1. Monad­ReaderOf.read (class method)
  49. read
    1. ReaderT.read
  50. read­Bin­File
    1. IO.FS.read­Bin­File
  51. read­Bin­To­End
    1. IO.FS.Handle.read­Bin­To­End
  52. read­Bin­To­End­Into
    1. IO.FS.Handle.read­Bin­To­End­Into
  53. read­Dir
    1. System.FilePath.read­Dir
  54. read­File
    1. IO.FS.read­File
  55. read­The
  56. read­To­End
    1. IO.FS.Handle.read­To­End
  57. real­Path
    1. IO.FS.real­Path
  58. rec
    1. Quot.rec
  59. rec
    1. Quotient.rec
  60. rec­Aux
    1. Nat.rec­Aux
  61. rec­On
    1. Quot.rec­On
  62. rec­On
    1. Quotient.rec­On
  63. rec­On­Subsingleton
    1. Quot.rec­On­Subsingleton
  64. rec­On­Subsingleton
    1. Quotient.rec­On­Subsingleton
  65. rec­On­Subsingleton₂
    1. Quotient.rec­On­Subsingleton₂
  66. recursor
  67. recv
    1. Std.Channel.recv
  68. reduce
  69. reduction
    1. ι (iota)
  70. refine
  71. refine'
  72. refl
    1. Equivalence.refl (structure field)
  73. refl
    1. Setoid.refl
  74. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  75. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  76. rel
    1. Lean.Order.PartialOrder.rel (class method)
  77. rel
    1. Well­FoundedRelation.rel (class method)
  78. rel_antisymm
    1. Lean.Order.PartialOrder.rel_antisymm (class method)
  79. rel_refl
    1. Lean.Order.PartialOrder.rel_refl (class method)
  80. rel_trans
    1. Lean.Order.PartialOrder.rel_trans (class method)
  81. relaxed­Auto­Implicit
  82. remaining­Bytes
    1. ByteArray.Iterator.remaining­Bytes
  83. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  84. remaining­To­String
    1. String.Iterator.remaining­To­String
  85. remove­All
    1. List.remove­All
  86. remove­Dir
    1. IO.FS.remove­Dir
  87. remove­Dir­All
    1. IO.FS.remove­Dir­All
  88. remove­File
    1. IO.FS.remove­File
  89. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  90. rename
  91. rename
    1. IO.FS.rename
  92. rename_i
  93. repair
    1. Substring.repair
  94. repeat (0) (1)
  95. repeat'
  96. repeat
    1. Nat.repeat
  97. repeat1'
  98. repeat­TR
    1. Nat.repeat­TR
  99. replace
  100. replace
    1. Array.replace
  101. replace
    1. List.replace
  102. replace
    1. String.replace
  103. replace­End
    1. String.Slice.replace­End
  104. replace­End
    1. String.replace­End
  105. replace­Start
    1. String.Slice.replace­Start
  106. replace­Start
    1. String.replace­Start
  107. replace­Start­End!
    1. String.Slice.replace­Start­End!
  108. replace­Start­End
    1. String.Slice.replace­Start­End
  109. replace­TR
    1. List.replace­TR
  110. replicate
    1. Array.replicate
  111. replicate
    1. BitVec.replicate
  112. replicate
    1. List.replicate
  113. replicate­TR
    1. List.replicate­TR
  114. repr
  115. repr
    1. Int.repr
  116. repr
    1. Nat.repr
  117. repr
    1. Option.repr
  118. repr
    1. USize.repr
  119. repr
    1. eval.derive.repr
  120. repr­Arg
  121. repr­Prec
    1. Repr.repr­Prec (class method)
  122. repr­Str
  123. resolve
    1. IO.Promise.resolve
  124. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  125. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  126. restore
    1. EStateM.Backtrackable.restore (class method)
  127. restore­M
    1. MonadControl.restore­M (class method)
  128. restore­M
    1. Monad­ControlT.restore­M (class method)
  129. result!
    1. IO.Promise.result!
  130. result
    1. trace.compiler.ir.result
  131. result?
    1. IO.Promise.result?
  132. result­D
    1. IO.Promise.result­D
  133. rev
    1. Fin.rev
  134. rev­Bytes
    1. String.Slice.rev­Bytes
  135. rev­Chars
    1. String.Slice.rev­Chars
  136. rev­Find
    1. String.rev­Find
  137. rev­Find?
    1. String.Slice.rev­Find?
  138. rev­Pos­Of
    1. String.rev­Pos­Of
  139. rev­Positions
    1. String.Slice.rev­Positions
  140. rev­Split
    1. String.Slice.rev­Split
  141. reverse
    1. Array.reverse
  142. reverse
    1. BitVec.reverse
  143. reverse
    1. List.reverse
  144. reverse­Induction
    1. Fin.reverse­Induction
  145. revert
  146. rewind
    1. IO.FS.Handle.rewind
  147. rewrite (0) (1)
  148. rewrite
    1. trace.Meta.Tactic.simp.rewrite
  149. rfl (0) (1) (2)
  150. rfl'
  151. rfl
    1. HEq.rfl
  152. rfl
    1. ReflBEq.rfl (class method)
  153. rhs
  154. right (0) (1)
  155. right
    1. And.right (structure field)
  156. right_distrib
    1. Lean.Grind.Semiring.one_mul (class method)
  157. rightpad
    1. Array.rightpad
  158. rightpad
    1. List.rightpad
  159. rintro
  160. root
    1. IO.FS.DirEntry.root (structure field)
  161. root
    1. [anonymous] (structure field)
  162. roots
    1. [anonymous] (structure field)
  163. rotate­Left
    1. BitVec.rotate­Left
  164. rotate­Left
    1. List.rotate­Left
  165. rotate­Right
    1. BitVec.rotate­Right
  166. rotate­Right
    1. List.rotate­Right
  167. rotate_left
  168. rotate_right
  169. round
    1. Float.round
  170. round
    1. Float32.round
  171. run (Elan command)
  172. run'
    1. EStateM.run'
  173. run'
    1. State­CpsT.run'
  174. run'
    1. State­RefT'.run'
  175. run'
    1. StateT.run'
  176. run
    1. EStateM.run
  177. run
    1. Except­CpsT.run
  178. run
    1. ExceptT.run
  179. run
    1. IO.Process.run
  180. run
    1. Id.run
  181. run
    1. OptionT.run
  182. run
    1. ReaderT.run
  183. run
    1. State­CpsT.run
  184. run
    1. State­RefT'.run
  185. run
    1. StateT.run
  186. run­Catch
    1. Except­CpsT.run­Catch
  187. run­EST
  188. run­K
    1. Except­CpsT.run­K
  189. run­K
    1. State­CpsT.run­K
  190. run­ST
  191. run_tac
  192. rw (0) (1)
  193. rw?
  194. rw_mod_cast
  195. rwa

S

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