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­Unsafe­Reducibility
  228. alter
    1. Std.DHashMap.alter
  229. alter
    1. Std.DTreeMap.alter
  230. alter
    1. Std.Ext­DHashMap.alter
  231. alter
    1. Std.Ext­HashMap.alter
  232. alter
    1. Std.HashMap.alter
  233. alter
    1. Std.TreeMap.alter
  234. and
    1. AndOp.and (class method)
  235. and
    1. BitVec.and
  236. and
    1. Bool.and
  237. and
    1. List.and
  238. and­M
  239. and_intros
  240. any
    1. Array.any
  241. any
    1. List.any
  242. any
    1. Nat.any
  243. any
    1. Option.any
  244. any
    1. Std.HashSet.any
  245. any
    1. Std.TreeMap.any
  246. any
    1. Std.TreeSet.any
  247. any
    1. String.any
  248. any
    1. Subarray.any
  249. any
    1. Substring.any
  250. any­I
    1. Prod.any­I
  251. any­M
    1. Array.any­M
  252. any­M
    1. List.any­M
  253. any­M
    1. Nat.any­M
  254. any­M
    1. Subarray.any­M
  255. any­TR
    1. Nat.any­TR
  256. any_goals (0) (1)
  257. app­Dir
    1. IO.app­Dir
  258. app­Path
    1. IO.app­Path
  259. append
    1. Append.append (class method)
  260. append
    1. Array.append
  261. append
    1. BitVec.append
  262. append
    1. ByteArray.append
  263. append
    1. List.append
  264. append
    1. String.append
  265. append­List
    1. Array.append­List
  266. append­TR
    1. List.append­TR
  267. apply (0) (1)
  268. apply?
  269. apply_assumption
  270. apply_ext_theorem
  271. apply_mod_cast
  272. apply_rfl
  273. apply_rules
  274. arg [@]i
  275. args
  276. args
    1. [anonymous] (structure field)
  277. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  278. array
    1. ByteArray.Iterator.array (structure field)
  279. as­String
    1. List.as­String
  280. as­Task
    1. BaseIO.as­Task
  281. as­Task
    1. EIO.as­Task
  282. as­Task
    1. IO.as­Task
  283. as_aux_lemma
  284. asin
    1. Float.asin
  285. asin
    1. Float32.asin
  286. asinh
    1. Float.asinh
  287. asinh
    1. Float32.asinh
  288. assumption
  289. assumption
    1. inaccessible
  290. assumption_mod_cast
  291. at­End
    1. ByteArray.Iterator.at­End
  292. at­End
    1. String.Iterator.at­End
  293. at­End
    1. String.at­End
  294. at­End
    1. Substring.at­End
  295. at­Idx!
    1. Std.TreeSet.at­Idx!
  296. at­Idx
    1. Std.TreeSet.at­Idx
  297. at­Idx?
    1. Std.TreeSet.at­Idx?
  298. at­Idx­D
    1. Std.TreeSet.at­Idx­D
  299. atan
    1. Float.atan
  300. atan
    1. Float32.atan
  301. atan2
    1. Float.atan2
  302. atan2
    1. Float32.atan2
  303. atanh
    1. Float.atanh
  304. atanh
    1. Float32.atanh
  305. atomically
    1. Std.Mutex.atomically
  306. atomically­Once
    1. Std.Mutex.atomically­Once
  307. attach
    1. Array.attach
  308. attach
    1. List.attach
  309. attach
    1. Option.attach
  310. attach­With
    1. Array.attach­With
  311. attach­With
    1. List.attach­With
  312. attach­With
    1. Option.attach­With
  313. auto­Implicit
  314. auto­Lift
  315. auto­Param
  316. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  317. auto­Unfold
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
  318. 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­Idx
    1. String.Pos.Raw.byte­Idx (structure field)
  255. byte­Size
    1. IO.FS.Metadata.byte­Size (structure field)
  256. bytes
    1. String.Slice.bytes
  257. bytes
    1. String.bytes (structure field)

C

  1. CC (environment variable)
  2. CCPO
    1. Lean.Order.CCPO
  3. Channel
    1. Std.Channel
  4. Char
  5. Char.is­Alpha
  6. Char.is­Alphanum
  7. Char.is­Digit
  8. Char.is­Lower
  9. Char.is­Upper
  10. Char.is­Valid­Char­Nat
  11. Char.is­Whitespace
  12. Char.le
  13. Char.lt
  14. Char.mk
    1. Constructor of Char
  15. Char.of­Nat
  16. Char.of­UInt8
  17. Char.quote
  18. Char.to­Lower
  19. Char.to­Nat
  20. Char.to­String
  21. Char.to­UInt8
  22. Char.to­Upper
  23. Char.utf16Size
  24. Char.utf8Size
  25. Char­Lit
    1. Lean.Syntax.Char­Lit
  26. Child
    1. IO.Process.Child
  27. Closeable­Channel
    1. Std.Closeable­Channel
  28. Coe
  29. Coe.mk
    1. Instance constructor of Coe
  30. Coe­Dep
  31. CoeDep.mk
    1. Instance constructor of Coe­Dep
  32. Coe­Fun
  33. CoeFun.mk
    1. Instance constructor of Coe­Fun
  34. Coe­HTC
  35. CoeHTC.mk
    1. Instance constructor of Coe­HTC
  36. Coe­HTCT
  37. CoeHTCT.mk
    1. Instance constructor of Coe­HTCT
  38. Coe­Head
  39. CoeHead.mk
    1. Instance constructor of Coe­Head
  40. Coe­OTC
  41. CoeOTC.mk
    1. Instance constructor of Coe­OTC
  42. Coe­Out
  43. CoeOut.mk
    1. Instance constructor of Coe­Out
  44. Coe­Sort
  45. CoeSort.mk
    1. Instance constructor of Coe­Sort
  46. Coe­T
  47. CoeT.mk
    1. Instance constructor of Coe­T
  48. Coe­TC
  49. CoeTC.mk
    1. Instance constructor of Coe­TC
  50. Coe­Tail
  51. CoeTail.mk
    1. Instance constructor of Coe­Tail
  52. Comm­Ring
    1. Lean.Grind.Comm­Ring
  53. Comm­Semiring
    1. Lean.Grind.Comm­Semiring
  54. Command
    1. Lean.Syntax.Command
  55. Condvar
    1. Std.Condvar
  56. Config
    1. Lean.Meta.DSimp.Config
  57. Config
    1. Lean.Meta.Rewrite.Config
  58. Config
    1. Lean.Meta.Simp.Config
  59. cache get (Lake command)
  60. cache put (Lake command)
  61. calc
  62. call-by-need
  63. cancel
    1. IO.cancel
  64. canon­Instances
    1. backward.synthInstance.canon­Instances
  65. capitalize
    1. String.capitalize
  66. carry
    1. BitVec.carry
  67. case
  68. case ... => ...
  69. case'
  70. case' ... => ...
  71. case­Strong­Rec­On
    1. Nat.case­Strong­Rec­On
  72. cases
  73. cases
    1. Fin.cases
  74. cases­Aux­On
    1. Nat.cases­Aux­On
  75. cast
  76. cast
    1. BitVec.cast
  77. cast
    1. Fin.cast
  78. cast
    1. Int.cast
  79. cast
    1. Nat.cast
  80. cast
    1. String.Slice.Pos.cast
  81. cast
    1. String.ValidPos.cast
  82. cast­Add
    1. Fin.cast­Add
  83. cast­LE
    1. Fin.cast­LE
  84. cast­LT
    1. Fin.cast­LT
  85. cast­Succ
    1. Fin.cast­Succ
  86. cast_heq
  87. catch­Exceptions
    1. EIO.catch­Exceptions
  88. catch­Runtime
    1. Lean.Meta.Simp.Config.catch­Runtime (structure field)
  89. cbrt
    1. Float.cbrt
  90. cbrt
    1. Float32.cbrt
  91. ceil
    1. Float.ceil
  92. ceil
    1. Float32.ceil
  93. chain
    1. of coercions
  94. chain­Task
    1. BaseIO.chain­Task
  95. chain­Task
    1. EIO.chain­Task
  96. chain­Task
    1. IO.chain­Task
  97. change (0) (1)
  98. change ... with ...
  99. char­Lit­Kind
    1. Lean.char­Lit­Kind
  100. chars
    1. String.Slice.chars
  101. check-build (Lake command)
  102. check-lint (Lake command)
  103. check-test (Lake command)
  104. check­Canceled
    1. IO.check­Canceled
  105. choice
    1. Option.choice
  106. choice­Kind
    1. Lean.choice­Kind
  107. choose
    1. Exists.choose
  108. classical
  109. clean (Lake command)
  110. clear
  111. cmd
    1. [anonymous] (structure field)
  112. coe
    1. Coe.coe (class method)
  113. coe
    1. CoeDep.coe (class method)
  114. coe
    1. CoeFun.coe (class method)
  115. coe
    1. CoeHTC.coe (class method)
  116. coe
    1. CoeHTCT.coe (class method)
  117. coe
    1. CoeHead.coe (class method)
  118. coe
    1. CoeOTC.coe (class method)
  119. coe
    1. CoeOut.coe (class method)
  120. coe
    1. CoeSort.coe (class method)
  121. coe
    1. CoeT.coe (class method)
  122. coe
    1. CoeTC.coe (class method)
  123. coe
    1. CoeTail.coe (class method)
  124. col­Eq
  125. col­Ge
  126. col­Gt
  127. comment
    1. block
  128. comment
    1. line
  129. common­Prefix
    1. Substring.common­Prefix
  130. common­Suffix
    1. Substring.common­Suffix
  131. comp
    1. Function.comp
  132. comp_map
    1. LawfulFunctor.comp_map (class method)
  133. compare
    1. Ord.compare (class method)
  134. compare­Lex
  135. compare­Of­Less­And­BEq
  136. compare­Of­Less­And­Eq
  137. compare­On
  138. complement
    1. ISize.complement
  139. complement
    1. Int16.complement
  140. complement
    1. Int32.complement
  141. complement
    1. Int64.complement
  142. complement
    1. Int8.complement
  143. complement
    1. UInt16.complement
  144. complement
    1. UInt32.complement
  145. complement
    1. UInt64.complement
  146. complement
    1. UInt8.complement
  147. complement
    1. USize.complement
  148. completions (Elan command)
  149. components
    1. System.FilePath.components
  150. concat
    1. BitVec.concat
  151. concat
    1. List.concat
  152. cond
  153. configuration
    1. of tactics
  154. congr (0) (1) (2)
  155. congr­Arg
  156. congr­Consts
    1. Lean.Meta.Simp.Config.congr­Consts (structure field)
  157. congr­Fun
  158. cons
    1. BitVec.cons
  159. const
    1. Function.const
  160. constructor (0) (1)
  161. contains
    1. Array.contains
  162. contains
    1. ByteSlice.contains
  163. contains
    1. List.contains
  164. contains
    1. Std.DHashMap.contains
  165. contains
    1. Std.DTreeMap.contains
  166. contains
    1. Std.Ext­DHashMap.contains
  167. contains
    1. Std.Ext­HashMap.contains
  168. contains
    1. Std.Ext­HashSet.contains
  169. contains
    1. Std.HashMap.contains
  170. contains
    1. Std.HashSet.contains
  171. contains
    1. Std.TreeMap.contains
  172. contains
    1. Std.TreeSet.contains
  173. contains
    1. String.Slice.contains
  174. contains
    1. String.contains
  175. contains
    1. Substring.contains
  176. contains­Then­Insert
    1. Std.DHashMap.contains­Then­Insert
  177. contains­Then­Insert
    1. Std.DTreeMap.contains­Then­Insert
  178. contains­Then­Insert
    1. Std.Ext­DHashMap.contains­Then­Insert
  179. contains­Then­Insert
    1. Std.Ext­HashMap.contains­Then­Insert
  180. contains­Then­Insert
    1. Std.Ext­HashSet.contains­Then­Insert
  181. contains­Then­Insert
    1. Std.HashMap.contains­Then­Insert
  182. contains­Then­Insert
    1. Std.HashSet.contains­Then­Insert
  183. contains­Then­Insert
    1. Std.TreeMap.contains­Then­Insert
  184. contains­Then­Insert
    1. Std.TreeSet.contains­Then­Insert
  185. contains­Then­Insert­If­New
    1. Std.DHashMap.contains­Then­Insert­If­New
  186. contains­Then­Insert­If­New
    1. Std.DTreeMap.contains­Then­Insert­If­New
  187. contains­Then­Insert­If­New
    1. Std.Ext­DHashMap.contains­Then­Insert­If­New
  188. contains­Then­Insert­If­New
    1. Std.Ext­HashMap.contains­Then­Insert­If­New
  189. contains­Then­Insert­If­New
    1. Std.HashMap.contains­Then­Insert­If­New
  190. contains­Then­Insert­If­New
    1. Std.TreeMap.contains­Then­Insert­If­New
  191. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  192. contradiction
  193. control
  194. control­At
  195. conv
  196. conv => ...
  197. conv' (0) (1)
  198. copy
    1. String.Slice.copy
  199. copy­Slice
    1. ByteArray.copy­Slice
  200. cos
    1. Float.cos
  201. cos
    1. Float32.cos
  202. cosh
    1. Float.cosh
  203. cosh
    1. Float32.cosh
  204. count
    1. Array.count
  205. count
    1. List.count
  206. count­P
    1. Array.count­P
  207. count­P
    1. List.count­P
  208. create­Dir
    1. IO.FS.create­Dir
  209. create­Dir­All
    1. IO.FS.create­Dir­All
  210. create­Temp­Dir
    1. IO.FS.create­Temp­Dir
  211. create­Temp­File
    1. IO.FS.create­Temp­File
  212. crlf­To­Lf
    1. String.crlf­To­Lf
  213. csup
    1. [anonymous] (class method)
  214. csup_spec
    1. [anonymous] (class method)
  215. cumulativity
  216. curr'
    1. ByteArray.Iterator.curr'
  217. curr'
    1. String.Iterator.curr'
  218. curr
    1. ByteArray.Iterator.curr
  219. curr
    1. String.Iterator.curr
  220. curr­Column
    1. Std.Format.Monad­PrettyFormat.curr­Column (class method)
  221. current­Dir
    1. IO.current­Dir
  222. curry
    1. Function.curry
  223. custom­Eliminators
    1. tactic.custom­Eliminators
  224. cwd
    1. [anonymous] (structure field)

