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
    1. Std.Do.PredTrans.apply (structure field)
  270. apply?
  271. apply_assumption
  272. apply_ext_theorem
  273. apply_mod_cast
  274. apply_rfl
  275. apply_rules
  276. arg [@]i
  277. args
  278. args
    1. [anonymous] (structure field)
  279. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  280. array
    1. ByteArray.Iterator.array (structure field)
  281. array
    1. Subarray.array
  282. as­String
    1. List.as­String
  283. as­Task
    1. BaseIO.as­Task
  284. as­Task
    1. EIO.as­Task
  285. as­Task
    1. IO.as­Task
  286. as_aux_lemma
  287. asin
    1. Float.asin
  288. asin
    1. Float32.asin
  289. asinh
    1. Float.asinh
  290. asinh
    1. Float32.asinh
  291. assumption
  292. assumption
    1. inaccessible
  293. assumption_mod_cast
  294. at­End
    1. ByteArray.Iterator.at­End
  295. at­End
    1. String.Iterator.at­End
  296. at­End
    1. String.Pos.Raw.at­End
  297. at­End
    1. Substring.at­End
  298. at­Idx!
    1. Std.TreeSet.at­Idx!
  299. at­Idx
    1. Std.TreeSet.at­Idx
  300. at­Idx?
    1. Std.TreeSet.at­Idx?
  301. at­Idx­D
    1. Std.TreeSet.at­Idx­D
  302. atan
    1. Float.atan
  303. atan
    1. Float32.atan
  304. atan2
    1. Float.atan2
  305. atan2
    1. Float32.atan2
  306. atanh
    1. Float.atanh
  307. atanh
    1. Float32.atanh
  308. atomically
    1. Std.Mutex.atomically
  309. atomically­Once
    1. Std.Mutex.atomically­Once
  310. attach
    1. Array.attach
  311. attach
    1. List.attach
  312. attach
    1. Option.attach
  313. attach­With
    1. Array.attach­With
  314. attach­With
    1. List.attach­With
  315. attach­With
    1. Option.attach­With
  316. auto­Implicit
  317. auto­Lift
  318. auto­Param
  319. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  320. auto­Unfold
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
  321. 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. conjunctive
    1. Std.Do.PredTrans.conjunctive (structure field)
  159. cons
    1. BitVec.cons
  160. const
    1. Function.const
  161. constructor (0) (1)
  162. contains
    1. Array.contains
  163. contains
    1. ByteSlice.contains
  164. contains
    1. List.contains
  165. contains
    1. Std.DHashMap.contains
  166. contains
    1. Std.DTreeMap.contains
  167. contains
    1. Std.Ext­DHashMap.contains
  168. contains
    1. Std.Ext­HashMap.contains
  169. contains
    1. Std.Ext­HashSet.contains
  170. contains
    1. Std.HashMap.contains
  171. contains
    1. Std.HashSet.contains
  172. contains
    1. Std.TreeMap.contains
  173. contains
    1. Std.TreeSet.contains
  174. contains
    1. String.Slice.contains
  175. contains
    1. String.contains
  176. contains
    1. Substring.contains
  177. contains­Then­Insert
    1. Std.DHashMap.contains­Then­Insert
  178. contains­Then­Insert
    1. Std.DTreeMap.contains­Then­Insert
  179. contains­Then­Insert
    1. Std.Ext­DHashMap.contains­Then­Insert
  180. contains­Then­Insert
    1. Std.Ext­HashMap.contains­Then­Insert
  181. contains­Then­Insert
    1. Std.Ext­HashSet.contains­Then­Insert
  182. contains­Then­Insert
    1. Std.HashMap.contains­Then­Insert
  183. contains­Then­Insert
    1. Std.HashSet.contains­Then­Insert
  184. contains­Then­Insert
    1. Std.TreeMap.contains­Then­Insert
  185. contains­Then­Insert
    1. Std.TreeSet.contains­Then­Insert
  186. contains­Then­Insert­If­New
    1. Std.DHashMap.contains­Then­Insert­If­New
  187. contains­Then­Insert­If­New
    1. Std.DTreeMap.contains­Then­Insert­If­New
  188. contains­Then­Insert­If­New
    1. Std.Ext­DHashMap.contains­Then­Insert­If­New
  189. contains­Then­Insert­If­New
    1. Std.Ext­HashMap.contains­Then­Insert­If­New
  190. contains­Then­Insert­If­New
    1. Std.HashMap.contains­Then­Insert­If­New
  191. contains­Then­Insert­If­New
    1. Std.TreeMap.contains­Then­Insert­If­New
  192. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  193. contradiction
  194. control
  195. control­At
  196. conv
  197. conv => ...
  198. conv' (0) (1)
  199. copy
    1. String.Slice.copy
  200. copy­Slice
    1. ByteArray.copy­Slice
  201. cos
    1. Float.cos
  202. cos
    1. Float32.cos
  203. cosh
    1. Float.cosh
  204. cosh
    1. Float32.cosh
  205. count
    1. Array.count
  206. count
    1. List.count
  207. count­P
    1. Array.count­P
  208. count­P
    1. List.count­P
  209. create­Dir
    1. IO.FS.create­Dir
  210. create­Dir­All
    1. IO.FS.create­Dir­All
  211. create­Temp­Dir
    1. IO.FS.create­Temp­Dir
  212. create­Temp­File
    1. IO.FS.create­Temp­File
  213. crlf­To­Lf
    1. String.crlf­To­Lf
  214. csup
    1. [anonymous] (class method)
  215. csup_spec
    1. [anonymous] (class method)
  216. cumulativity
  217. curr'
    1. ByteArray.Iterator.curr'
  218. curr'
    1. String.Iterator.curr'
  219. curr
    1. ByteArray.Iterator.curr
  220. curr
    1. String.Iterator.curr
  221. curr­Column
    1. Std.Format.Monad­PrettyFormat.curr­Column (class method)
  222. current­Dir
    1. IO.current­Dir
  223. curry
    1. Function.curry
  224. custom­Eliminators
    1. tactic.custom­Eliminators
  225. cwd
    1. [anonymous] (structure field)