D

  1. DHash­Map
    1. Std.DHash­Map
  2. DTree­Map
    1. Std.DTree­Map
  3. Decidable
  4. Decidable.by­Cases
  5. Decidable.decide
  6. Decidable.is­False
    1. Constructor of Decidable
  7. Decidable.is­True
    1. Constructor of Decidable
  8. Decidable­Eq
  9. Decidable­LE
  10. Decidable­LT
  11. Decidable­Pred
  12. Decidable­Rel
  13. Dir­Entry
    1. IO.FS.Dir­Entry
  14. Div
  15. Div.mk
    1. Instance constructor of Div
  16. Dvd
  17. Dvd.mk
    1. Instance constructor of Dvd
  18. data
    1. ByteArray.data (structure field)
  19. data
    1. IO.FS.Stream.Buffer.data (structure field)
  20. dbg­Trace­If­Shared
  21. dbg_trace
  22. dcond
    1. Bool.dcond
  23. dec
    1. String.Pos.Raw.dec
  24. dec­Eq
    1. BitVec.dec­Eq
  25. dec­Eq
    1. Bool.dec­Eq
  26. dec­Eq
    1. ISize.dec­Eq
  27. dec­Eq
    1. Int.dec­Eq
  28. dec­Eq
    1. Int16.dec­Eq
  29. dec­Eq
    1. Int32.dec­Eq
  30. dec­Eq
    1. Int64.dec­Eq
  31. dec­Eq
    1. Int8.dec­Eq
  32. dec­Eq
    1. Nat.dec­Eq
  33. dec­Eq
    1. String.dec­Eq
  34. dec­Eq
    1. UInt16.dec­Eq
  35. dec­Eq
    1. UInt32.dec­Eq
  36. dec­Eq
    1. UInt64.dec­Eq
  37. dec­Eq
    1. UInt8.dec­Eq
  38. dec­Eq
    1. USize.dec­Eq
  39. dec­Le
    1. Float.dec­Le
  40. dec­Le
    1. Float32.dec­Le
  41. dec­Le
    1. ISize.dec­Le
  42. dec­Le
    1. Int16.dec­Le
  43. dec­Le
    1. Int32.dec­Le
  44. dec­Le
    1. Int64.dec­Le
  45. dec­Le
    1. Int8.dec­Le
  46. dec­Le
    1. Nat.dec­Le
  47. dec­Le
    1. UInt16.dec­Le
  48. dec­Le
    1. UInt32.dec­Le
  49. dec­Le
    1. UInt64.dec­Le
  50. dec­Le
    1. UInt8.dec­Le
  51. dec­Le
    1. USize.dec­Le
  52. dec­Lt
    1. Float.dec­Lt
  53. dec­Lt
    1. Float32.dec­Lt
  54. dec­Lt
    1. ISize.dec­Lt
  55. dec­Lt
    1. Int16.dec­Lt
  56. dec­Lt
    1. Int32.dec­Lt
  57. dec­Lt
    1. Int64.dec­Lt
  58. dec­Lt
    1. Int8.dec­Lt
  59. dec­Lt
    1. Nat.dec­Lt
  60. dec­Lt
    1. UInt16.dec­Lt
  61. dec­Lt
    1. UInt32.dec­Lt
  62. dec­Lt
    1. UInt64.dec­Lt
  63. dec­Lt
    1. UInt8.dec­Lt
  64. dec­Lt
    1. USize.dec­Lt
  65. decapitalize
    1. String.decapitalize
  66. decidable
  67. decidable­Eq­None
    1. Option.decidable­Eq­None
  68. decide
  69. decide
    1. Decidable.decide
  70. decide
    1. Lean.Meta.DSimp.Config.decide (structure field)
  71. decide
    1. Lean.Meta.Simp.Config.decide (structure field)
  72. decreasing_tactic
  73. decreasing_trivial
  74. decreasing_with
  75. dedicated
    1. Task.Priority.dedicated
  76. deep­Terms
    1. pp.deep­Terms
  77. def­Indent
    1. Std.Format.def­Indent
  78. def­Width
    1. Std.Format.def­Width
  79. default (Elan command)
  80. default
    1. Inhabited.default (class method)
  81. default
    1. Task.Priority.default
  82. default­Facets
    1. [anonymous] (structure field)
  83. delta (0) (1)
  84. diff
    1. guard_msgs.diff
  85. digit­Char
    1. Nat.digit­Char
  86. discard
    1. Functor.discard
  87. discharge
    1. trace.Meta.Tactic.simp.discharge
  88. div
    1. Div.div (class method)
  89. div
    1. Fin.div
  90. div
    1. Float.div
  91. div
    1. Float32.div
  92. div
    1. ISize.div
  93. div
    1. Int16.div
  94. div
    1. Int32.div
  95. div
    1. Int64.div
  96. div
    1. Int8.div
  97. div
    1. Nat.div
  98. div
    1. UInt16.div
  99. div
    1. UInt32.div
  100. div
    1. UInt64.div
  101. div
    1. UInt8.div
  102. div
    1. USize.div
  103. div2Induction
    1. Nat.div2Induction
  104. div­Rec
    1. BitVec.div­Rec
  105. div­Subtract­Shift
    1. BitVec.div­Subtract­Shift
  106. div_eq_mul_inv
    1. [anonymous] (class method)
  107. done (0) (1)
  108. down
    1. PLift.down (structure field)
  109. down
    1. ULift.down (structure field)
  110. drop
    1. Array.drop
  111. drop
    1. List.drop
  112. drop
    1. String.Slice.drop
  113. drop
    1. String.drop
  114. drop
    1. Subarray.drop
  115. drop
    1. Substring.drop
  116. drop­End
    1. String.Slice.drop­End
  117. drop­End­While
    1. String.Slice.drop­End­While
  118. drop­Last
    1. List.drop­Last
  119. drop­Last­TR
    1. List.drop­Last­TR
  120. drop­Prefix
    1. String.Slice.drop­Prefix
  121. drop­Prefix?
    1. String.Slice.Pattern.ForwardPattern.drop­Prefix? (class method)
  122. drop­Prefix?
    1. String.Slice.drop­Prefix?
  123. drop­Prefix?
    1. String.drop­Prefix?
  124. drop­Prefix?
    1. Substring.drop­Prefix?
  125. drop­Right
    1. String.drop­Right
  126. drop­Right
    1. Substring.drop­Right
  127. drop­Right­While
    1. String.drop­Right­While
  128. drop­Right­While
    1. Substring.drop­Right­While
  129. drop­Suffix
    1. String.Slice.drop­Suffix
  130. drop­Suffix?
    1. String.Slice.Pattern.BackwardPattern.drop­Suffix? (class method)
  131. drop­Suffix?
    1. String.Slice.drop­Suffix?
  132. drop­Suffix?
    1. String.drop­Suffix?
  133. drop­Suffix?
    1. Substring.drop­Suffix?
  134. drop­While
    1. List.drop­While
  135. drop­While
    1. String.Slice.drop­While
  136. drop­While
    1. String.drop­While
  137. drop­While
    1. Substring.drop­While
  138. dsimp (0) (1)
  139. dsimp!
  140. dsimp
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  141. dsimp?
  142. dsimp?!
  143. 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. ends­With
    1. String.Slice.Pattern.BackwardPattern.ends­With (class method)
  127. ends­With
    1. String.Slice.ends­With
  128. ends­With
    1. String.ends­With
  129. enter
  130. entry­At­Idx!
    1. Std.TreeMap.entry­At­Idx!
  131. entry­At­Idx
    1. Std.TreeMap.entry­At­Idx
  132. entry­At­Idx?
    1. Std.TreeMap.entry­At­Idx?
  133. entry­At­Idx­D
    1. Std.TreeMap.entry­At­Idx­D
  134. env (Lake command)
  135. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  136. environment variables
  137. eprint
    1. IO.eprint
  138. eprintln
    1. IO.eprintln
  139. eq­Ignore­Ascii­Case
    1. String.Slice.eq­Ignore­Ascii­Case
  140. eq­Rec_heq
  141. eq_of_beq
    1. [anonymous] (class method)
  142. eq_of_heq
  143. eq_refl
  144. erase
    1. Array.erase
  145. erase
    1. List.erase
  146. erase
    1. Std.DHashMap.erase
  147. erase
    1. Std.DTreeMap.erase
  148. erase
    1. Std.Ext­DHashMap.erase
  149. erase
    1. Std.Ext­HashMap.erase
  150. erase
    1. Std.Ext­HashSet.erase
  151. erase
    1. Std.HashMap.erase
  152. erase
    1. Std.HashSet.erase
  153. erase
    1. Std.TreeMap.erase
  154. erase
    1. Std.TreeSet.erase
  155. erase­Dups
    1. List.erase­Dups
  156. erase­Idx!
    1. Array.erase­Idx!
  157. erase­Idx
    1. Array.erase­Idx
  158. erase­Idx
    1. List.erase­Idx
  159. erase­Idx­If­In­Bounds
    1. Array.erase­Idx­If­In­Bounds
  160. erase­Idx­TR
    1. List.erase­Idx­TR
  161. erase­Many
    1. Std.TreeMap.erase­Many
  162. erase­Many
    1. Std.TreeSet.erase­Many
  163. erase­P
    1. Array.erase­P
  164. erase­P
    1. List.erase­P
  165. erase­PTR
    1. List.erase­PTR
  166. erase­Reps
    1. Array.erase­Reps
  167. erase­Reps
    1. List.erase­Reps
  168. erase­TR
    1. List.erase­TR
  169. erw (0) (1)
  170. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
  171. eta
    1. Lean.Meta.Simp.Config.eta (structure field)
  172. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
  173. eta­Struct
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  174. eval.derive.repr
  175. eval.pp
  176. eval.type
  177. exact
  178. exact
    1. Quotient.exact
  179. exact?
  180. exact_mod_cast
  181. exe (Lake command)
  182. exe­Extension
    1. System.FilePath.exe­Extension
  183. exe­Name
    1. [anonymous] (structure field)
  184. execution
    1. IO.AccessRight.execution (structure field)
  185. exfalso
  186. exists
  187. exit
    1. IO.Process.exit
  188. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  189. exp
    1. Float.exp
  190. exp
    1. Float32.exp
  191. exp2
    1. Float.exp2
  192. exp2
    1. Float32.exp2
  193. expand­Macro?
    1. Lean.Macro.expand­Macro?
  194. expose_names
  195. ext (0) (1)
  196. ext1
  197. ext­Separator
    1. System.FilePath.ext­Separator
  198. extension
    1. System.FilePath.extension
  199. extensionality
    1. of propositions
  200. extra­Dep­Targets
    1. [anonymous] (structure field) (0) (1)
  201. extract
    1. Array.extract
  202. extract
    1. ByteArray.extract
  203. extract
    1. List.extract
  204. extract
    1. String.Iterator.extract
  205. extract
    1. String.ValidPos.extract
  206. extract
    1. String.extract
  207. extract
    1. Substring.extract
  208. extract­Lsb'
    1. BitVec.extract­Lsb'
  209. 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­Map
    1. Array.filter­Map
  228. filter­Map
    1. List.filter­Map
  229. filter­Map
    1. Std.DHashMap.filter­Map
  230. filter­Map
    1. Std.DTreeMap.filter­Map
  231. filter­Map
    1. Std.Ext­DHashMap.filter­Map
  232. filter­Map
    1. Std.Ext­HashMap.filter­Map
  233. filter­Map
    1. Std.HashMap.filter­Map
  234. filter­Map
    1. Std.TreeMap.filter­Map
  235. filter­Map­M
    1. Array.filter­Map­M
  236. filter­Map­M
    1. List.filter­Map­M
  237. filter­Map­TR
    1. List.filter­Map­TR
  238. filter­Rev­M
    1. Array.filter­Rev­M
  239. filter­Rev­M
    1. List.filter­Rev­M
  240. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  241. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  242. filter­TR
    1. List.filter­TR
  243. fin­Idx­Of?
    1. Array.fin­Idx­Of?
  244. fin­Idx­Of?
    1. List.fin­Idx­Of?
  245. fin­Range
    1. Array.fin­Range
  246. fin­Range
    1. List.fin­Range
  247. find
    1. String.Iterator.find
  248. find
    1. String.find
  249. find?
    1. Array.find?
  250. find?
    1. List.find?
  251. find?
    1. String.Slice.find?
  252. find­Extern­Lib?
    1. Lake.find­Extern­Lib?
  253. find­Fin­Idx?
    1. Array.find­Fin­Idx?
  254. find­Fin­Idx?
    1. ByteArray.find­Fin­Idx?
  255. find­Fin­Idx?
    1. List.find­Fin­Idx?
  256. find­Idx
    1. Array.find­Idx
  257. find­Idx
    1. List.find­Idx
  258. find­Idx?
    1. Array.find­Idx?
  259. find­Idx?
    1. ByteArray.find­Idx?
  260. find­Idx?
    1. List.find­Idx?
  261. find­Idx­M?
    1. Array.find­Idx­M?
  262. find­Lean­Exe?
    1. Lake.find­Lean­Exe?
  263. find­Lean­Lib?
    1. Lake.find­Lean­Lib?
  264. find­Line­Start
    1. String.find­Line­Start
  265. find­M?
    1. Array.find­M?
  266. find­M?
    1. List.find­M?
  267. find­Module?
    1. Lake.find­Module?
  268. find­Next­Pos
    1. String.Slice.find­Next­Pos
  269. find­Package?
    1. Lake.find­Package?
  270. find­Rev?
    1. Array.find­Rev?
  271. find­Rev?
    1. Subarray.find­Rev?
  272. find­Rev­M?
    1. Array.find­Rev­M?
  273. find­Rev­M?
    1. Subarray.find­Rev­M?
  274. find­Some!
    1. Array.find­Some!
  275. find­Some?
    1. Array.find­Some?
  276. find­Some?
    1. List.find­Some?
  277. find­Some­M?
    1. Array.find­Some­M?
  278. find­Some­M?
    1. List.find­Some­M?
  279. find­Some­Rev?
    1. Array.find­Some­Rev?
  280. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
  281. find­Some­Rev­M?
    1. Subarray.find­Some­Rev­M?
  282. first (0) (1)
  283. first­Diff­Pos
    1. String.first­Diff­Pos
  284. first­M
    1. Array.first­M
  285. first­M
    1. List.first­M
  286. fix
    1. Lean.Order.fix
  287. fix
    1. WellFounded.fix
  288. fix_eq
    1. Lean.Order.fix_eq
  289. flags
    1. IO.AccessRight.flags
  290. flags
    1. IO.FileRight.flags
  291. flat­Map
    1. Array.flat­Map
  292. flat­Map
    1. List.flat­Map
  293. flat­Map­M
    1. Array.flat­Map­M
  294. flat­Map­M
    1. List.flat­Map­M
  295. flat­Map­TR
    1. List.flat­Map­TR
  296. flatten
    1. Array.flatten
  297. flatten
    1. List.flatten
  298. flatten­TR
    1. List.flatten­TR
  299. floor
    1. Float.floor
  300. floor
    1. Float32.floor
  301. flush
    1. IO.FS.Handle.flush
  302. flush
    1. IO.FS.Stream.flush (structure field)
  303. fmod
    1. Int.fmod
  304. fn
    1. Thunk.fn (structure field)
  305. focus (0) (1)
  306. fold
    1. Nat.fold
  307. fold
    1. Std.DHashMap.fold
  308. fold
    1. Std.HashMap.fold
  309. fold
    1. Std.HashSet.fold
  310. fold­I
    1. Prod.fold­I
  311. fold­M
    1. Nat.fold­M
  312. fold­M
    1. Std.DHashMap.fold­M
  313. fold­M
    1. Std.HashMap.fold­M
  314. fold­M
    1. Std.HashSet.fold­M
  315. fold­Rev
    1. Nat.fold­Rev
  316. fold­Rev­M
    1. Nat.fold­Rev­M
  317. fold­TR
    1. Nat.fold­TR
  318. fold­Until
    1. String.Iterator.fold­Until
  319. foldl
    1. Array.foldl
  320. foldl
    1. ByteArray.foldl
  321. foldl
    1. Fin.foldl
  322. foldl
    1. List.foldl
  323. foldl
    1. Std.DTreeMap.foldl
  324. foldl
    1. Std.TreeMap.foldl
  325. foldl
    1. Std.TreeSet.foldl
  326. foldl
    1. String.Slice.foldl
  327. foldl
    1. String.foldl
  328. foldl
    1. Subarray.foldl
  329. foldl
    1. Substring.foldl
  330. foldl­M
    1. Array.foldl­M
  331. foldl­M
    1. ByteArray.foldl­M
  332. foldl­M
    1. Fin.foldl­M
  333. foldl­M
    1. List.foldl­M
  334. foldl­M
    1. Std.DTreeMap.foldl­M
  335. foldl­M
    1. Std.TreeMap.foldl­M
  336. foldl­M
    1. Std.TreeSet.foldl­M
  337. foldl­M
    1. Subarray.foldl­M
  338. foldl­Rec­On
    1. List.foldl­Rec­On
  339. foldr
    1. Array.foldr
  340. foldr
    1. ByteSlice.foldr
  341. foldr
    1. Fin.foldr
  342. foldr
    1. List.foldr
  343. foldr
    1. Std.TreeMap.foldr
  344. foldr
    1. Std.TreeSet.foldr
  345. foldr
    1. String.Slice.foldr
  346. foldr
    1. String.foldr
  347. foldr
    1. Subarray.foldr
  348. foldr
    1. Substring.foldr
  349. foldr­M
    1. Array.foldr­M
  350. foldr­M
    1. ByteSlice.foldr­M
  351. foldr­M
    1. Fin.foldr­M
  352. foldr­M
    1. List.foldr­M
  353. foldr­M
    1. Std.TreeMap.foldr­M
  354. foldr­M
    1. Std.TreeSet.foldr­M
  355. foldr­M
    1. Subarray.foldr­M
  356. foldr­Rec­On
    1. List.foldr­Rec­On
  357. foldr­TR
    1. List.foldr­TR
  358. for­A
    1. List.for­A
  359. for­Async
    1. Std.Channel.for­Async
  360. for­In'
    1. ForIn'.for­In' (class method)
  361. for­In
    1. ByteArray.for­In
  362. for­In
    1. ForIn.for­In (class method)
  363. for­In
    1. ForM.for­In
  364. for­In
    1. Std.DHashMap.for­In
  365. for­In
    1. Std.DTreeMap.for­In
  366. for­In
    1. Std.HashMap.for­In
  367. for­In
    1. Std.HashSet.for­In
  368. for­In
    1. Std.TreeMap.for­In
  369. for­In
    1. Std.TreeSet.for­In
  370. for­In
    1. Subarray.for­In
  371. for­M
    1. Array.for­M
  372. for­M
    1. ByteSlice.for­M
  373. for­M
    1. ForM.for­M (class method)
  374. for­M
    1. List.for­M
  375. for­M
    1. Nat.for­M
  376. for­M
    1. Option.for­M
  377. for­M
    1. Std.DHashMap.for­M
  378. for­M
    1. Std.DTreeMap.for­M
  379. for­M
    1. Std.HashMap.for­M
  380. for­M
    1. Std.HashSet.for­M
  381. for­M
    1. Std.TreeMap.for­M
  382. for­M
    1. Std.TreeSet.for­M
  383. for­M
    1. Subarray.for­M
  384. for­Rev­M
    1. Array.for­Rev­M
  385. for­Rev­M
    1. Nat.for­Rev­M
  386. for­Rev­M
    1. Subarray.for­Rev­M
  387. format
    1. Option.format
  388. format
    1. Std.ToFormat.format (class method)
  389. forward
    1. ByteArray.Iterator.forward
  390. forward
    1. String.Iterator.forward
  391. fr­Exp
    1. Float.fr­Exp
  392. fr­Exp
    1. Float32.fr­Exp
  393. from­State­M
    1. EStateM.from­State­M
  394. from­UTF8!
    1. String.from­UTF8!
  395. from­UTF8
    1. String.from­UTF8
  396. from­UTF8?
    1. String.from­UTF8?
  397. front
    1. String.Slice.front
  398. front
    1. String.front
  399. front
    1. Substring.front
  400. front?
    1. String.Slice.front?
  401. fst
    1. MProd.fst (structure field)
  402. fst
    1. PProd.fst (structure field)
  403. fst
    1. PSigma.fst (structure field)
  404. fst
    1. Prod.fst (structure field)
  405. fst
    1. Sigma.fst (structure field)
  406. fun
  407. fun_cases
  408. fun_induction
  409. 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.Slice.Pos.get!
  22. get!
    1. String.ValidPos.get!
  23. get!
    1. String.get!
  24. get!
    1. Subarray.get!
  25. get'
    1. String.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.Slice.Pos.get
  47. get
    1. String.ValidPos.get
  48. get
    1. String.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.Slice.Pos.get?
  63. get?
    1. String.ValidPos.get?
  64. get?
    1. String.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. ind
    1. Quot.ind
  418. ind
    1. Quotient.ind
  419. ind
    1. Squash.ind
  420. indent­D
    1. Std.Format.indent­D
  421. index
    1. Lean.Meta.DSimp.Config.index (structure field)
  422. index
    1. Lean.Meta.Simp.Config.index (structure field)
  423. index
    1. of inductive type
  424. indexed family
    1. of types
  425. induction
  426. induction
    1. Fin.induction
  427. induction­On
    1. Fin.induction­On
  428. induction­On
    1. Nat.div.induction­On
  429. induction­On
    1. Nat.mod.induction­On
  430. inductive.auto­Promote­Indices
  431. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  432. infer­Instance
  433. infer­Instance­As
  434. infer_instance
  435. inhabited­Left
    1. PSum.inhabited­Left
  436. inhabited­Left
    1. Sum.inhabited­Left
  437. inhabited­Right
    1. PSum.inhabited­Right
  438. inhabited­Right
    1. Sum.inhabited­Right
  439. inherit­Env
    1. IO.Process.SpawnArgs.args (structure field)
  440. init (Lake command)
  441. injection
  442. injections
  443. inner
    1. Std.DHashMap.Equiv.inner (structure field)
  444. inner
    1. Std.DTreeMap.Raw.inner (structure field)
  445. inner
    1. Std.Ext­HashSet.inner (structure field)
  446. inner
    1. Std.HashMap.Equiv.inner (structure field)
  447. inner
    1. Std.HashMap.Raw.inner (structure field)
  448. inner
    1. Std.HashSet.Equiv.inner (structure field)
  449. inner
    1. Std.HashSet.Raw.inner (structure field)
  450. inner
    1. Std.HashSet.inner (structure field)
  451. inner
    1. Std.TreeMap.Raw.inner (structure field)
  452. inner
    1. Std.TreeSet.Raw.inner (structure field)
  453. insert
    1. List.insert
  454. insert
    1. Std.DHashMap.insert
  455. insert
    1. Std.DTreeMap.insert
  456. insert
    1. Std.Ext­DHashMap.insert
  457. insert
    1. Std.Ext­HashMap.insert
  458. insert
    1. Std.Ext­HashSet.insert
  459. insert
    1. Std.HashMap.insert
  460. insert
    1. Std.HashSet.insert
  461. insert
    1. Std.TreeMap.insert
  462. insert
    1. Std.TreeSet.insert
  463. insert­Idx!
    1. Array.insert­Idx!
  464. insert­Idx
    1. Array.insert­Idx
  465. insert­Idx
    1. List.insert­Idx
  466. insert­Idx­If­In­Bounds
    1. Array.insert­Idx­If­In­Bounds
  467. insert­Idx­TR
    1. List.insert­Idx­TR
  468. insert­If­New
    1. Std.DHashMap.insert­If­New
  469. insert­If­New
    1. Std.DTreeMap.insert­If­New
  470. insert­If­New
    1. Std.Ext­DHashMap.insert­If­New
  471. insert­If­New
    1. Std.Ext­HashMap.insert­If­New
  472. insert­If­New
    1. Std.HashMap.insert­If­New
  473. insert­If­New
    1. Std.TreeMap.insert­If­New
  474. insert­Many
    1. Std.DHashMap.insert­Many
  475. insert­Many
    1. Std.DTreeMap.insert­Many
  476. insert­Many
    1. Std.Ext­DHashMap.insert­Many
  477. insert­Many
    1. Std.Ext­HashMap.insert­Many
  478. insert­Many
    1. Std.Ext­HashSet.insert­Many
  479. insert­Many
    1. Std.HashMap.insert­Many
  480. insert­Many
    1. Std.HashSet.insert­Many
  481. insert­Many
    1. Std.TreeMap.insert­Many
  482. insert­Many
    1. Std.TreeSet.insert­Many
  483. insert­Many­If­New­Unit
    1. Std.Ext­HashMap.insert­Many­If­New­Unit
  484. insert­Many­If­New­Unit
    1. Std.HashMap.insert­Many­If­New­Unit
  485. insert­Many­If­New­Unit
    1. Std.TreeMap.insert­Many­If­New­Unit
  486. insertion­Sort
    1. Array.insertion­Sort
  487. instance synthesis
  488. instance
    1. trace.grind.ematch.instance
  489. int­Cast
    1. IntCast.int­Cast (class method)
  490. int­Cast
    1. [anonymous] (class method)
  491. int­Cast_neg
    1. [anonymous] (class method)
  492. int­Cast_of­Nat
    1. [anonymous] (class method)
  493. int­Max
    1. BitVec.int­Max
  494. int­Min
    1. BitVec.int­Min
  495. intercalate
    1. List.intercalate
  496. intercalate
    1. String.intercalate
  497. intercalate­TR
    1. List.intercalate­TR
  498. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  499. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  500. intersperse
    1. List.intersperse
  501. intersperse­TR
    1. List.intersperse­TR
  502. intro (0) (1)
  503. intro | ... => ... | ... => ...
  504. intros
  505. inv­Image
  506. inv_zero
    1. [anonymous] (class method)
  507. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
  508. iota
    1. Lean.Meta.Simp.Config.iota (structure field)
  509. is­Absolute
    1. System.FilePath.is­Absolute
  510. is­Alpha
    1. Char.is­Alpha
  511. is­Alphanum
    1. Char.is­Alphanum
  512. is­Digit
    1. Char.is­Digit
  513. is­Dir
    1. System.FilePath.is­Dir
  514. is­Empty
    1. Array.is­Empty
  515. is­Empty
    1. ByteArray.is­Empty
  516. is­Empty
    1. List.is­Empty
  517. is­Empty
    1. Std.DHashMap.is­Empty
  518. is­Empty
    1. Std.DTreeMap.is­Empty
  519. is­Empty
    1. Std.Ext­DHashMap.is­Empty
  520. is­Empty
    1. Std.Ext­HashMap.is­Empty
  521. is­Empty
    1. Std.Ext­HashSet.is­Empty
  522. is­Empty
    1. Std.Format.is­Empty
  523. is­Empty
    1. Std.HashMap.is­Empty
  524. is­Empty
    1. Std.HashSet.is­Empty
  525. is­Empty
    1. Std.TreeMap.is­Empty
  526. is­Empty
    1. Std.TreeSet.is­Empty
  527. is­Empty
    1. String.Slice.is­Empty
  528. is­Empty
    1. String.is­Empty
  529. is­Empty
    1. Substring.is­Empty
  530. is­Emscripten
    1. System.Platform.is­Emscripten
  531. is­Eq
    1. Ordering.is­Eq
  532. is­Eq­Some
    1. Option.is­Eq­Some
  533. is­Eqv
    1. Array.is­Eqv
  534. is­Eqv
    1. List.is­Eqv
  535. is­Exclusive­Unsafe
  536. is­Finite
    1. Float.is­Finite
  537. is­Finite
    1. Float32.is­Finite
  538. is­GE
    1. Ordering.is­GE
  539. is­GT
    1. Ordering.is­GT
  540. is­Inf
    1. Float.is­Inf
  541. is­Inf
    1. Float32.is­Inf
  542. is­Int
    1. String.is­Int
  543. is­LE
    1. Ordering.is­LE
  544. is­LT
    1. Ordering.is­LT
  545. is­Left
    1. Sum.is­Left
  546. is­Lower
    1. Char.is­Lower
  547. is­Lt
    1. Fin.is­Lt (structure field)
  548. is­Na­N
    1. Float.is­Na­N
  549. is­Na­N
    1. Float32.is­Na­N
  550. is­Nat
    1. String.Slice.is­Nat
  551. is­Nat
    1. String.is­Nat
  552. is­Nat
    1. Substring.is­Nat
  553. is­Ne
    1. Ordering.is­Ne
  554. is­Nil
    1. Std.Format.is­Nil
  555. is­None
    1. Option.is­None
  556. is­OSX
    1. System.Platform.is­OSX
  557. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  558. is­Ok
    1. Except.is­Ok
  559. is­Perm
    1. List.is­Perm
  560. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  561. is­Prefix­Of
    1. Array.is­Prefix­Of
  562. is­Prefix­Of
    1. List.is­Prefix­Of
  563. is­Prefix­Of
    1. String.is­Prefix­Of
  564. is­Prefix­Of?
    1. List.is­Prefix­Of?
  565. is­Relative
    1. System.FilePath.is­Relative
  566. is­Resolved
    1. IO.Promise.is­Resolved
  567. is­Right
    1. Sum.is­Right
  568. is­Some
    1. Option.is­Some
  569. is­Sublist
    1. List.is­Sublist
  570. is­Suffix­Of
    1. List.is­Suffix­Of
  571. is­Suffix­Of?
    1. List.is­Suffix­Of?
  572. is­Tty
    1. IO.FS.Handle.is­Tty
  573. is­Tty
    1. IO.FS.Stream.is­Tty (structure field)
  574. is­Upper
    1. Char.is­Upper
  575. is­Valid
    1. String.Pos.Raw.is­Valid
  576. is­Valid
    1. String.ValidPos.is­Valid (structure field)
  577. is­Valid­Char
    1. Nat.is­Valid­Char
  578. is­Valid­Char
    1. UInt32.is­Valid­Char
  579. is­Valid­Char­Nat
    1. Char.is­Valid­Char­Nat
  580. is­Valid­For­Slice
    1. String.Pos.Raw.is­Valid­For­Slice
  581. is­Valid­For­Slice
    1. String.Slice.Pos.is­Valid­For­Slice (structure field)
  582. is­Valid­UTF8
    1. String.is­Valid­UTF8 (structure field)
  583. is­Whitespace
    1. Char.is­Whitespace
  584. is­Windows
    1. System.Platform.is­Windows
  585. iseqv
    1. Setoid.iseqv (class method)
  586. iter
    1. ByteArray.iter
  587. iter
    1. String.iter
  588. iterate
  589. iterate
    1. IO.iterate
  590. iunfoldr
    1. BitVec.iunfoldr
  591. 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­File­Path
    1. System.mk­File­Path
  196. mk­Iterator
    1. String.mk­Iterator
  197. mk­Ref
    1. IO.mk­Ref
  198. mk­Ref
    1. ST.mk­Ref
  199. mk­Std­Gen
  200. mleave
  201. mleft
  202. mod
    1. Fin.mod
  203. mod
    1. ISize.mod
  204. mod
    1. Int16.mod
  205. mod
    1. Int32.mod
  206. mod
    1. Int64.mod
  207. mod
    1. Int8.mod
  208. mod
    1. Mod.mod (class method)
  209. mod
    1. Nat.mod
  210. mod
    1. UInt16.mod
  211. mod
    1. UInt32.mod
  212. mod
    1. UInt64.mod
  213. mod
    1. UInt8.mod
  214. mod
    1. USize.mod
  215. mod­Core
    1. Nat.mod­Core
  216. modified
    1. IO.FS.Metadata.modified (structure field)
  217. modify
  218. modify
    1. Array.modify
  219. modify
    1. List.modify
  220. modify
    1. ST.Ref.modify
  221. modify
    1. Std.DHashMap.modify
  222. modify
    1. Std.DTreeMap.modify
  223. modify
    1. Std.Ext­DHashMap.modify
  224. modify
    1. Std.Ext­HashMap.modify
  225. modify
    1. Std.HashMap.modify
  226. modify
    1. Std.TreeMap.modify
  227. modify
    1. String.modify
  228. modify­Get
    1. EStateM.modify­Get
  229. modify­Get
    1. MonadState.modify­Get
  230. modify­Get
    1. MonadState.modify­Get (class method)
  231. modify­Get
    1. Monad­StateOf.modify­Get (class method)
  232. modify­Get
    1. ST.Ref.modify­Get
  233. modify­Get
    1. State­RefT'.modify­Get
  234. modify­Get
    1. StateT.modify­Get
  235. modify­Get­The
  236. modify­Head
    1. List.modify­Head
  237. modify­M
    1. Array.modify­M
  238. modify­Op
    1. Array.modify­Op
  239. modify­TR
    1. List.modify­TR
  240. modify­Tail­Idx
    1. List.modify­Tail­Idx
  241. modify­The
  242. modn
    1. Fin.modn
  243. monad­Eval
    1. MonadEval.monad­Eval (class method)
  244. monad­Eval
    1. Monad­EvalT.monad­Eval (class method)
  245. monad­Lift
    1. MonadLift.monad­Lift (class method)
  246. monad­Lift
    1. Monad­LiftT.monad­Lift (class method)
  247. monad­Map
    1. MonadFunctor.monad­Map (class method)
  248. monad­Map
    1. Monad­FunctorT.monad­Map (class method)
  249. mono­Ms­Now
    1. IO.mono­Ms­Now
  250. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  251. monotone
    1. Lean.Order.monotone
  252. mp
    1. Eq.mp
  253. mp
    1. Iff.mp (structure field)
  254. mpr
    1. Eq.mpr
  255. mpr
    1. Iff.mpr (structure field)
  256. mpure
  257. mpure_intro
  258. mrefine
  259. mrename_i
  260. mreplace
  261. mright
  262. msb
    1. BitVec.msb
  263. mspec
  264. mspecialize
  265. mspecialize_pure
  266. mstart
  267. mstop
  268. mul
    1. BitVec.mul
  269. mul
    1. Fin.mul
  270. mul
    1. Float.mul
  271. mul
    1. Float32.mul
  272. mul
    1. ISize.mul
  273. mul
    1. Int.mul
  274. mul
    1. Int16.mul
  275. mul
    1. Int32.mul
  276. mul
    1. Int64.mul
  277. mul
    1. Int8.mul
  278. mul
    1. Mul.mul (class method)
  279. mul
    1. Nat.mul
  280. mul
    1. UInt16.mul
  281. mul
    1. UInt32.mul
  282. mul
    1. UInt64.mul
  283. mul
    1. UInt8.mul
  284. mul
    1. USize.mul
  285. mul­Rec
    1. BitVec.mul­Rec
  286. mul_assoc
    1. Lean.Grind.Semiring.add_comm (class method)
  287. mul_comm
    1. [anonymous] (class method) (0) (1)
  288. mul_inv_cancel
    1. [anonymous] (class method)
  289. mul_lt_mul_of_pos_left
    1. Lean.Grind.OrderedRing.zero_lt_one (class method)
  290. mul_lt_mul_of_pos_right
    1. Lean.Grind.OrderedRing.mul_lt_mul_of_pos_left (class method)
  291. mul_one
    1. Lean.Grind.Semiring.add_assoc (class method)
  292. mul_zero
    1. Lean.Grind.Semiring.right_distrib (class method)
  293. mvars
    1. pp.mvars
  294. 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.next'
  145. next
    1. ByteArray.Iterator.next
  146. next
    1. RandomGen.next (class method)
  147. next
    1. String.Iterator.next
  148. next
    1. String.Slice.Pos.next
  149. next
    1. String.ValidPos.next
  150. next
    1. String.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.next­Until
  156. next­While
    1. String.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.for­M
  19. Option.format
  20. Option.get
  21. Option.get!
  22. Option.get­D
  23. Option.get­DM
  24. Option.get­M
  25. Option.guard
  26. Option.is­Eq­Some
  27. Option.is­None
  28. Option.is­Some
  29. Option.join
  30. Option.lt
  31. Option.map
  32. Option.map­A
  33. Option.map­M
  34. Option.max
  35. Option.merge
  36. Option.min
  37. Option.none
    1. Constructor of Option
  38. Option.or
  39. Option.or­Else
  40. Option.pbind
  41. Option.pelim
  42. Option.pmap
  43. Option.repr
  44. Option.sequence
  45. Option.some
    1. Constructor of Option
  46. Option.to­Array
  47. Option.to­List
  48. Option.try­Catch
  49. Option.unattach
  50. Option­T
  51. OptionT.bind
  52. OptionT.fail
  53. OptionT.lift
  54. OptionT.mk
  55. OptionT.or­Else
  56. OptionT.pure
  57. OptionT.run
  58. OptionT.try­Catch
  59. Or
  60. Or.by_cases
  61. Or.by_cases'
  62. Or.inl
    1. Constructor of Or
  63. Or.inr
    1. Constructor of Or
  64. Or­Op
  65. OrOp.mk
    1. Instance constructor of Or­Op
  66. Ord
  67. Ord.lex
  68. Ord.lex'
  69. Ord.mk
    1. Instance constructor of Ord
  70. Ord.on
  71. Ord.opposite
  72. Ord.to­BEq
  73. Ord.to­LE
  74. Ord.to­LT
  75. Ordered­Add
    1. Lean.Grind.Ordered­Add
  76. Ordered­Ring
    1. Lean.Grind.Ordered­Ring
  77. Ordering
  78. Ordering.eq
    1. Constructor of Ordering
  79. Ordering.gt
    1. Constructor of Ordering
  80. Ordering.is­Eq
  81. Ordering.is­GE
  82. Ordering.is­GT
  83. Ordering.is­LE
  84. Ordering.is­LT
  85. Ordering.is­Ne
  86. Ordering.lt
    1. Constructor of Ordering
  87. Ordering.swap
  88. Ordering.then
  89. Output
    1. IO.Process.Output
  90. obtain
  91. occs
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  92. of­Array
    1. Std.Ext­HashSet.of­Array
  93. of­Array
    1. Std.HashSet.of­Array
  94. of­Array
    1. Std.TreeMap.of­Array
  95. of­Array
    1. Std.TreeSet.of­Array
  96. of­Binary­Scientific
    1. Float.of­Binary­Scientific
  97. of­Binary­Scientific
    1. Float32.of­Binary­Scientific
  98. of­Bit­Vec
    1. ISize.of­Bit­Vec
  99. of­Bit­Vec
    1. Int16.of­Bit­Vec
  100. of­Bit­Vec
    1. Int32.of­Bit­Vec
  101. of­Bit­Vec
    1. Int64.of­Bit­Vec
  102. of­Bit­Vec
    1. Int8.of­Bit­Vec
  103. of­Bits
    1. Float.of­Bits
  104. of­Bits
    1. Float32.of­Bits
  105. of­Bool
    1. BitVec.of­Bool
  106. of­Bool­List­BE
    1. BitVec.of­Bool­List­BE
  107. of­Bool­List­LE
    1. BitVec.of­Bool­List­LE
  108. of­Buffer
    1. IO.FS.Stream.of­Buffer
  109. of­Byte­Array
    1. ByteSlice.of­Byte­Array
  110. of­Copy
    1. String.ValidPos.of­Copy
  111. of­Except
    1. IO.of­Except
  112. of­Except
    1. MonadExcept.of­Except
  113. of­Fin
    1. UInt16.of­Fin
  114. of­Fin
    1. UInt32.of­Fin
  115. of­Fin
    1. UInt64.of­Fin
  116. of­Fin
    1. UInt8.of­Fin
  117. of­Fin
    1. USize.of­Fin
  118. of­Fn
    1. Array.of­Fn
  119. of­Fn
    1. List.of­Fn
  120. of­Handle
    1. IO.FS.Stream.of­Handle
  121. of­Int
    1. BitVec.of­Int
  122. of­Int
    1. Float.of­Int
  123. of­Int
    1. Float32.of­Int
  124. of­Int
    1. ISize.of­Int
  125. of­Int
    1. Int16.of­Int
  126. of­Int
    1. Int32.of­Int
  127. of­Int
    1. Int64.of­Int
  128. of­Int
    1. Int8.of­Int
  129. of­Int­LE
    1. ISize.of­Int­LE
  130. of­Int­LE
    1. Int16.of­Int­LE
  131. of­Int­LE
    1. Int32.of­Int­LE
  132. of­Int­LE
    1. Int64.of­Int­LE
  133. of­Int­LE
    1. Int8.of­Int­LE
  134. of­Int­Truncate
    1. ISize.of­Int­Truncate
  135. of­Int­Truncate
    1. Int16.of­Int­Truncate
  136. of­Int­Truncate
    1. Int32.of­Int­Truncate
  137. of­Int­Truncate
    1. Int64.of­Int­Truncate
  138. of­Int­Truncate
    1. Int8.of­Int­Truncate
  139. of­List
    1. Std.DHashMap.of­List
  140. of­List
    1. Std.DTreeMap.of­List
  141. of­List
    1. Std.Ext­DHashMap.of­List
  142. of­List
    1. Std.Ext­HashMap.of­List
  143. of­List
    1. Std.Ext­HashSet.of­List
  144. of­List
    1. Std.HashMap.of­List
  145. of­List
    1. Std.HashSet.of­List
  146. of­List
    1. Std.TreeMap.of­List
  147. of­List
    1. Std.TreeSet.of­List
  148. of­Nat
    1. BitVec.of­Nat
  149. of­Nat
    1. Char.of­Nat
  150. of­Nat
    1. Fin.of­Nat
  151. of­Nat
    1. Float.of­Nat
  152. of­Nat
    1. Float32.of­Nat
  153. of­Nat
    1. ISize.of­Nat
  154. of­Nat
    1. Int16.of­Nat
  155. of­Nat
    1. Int32.of­Nat
  156. of­Nat
    1. Int64.of­Nat
  157. of­Nat
    1. Int8.of­Nat
  158. of­Nat
    1. OfNat.of­Nat (class method)
  159. of­Nat
    1. UInt16.of­Nat
  160. of­Nat
    1. UInt32.of­Nat
  161. of­Nat
    1. UInt64.of­Nat
  162. of­Nat
    1. UInt8.of­Nat
  163. of­Nat
    1. USize.of­Nat
  164. of­Nat
    1. [anonymous] (class method)
  165. of­Nat32
    1. USize.of­Nat32
  166. of­Nat­LT
    1. BitVec.of­Nat­LT
  167. of­Nat­LT
    1. UInt16.of­Nat­LT
  168. of­Nat­LT
    1. UInt32.of­Nat­LT
  169. of­Nat­LT
    1. UInt64.of­Nat­LT
  170. of­Nat­LT
    1. UInt8.of­Nat­LT
  171. of­Nat­LT
    1. USize.of­Nat­LT
  172. of­Nat­Truncate
    1. UInt16.of­Nat­Truncate
  173. of­Nat­Truncate
    1. UInt32.of­Nat­Truncate
  174. of­Nat­Truncate
    1. UInt64.of­Nat­Truncate
  175. of­Nat­Truncate
    1. UInt8.of­Nat­Truncate
  176. of­Nat­Truncate
    1. USize.of­Nat­Truncate
  177. of­Nat_eq_nat­Cast
    1. Lean.Grind.Semiring.pow_succ (class method)
  178. of­Nat_ext_iff
    1. Lean.Grind.Is­CharP.of­Nat_ext_iff (class method)
  179. of­Nat_succ
    1. Lean.Grind.Semiring.pow_zero (class method)
  180. of­Replace­Start
    1. String.Slice.Pos.of­Replace­Start
  181. of­Scientific
    1. Float.of­Scientific
  182. of­Scientific
    1. Float32.of­Scientific
  183. of­Scientific
    1. OfScientific.of­Scientific (class method)
  184. of­Slice
    1. String.Slice.Pos.of­Slice
  185. of­Subarray
    1. Array.of­Subarray
  186. of­UInt8
    1. Char.of­UInt8
  187. offset
    1. String.Slice.Pos.offset (structure field)
  188. offset
    1. String.ValidPos.offset (structure field)
  189. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  190. offset­Of­Pos
    1. String.offset­Of­Pos
  191. omega
  192. on
    1. Ord.on
  193. one_mul
    1. Lean.Grind.Semiring.mul_assoc (class method)
  194. one_zsmul
    1. [anonymous] (class method)
  195. open
  196. opposite
    1. Ord.opposite
  197. opt­Param
  198. optional
  199. or
    1. BitVec.or
  200. or
    1. Bool.or
  201. or
    1. List.or
  202. or
    1. Option.or
  203. or
    1. OrOp.or (class method)
  204. or­Else'
    1. EStateM.or­Else'
  205. or­Else
    1. EStateM.or­Else
  206. or­Else
    1. MonadExcept.or­Else
  207. or­Else
    1. Option.or­Else
  208. or­Else
    1. OptionT.or­Else
  209. or­Else
    1. ReaderT.or­Else
  210. or­Else
    1. StateT.or­Else
  211. or­Else
    1. [anonymous] (class method)
  212. or­Else­Lazy
    1. Except.or­Else­Lazy
  213. or­M
  214. orelse'
    1. MonadExcept.orelse'
  215. other
    1. IO.FileRight.other (structure field)
  216. out
    1. NeZero.out (class method)
  217. out
    1. Std.DTreeMap.Raw.WF.out (structure field)
  218. out
    1. Std.HashMap.Raw.WF.out (structure field)
  219. out
    1. Std.HashSet.Raw.WF.out (structure field)
  220. out
    1. Std.TreeMap.Raw.WF.out (structure field)
  221. out
    1. Std.TreeSet.Raw.WF.out (structure field)
  222. out­Param
  223. output
    1. IO.Process.output
  224. override list (Elan command)
  225. override set (Elan command)
  226. override unset (Elan command)

P

  1. PEmpty
  2. PEmpty.elim
  3. PLift
  4. PLift.up
    1. Constructor of PLift
  5. PProd
  6. PProd.mk
    1. Constructor of PProd
  7. PSigma
  8. PSigma.mk
    1. Constructor of PSigma
  9. PSum
  10. PSum.inhabited­Left
  11. PSum.inhabited­Right
  12. PSum.inl
    1. Constructor of PSum
  13. PSum.inr
    1. Constructor of PSum
  14. PUnit
  15. PUnit.unit
    1. Constructor of PUnit
  16. Pairwise
    1. List.Pairwise
  17. Partial­Order
    1. Lean.Order.Partial­Order
  18. Perm
    1. List.Perm
  19. Pos
    1. String.Slice.Pos
  20. Pow
  21. Pow.mk
    1. Instance constructor of Pow
  22. Prec
    1. Lean.Syntax.Prec
  23. Preresolved
    1. Lean.Syntax.Preresolved
  24. Prio
    1. Lean.Syntax.Prio
  25. Priority
    1. Task.Priority
  26. Prod
  27. Prod.all­I
  28. Prod.any­I
  29. Prod.fold­I
  30. Prod.lex­Lt
  31. Prod.map
  32. Prod.mk
    1. Constructor of Prod
  33. Prod.swap
  34. Promise
    1. IO.Promise
  35. Prop
  36. Pure
  37. Pure.mk
    1. Instance constructor of Pure
  38. pack (Lake command)
  39. parameter
    1. of inductive type
  40. paren
    1. Std.Format.paren
  41. parent
    1. System.FilePath.parent
  42. parser
  43. partition
    1. Array.partition
  44. partition
    1. List.partition
  45. partition
    1. Std.DHashMap.partition
  46. partition
    1. Std.DTreeMap.partition
  47. partition
    1. Std.HashMap.partition
  48. partition
    1. Std.HashSet.partition
  49. partition
    1. Std.TreeMap.partition
  50. partition
    1. Std.TreeSet.partition
  51. partition­M
    1. List.partition­M
  52. partition­Map
    1. List.partition­Map
  53. path
    1. IO.FS.DirEntry.path
  54. path­Exists
    1. System.FilePath.path­Exists
  55. path­Separator
    1. System.FilePath.path­Separator
  56. path­Separators
    1. System.FilePath.path­Separators
  57. pattern
  58. pbind
    1. Option.pbind
  59. pelim
    1. Option.pelim
  60. placeholder term
  61. pmap
    1. Array.pmap
  62. pmap
    1. List.pmap
  63. pmap
    1. Option.pmap
  64. polymorphism
    1. universe
  65. pop
    1. Array.pop
  66. pop­Front
    1. Subarray.pop­Front
  67. pop­While
    1. Array.pop­While
  68. pos!
    1. String.Slice.pos!
  69. pos
    1. ByteArray.Iterator.pos
  70. pos
    1. IO.FS.Stream.Buffer.pos (structure field)
  71. pos
    1. String.Iterator.pos
  72. pos
    1. String.Slice.pos
  73. pos?
    1. String.Slice.pos?
  74. pos­Of
    1. String.pos­Of
  75. pos­Of
    1. Substring.pos­Of
  76. positions
    1. String.Slice.positions
  77. pow
    1. Float.pow
  78. pow
    1. Float32.pow
  79. pow
    1. HomogeneousPow.pow (class method)
  80. pow
    1. Int.pow
  81. pow
    1. Nat.pow
  82. pow
    1. NatPow.pow (class method)
  83. pow
    1. Pow.pow (class method)
  84. pow_succ
    1. Lean.Grind.Semiring.mul_zero (class method)
  85. pow_zero
    1. Lean.Grind.Semiring.zero_mul (class method)
  86. pp
    1. eval.pp
  87. pp.deep­Terms
  88. pp.deepTerms.threshold
  89. pp.field­Notation
  90. pp.match
  91. pp.max­Steps
  92. pp.mvars
  93. pp.proofs
  94. pp.proofs.threshold
  95. precompile­Modules
    1. [anonymous] (structure field)
  96. pred
    1. Fin.pred
  97. pred
    1. Nat.pred
  98. predicative
  99. prefix­Join
    1. Std.Format.prefix­Join
  100. pretty
    1. Std.Format.pretty
  101. pretty­M
    1. Std.Format.pretty­M
  102. prev!
    1. String.Slice.Pos.prev!
  103. prev!
    1. String.ValidPos.prev!
  104. prev
    1. ByteArray.Iterator.prev
  105. prev
    1. String.Iterator.prev
  106. prev
    1. String.Slice.Pos.prev
  107. prev
    1. String.ValidPos.prev
  108. prev
    1. String.prev
  109. prev
    1. Substring.prev
  110. prev?
    1. String.Slice.Pos.prev?
  111. prev?
    1. String.ValidPos.prev?
  112. prevn
    1. ByteArray.Iterator.prevn
  113. prevn
    1. String.Iterator.prevn
  114. prevn
    1. String.Slice.Pos.prevn
  115. prevn
    1. Substring.prevn
  116. print
    1. IO.print
  117. println
    1. IO.println
  118. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
  119. proj
    1. Lean.Meta.Simp.Config.proj (structure field)
  120. proof state
  121. proofs
    1. pp.proofs
  122. property
    1. Subtype.property (structure field)
  123. propext
  124. proposition
  125. proposition
    1. decidable
  126. ptr­Addr­Unsafe
  127. ptr­Eq
  128. ptr­Eq
    1. ST.Ref.ptr­Eq
  129. ptr­Eq­List
  130. pure
    1. EStateM.pure
  131. pure
    1. Except.pure
  132. pure
    1. ExceptT.pure
  133. pure
    1. OptionT.pure
  134. pure
    1. Pure.pure (class method)
  135. pure
    1. ReaderT.pure
  136. pure
    1. StateT.pure
  137. pure
    1. Task.pure
  138. pure
    1. Thunk.pure
  139. pure_bind
    1. [anonymous] (class method)
  140. pure_seq
    1. [anonymous] (class method)
  141. push
    1. Array.push
  142. push
    1. ByteArray.push
  143. push
    1. String.push
  144. push­Newline
    1. Std.Format.Monad­PrettyFormat.push­Newline (class method)
  145. push­Output
    1. Std.Format.Monad­PrettyFormat.push­Output (class method)
  146. push_cast
  147. pushn
    1. String.pushn
  148. put­Str
    1. IO.FS.Handle.put­Str
  149. put­Str
    1. IO.FS.Stream.put­Str (structure field)
  150. put­Str­Ln
    1. IO.FS.Handle.put­Str­Ln
  151. 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. rcases
  43. read
    1. IO.AccessRight.read (structure field)
  44. read
    1. IO.FS.Handle.read
  45. read
    1. IO.FS.Stream.read (structure field)
  46. read
    1. MonadReader.read (class method)
  47. read
    1. Monad­ReaderOf.read (class method)
  48. read
    1. ReaderT.read
  49. read­Bin­File
    1. IO.FS.read­Bin­File
  50. read­Bin­To­End
    1. IO.FS.Handle.read­Bin­To­End
  51. read­Bin­To­End­Into
    1. IO.FS.Handle.read­Bin­To­End­Into
  52. read­Dir
    1. System.FilePath.read­Dir
  53. read­File
    1. IO.FS.read­File
  54. read­The
  55. read­To­End
    1. IO.FS.Handle.read­To­End
  56. real­Path
    1. IO.FS.real­Path
  57. rec
    1. Quot.rec
  58. rec
    1. Quotient.rec
  59. rec­Aux
    1. Nat.rec­Aux
  60. rec­On
    1. Quot.rec­On
  61. rec­On
    1. Quotient.rec­On
  62. rec­On­Subsingleton
    1. Quot.rec­On­Subsingleton
  63. rec­On­Subsingleton
    1. Quotient.rec­On­Subsingleton
  64. rec­On­Subsingleton₂
    1. Quotient.rec­On­Subsingleton₂
  65. recursor
  66. recv
    1. Std.Channel.recv
  67. reduce
  68. reduction
    1. ι (iota)
  69. refine
  70. refine'
  71. refl
    1. Equivalence.refl (structure field)
  72. refl
    1. Setoid.refl
  73. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  74. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  75. rel
    1. Lean.Order.PartialOrder.rel (class method)
  76. rel
    1. Well­FoundedRelation.rel (class method)
  77. rel_antisymm
    1. Lean.Order.PartialOrder.rel_antisymm (class method)
  78. rel_refl
    1. Lean.Order.PartialOrder.rel_refl (class method)
  79. rel_trans
    1. Lean.Order.PartialOrder.rel_trans (class method)
  80. relaxed­Auto­Implicit
  81. remaining­Bytes
    1. ByteArray.Iterator.remaining­Bytes
  82. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  83. remaining­To­String
    1. String.Iterator.remaining­To­String
  84. remove­All
    1. List.remove­All
  85. remove­Dir
    1. IO.FS.remove­Dir
  86. remove­Dir­All
    1. IO.FS.remove­Dir­All
  87. remove­File
    1. IO.FS.remove­File
  88. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  89. rename
  90. rename
    1. IO.FS.rename
  91. rename_i
  92. repair
    1. Substring.repair
  93. repeat (0) (1)
  94. repeat'
  95. repeat
    1. Nat.repeat
  96. repeat1'
  97. repeat­TR
    1. Nat.repeat­TR
  98. replace
  99. replace
    1. Array.replace
  100. replace
    1. List.replace
  101. replace
    1. String.replace
  102. replace­End
    1. String.Slice.replace­End
  103. replace­Start
    1. String.Slice.replace­Start
  104. replace­Start­End!
    1. String.Slice.replace­Start­End!
  105. replace­Start­End
    1. String.Slice.replace­Start­End
  106. replace­TR
    1. List.replace­TR
  107. replicate
    1. Array.replicate
  108. replicate
    1. BitVec.replicate
  109. replicate
    1. List.replicate
  110. replicate­TR
    1. List.replicate­TR
  111. repr
  112. repr
    1. Int.repr
  113. repr
    1. Nat.repr
  114. repr
    1. Option.repr
  115. repr
    1. USize.repr
  116. repr
    1. eval.derive.repr
  117. repr­Arg
  118. repr­Prec
    1. Repr.repr­Prec (class method)
  119. repr­Str
  120. resolve
    1. IO.Promise.resolve
  121. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  122. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  123. restore
    1. EStateM.Backtrackable.restore (class method)
  124. restore­M
    1. MonadControl.restore­M (class method)
  125. restore­M
    1. Monad­ControlT.restore­M (class method)
  126. result!
    1. IO.Promise.result!
  127. result
    1. trace.compiler.ir.result
  128. result?
    1. IO.Promise.result?
  129. result­D
    1. IO.Promise.result­D
  130. rev
    1. Fin.rev
  131. rev­Bytes
    1. String.Slice.rev­Bytes
  132. rev­Chars
    1. String.Slice.rev­Chars
  133. rev­Find
    1. String.rev­Find
  134. rev­Find?
    1. String.Slice.rev­Find?
  135. rev­Pos­Of
    1. String.rev­Pos­Of
  136. rev­Positions
    1. String.Slice.rev­Positions
  137. rev­Split
    1. String.Slice.rev­Split
  138. reverse
    1. Array.reverse
  139. reverse
    1. BitVec.reverse
  140. reverse
    1. List.reverse
  141. reverse­Induction
    1. Fin.reverse­Induction
  142. revert
  143. rewind
    1. IO.FS.Handle.rewind
  144. rewrite (0) (1)
  145. rewrite
    1. trace.Meta.Tactic.simp.rewrite
  146. rfl (0) (1) (2)
  147. rfl'
  148. rfl
    1. HEq.rfl
  149. rfl
    1. ReflBEq.rfl (class method)
  150. rhs
  151. right (0) (1)
  152. right
    1. And.right (structure field)
  153. right_distrib
    1. Lean.Grind.Semiring.one_mul (class method)
  154. rightpad
    1. Array.rightpad
  155. rightpad
    1. List.rightpad
  156. rintro
  157. root
    1. IO.FS.DirEntry.root (structure field)
  158. root
    1. [anonymous] (structure field)
  159. roots
    1. [anonymous] (structure field)
  160. rotate­Left
    1. BitVec.rotate­Left
  161. rotate­Left
    1. List.rotate­Left
  162. rotate­Right
    1. BitVec.rotate­Right
  163. rotate­Right
    1. List.rotate­Right
  164. rotate_left
  165. rotate_right
  166. round
    1. Float.round
  167. round
    1. Float32.round
  168. run (Elan command)
  169. run'
    1. EStateM.run'
  170. run'
    1. State­CpsT.run'
  171. run'
    1. State­RefT'.run'
  172. run'
    1. StateT.run'
  173. run
    1. EStateM.run
  174. run
    1. Except­CpsT.run
  175. run
    1. ExceptT.run
  176. run
    1. IO.Process.run
  177. run
    1. Id.run
  178. run
    1. OptionT.run
  179. run
    1. ReaderT.run
  180. run
    1. State­CpsT.run
  181. run
    1. State­RefT'.run
  182. run
    1. StateT.run
  183. run­Catch
    1. Except­CpsT.run­Catch
  184. run­EST
  185. run­K
    1. Except­CpsT.run­K
  186. run­K
    1. State­CpsT.run­K
  187. run­ST
  188. run_tac
  189. rw (0) (1)
  190. rw?
  191. rw_mod_cast
  192. rwa