D

  1. DHash­Map
    1. Std.DHash­Map
  2. DTree­Map
    1. Std.DTree­Map
  3. Decidable
  4. Decidable.by­Cases
  5. Decidable.decide
  6. Decidable.is­False
    1. Constructor of Decidable
  7. Decidable.is­True
    1. Constructor of Decidable
  8. Decidable­Eq
  9. Decidable­LE
  10. Decidable­LT
  11. Decidable­Pred
  12. Decidable­Rel
  13. Dir­Entry
    1. IO.FS.Dir­Entry
  14. Div
  15. Div.mk
    1. Instance constructor of Div
  16. Dvd
  17. Dvd.mk
    1. Instance constructor of Dvd
  18. data
    1. ByteArray.data (structure field)
  19. data
    1. IO.FS.Stream.Buffer.data (structure field)
  20. 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. entails
    1. Std.Do.SPred.entails
  131. enter
  132. entry­At­Idx!
    1. Std.TreeMap.entry­At­Idx!
  133. entry­At­Idx
    1. Std.TreeMap.entry­At­Idx
  134. entry­At­Idx?
    1. Std.TreeMap.entry­At­Idx?
  135. entry­At­Idx­D
    1. Std.TreeMap.entry­At­Idx­D
  136. env (Lake command)
  137. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  138. environment variables
  139. eprint
    1. IO.eprint
  140. eprintln
    1. IO.eprintln
  141. eq­Ignore­Ascii­Case
    1. String.Slice.eq­Ignore­Ascii­Case
  142. eq­Rec_heq
  143. eq_of_beq
    1. [anonymous] (class method)
  144. eq_of_heq
  145. eq_refl
  146. erase
    1. Array.erase
  147. erase
    1. List.erase
  148. erase
    1. Std.DHashMap.erase
  149. erase
    1. Std.DTreeMap.erase
  150. erase
    1. Std.Ext­DHashMap.erase
  151. erase
    1. Std.Ext­HashMap.erase
  152. erase
    1. Std.Ext­HashSet.erase
  153. erase
    1. Std.HashMap.erase
  154. erase
    1. Std.HashSet.erase
  155. erase
    1. Std.TreeMap.erase
  156. erase
    1. Std.TreeSet.erase
  157. erase­Dups
    1. List.erase­Dups
  158. erase­Idx!
    1. Array.erase­Idx!
  159. erase­Idx
    1. Array.erase­Idx
  160. erase­Idx
    1. List.erase­Idx
  161. erase­Idx­If­In­Bounds
    1. Array.erase­Idx­If­In­Bounds
  162. erase­Idx­TR
    1. List.erase­Idx­TR
  163. erase­Many
    1. Std.TreeMap.erase­Many
  164. erase­Many
    1. Std.TreeSet.erase­Many
  165. erase­P
    1. Array.erase­P
  166. erase­P
    1. List.erase­P
  167. erase­PTR
    1. List.erase­PTR
  168. erase­Reps
    1. Array.erase­Reps
  169. erase­Reps
    1. List.erase­Reps
  170. erase­TR
    1. List.erase­TR
  171. erw (0) (1)
  172. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
  173. eta
    1. Lean.Meta.Simp.Config.eta (structure field)
  174. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
  175. eta­Struct
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  176. eval.derive.repr
  177. eval.pp
  178. eval.type
  179. exact
  180. exact
    1. Quotient.exact
  181. exact?
  182. exact_mod_cast
  183. exe (Lake command)
  184. exe­Extension
    1. System.FilePath.exe­Extension
  185. exe­Name
    1. [anonymous] (structure field)
  186. execution
    1. IO.AccessRight.execution (structure field)
  187. exfalso
  188. exists
  189. exit
    1. IO.Process.exit
  190. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  191. exp
    1. Float.exp
  192. exp
    1. Float32.exp
  193. exp2
    1. Float.exp2
  194. exp2
    1. Float32.exp2
  195. expand­Macro?
    1. Lean.Macro.expand­Macro?
  196. expose_names
  197. ext (0) (1)
  198. ext1
  199. ext­Separator
    1. System.FilePath.ext­Separator
  200. extension
    1. System.FilePath.extension
  201. extensionality
    1. of propositions
  202. extra­Dep­Targets
    1. [anonymous] (structure field) (0) (1)
  203. extract
    1. Array.extract
  204. extract
    1. ByteArray.extract
  205. extract
    1. List.extract
  206. extract
    1. String.Iterator.extract
  207. extract
    1. String.Pos.Raw.extract
  208. extract
    1. String.ValidPos.extract
  209. extract
    1. Substring.extract
  210. extract­Lsb'
    1. BitVec.extract­Lsb'
  211. 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. Pred­Trans
    1. Std.Do.Pred­Trans
  24. Preresolved
    1. Lean.Syntax.Preresolved
  25. Prio
    1. Lean.Syntax.Prio
  26. Priority
    1. Task.Priority
  27. Prod
  28. Prod.all­I
  29. Prod.any­I
  30. Prod.fold­I
  31. Prod.lex­Lt
  32. Prod.map
  33. Prod.mk
    1. Constructor of Prod
  34. Prod.swap
  35. Promise
    1. IO.Promise
  36. Prop
  37. Pure
  38. Pure.mk
    1. Instance constructor of Pure
  39. pack (Lake command)
  40. parameter
    1. of inductive type
  41. paren
    1. Std.Format.paren
  42. parent
    1. System.FilePath.parent
  43. parser
  44. partition
    1. Array.partition
  45. partition
    1. List.partition
  46. partition
    1. Std.DHashMap.partition
  47. partition
    1. Std.DTreeMap.partition
  48. partition
    1. Std.HashMap.partition
  49. partition
    1. Std.HashSet.partition
  50. partition
    1. Std.TreeMap.partition
  51. partition
    1. Std.TreeSet.partition
  52. partition­M
    1. List.partition­M
  53. partition­Map
    1. List.partition­Map
  54. path
    1. IO.FS.DirEntry.path
  55. path­Exists
    1. System.FilePath.path­Exists
  56. path­Separator
    1. System.FilePath.path­Separator
  57. path­Separators
    1. System.FilePath.path­Separators
  58. pattern
  59. pbind
    1. Option.pbind
  60. pelim
    1. Option.pelim
  61. placeholder term
  62. pmap
    1. Array.pmap
  63. pmap
    1. List.pmap
  64. pmap
    1. Option.pmap
  65. polymorphism
    1. universe
  66. pop
    1. Array.pop
  67. pop­Front
    1. Subarray.pop­Front
  68. pop­While
    1. Array.pop­While
  69. pos!
    1. String.Slice.pos!
  70. pos!
    1. String.pos!
  71. pos
    1. ByteArray.Iterator.pos
  72. pos
    1. IO.FS.Stream.Buffer.pos (structure field)
  73. pos
    1. String.Iterator.pos
  74. pos
    1. String.Slice.pos
  75. pos
    1. String.pos
  76. pos?
    1. String.Slice.pos?
  77. pos?
    1. String.pos?
  78. pos­Of
    1. String.pos­Of
  79. pos­Of
    1. Substring.pos­Of
  80. positions
    1. String.Slice.positions
  81. pow
    1. Float.pow
  82. pow
    1. Float32.pow
  83. pow
    1. HomogeneousPow.pow (class method)
  84. pow
    1. Int.pow
  85. pow
    1. Nat.pow
  86. pow
    1. NatPow.pow (class method)
  87. pow
    1. Pow.pow (class method)
  88. pow_succ
    1. Lean.Grind.Semiring.mul_zero (class method)
  89. pow_zero
    1. Lean.Grind.Semiring.zero_mul (class method)
  90. pp
    1. eval.pp
  91. pp.deep­Terms
  92. pp.deepTerms.threshold
  93. pp.field­Notation
  94. pp.match
  95. pp.max­Steps
  96. pp.mvars
  97. pp.proofs
  98. pp.proofs.threshold
  99. precompile­Modules
    1. [anonymous] (structure field)
  100. pred
    1. Fin.pred
  101. pred
    1. Nat.pred
  102. predicative
  103. prefix­Join
    1. Std.Format.prefix­Join
  104. pretty
    1. Std.Format.pretty
  105. pretty­M
    1. Std.Format.pretty­M
  106. prev!
    1. String.Slice.Pos.prev!
  107. prev!
    1. String.ValidPos.prev!
  108. prev
    1. ByteArray.Iterator.prev
  109. prev
    1. String.Iterator.prev
  110. prev
    1. String.Pos.Raw.prev
  111. prev
    1. String.Slice.Pos.prev
  112. prev
    1. String.ValidPos.prev
  113. prev
    1. Substring.prev
  114. prev?
    1. String.Slice.Pos.prev?
  115. prev?
    1. String.ValidPos.prev?
  116. prevn
    1. ByteArray.Iterator.prevn
  117. prevn
    1. String.Iterator.prevn
  118. prevn
    1. String.Slice.Pos.prevn
  119. prevn
    1. Substring.prevn
  120. print
    1. IO.print
  121. println
    1. IO.println
  122. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
  123. proj
    1. Lean.Meta.Simp.Config.proj (structure field)
  124. proof state
  125. proofs
    1. pp.proofs
  126. property
    1. Subtype.property (structure field)
  127. propext
  128. proposition
  129. proposition
    1. decidable
  130. ptr­Addr­Unsafe
  131. ptr­Eq
  132. ptr­Eq
    1. ST.Ref.ptr­Eq
  133. ptr­Eq­List
  134. pure
    1. EStateM.pure
  135. pure
    1. Except.pure
  136. pure
    1. ExceptT.pure
  137. pure
    1. OptionT.pure
  138. pure
    1. Pure.pure (class method)
  139. pure
    1. ReaderT.pure
  140. pure
    1. StateT.pure
  141. pure
    1. Task.pure
  142. pure
    1. Thunk.pure
  143. pure_bind
    1. [anonymous] (class method)
  144. pure_seq
    1. [anonymous] (class method)
  145. push
    1. Array.push
  146. push
    1. ByteArray.push
  147. push
    1. String.push
  148. push­Newline
    1. Std.Format.Monad­PrettyFormat.push­Newline (class method)
  149. push­Output
    1. Std.Format.Monad­PrettyFormat.push­Output (class method)
  150. push_cast
  151. pushn
    1. String.pushn
  152. put­Str
    1. IO.FS.Handle.put­Str
  153. put­Str
    1. IO.FS.Stream.put­Str (structure field)
  154. put­Str­Ln
    1. IO.FS.Handle.put­Str­Ln
  155. put­Str­Ln
    1. IO.FS.Stream.put­Str­Ln