S

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

T

  1. TSep­Array
    1. Lean.Syntax.TSep­Array
  2. TSyntax
    1. Lean.TSyntax
  3. TSyntax­Array
    1. Lean.TSyntax­Array
  4. Tactic
    1. Lean.Syntax.Tactic
  5. Task
  6. Task.Priority
  7. Task.Priority.dedicated
  8. Task.Priority.default
  9. Task.Priority.max
  10. Task.bind
  11. Task.get
  12. Task.map
  13. Task.map­List
  14. Task.pure
  15. Task.spawn
  16. Task­State
    1. IO.Task­State
  17. Term
    1. Lean.Syntax.Term
  18. Thunk
  19. Thunk.bind
  20. Thunk.get
  21. Thunk.map
  22. Thunk.mk
    1. Constructor of Thunk
  23. Thunk.pure
  24. To­Backward­Searcher
    1. String.Slice.Pattern.To­Backward­Searcher
  25. To­Format
    1. Std.To­Format
  26. To­Forward­Searcher
    1. String.Slice.Pattern.To­Forward­Searcher
  27. To­Int
    1. Lean.Grind.To­Int
  28. Trans
  29. Trans.mk
    1. Instance constructor of Trans
  30. Transparency­Mode
    1. Lean.Meta.Transparency­Mode
  31. Tree­Map
    1. Std.Tree­Map
  32. Tree­Set
    1. Std.Tree­Set
  33. True
  34. True.intro
    1. Constructor of True
  35. Type
  36. tactic
  37. tactic'
  38. tactic.custom­Eliminators
  39. tactic.hygienic
  40. tactic.simp.trace (0) (1)
  41. tactic.skip­Assigned­Instances
  42. tail!
    1. List.tail!
  43. tail
    1. List.tail
  44. tail?
    1. List.tail?
  45. tail­D
    1. List.tail­D
  46. take
    1. Array.take
  47. take
    1. List.take
  48. take
    1. ST.Ref.take
  49. take
    1. String.Slice.take
  50. take
    1. String.take
  51. take
    1. Subarray.take
  52. take
    1. Substring.take
  53. take­End
    1. String.Slice.take­End
  54. take­End­While
    1. String.Slice.take­End­While
  55. take­Right
    1. String.take­Right
  56. take­Right
    1. Substring.take­Right
  57. take­Right­While
    1. String.take­Right­While
  58. take­Right­While
    1. Substring.take­Right­While
  59. take­Stdin
    1. IO.Process.Child.take­Stdin
  60. take­TR
    1. List.take­TR
  61. take­While
    1. Array.take­While
  62. take­While
    1. List.take­While
  63. take­While
    1. String.Slice.take­While
  64. take­While
    1. String.take­While
  65. take­While
    1. Substring.take­While
  66. take­While­TR
    1. List.take­While­TR
  67. tan
    1. Float.tan
  68. tan
    1. Float32.tan
  69. tanh
    1. Float.tanh
  70. tanh
    1. Float32.tanh
  71. target
    1. System.Platform.target
  72. tdiv
    1. Int.tdiv
  73. term
    1. placeholder
  74. test (Lake command)
  75. test­Bit
    1. Nat.test­Bit
  76. then
    1. Ordering.then
  77. threshold
    1. pp.deepTerms.threshold
  78. threshold
    1. pp.proofs.threshold
  79. throw
    1. EStateM.throw
  80. throw
    1. MonadExcept.throw (class method)
  81. throw
    1. Monad­ExceptOf.throw (class method)
  82. throw­Error
    1. Lean.Macro.throw­Error
  83. throw­Error­At
    1. Lean.Macro.throw­Error­At
  84. throw­The
  85. throw­Unsupported
    1. Lean.Macro.throw­Unsupported
  86. tmod
    1. Int.tmod
  87. to­Add
    1. Lean.Grind.Semiring.to­Add (class method)
  88. to­Add­Comm­Group
    1. Lean.Grind.IntModule.to­Add­Comm­Group (class method)
  89. to­Add­Comm­Monoid
    1. Lean.Grind.NatModule.to­Add­Comm­Monoid (class method)
  90. to­Applicative
    1. Alternative.to­Applicative (class method)
  91. to­Applicative
    1. Monad.to­Applicative (class method)
  92. to­Array
    1. List.to­Array
  93. to­Array
    1. Option.to­Array
  94. to­Array
    1. Std.DHashMap.to­Array
  95. to­Array
    1. Std.DTreeMap.to­Array
  96. to­Array
    1. Std.HashMap.to­Array
  97. to­Array
    1. Std.HashSet.to­Array
  98. to­Array
    1. Std.TreeMap.to­Array
  99. to­Array
    1. Std.TreeSet.to­Array
  100. to­Array
    1. Subarray.to­Array
  101. to­Array­Impl
    1. List.to­Array­Impl
  102. to­BEq
    1. Ord.to­BEq
  103. to­Base­IO
    1. EIO.to­Base­IO
  104. to­Bind
    1. [anonymous] (class method)
  105. to­Bit­Vec
    1. ISize.to­Bit­Vec
  106. to­Bit­Vec
    1. Int16.to­Bit­Vec
  107. to­Bit­Vec
    1. Int32.to­Bit­Vec
  108. to­Bit­Vec
    1. Int64.to­Bit­Vec
  109. to­Bit­Vec
    1. Int8.to­Bit­Vec
  110. to­Bit­Vec
    1. UInt16.to­Bit­Vec (structure field)
  111. to­Bit­Vec
    1. UInt32.to­Bit­Vec (structure field)
  112. to­Bit­Vec
    1. UInt64.to­Bit­Vec (structure field)
  113. to­Bit­Vec
    1. UInt8.to­Bit­Vec (structure field)
  114. to­Bit­Vec
    1. USize.to­Bit­Vec (structure field)
  115. to­Bits
    1. Float.to­Bits
  116. to­Bits
    1. Float32.to­Bits
  117. to­Bool
    1. Except.to­Bool
  118. to­Byte­Array
    1. ByteSlice.to­Byte­Array
  119. to­Byte­Array
    1. List.to­Byte­Array
  120. to­Byte­Slice
    1. ByteArray.to­Byte­Slice
  121. to­Comm­Ring
    1. Lean.Grind.Field.to­Comm­Ring (class method)
  122. to­Copy
    1. String.Slice.Pos.to­Copy
  123. to­Digits
    1. Nat.to­Digits
  124. to­Div
    1. [anonymous] (class method)
  125. to­EIO
    1. BaseIO.to­EIO
  126. to­EIO
    1. IO.to­EIO
  127. to­End
    1. ByteArray.Iterator.to­End
  128. to­End
    1. String.Iterator.to­End
  129. to­Fin
    1. BitVec.to­Fin (structure field)
  130. to­Fin
    1. UInt16.to­Fin
  131. to­Fin
    1. UInt32.to­Fin
  132. to­Fin
    1. UInt64.to­Fin
  133. to­Fin
    1. UInt8.to­Fin
  134. to­Fin
    1. USize.to­Fin
  135. to­Float
    1. Float32.to­Float
  136. to­Float
    1. ISize.to­Float
  137. to­Float
    1. Int16.to­Float
  138. to­Float
    1. Int32.to­Float
  139. to­Float
    1. Int64.to­Float
  140. to­Float
    1. Int8.to­Float
  141. to­Float
    1. Nat.to­Float
  142. to­Float
    1. UInt16.to­Float
  143. to­Float
    1. UInt32.to­Float
  144. to­Float
    1. UInt64.to­Float
  145. to­Float
    1. UInt8.to­Float
  146. to­Float
    1. USize.to­Float
  147. to­Float32
    1. Float.to­Float32
  148. to­Float32
    1. ISize.to­Float32
  149. to­Float32
    1. Int16.to­Float32
  150. to­Float32
    1. Int32.to­Float32
  151. to­Float32
    1. Int64.to­Float32
  152. to­Float32
    1. Int8.to­Float32
  153. to­Float32
    1. Nat.to­Float32
  154. to­Float32
    1. UInt16.to­Float32
  155. to­Float32
    1. UInt32.to­Float32
  156. to­Float32
    1. UInt64.to­Float32
  157. to­Float32
    1. UInt8.to­Float32
  158. to­Float32
    1. USize.to­Float32
  159. to­Float­Array
    1. List.to­Float­Array
  160. to­Format
    1. String.to­Format
  161. to­Functor
    1. Applicative.to­Functor (class method)
  162. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  163. to­Handle­Type
    1. IO.Process.Stdio.to­Handle­Type
  164. to­Hex
    1. BitVec.to­Hex
  165. to­IO'
    1. EIO.to­IO'
  166. to­IO
    1. BaseIO.to­IO
  167. to­IO
    1. EIO.to­IO
  168. to­ISize
    1. Bool.to­ISize
  169. to­ISize
    1. Float.to­ISize
  170. to­ISize
    1. Float32.to­ISize
  171. to­ISize
    1. Int.to­ISize
  172. to­ISize
    1. Int16.to­ISize
  173. to­ISize
    1. Int32.to­ISize
  174. to­ISize
    1. Int64.to­ISize
  175. to­ISize
    1. Int8.to­ISize
  176. to­ISize
    1. Nat.to­ISize
  177. to­ISize
    1. USize.to­ISize
  178. to­Int!
    1. String.to­Int!
  179. to­Int
    1. BitVec.to­Int
  180. to­Int
    1. Bool.to­Int
  181. to­Int
    1. ISize.to­Int
  182. to­Int
    1. Int16.to­Int
  183. to­Int
    1. Int32.to­Int
  184. to­Int
    1. Int64.to­Int
  185. to­Int
    1. Int8.to­Int
  186. to­Int
    1. Lean.Grind.ToInt.to­Int (class method)
  187. to­Int16
    1. Bool.to­Int16
  188. to­Int16
    1. Float.to­Int16
  189. to­Int16
    1. Float32.to­Int16
  190. to­Int16
    1. ISize.to­Int16
  191. to­Int16
    1. Int.to­Int16
  192. to­Int16
    1. Int32.to­Int16
  193. to­Int16
    1. Int64.to­Int16
  194. to­Int16
    1. Int8.to­Int16
  195. to­Int16
    1. Nat.to­Int16
  196. to­Int16
    1. UInt16.to­Int16
  197. to­Int32
    1. Bool.to­Int32
  198. to­Int32
    1. Float.to­Int32
  199. to­Int32
    1. Float32.to­Int32
  200. to­Int32
    1. ISize.to­Int32
  201. to­Int32
    1. Int.to­Int32
  202. to­Int32
    1. Int16.to­Int32
  203. to­Int32
    1. Int64.to­Int32
  204. to­Int32
    1. Int8.to­Int32
  205. to­Int32
    1. Nat.to­Int32
  206. to­Int32
    1. UInt32.to­Int32
  207. to­Int64
    1. Bool.to­Int64
  208. to­Int64
    1. Float.to­Int64
  209. to­Int64
    1. Float32.to­Int64
  210. to­Int64
    1. ISize.to­Int64
  211. to­Int64
    1. Int.to­Int64
  212. to­Int64
    1. Int16.to­Int64
  213. to­Int64
    1. Int32.to­Int64
  214. to­Int64
    1. Int8.to­Int64
  215. to­Int64
    1. Nat.to­Int64
  216. to­Int64
    1. UInt64.to­Int64
  217. to­Int8
    1. Bool.to­Int8
  218. to­Int8
    1. Float.to­Int8
  219. to­Int8
    1. Float32.to­Int8
  220. to­Int8
    1. ISize.to­Int8
  221. to­Int8
    1. Int.to­Int8
  222. to­Int8
    1. Int16.to­Int8
  223. to­Int8
    1. Int32.to­Int8
  224. to­Int8
    1. Int64.to­Int8
  225. to­Int8
    1. Nat.to­Int8
  226. to­Int8
    1. UInt8.to­Int8
  227. to­Int?
    1. String.to­Int?
  228. to­Int_inj
    1. Lean.Grind.ToInt.to­Int_inj (class method)
  229. to­Int_mem
    1. Lean.Grind.ToInt.to­Int_mem (class method)
  230. to­Inv
    1. [anonymous] (class method)
  231. to­Iterator
    1. Substring.to­Iterator
  232. to­LE
    1. Ord.to­LE
  233. to­LT
    1. Ord.to­LT
  234. to­Lawful­Applicative
    1. LawfulMonad.to­Lawful­Applicative (class method)
  235. to­Lawful­Functor
    1. LawfulApplicative.to­Lawful­Functor (class method)
  236. to­Lean­Config
    1. Lake.Lean­ExeConfig.to­Lean­Config (structure field)
  237. to­Lean­Config
    1. Lake.Lean­LibConfig.to­Lean­Config (structure field)
  238. to­List
    1. Array.to­List
  239. to­List
    1. Array.to­List (structure field)
  240. to­List
    1. ByteArray.to­List
  241. to­List
    1. Option.to­List
  242. to­List
    1. Std.DHashMap.to­List
  243. to­List
    1. Std.DTreeMap.to­List
  244. to­List
    1. Std.HashMap.to­List
  245. to­List
    1. Std.HashSet.to­List
  246. to­List
    1. Std.TreeMap.to­List
  247. to­List
    1. Std.TreeSet.to­List
  248. to­List
    1. String.to­List
  249. to­List­Append
    1. Array.to­List­Append
  250. to­List­Rev
    1. Array.to­List­Rev
  251. to­Lower
    1. Char.to­Lower
  252. to­Lower
    1. String.to­Lower
  253. to­Monad­State­Of
    1. ST.Ref.to­Monad­State­Of
  254. to­Mul
    1. [anonymous] (class method)
  255. to­Name
    1. String.to­Name
  256. to­Name
    1. Substring.to­Name
  257. to­Nat!
    1. String.Slice.to­Nat!
  258. to­Nat!
    1. String.to­Nat!
  259. to­Nat
    1. BitVec.to­Nat
  260. to­Nat
    1. Bool.to­Nat
  261. to­Nat
    1. Char.to­Nat
  262. to­Nat
    1. Fin.to­Nat
  263. to­Nat
    1. Int.to­Nat
  264. to­Nat
    1. UInt16.to­Nat
  265. to­Nat
    1. UInt32.to­Nat
  266. to­Nat
    1. UInt64.to­Nat
  267. to­Nat
    1. UInt8.to­Nat
  268. to­Nat
    1. USize.to­Nat
  269. to­Nat?
    1. Int.to­Nat?
  270. to­Nat?
    1. String.Slice.to­Nat?
  271. to­Nat?
    1. String.to­Nat?
  272. to­Nat?
    1. Substring.to­Nat?
  273. to­Nat­Clamp­Neg
    1. ISize.to­Nat­Clamp­Neg
  274. to­Nat­Clamp­Neg
    1. Int16.to­Nat­Clamp­Neg
  275. to­Nat­Clamp­Neg
    1. Int32.to­Nat­Clamp­Neg
  276. to­Nat­Clamp­Neg
    1. Int64.to­Nat­Clamp­Neg
  277. to­Nat­Clamp­Neg
    1. Int8.to­Nat­Clamp­Neg
  278. to­Neg
    1. [anonymous] (class method)
  279. to­Option
    1. Except.to­Option
  280. to­Ordered­Add
    1. Lean.Grind.OrderedRing.to­Ordered­Add (class method)
  281. to­Partial­Equiv­BEq
    1. EquivBEq.to­Partial­Equiv­BEq (class method)
  282. to­Partial­Order
    1. Lean.Order.CCPO.to­Partial­Order (class method)
  283. to­Pure
    1. [anonymous] (class method)
  284. to­Refl­BEq
    1. LawfulBEq.to­Refl­BEq (class method)
  285. to­Refl­BEq
    1. [anonymous] (class method)
  286. to­Replace­Start
    1. String.Slice.Pos.to­Replace­Start
  287. to­Ring
    1. Lean.Grind.CommRing.to­Ring (class method)
  288. to­Searcher
    1. String.Slice.Pattern.To­BackwardSearcher.to­Searcher (class method)
  289. to­Searcher
    1. String.Slice.Pattern.To­ForwardSearcher.to­Searcher (class method)
  290. to­Semiring
    1. Lean.Grind.CommSemiring.to­Semiring (class method)
  291. to­Semiring
    1. Lean.Grind.Ring.to­Semiring (class method)
  292. to­Seq
    1. [anonymous] (class method)
  293. to­Seq­Left
    1. Applicative.to­Pure (class method)
  294. to­Seq­Right
    1. [anonymous] (class method)
  295. to­Slice
    1. String.ValidPos.to­Slice
  296. to­Stdio­Config
    1. IO.Process.SpawnArgs.to­Stdio­Config (structure field)
  297. to­String
    1. Char.to­String
  298. to­String
    1. Float.to­String
  299. to­String
    1. Float32.to­String
  300. to­String
    1. IO.Error.to­String
  301. to­String
    1. List.to­String
  302. to­String
    1. String.Iterator.to­String
  303. to­String
    1. Substring.to­String
  304. to­String
    1. System.FilePath.to­String (structure field)
  305. to­Sub
    1. [anonymous] (class method)
  306. to­Sub­Digits
    1. Nat.to­Sub­Digits
  307. to­Subarray
    1. Array.to­Subarray
  308. to­Subscript­String
    1. Nat.to­Subscript­String
  309. to­Substring'
    1. String.to­Substring'
  310. to­Substring
    1. String.to­Substring
  311. to­Super­Digits
    1. Nat.to­Super­Digits
  312. to­Superscript­String
    1. Nat.to­Superscript­String
  313. to­UInt16
    1. Bool.to­UInt16
  314. to­UInt16
    1. Float.to­UInt16
  315. to­UInt16
    1. Float32.to­UInt16
  316. to­UInt16
    1. Int16.to­UInt16 (structure field)
  317. to­UInt16
    1. Nat.to­UInt16
  318. to­UInt16
    1. UInt32.to­UInt16
  319. to­UInt16
    1. UInt64.to­UInt16
  320. to­UInt16
    1. UInt8.to­UInt16
  321. to­UInt16
    1. USize.to­UInt16
  322. to­UInt32
    1. Bool.to­UInt32
  323. to­UInt32
    1. Float.to­UInt32
  324. to­UInt32
    1. Float32.to­UInt32
  325. to­UInt32
    1. Int32.to­UInt32 (structure field)
  326. to­UInt32
    1. Nat.to­UInt32
  327. to­UInt32
    1. UInt16.to­UInt32
  328. to­UInt32
    1. UInt64.to­UInt32
  329. to­UInt32
    1. UInt8.to­UInt32
  330. to­UInt32
    1. USize.to­UInt32
  331. to­UInt64
    1. Bool.to­UInt64
  332. to­UInt64
    1. Float.to­UInt64
  333. to­UInt64
    1. Float32.to­UInt64
  334. to­UInt64
    1. Int64.to­UInt64 (structure field)
  335. to­UInt64
    1. Nat.to­UInt64
  336. to­UInt64
    1. UInt16.to­UInt64
  337. to­UInt64
    1. UInt32.to­UInt64
  338. to­UInt64
    1. UInt8.to­UInt64
  339. to­UInt64
    1. USize.to­UInt64
  340. to­UInt64BE!
    1. ByteArray.to­UInt64BE!
  341. to­UInt64LE!
    1. ByteArray.to­UInt64LE!
  342. to­UInt8
    1. Bool.to­UInt8
  343. to­UInt8
    1. Char.to­UInt8
  344. to­UInt8
    1. Float.to­UInt8
  345. to­UInt8
    1. Float32.to­UInt8
  346. to­UInt8
    1. Int8.to­UInt8 (structure field)
  347. to­UInt8
    1. Nat.to­UInt8
  348. to­UInt8
    1. UInt16.to­UInt8
  349. to­UInt8
    1. UInt32.to­UInt8
  350. to­UInt8
    1. UInt64.to­UInt8
  351. to­UInt8
    1. USize.to­UInt8
  352. to­USize
    1. Bool.to­USize
  353. to­USize
    1. Float.to­USize
  354. to­USize
    1. Float32.to­USize
  355. to­USize
    1. ISize.to­USize (structure field)
  356. to­USize
    1. Nat.to­USize
  357. to­USize
    1. UInt16.to­USize
  358. to­USize
    1. UInt32.to­USize
  359. to­USize
    1. UInt64.to­USize
  360. to­USize
    1. UInt8.to­USize
  361. to­UTF8
    1. String.to­UTF8
  362. to­Upper
    1. Char.to­Upper
  363. to­Upper
    1. String.to­Upper
  364. to­Vector
    1. Array.to­Vector
  365. toolchain gc (Elan command)
  366. toolchain install (Elan command)
  367. toolchain link (Elan command)
  368. toolchain list (Elan command)
  369. toolchain uninstall (Elan command)
  370. trace
  371. trace
    1. Lean.Macro.trace
  372. trace
    1. tactic.simp.trace (0) (1)
  373. trace.Elab.definition.wf
  374. trace.Meta.Tactic.simp.discharge
  375. trace.Meta.Tactic.simp.rewrite
  376. trace.compiler.ir.result
  377. trace.grind.ematch.instance
  378. trace.grind.split
  379. trace_state (0) (1)
  380. trans
    1. Eq.trans
  381. trans
    1. Equivalence.trans (structure field)
  382. trans
    1. Setoid.trans
  383. trans
    1. Trans.trans (class method)
  384. translate-config (Lake command)
  385. transparency
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  386. trim
    1. String.trim
  387. trim
    1. Substring.trim
  388. trim­Ascii
    1. String.Slice.trim­Ascii
  389. trim­Ascii­End
    1. String.Slice.trim­Ascii­End
  390. trim­Ascii­Start
    1. String.Slice.trim­Ascii­Start
  391. trim­Left
    1. String.trim­Left
  392. trim­Left
    1. Substring.trim­Left
  393. trim­Right
    1. String.trim­Right
  394. trim­Right
    1. Substring.trim­Right
  395. trivial
  396. truncate
    1. BitVec.truncate
  397. truncate
    1. IO.FS.Handle.truncate
  398. try (0) (1)
  399. try­Catch
    1. EStateM.try­Catch
  400. try­Catch
    1. Except.try­Catch
  401. try­Catch
    1. ExceptT.try­Catch
  402. try­Catch
    1. MonadExcept.try­Catch (class method)
  403. try­Catch
    1. Monad­ExceptOf.try­Catch (class method)
  404. try­Catch
    1. Option.try­Catch
  405. try­Catch
    1. OptionT.try­Catch
  406. try­Catch­The
  407. try­Finally'
    1. MonadFinally.try­Finally' (class method)
  408. try­Lock
    1. IO.FS.Handle.try­Lock
  409. try­Wait
    1. IO.Process.Child.try­Wait
  410. two­Pow
    1. BitVec.two­Pow
  411. type constructor
  412. type
    1. IO.FS.Metadata.type (structure field)
  413. type
    1. eval.type
  414. 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. unpack (Lake command)
  210. unsafe­Base­IO
  211. unsafe­Cast
  212. unsafe­EIO
  213. unsafe­IO
  214. unsupported­Syntax
    1. Lean.Macro.Exception.unsupported­Syntax
  215. unzip
    1. Array.unzip
  216. unzip
    1. List.unzip
  217. unzip­TR
    1. List.unzip­TR
  218. update (Lake command)
  219. upload (Lake command)
  220. user
    1. IO.FileRight.user (structure field)
  221. user­Error
    1. IO.user­Error
  222. uset
    1. Array.uset
  223. uset
    1. ByteArray.uset
  224. ushift­Right
    1. BitVec.ushift­Right
  225. ushift­Right­Rec
    1. BitVec.ushift­Right­Rec
  226. usize
    1. Array.usize
  227. usize
    1. ByteArray.usize
  228. usub­Overflow
    1. BitVec.usub­Overflow
  229. utf16Size
    1. Char.utf16Size
  230. utf8Byte­Size
    1. String.Slice.utf8Byte­Size
  231. utf8Byte­Size
    1. String.utf8Byte­Size
  232. utf8Decode?
    1. ByteArray.utf8Decode?
  233. utf8Decode­Char
    1. ByteArray.utf8Decode­Char
  234. utf8Decode­Char?
    1. ByteArray.utf8Decode­Char?
  235. utf8Encode­Char
    1. String.utf8Encode­Char
  236. utf8Size
    1. Char.utf8Size

V

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

W

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

X

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

Z

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