Q

  1. Quot
  2. Quot.hrec­On
  3. Quot.ind
  4. Quot.lift
  5. Quot.lift­On
  6. Quot.mk
  7. Quot.rec
  8. Quot.rec­On
  9. Quot.rec­On­Subsingleton
  10. Quot.sound
  11. Quotient
  12. Quotient.exact
  13. Quotient.hrec­On
  14. Quotient.ind
  15. Quotient.lift
  16. Quotient.lift­On
  17. Quotient.lift­On₂
  18. Quotient.lift₂
  19. Quotient.mk
  20. Quotient.mk'
  21. Quotient.rec
  22. Quotient.rec­On
  23. Quotient.rec­On­Subsingleton
  24. Quotient.rec­On­Subsingleton₂
  25. Quotient.sound
  26. qsort
    1. Array.qsort
  27. qsort­Ord
    1. Array.qsort­Ord
  28. quantification
    1. impredicative
  29. quantification
    1. predicative
  30. query (Lake command)
  31. quote
    1. Char.quote
  32. quote
    1. String.quote

R

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

U

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

V

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

W

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

X

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

Z

  1. Zero
  2. Zero.mk
    1. Instance constructor of Zero
  3. zero
    1. BitVec.zero
  4. zero
    1. Zero.zero (class method)
  5. zero­Extend
    1. BitVec.zero­Extend
  6. zero_lt_one
    1. [anonymous] (class method)
  7. zero_mul
    1. Lean.Grind.Semiring.left_distrib (class method)
  8. zero_ne_one
    1. [anonymous] (class method)
  9. zero_nsmul
    1. [anonymous] (class method)
  10. zero_zsmul
    1. [anonymous] (class method)
  11. zeta
  12. zeta
    1. Lean.Meta.DSimp.Config.zeta (structure field)
  13. zeta
    1. Lean.Meta.Simp.Config.zeta (structure field)
  14. zeta­Delta
    1. Lean.Meta.DSimp.Config.zeta­Delta (structure field)
  15. zeta­Delta
    1. Lean.Meta.Simp.Config.zeta­Delta (structure field)
  16. zeta­Have
    1. Lean.Meta.DSimp.Config.zeta­Have (structure field)
  17. zeta­Have
    1. Lean.Meta.Simp.Config.zeta­Have (structure field)
  18. zeta­Unused
    1. Lean.Meta.DSimp.Config.zeta­Unused (structure field)
  19. zeta­Unused
    1. Lean.Meta.Simp.Config.zeta­Unused (structure field)
  20. zip
    1. Array.zip
  21. zip
    1. List.zip
  22. zip­Idx
    1. Array.zip­Idx
  23. zip­Idx
    1. List.zip­Idx
  24. zip­Idx­TR
    1. List.zip­Idx­TR
  25. zip­With
    1. Array.zip­With
  26. zip­With
    1. List.zip­With
  27. zip­With­All
    1. Array.zip­With­All
  28. zip­With­All
    1. List.zip­With­All
  29. zip­With­TR
    1. List.zip­With­TR
  30. zpow
    1. [anonymous] (class method)
  31. zpow_neg
    1. [anonymous] (class method)
  32. zpow_succ
    1. [anonymous] (class method)
  33. zpow_zero
    1. [anonymous] (class method)
  34. zsmul
    1. [anonymous] (class method) (0) (1)
  35. zsmul_nat­Cast_eq_nsmul
    1. [anonymous] (class method) (0) (1)