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. Append
  14. Append.mk
    1. Instance constructor of Append
  15. Applicative
  16. Applicative.mk
    1. Instance constructor of Applicative
  17. Array
  18. Array.all
  19. Array.all­Diff
  20. Array.all­M
  21. Array.any
  22. Array.any­M
  23. Array.append
  24. Array.append­List
  25. Array.attach
  26. Array.attach­With
  27. Array.back
  28. Array.back!
  29. Array.back?
  30. Array.bin­Insert
  31. Array.bin­Insert­M
  32. Array.bin­Search
  33. Array.bin­Search­Contains
  34. Array.contains
  35. Array.count
  36. Array.count­P
  37. Array.drop
  38. Array.elem
  39. Array.empty
  40. Array.empty­With­Capacity
  41. Array.erase
  42. Array.erase­Idx
  43. Array.erase­Idx!
  44. Array.erase­Idx­If­In­Bounds
  45. Array.erase­P
  46. Array.erase­Reps
  47. Array.extract
  48. Array.filter
  49. Array.filter­M
  50. Array.filter­Map
  51. Array.filter­Map­M
  52. Array.filter­Rev­M
  53. Array.filter­Sep­Elems
  54. Array.filter­Sep­Elems­M
  55. Array.fin­Idx­Of?
  56. Array.fin­Range
  57. Array.find?
  58. Array.find­Fin­Idx?
  59. Array.find­Idx
  60. Array.find­Idx?
  61. Array.find­Idx­M?
  62. Array.find­M?
  63. Array.find­Rev?
  64. Array.find­Rev­M?
  65. Array.find­Some!
  66. Array.find­Some?
  67. Array.find­Some­M?
  68. Array.find­Some­Rev?
  69. Array.find­Some­Rev­M?
  70. Array.first­M
  71. Array.flat­Map
  72. Array.flat­Map­M
  73. Array.flatten
  74. Array.foldl
  75. Array.foldl­M
  76. Array.foldr
  77. Array.foldr­M
  78. Array.for­M
  79. Array.for­Rev­M
  80. Array.get­D
  81. Array.get­Even­Elems
  82. Array.get­Max?
  83. Array.group­By­Key
  84. Array.idx­Of
  85. Array.idx­Of?
  86. Array.insert­Idx
  87. Array.insert­Idx!
  88. Array.insert­Idx­If­In­Bounds
  89. Array.insertion­Sort
  90. Array.is­Empty
  91. Array.is­Eqv
  92. Array.is­Prefix­Of
  93. Array.leftpad
  94. Array.lex
  95. Array.map
  96. Array.map­Fin­Idx
  97. Array.map­Fin­Idx­M
  98. Array.map­Idx
  99. Array.map­Idx­M
  100. Array.map­M
  101. Array.map­M'
  102. Array.map­Mono
  103. Array.map­Mono­M
  104. Array.mk
    1. Constructor of Array
  105. Array.modify
  106. Array.modify­M
  107. Array.modify­Op
  108. Array.of­Fn
  109. Array.of­Subarray
  110. Array.partition
  111. Array.pmap
  112. Array.pop
  113. Array.pop­While
  114. Array.push
  115. Array.qsort
  116. Array.qsort­Ord
  117. Array.range
  118. Array.range'
  119. Array.replace
  120. Array.replicate
  121. Array.reverse
  122. Array.rightpad
  123. Array.set
  124. Array.set!
  125. Array.set­If­In­Bounds
  126. Array.shrink
  127. Array.singleton
  128. Array.size
  129. Array.sum
  130. Array.swap
  131. Array.swap­At
  132. Array.swap­At!
  133. Array.swap­If­In­Bounds
  134. Array.take
  135. Array.take­While
  136. Array.to­List
  137. Array.to­List­Append
  138. Array.to­List­Rev
  139. Array.to­Subarray
  140. Array.to­Vector
  141. Array.uget
  142. Array.unattach
  143. Array.unzip
  144. Array.uset
  145. Array.usize
  146. Array.zip
  147. Array.zip­Idx
  148. Array.zip­With
  149. Array.zip­With­All
  150. Atomic­T
    1. Std.Atomic­T
  151. abs
    1. BitVec.abs
  152. abs
    1. Float.abs
  153. abs
    1. Float32.abs
  154. abs
    1. ISize.abs
  155. abs
    1. Int16.abs
  156. abs
    1. Int32.abs
  157. abs
    1. Int64.abs
  158. abs
    1. Int8.abs
  159. absurd
  160. ac_nf
  161. ac_nf0
  162. ac_rfl
  163. accessed
    1. IO.FS.Metadata.accessed (structure field)
  164. acos
    1. Float.acos
  165. acos
    1. Float32.acos
  166. acosh
    1. Float.acosh
  167. acosh
    1. Float32.acosh
  168. adapt
    1. ExceptT.adapt
  169. adapt
    1. ReaderT.adapt
  170. adapt­Except
    1. EStateM.adapt­Except
  171. adc
    1. BitVec.adc
  172. adcb
    1. BitVec.adcb
  173. add
    1. Add.add (class method)
  174. add
    1. BitVec.add
  175. add
    1. Fin.add
  176. add
    1. Float.add
  177. add
    1. Float32.add
  178. add
    1. ISize.add
  179. add
    1. Int.add
  180. add
    1. Int16.add
  181. add
    1. Int32.add
  182. add
    1. Int64.add
  183. add
    1. Int8.add
  184. add
    1. Nat.add
  185. add
    1. UInt16.add
  186. add
    1. UInt32.add
  187. add
    1. UInt64.add
  188. add
    1. UInt8.add
  189. add
    1. USize.add
  190. add­App­Paren
    1. Repr.add­App­Paren
  191. add­Cases
    1. Fin.add­Cases
  192. add­Extension
    1. System.FilePath.add­Extension
  193. add­Heartbeats
    1. IO.add­Heartbeats
  194. add­Macro­Scope
    1. Lean.Macro.add­Macro­Scope
  195. add­Nat
    1. Fin.add­Nat
  196. add_assoc
    1. Lean.Grind.Semiring.add_zero (class method)
  197. add_comm
    1. Lean.Grind.Semiring.npow (class method)
  198. add_le_left_iff
    1. Lean.Grind.OrderedAdd.add_le_left_iff (class method)
  199. add_one_nsmul
    1. [anonymous] (class method)
  200. add_right_cancel
    1. Lean.Grind.Add­RightCancel.add_right_cancel (class method)
  201. add_zero
    1. Lean.Grind.Semiring.nsmul (class method)
  202. add_zsmul
    1. [anonymous] (class method)
  203. admit
  204. all
    1. Array.all
  205. all
    1. List.all
  206. all
    1. Nat.all
  207. all
    1. Option.all
  208. all
    1. Std.HashSet.all
  209. all
    1. Std.TreeMap.all
  210. all
    1. Std.TreeSet.all
  211. all
    1. String.all
  212. all
    1. Subarray.all
  213. all
    1. Substring.all
  214. all­Diff
    1. Array.all­Diff
  215. all­Eq
    1. Subsingleton.all­Eq (class method)
  216. all­I
    1. Prod.all­I
  217. all­M
    1. Array.all­M
  218. all­M
    1. List.all­M
  219. all­M
    1. Nat.all­M
  220. all­M
    1. Subarray.all­M
  221. all­Ones
    1. BitVec.all­Ones
  222. all­TR
    1. Nat.all­TR
  223. all_goals (0) (1)
  224. allow­Unsafe­Reducibility
  225. alter
    1. Std.DHashMap.alter
  226. alter
    1. Std.DTreeMap.alter
  227. alter
    1. Std.Ext­DHashMap.alter
  228. alter
    1. Std.Ext­HashMap.alter
  229. alter
    1. Std.HashMap.alter
  230. alter
    1. Std.TreeMap.alter
  231. and
    1. BitVec.and
  232. and
    1. Bool.and
  233. and
    1. List.and
  234. and­M
  235. and_intros
  236. any
    1. Array.any
  237. any
    1. List.any
  238. any
    1. Nat.any
  239. any
    1. Option.any
  240. any
    1. Std.HashSet.any
  241. any
    1. Std.TreeMap.any
  242. any
    1. Std.TreeSet.any
  243. any
    1. String.any
  244. any
    1. Subarray.any
  245. any
    1. Substring.any
  246. any­I
    1. Prod.any­I
  247. any­M
    1. Array.any­M
  248. any­M
    1. List.any­M
  249. any­M
    1. Nat.any­M
  250. any­M
    1. Subarray.any­M
  251. any­TR
    1. Nat.any­TR
  252. any_goals (0) (1)
  253. app­Dir
    1. IO.app­Dir
  254. app­Path
    1. IO.app­Path
  255. append
    1. Append.append (class method)
  256. append
    1. Array.append
  257. append
    1. BitVec.append
  258. append
    1. List.append
  259. append
    1. String.append
  260. append­List
    1. Array.append­List
  261. append­TR
    1. List.append­TR
  262. apply (0) (1)
  263. apply?
  264. apply_assumption
  265. apply_ext_theorem
  266. apply_mod_cast
  267. apply_rfl
  268. apply_rules
  269. arg [@]i
  270. args
  271. args
    1. [anonymous] (structure field)
  272. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  273. as­String
    1. List.as­String
  274. as­Task
    1. BaseIO.as­Task
  275. as­Task
    1. EIO.as­Task
  276. as­Task
    1. IO.as­Task
  277. as_aux_lemma
  278. asin
    1. Float.asin
  279. asin
    1. Float32.asin
  280. asinh
    1. Float.asinh
  281. asinh
    1. Float32.asinh
  282. assumption
  283. assumption
    1. inaccessible
  284. assumption_mod_cast
  285. at­End
    1. String.Iterator.at­End
  286. at­End
    1. String.at­End
  287. at­End
    1. Substring.at­End
  288. at­Idx!
    1. Std.TreeSet.at­Idx!
  289. at­Idx
    1. Std.TreeSet.at­Idx
  290. at­Idx?
    1. Std.TreeSet.at­Idx?
  291. at­Idx­D
    1. Std.TreeSet.at­Idx­D
  292. atan
    1. Float.atan
  293. atan
    1. Float32.atan
  294. atan2
    1. Float.atan2
  295. atan2
    1. Float32.atan2
  296. atanh
    1. Float.atanh
  297. atanh
    1. Float32.atanh
  298. atomically
    1. Std.Mutex.atomically
  299. atomically­Once
    1. Std.Mutex.atomically­Once
  300. attach
    1. Array.attach
  301. attach
    1. List.attach
  302. attach
    1. Option.attach
  303. attach­With
    1. Array.attach­With
  304. attach­With
    1. List.attach­With
  305. attach­With
    1. Option.attach­With
  306. auto­Implicit
  307. auto­Lift
  308. auto­Param
  309. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  310. auto­Unfold
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
  311. auto­Unfold
    1. Lean.Meta.Simp.Config.auto­Unfold (structure field)

B

  1. BEq
  2. BEq.mk
    1. Instance constructor of BEq
  3. Backend
    1. Lake.Backend
  4. Backtrackable
    1. EStateM.Backtrackable
  5. Base­IO
  6. BaseIO.as­Task
  7. BaseIO.bind­Task
  8. BaseIO.chain­Task
  9. BaseIO.map­Task
  10. BaseIO.map­Tasks
  11. BaseIO.to­EIO
  12. BaseIO.to­IO
  13. Bind
  14. Bind.bind­Left
  15. Bind.kleisli­Left
  16. Bind.kleisli­Right
  17. Bind.mk
    1. Instance constructor of Bind
  18. Bit­Vec
  19. BitVec.abs
  20. BitVec.adc
  21. BitVec.adcb
  22. BitVec.add
  23. BitVec.all­Ones
  24. BitVec.and
  25. BitVec.append
  26. BitVec.carry
  27. BitVec.cast
  28. BitVec.concat
  29. BitVec.cons
  30. BitVec.dec­Eq
  31. BitVec.div­Rec
  32. BitVec.div­Subtract­Shift
  33. BitVec.extract­Lsb
  34. BitVec.extract­Lsb'
  35. BitVec.fill
  36. BitVec.get­Lsb
  37. BitVec.get­Lsb?
  38. BitVec.get­Lsb­D
  39. BitVec.get­Msb
  40. BitVec.get­Msb?
  41. BitVec.get­Msb­D
  42. BitVec.hash
  43. BitVec.int­Max
  44. BitVec.int­Min
  45. BitVec.iunfoldr
  46. BitVec.iunfoldr_replace
  47. BitVec.msb
  48. BitVec.mul
  49. BitVec.mul­Rec
  50. BitVec.neg
  51. BitVec.nil
  52. BitVec.not
  53. BitVec.of­Bool
  54. BitVec.of­Bool­List­BE
  55. BitVec.of­Bool­List­LE
  56. BitVec.of­Fin
    1. Constructor of Bit­Vec
  57. BitVec.of­Int
  58. BitVec.of­Nat
  59. BitVec.of­Nat­LT
  60. BitVec.or
  61. BitVec.replicate
  62. BitVec.reverse
  63. BitVec.rotate­Left
  64. BitVec.rotate­Right
  65. BitVec.sadd­Overflow
  66. BitVec.sdiv
  67. BitVec.set­Width
  68. BitVec.set­Width'
  69. BitVec.shift­Concat
  70. BitVec.shift­Left
  71. BitVec.shift­Left­Rec
  72. BitVec.shift­Left­Zero­Extend
  73. BitVec.sign­Extend
  74. BitVec.sle
  75. BitVec.slt
  76. BitVec.smod
  77. BitVec.smt­SDiv
  78. BitVec.smt­UDiv
  79. BitVec.srem
  80. BitVec.sshift­Right
  81. BitVec.sshift­Right'
  82. BitVec.sshift­Right­Rec
  83. BitVec.ssub­Overflow
  84. BitVec.sub
  85. BitVec.to­Hex
  86. BitVec.to­Int
  87. BitVec.to­Nat
  88. BitVec.truncate
  89. BitVec.two­Pow
  90. BitVec.uadd­Overflow
  91. BitVec.udiv
  92. BitVec.ule
  93. BitVec.ult
  94. BitVec.umod
  95. BitVec.ushift­Right
  96. BitVec.ushift­Right­Rec
  97. BitVec.usub­Overflow
  98. BitVec.xor
  99. BitVec.zero
  100. BitVec.zero­Extend
  101. Bool
  102. Bool.and
  103. Bool.dcond
  104. Bool.dec­Eq
  105. Bool.false
    1. Constructor of Bool
  106. Bool.not
  107. Bool.or
  108. Bool.to­ISize
  109. Bool.to­Int
  110. Bool.to­Int16
  111. Bool.to­Int32
  112. Bool.to­Int64
  113. Bool.to­Int8
  114. Bool.to­Nat
  115. Bool.to­UInt16
  116. Bool.to­UInt32
  117. Bool.to­UInt64
  118. Bool.to­UInt8
  119. Bool.to­USize
  120. Bool.true
    1. Constructor of Bool
  121. Bool.xor
  122. Buffer
    1. IO.FS.Stream.Buffer
  123. Build­Type
    1. Lake.Build­Type
  124. back!
    1. Array.back!
  125. back
    1. Array.back
  126. back
    1. String.back
  127. back?
    1. Array.back?
  128. backward.synthInstance.canon­Instances
  129. bdiv
    1. Int.bdiv
  130. beq
    1. BEq.beq (class method)
  131. beq
    1. Float.beq
  132. beq
    1. Float32.beq
  133. beq
    1. List.beq
  134. beq
    1. Nat.beq
  135. beq
    1. Substring.beq
  136. beta
    1. Lean.Meta.DSimp.Config.beta (structure field)
  137. beta
    1. Lean.Meta.Simp.Config.beta (structure field)
  138. bin­Insert
    1. Array.bin­Insert
  139. bin­Insert­M
    1. Array.bin­Insert­M
  140. bin­Search
    1. Array.bin­Search
  141. bin­Search­Contains
    1. Array.bin­Search­Contains
  142. bind
    1. Bind.bind (class method)
  143. bind
    1. EStateM.bind
  144. bind
    1. Except.bind
  145. bind
    1. ExceptT.bind
  146. bind
    1. Option.bind
  147. bind
    1. OptionT.bind
  148. bind
    1. ReaderT.bind
  149. bind
    1. StateT.bind
  150. bind
    1. Task.bind
  151. bind
    1. Thunk.bind
  152. bind­Cont
    1. ExceptT.bind­Cont
  153. bind­Left
    1. Bind.bind­Left
  154. bind­M
    1. Option.bind­M
  155. bind­Task
    1. BaseIO.bind­Task
  156. bind­Task
    1. EIO.bind­Task
  157. bind­Task
    1. IO.bind­Task
  158. bind_assoc
    1. [anonymous] (class method)
  159. bind_map
    1. [anonymous] (class method)
  160. bind_pure_comp
    1. [anonymous] (class method)
  161. binder­Name­Hint
  162. bit­Vec­Of­Nat
    1. Lean.Meta.Simp.Config.bit­Vec­Of­Nat (structure field)
  163. bitwise
    1. Nat.bitwise
  164. ble
    1. Nat.ble
  165. blt
    1. Nat.blt
  166. bmod
    1. Int.bmod
  167. bootstrap.inductive­Check­Resulting­Universe
  168. bracket
    1. Std.Format.bracket
  169. bracket­Fill
    1. Std.Format.bracket­Fill
  170. bsize
    1. Substring.bsize
  171. buckets
    1. Std.DHashMap.Raw.buckets (structure field)
  172. build (Lake command)
  173. bv_check
  174. bv_decide
  175. bv_decide?
  176. bv_normalize
  177. bv_omega
  178. by­Cases
    1. Decidable.by­Cases
  179. by_cases
  180. by_cases'
    1. Or.by_cases'
  181. by_cases
    1. Or.by_cases
  182. byte­Idx
    1. String.Pos.byte­Idx (structure field)
  183. byte­Size
    1. IO.FS.Metadata.byte­Size (structure field)

C

  1. CC (environment variable)
  2. CCPO
    1. Lean.Order.CCPO
  3. Channel
    1. Std.Channel
  4. Char
  5. Char.is­Alpha
  6. Char.is­Alphanum
  7. Char.is­Digit
  8. Char.is­Lower
  9. Char.is­Upper
  10. Char.is­Valid­Char­Nat
  11. Char.is­Whitespace
  12. Char.le
  13. Char.lt
  14. Char.mk
    1. Constructor of Char
  15. Char.of­Nat
  16. Char.of­UInt8
  17. Char.quote
  18. Char.to­Lower
  19. Char.to­Nat
  20. Char.to­String
  21. Char.to­UInt8
  22. Char.to­Upper
  23. Char.utf16Size
  24. Char.utf8Size
  25. Char­Lit
    1. Lean.Syntax.Char­Lit
  26. Child
    1. IO.Process.Child
  27. Closeable­Channel
    1. Std.Closeable­Channel
  28. Coe
  29. Coe.mk
    1. Instance constructor of Coe
  30. Coe­Dep
  31. CoeDep.mk
    1. Instance constructor of Coe­Dep
  32. Coe­Fun
  33. CoeFun.mk
    1. Instance constructor of Coe­Fun
  34. Coe­HTC
  35. CoeHTC.mk
    1. Instance constructor of Coe­HTC
  36. Coe­HTCT
  37. CoeHTCT.mk
    1. Instance constructor of Coe­HTCT
  38. Coe­Head
  39. CoeHead.mk
    1. Instance constructor of Coe­Head
  40. Coe­OTC
  41. CoeOTC.mk
    1. Instance constructor of Coe­OTC
  42. Coe­Out
  43. CoeOut.mk
    1. Instance constructor of Coe­Out
  44. Coe­Sort
  45. CoeSort.mk
    1. Instance constructor of Coe­Sort
  46. Coe­T
  47. CoeT.mk
    1. Instance constructor of Coe­T
  48. Coe­TC
  49. CoeTC.mk
    1. Instance constructor of Coe­TC
  50. Coe­Tail
  51. CoeTail.mk
    1. Instance constructor of Coe­Tail
  52. 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. calc
  60. call-by-need
  61. cancel
    1. IO.cancel
  62. canon­Instances
    1. backward.synthInstance.canon­Instances
  63. capitalize
    1. String.capitalize
  64. carry
    1. BitVec.carry
  65. case
  66. case ... => ...
  67. case'
  68. case' ... => ...
  69. case­Strong­Rec­On
    1. Nat.case­Strong­Rec­On
  70. cases
  71. cases
    1. Fin.cases
  72. cases­Aux­On
    1. Nat.cases­Aux­On
  73. cast
  74. cast
    1. BitVec.cast
  75. cast
    1. Fin.cast
  76. cast
    1. Int.cast
  77. cast
    1. Nat.cast
  78. cast­Add
    1. Fin.cast­Add
  79. cast­LE
    1. Fin.cast­LE
  80. cast­LT
    1. Fin.cast­LT
  81. cast­Succ
    1. Fin.cast­Succ
  82. cast_heq
  83. catch­Exceptions
    1. EIO.catch­Exceptions
  84. catch­Runtime
    1. Lean.Meta.Simp.Config.catch­Runtime (structure field)
  85. cbrt
    1. Float.cbrt
  86. cbrt
    1. Float32.cbrt
  87. ceil
    1. Float.ceil
  88. ceil
    1. Float32.ceil
  89. chain
    1. of coercions
  90. chain­Task
    1. BaseIO.chain­Task
  91. chain­Task
    1. EIO.chain­Task
  92. chain­Task
    1. IO.chain­Task
  93. change (0) (1)
  94. change ... with ...
  95. char­Lit­Kind
    1. Lean.char­Lit­Kind
  96. check-build (Lake command)
  97. check-lint (Lake command)
  98. check-test (Lake command)
  99. check­Canceled
    1. IO.check­Canceled
  100. choice
    1. Option.choice
  101. choice­Kind
    1. Lean.choice­Kind
  102. choose
    1. Exists.choose
  103. classical
  104. clean (Lake command)
  105. clear
  106. cmd
    1. [anonymous] (structure field)
  107. coe
    1. Coe.coe (class method)
  108. coe
    1. CoeDep.coe (class method)
  109. coe
    1. CoeFun.coe (class method)
  110. coe
    1. CoeHTC.coe (class method)
  111. coe
    1. CoeHTCT.coe (class method)
  112. coe
    1. CoeHead.coe (class method)
  113. coe
    1. CoeOTC.coe (class method)
  114. coe
    1. CoeOut.coe (class method)
  115. coe
    1. CoeSort.coe (class method)
  116. coe
    1. CoeT.coe (class method)
  117. coe
    1. CoeTC.coe (class method)
  118. coe
    1. CoeTail.coe (class method)
  119. col­Eq
  120. col­Ge
  121. col­Gt
  122. comment
    1. block
  123. comment
    1. line
  124. common­Prefix
    1. Substring.common­Prefix
  125. common­Suffix
    1. Substring.common­Suffix
  126. comp
    1. Function.comp
  127. comp_map
    1. LawfulFunctor.comp_map (class method)
  128. compare
    1. Ord.compare (class method)
  129. compare­Lex
  130. compare­Of­Less­And­BEq
  131. compare­Of­Less­And­Eq
  132. compare­On
  133. complement
    1. ISize.complement
  134. complement
    1. Int16.complement
  135. complement
    1. Int32.complement
  136. complement
    1. Int64.complement
  137. complement
    1. Int8.complement
  138. complement
    1. UInt16.complement
  139. complement
    1. UInt32.complement
  140. complement
    1. UInt64.complement
  141. complement
    1. UInt8.complement
  142. complement
    1. USize.complement
  143. completions (Elan command)
  144. components
    1. System.FilePath.components
  145. concat
    1. BitVec.concat
  146. concat
    1. List.concat
  147. cond
  148. configuration
    1. of tactics
  149. congr (0) (1) (2)
  150. congr­Arg
  151. congr­Consts
    1. Lean.Meta.Simp.Config.congr­Consts (structure field)
  152. congr­Fun
  153. cons
    1. BitVec.cons
  154. const
    1. Function.const
  155. constructor (0) (1)
  156. contains
    1. Array.contains
  157. contains
    1. List.contains
  158. contains
    1. Std.DHashMap.contains
  159. contains
    1. Std.DTreeMap.contains
  160. contains
    1. Std.Ext­DHashMap.contains
  161. contains
    1. Std.Ext­HashMap.contains
  162. contains
    1. Std.Ext­HashSet.contains
  163. contains
    1. Std.HashMap.contains
  164. contains
    1. Std.HashSet.contains
  165. contains
    1. Std.TreeMap.contains
  166. contains
    1. Std.TreeSet.contains
  167. contains
    1. String.contains
  168. contains
    1. Substring.contains
  169. contains­Then­Insert
    1. Std.DHashMap.contains­Then­Insert
  170. contains­Then­Insert
    1. Std.DTreeMap.contains­Then­Insert
  171. contains­Then­Insert
    1. Std.Ext­DHashMap.contains­Then­Insert
  172. contains­Then­Insert
    1. Std.Ext­HashMap.contains­Then­Insert
  173. contains­Then­Insert
    1. Std.Ext­HashSet.contains­Then­Insert
  174. contains­Then­Insert
    1. Std.HashMap.contains­Then­Insert
  175. contains­Then­Insert
    1. Std.HashSet.contains­Then­Insert
  176. contains­Then­Insert
    1. Std.TreeMap.contains­Then­Insert
  177. contains­Then­Insert
    1. Std.TreeSet.contains­Then­Insert
  178. contains­Then­Insert­If­New
    1. Std.DHashMap.contains­Then­Insert­If­New
  179. contains­Then­Insert­If­New
    1. Std.DTreeMap.contains­Then­Insert­If­New
  180. contains­Then­Insert­If­New
    1. Std.Ext­DHashMap.contains­Then­Insert­If­New
  181. contains­Then­Insert­If­New
    1. Std.Ext­HashMap.contains­Then­Insert­If­New
  182. contains­Then­Insert­If­New
    1. Std.HashMap.contains­Then­Insert­If­New
  183. contains­Then­Insert­If­New
    1. Std.TreeMap.contains­Then­Insert­If­New
  184. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  185. contradiction
  186. control
  187. control­At
  188. conv
  189. conv => ...
  190. conv' (0) (1)
  191. cos
    1. Float.cos
  192. cos
    1. Float32.cos
  193. cosh
    1. Float.cosh
  194. cosh
    1. Float32.cosh
  195. count
    1. Array.count
  196. count
    1. List.count
  197. count­P
    1. Array.count­P
  198. count­P
    1. List.count­P
  199. create­Dir
    1. IO.FS.create­Dir
  200. create­Dir­All
    1. IO.FS.create­Dir­All
  201. create­Temp­Dir
    1. IO.FS.create­Temp­Dir
  202. create­Temp­File
    1. IO.FS.create­Temp­File
  203. crlf­To­Lf
    1. String.crlf­To­Lf
  204. csup
    1. [anonymous] (class method)
  205. csup_spec
    1. [anonymous] (class method)
  206. cumulativity
  207. curr
    1. String.Iterator.curr
  208. curr­Column
    1. Std.Format.Monad­PrettyFormat.curr­Column (class method)
  209. current­Dir
    1. IO.current­Dir
  210. curry
    1. Function.curry
  211. custom­Eliminators
    1. tactic.custom­Eliminators
  212. 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. IO.FS.Stream.Buffer.data (structure field)
  19. data
    1. String.data (structure field)
  20. dbg­Trace­If­Shared
  21. dbg_trace
  22. dcond
    1. Bool.dcond
  23. dec­Eq
    1. BitVec.dec­Eq
  24. dec­Eq
    1. Bool.dec­Eq
  25. dec­Eq
    1. ISize.dec­Eq
  26. dec­Eq
    1. Int.dec­Eq
  27. dec­Eq
    1. Int16.dec­Eq
  28. dec­Eq
    1. Int32.dec­Eq
  29. dec­Eq
    1. Int64.dec­Eq
  30. dec­Eq
    1. Int8.dec­Eq
  31. dec­Eq
    1. Nat.dec­Eq
  32. dec­Eq
    1. String.dec­Eq
  33. dec­Eq
    1. UInt16.dec­Eq
  34. dec­Eq
    1. UInt32.dec­Eq
  35. dec­Eq
    1. UInt64.dec­Eq
  36. dec­Eq
    1. UInt8.dec­Eq
  37. dec­Eq
    1. USize.dec­Eq
  38. dec­Le
    1. Float.dec­Le
  39. dec­Le
    1. Float32.dec­Le
  40. dec­Le
    1. ISize.dec­Le
  41. dec­Le
    1. Int16.dec­Le
  42. dec­Le
    1. Int32.dec­Le
  43. dec­Le
    1. Int64.dec­Le
  44. dec­Le
    1. Int8.dec­Le
  45. dec­Le
    1. Nat.dec­Le
  46. dec­Le
    1. UInt16.dec­Le
  47. dec­Le
    1. UInt32.dec­Le
  48. dec­Le
    1. UInt64.dec­Le
  49. dec­Le
    1. UInt8.dec­Le
  50. dec­Le
    1. USize.dec­Le
  51. dec­Lt
    1. Float.dec­Lt
  52. dec­Lt
    1. Float32.dec­Lt
  53. dec­Lt
    1. ISize.dec­Lt
  54. dec­Lt
    1. Int16.dec­Lt
  55. dec­Lt
    1. Int32.dec­Lt
  56. dec­Lt
    1. Int64.dec­Lt
  57. dec­Lt
    1. Int8.dec­Lt
  58. dec­Lt
    1. Nat.dec­Lt
  59. dec­Lt
    1. UInt16.dec­Lt
  60. dec­Lt
    1. UInt32.dec­Lt
  61. dec­Lt
    1. UInt64.dec­Lt
  62. dec­Lt
    1. UInt8.dec­Lt
  63. dec­Lt
    1. USize.dec­Lt
  64. decapitalize
    1. String.decapitalize
  65. decidable
  66. decidable­Eq­None
    1. Option.decidable­Eq­None
  67. decide
  68. decide
    1. Decidable.decide
  69. decide
    1. Lean.Meta.DSimp.Config.decide (structure field)
  70. decide
    1. Lean.Meta.Simp.Config.decide (structure field)
  71. decreasing_tactic
  72. decreasing_trivial
  73. decreasing_with
  74. dedicated
    1. Task.Priority.dedicated
  75. deep­Terms
    1. pp.deep­Terms
  76. def­Indent
    1. Std.Format.def­Indent
  77. def­Width
    1. Std.Format.def­Width
  78. default (Elan command)
  79. default
    1. Inhabited.default (class method)
  80. default
    1. Task.Priority.default
  81. default­Facets
    1. [anonymous] (structure field)
  82. delta (0) (1)
  83. diff
    1. guard_msgs.diff
  84. digit­Char
    1. Nat.digit­Char
  85. discard
    1. Functor.discard
  86. discharge
    1. trace.Meta.Tactic.simp.discharge
  87. div
    1. Div.div (class method)
  88. div
    1. Fin.div
  89. div
    1. Float.div
  90. div
    1. Float32.div
  91. div
    1. ISize.div
  92. div
    1. Int16.div
  93. div
    1. Int32.div
  94. div
    1. Int64.div
  95. div
    1. Int8.div
  96. div
    1. Nat.div
  97. div
    1. UInt16.div
  98. div
    1. UInt32.div
  99. div
    1. UInt64.div
  100. div
    1. UInt8.div
  101. div
    1. USize.div
  102. div2Induction
    1. Nat.div2Induction
  103. div­Rec
    1. BitVec.div­Rec
  104. div­Subtract­Shift
    1. BitVec.div­Subtract­Shift
  105. div_eq_mul_inv
    1. [anonymous] (class method)
  106. done (0) (1)
  107. down
    1. PLift.down (structure field)
  108. down
    1. ULift.down (structure field)
  109. drop
    1. Array.drop
  110. drop
    1. List.drop
  111. drop
    1. String.drop
  112. drop
    1. Subarray.drop
  113. drop
    1. Substring.drop
  114. drop­Last
    1. List.drop­Last
  115. drop­Last­TR
    1. List.drop­Last­TR
  116. drop­Prefix?
    1. String.drop­Prefix?
  117. drop­Prefix?
    1. Substring.drop­Prefix?
  118. drop­Right
    1. String.drop­Right
  119. drop­Right
    1. Substring.drop­Right
  120. drop­Right­While
    1. String.drop­Right­While
  121. drop­Right­While
    1. Substring.drop­Right­While
  122. drop­Suffix?
    1. String.drop­Suffix?
  123. drop­Suffix?
    1. Substring.drop­Suffix?
  124. drop­While
    1. List.drop­While
  125. drop­While
    1. String.drop­While
  126. drop­While
    1. Substring.drop­While
  127. dsimp (0) (1)
  128. dsimp!
  129. dsimp
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  130. dsimp?
  131. dsimp?!
  132. 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. Std.DTreeMap.empty
  109. empty
    1. Std.TreeMap.empty
  110. empty
    1. Std.TreeSet.empty
  111. empty
    1. Subarray.empty
  112. empty­With­Capacity
    1. Array.empty­With­Capacity
  113. empty­With­Capacity
    1. Std.DHashMap.empty­With­Capacity
  114. empty­With­Capacity
    1. Std.Ext­DHashMap.empty­With­Capacity
  115. empty­With­Capacity
    1. Std.Ext­HashMap.empty­With­Capacity
  116. empty­With­Capacity
    1. Std.Ext­HashSet.empty­With­Capacity
  117. empty­With­Capacity
    1. Std.HashMap.empty­With­Capacity
  118. empty­With­Capacity
    1. Std.HashSet.empty­With­Capacity
  119. end­Pos
    1. String.end­Pos
  120. end­Tags
    1. Std.Format.Monad­PrettyFormat.end­Tags (class method)
  121. ends­With
    1. String.ends­With
  122. enter
  123. entry­At­Idx!
    1. Std.TreeMap.entry­At­Idx!
  124. entry­At­Idx
    1. Std.TreeMap.entry­At­Idx
  125. entry­At­Idx?
    1. Std.TreeMap.entry­At­Idx?
  126. entry­At­Idx­D
    1. Std.TreeMap.entry­At­Idx­D
  127. env (Lake command)
  128. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  129. environment variables
  130. eprint
    1. IO.eprint
  131. eprintln
    1. IO.eprintln
  132. eq­Rec_heq
  133. eq_of_beq
    1. [anonymous] (class method)
  134. eq_of_heq
  135. eq_refl
  136. erase
    1. Array.erase
  137. erase
    1. List.erase
  138. erase
    1. Std.DHashMap.erase
  139. erase
    1. Std.DTreeMap.erase
  140. erase
    1. Std.Ext­DHashMap.erase
  141. erase
    1. Std.Ext­HashMap.erase
  142. erase
    1. Std.Ext­HashSet.erase
  143. erase
    1. Std.HashMap.erase
  144. erase
    1. Std.HashSet.erase
  145. erase
    1. Std.TreeMap.erase
  146. erase
    1. Std.TreeSet.erase
  147. erase­Dups
    1. List.erase­Dups
  148. erase­Idx!
    1. Array.erase­Idx!
  149. erase­Idx
    1. Array.erase­Idx
  150. erase­Idx
    1. List.erase­Idx
  151. erase­Idx­If­In­Bounds
    1. Array.erase­Idx­If­In­Bounds
  152. erase­Idx­TR
    1. List.erase­Idx­TR
  153. erase­Many
    1. Std.TreeMap.erase­Many
  154. erase­Many
    1. Std.TreeSet.erase­Many
  155. erase­P
    1. Array.erase­P
  156. erase­P
    1. List.erase­P
  157. erase­PTR
    1. List.erase­PTR
  158. erase­Reps
    1. Array.erase­Reps
  159. erase­Reps
    1. List.erase­Reps
  160. erase­TR
    1. List.erase­TR
  161. erw (0) (1)
  162. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
  163. eta
    1. Lean.Meta.Simp.Config.eta (structure field)
  164. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
  165. eta­Struct
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  166. eval.derive.repr
  167. eval.pp
  168. eval.type
  169. exact
  170. exact
    1. Quotient.exact
  171. exact?
  172. exact_mod_cast
  173. exe (Lake command)
  174. exe­Extension
    1. System.FilePath.exe­Extension
  175. exe­Name
    1. [anonymous] (structure field)
  176. execution
    1. IO.AccessRight.execution (structure field)
  177. exfalso
  178. exists
  179. exit
    1. IO.Process.exit
  180. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  181. exp
    1. Float.exp
  182. exp
    1. Float32.exp
  183. exp2
    1. Float.exp2
  184. exp2
    1. Float32.exp2
  185. expand­Macro?
    1. Lean.Macro.expand­Macro?
  186. expose_names
  187. ext (0) (1)
  188. ext1
  189. ext­Separator
    1. System.FilePath.ext­Separator
  190. extension
    1. System.FilePath.extension
  191. extensionality
    1. of propositions
  192. extra­Dep­Targets
    1. [anonymous] (structure field) (0) (1)
  193. extract
    1. Array.extract
  194. extract
    1. List.extract
  195. extract
    1. String.Iterator.extract
  196. extract
    1. String.extract
  197. extract
    1. Substring.extract
  198. extract­Lsb'
    1. BitVec.extract­Lsb'
  199. 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. Function.comp
  181. Function.const
  182. Function.curry
  183. Function.uncurry
  184. Functor
  185. Functor.discard
  186. Functor.map­Rev
  187. Functor.mk
    1. Instance constructor of Functor
  188. fail
  189. fail
    1. OptionT.fail
  190. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
  191. fail­If­Unchanged
    1. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  192. fail_if_success (0) (1)
  193. failure
    1. ReaderT.failure
  194. failure
    1. StateT.failure
  195. failure
    1. [anonymous] (class method)
  196. false_or_by_contra
  197. fdiv
    1. Int.fdiv
  198. field­Idx­Kind
    1. Lean.field­Idx­Kind
  199. field­Notation
    1. pp.field­Notation
  200. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
  201. file­Name
    1. System.FilePath.file­Name
  202. file­Stem
    1. System.FilePath.file­Stem
  203. fill
    1. BitVec.fill
  204. fill
    1. Std.Format.fill
  205. filter
    1. Array.filter
  206. filter
    1. List.filter
  207. filter
    1. Option.filter
  208. filter
    1. Std.DHashMap.filter
  209. filter
    1. Std.DTreeMap.filter
  210. filter
    1. Std.Ext­DHashMap.filter
  211. filter
    1. Std.Ext­HashMap.filter
  212. filter
    1. Std.Ext­HashSet.filter
  213. filter
    1. Std.HashMap.filter
  214. filter
    1. Std.HashSet.filter
  215. filter
    1. Std.TreeMap.filter
  216. filter
    1. Std.TreeSet.filter
  217. filter­M
    1. Array.filter­M
  218. filter­M
    1. List.filter­M
  219. filter­Map
    1. Array.filter­Map
  220. filter­Map
    1. List.filter­Map
  221. filter­Map
    1. Std.DHashMap.filter­Map
  222. filter­Map
    1. Std.DTreeMap.filter­Map
  223. filter­Map
    1. Std.Ext­DHashMap.filter­Map
  224. filter­Map
    1. Std.Ext­HashMap.filter­Map
  225. filter­Map
    1. Std.HashMap.filter­Map
  226. filter­Map
    1. Std.TreeMap.filter­Map
  227. filter­Map­M
    1. Array.filter­Map­M
  228. filter­Map­M
    1. List.filter­Map­M
  229. filter­Map­TR
    1. List.filter­Map­TR
  230. filter­Rev­M
    1. Array.filter­Rev­M
  231. filter­Rev­M
    1. List.filter­Rev­M
  232. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  233. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  234. filter­TR
    1. List.filter­TR
  235. fin­Idx­Of?
    1. Array.fin­Idx­Of?
  236. fin­Idx­Of?
    1. List.fin­Idx­Of?
  237. fin­Range
    1. Array.fin­Range
  238. fin­Range
    1. List.fin­Range
  239. find
    1. String.find
  240. find?
    1. Array.find?
  241. find?
    1. List.find?
  242. find­Extern­Lib?
    1. Lake.find­Extern­Lib?
  243. find­Fin­Idx?
    1. Array.find­Fin­Idx?
  244. find­Fin­Idx?
    1. List.find­Fin­Idx?
  245. find­Idx
    1. Array.find­Idx
  246. find­Idx
    1. List.find­Idx
  247. find­Idx?
    1. Array.find­Idx?
  248. find­Idx?
    1. List.find­Idx?
  249. find­Idx­M?
    1. Array.find­Idx­M?
  250. find­Lean­Exe?
    1. Lake.find­Lean­Exe?
  251. find­Lean­Lib?
    1. Lake.find­Lean­Lib?
  252. find­Line­Start
    1. String.find­Line­Start
  253. find­M?
    1. Array.find­M?
  254. find­M?
    1. List.find­M?
  255. find­Module?
    1. Lake.find­Module?
  256. find­Package?
    1. Lake.find­Package?
  257. find­Rev?
    1. Array.find­Rev?
  258. find­Rev?
    1. Subarray.find­Rev?
  259. find­Rev­M?
    1. Array.find­Rev­M?
  260. find­Rev­M?
    1. Subarray.find­Rev­M?
  261. find­Some!
    1. Array.find­Some!
  262. find­Some?
    1. Array.find­Some?
  263. find­Some?
    1. List.find­Some?
  264. find­Some­M?
    1. Array.find­Some­M?
  265. find­Some­M?
    1. List.find­Some­M?
  266. find­Some­Rev?
    1. Array.find­Some­Rev?
  267. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
  268. find­Some­Rev­M?
    1. Subarray.find­Some­Rev­M?
  269. first (0) (1)
  270. first­Diff­Pos
    1. String.first­Diff­Pos
  271. first­M
    1. Array.first­M
  272. first­M
    1. List.first­M
  273. fix
    1. Lean.Order.fix
  274. fix
    1. WellFounded.fix
  275. fix_eq
    1. Lean.Order.fix_eq
  276. flags
    1. IO.AccessRight.flags
  277. flags
    1. IO.FileRight.flags
  278. flat­Map
    1. Array.flat­Map
  279. flat­Map
    1. List.flat­Map
  280. flat­Map­M
    1. Array.flat­Map­M
  281. flat­Map­M
    1. List.flat­Map­M
  282. flat­Map­TR
    1. List.flat­Map­TR
  283. flatten
    1. Array.flatten
  284. flatten
    1. List.flatten
  285. flatten­TR
    1. List.flatten­TR
  286. floor
    1. Float.floor
  287. floor
    1. Float32.floor
  288. flush
    1. IO.FS.Handle.flush
  289. flush
    1. IO.FS.Stream.flush (structure field)
  290. fmod
    1. Int.fmod
  291. fn
    1. Thunk.fn (structure field)
  292. focus (0) (1)
  293. fold
    1. Nat.fold
  294. fold
    1. Std.DHashMap.fold
  295. fold
    1. Std.HashMap.fold
  296. fold
    1. Std.HashSet.fold
  297. fold­I
    1. Prod.fold­I
  298. fold­M
    1. Nat.fold­M
  299. fold­M
    1. Std.DHashMap.fold­M
  300. fold­M
    1. Std.HashMap.fold­M
  301. fold­M
    1. Std.HashSet.fold­M
  302. fold­Rev
    1. Nat.fold­Rev
  303. fold­Rev­M
    1. Nat.fold­Rev­M
  304. fold­TR
    1. Nat.fold­TR
  305. foldl
    1. Array.foldl
  306. foldl
    1. Fin.foldl
  307. foldl
    1. List.foldl
  308. foldl
    1. Std.DTreeMap.foldl
  309. foldl
    1. Std.TreeMap.foldl
  310. foldl
    1. Std.TreeSet.foldl
  311. foldl
    1. String.foldl
  312. foldl
    1. Subarray.foldl
  313. foldl
    1. Substring.foldl
  314. foldl­M
    1. Array.foldl­M
  315. foldl­M
    1. Fin.foldl­M
  316. foldl­M
    1. List.foldl­M
  317. foldl­M
    1. Std.DTreeMap.foldl­M
  318. foldl­M
    1. Std.TreeMap.foldl­M
  319. foldl­M
    1. Std.TreeSet.foldl­M
  320. foldl­M
    1. Subarray.foldl­M
  321. foldl­Rec­On
    1. List.foldl­Rec­On
  322. foldr
    1. Array.foldr
  323. foldr
    1. Fin.foldr
  324. foldr
    1. List.foldr
  325. foldr
    1. Std.TreeMap.foldr
  326. foldr
    1. Std.TreeSet.foldr
  327. foldr
    1. String.foldr
  328. foldr
    1. Subarray.foldr
  329. foldr
    1. Substring.foldr
  330. foldr­M
    1. Array.foldr­M
  331. foldr­M
    1. Fin.foldr­M
  332. foldr­M
    1. List.foldr­M
  333. foldr­M
    1. Std.TreeMap.foldr­M
  334. foldr­M
    1. Std.TreeSet.foldr­M
  335. foldr­M
    1. Subarray.foldr­M
  336. foldr­Rec­On
    1. List.foldr­Rec­On
  337. foldr­TR
    1. List.foldr­TR
  338. for­A
    1. List.for­A
  339. for­Async
    1. Std.Channel.for­Async
  340. for­In'
    1. ForIn'.for­In' (class method)
  341. for­In
    1. ForIn.for­In (class method)
  342. for­In
    1. ForM.for­In
  343. for­In
    1. Std.DHashMap.for­In
  344. for­In
    1. Std.DTreeMap.for­In
  345. for­In
    1. Std.HashMap.for­In
  346. for­In
    1. Std.HashSet.for­In
  347. for­In
    1. Std.TreeMap.for­In
  348. for­In
    1. Std.TreeSet.for­In
  349. for­In
    1. Subarray.for­In
  350. for­M
    1. Array.for­M
  351. for­M
    1. ForM.for­M (class method)
  352. for­M
    1. List.for­M
  353. for­M
    1. Nat.for­M
  354. for­M
    1. Option.for­M
  355. for­M
    1. Std.DHashMap.for­M
  356. for­M
    1. Std.DTreeMap.for­M
  357. for­M
    1. Std.HashMap.for­M
  358. for­M
    1. Std.HashSet.for­M
  359. for­M
    1. Std.TreeMap.for­M
  360. for­M
    1. Std.TreeSet.for­M
  361. for­M
    1. Subarray.for­M
  362. for­Rev­M
    1. Array.for­Rev­M
  363. for­Rev­M
    1. Nat.for­Rev­M
  364. for­Rev­M
    1. Subarray.for­Rev­M
  365. format
    1. Option.format
  366. format
    1. Std.ToFormat.format (class method)
  367. forward
    1. String.Iterator.forward
  368. fr­Exp
    1. Float.fr­Exp
  369. fr­Exp
    1. Float32.fr­Exp
  370. from­State­M
    1. EStateM.from­State­M
  371. from­UTF8!
    1. String.from­UTF8!
  372. from­UTF8
    1. String.from­UTF8
  373. from­UTF8?
    1. String.from­UTF8?
  374. front
    1. String.front
  375. front
    1. Substring.front
  376. fst
    1. MProd.fst (structure field)
  377. fst
    1. PProd.fst (structure field)
  378. fst
    1. PSigma.fst (structure field)
  379. fst
    1. Prod.fst (structure field)
  380. fst
    1. Sigma.fst (structure field)
  381. fun
  382. fun_cases
  383. fun_induction
  384. funext (0) (1)

G

  1. Get­Elem
  2. GetElem.mk
    1. Instance constructor of Get­Elem
  3. Get­Elem?
  4. GetElem?.mk
    1. Instance constructor of Get­Elem?
  5. Glob
    1. Lake.Glob
  6. gcd
    1. Int.gcd
  7. gcd
    1. Nat.gcd
  8. generalize
  9. get!
    1. Option.get!
  10. get!
    1. Std.DHashMap.get!
  11. get!
    1. Std.DTreeMap.get!
  12. get!
    1. Std.Ext­DHashMap.get!
  13. get!
    1. Std.Ext­HashMap.get!
  14. get!
    1. Std.Ext­HashSet.get!
  15. get!
    1. Std.HashMap.get!
  16. get!
    1. Std.HashSet.get!
  17. get!
    1. Std.TreeMap.get!
  18. get!
    1. Std.TreeSet.get!
  19. get!
    1. String.get!
  20. get!
    1. Subarray.get!
  21. get'
    1. String.get'
  22. get
    1. EStateM.get
  23. get
    1. List.get
  24. get
    1. MonadState.get
  25. get
    1. MonadState.get (class method)
  26. get
    1. Monad­StateOf.get (class method)
  27. get
    1. Option.get
  28. get
    1. ST.Ref.get
  29. get
    1. State­RefT'.get
  30. get
    1. StateT.get
  31. get
    1. Std.DHashMap.get
  32. get
    1. Std.DTreeMap.get
  33. get
    1. Std.Ext­DHashMap.get
  34. get
    1. Std.Ext­HashMap.get
  35. get
    1. Std.Ext­HashSet.get
  36. get
    1. Std.HashMap.get
  37. get
    1. Std.HashSet.get
  38. get
    1. Std.TreeMap.get
  39. get
    1. Std.TreeSet.get
  40. get
    1. String.get
  41. get
    1. Subarray.get
  42. get
    1. Substring.get
  43. get
    1. Task.get
  44. get
    1. Thunk.get
  45. get?
    1. Std.DHashMap.get?
  46. get?
    1. Std.DTreeMap.get?
  47. get?
    1. Std.Ext­DHashMap.get?
  48. get?
    1. Std.Ext­HashMap.get?
  49. get?
    1. Std.Ext­HashSet.get?
  50. get?
    1. Std.HashMap.get?
  51. get?
    1. Std.HashSet.get?
  52. get?
    1. Std.TreeMap.get?
  53. get?
    1. Std.TreeSet.get?
  54. get?
    1. String.get?
  55. get­Augmented­Env
    1. Lake.get­Augmented­Env
  56. get­Augmented­Lean­Path
    1. Lake.get­Augmented­Lean­Path
  57. get­Augmented­Lean­Src­Path
    1. Lake.get­Augmented­Lean­Src­Path
  58. get­Augmented­Shared­Lib­Path
    1. Lake.get­Augmented­Shared­Lib­Path
  59. get­Char
    1. Lean.TSyntax.get­Char
  60. get­Curr­Namespace
    1. Lean.Macro.get­Curr­Namespace
  61. get­Current­Dir
    1. IO.Process.get­Current­Dir
  62. get­D
    1. Array.get­D
  63. get­D
    1. List.get­D
  64. get­D
    1. Option.get­D
  65. get­D
    1. Std.DHashMap.get­D
  66. get­D
    1. Std.DTreeMap.get­D
  67. get­D
    1. Std.Ext­DHashMap.get­D
  68. get­D
    1. Std.Ext­HashMap.get­D
  69. get­D
    1. Std.Ext­HashSet.get­D
  70. get­D
    1. Std.HashMap.get­D
  71. get­D
    1. Std.HashSet.get­D
  72. get­D
    1. Std.TreeMap.get­D
  73. get­D
    1. Std.TreeSet.get­D
  74. get­D
    1. Subarray.get­D
  75. get­DM
    1. Option.get­DM
  76. get­Elan?
    1. Lake.get­Elan?
  77. get­Elan­Home?
    1. Lake.get­Elan­Home?
  78. get­Elan­Install?
    1. Lake.get­Elan­Install?
  79. get­Elan­Toolchain
    1. Lake.get­Elan­Toolchain
  80. get­Elem!
    1. GetElem?.get­Elem? (class method)
  81. get­Elem!_def
    1. Lawful­GetElem.get­Elem!_def (class method)
  82. get­Elem
    1. GetElem.get­Elem (class method)
  83. get­Elem?
    1. [anonymous] (class method)
  84. get­Elem?_def
    1. Lawful­GetElem.get­Elem?_def (class method)
  85. get­Entry­GE!
    1. Std.TreeMap.get­Entry­GE!
  86. get­Entry­GE
    1. Std.TreeMap.get­Entry­GE
  87. get­Entry­GE?
    1. Std.TreeMap.get­Entry­GE?
  88. get­Entry­GED
    1. Std.TreeMap.get­Entry­GED
  89. get­Entry­GT!
    1. Std.TreeMap.get­Entry­GT!
  90. get­Entry­GT
    1. Std.TreeMap.get­Entry­GT
  91. get­Entry­GT?
    1. Std.TreeMap.get­Entry­GT?
  92. get­Entry­GTD
    1. Std.TreeMap.get­Entry­GTD
  93. get­Entry­LE!
    1. Std.TreeMap.get­Entry­LE!
  94. get­Entry­LE
    1. Std.TreeMap.get­Entry­LE
  95. get­Entry­LE?
    1. Std.TreeMap.get­Entry­LE?
  96. get­Entry­LED
    1. Std.TreeMap.get­Entry­LED
  97. get­Entry­LT!
    1. Std.TreeMap.get­Entry­LT!
  98. get­Entry­LT
    1. Std.TreeMap.get­Entry­LT
  99. get­Entry­LT?
    1. Std.TreeMap.get­Entry­LT?
  100. get­Entry­LTD
    1. Std.TreeMap.get­Entry­LTD
  101. get­Env
    1. IO.get­Env
  102. get­Env­Lean­Path
    1. Lake.get­Env­Lean­Path
  103. get­Env­Lean­Src­Path
    1. Lake.get­Env­Lean­Src­Path
  104. get­Env­Shared­Lib­Path
    1. Lake.get­Env­Shared­Lib­Path
  105. get­Even­Elems
    1. Array.get­Even­Elems
  106. get­GE!
    1. Std.TreeSet.get­GE!
  107. get­GE
    1. Std.TreeSet.get­GE
  108. get­GE?
    1. Std.TreeSet.get­GE?
  109. get­GED
    1. Std.TreeSet.get­GED
  110. get­GT!
    1. Std.TreeSet.get­GT!
  111. get­GT
    1. Std.TreeSet.get­GT
  112. get­GT?
    1. Std.TreeSet.get­GT?
  113. get­GTD
    1. Std.TreeSet.get­GTD
  114. get­Hygiene­Info
    1. Lean.TSyntax.get­Hygiene­Info
  115. get­Id
    1. Lean.TSyntax.get­Id
  116. get­Key!
    1. Std.DHashMap.get­Key!
  117. get­Key!
    1. Std.DTreeMap.get­Key!
  118. get­Key!
    1. Std.Ext­DHashMap.get­Key!
  119. get­Key!
    1. Std.Ext­HashMap.get­Key!
  120. get­Key!
    1. Std.HashMap.get­Key!
  121. get­Key!
    1. Std.TreeMap.get­Key!
  122. get­Key
    1. Std.DHashMap.get­Key
  123. get­Key
    1. Std.DTreeMap.get­Key
  124. get­Key
    1. Std.Ext­DHashMap.get­Key
  125. get­Key
    1. Std.Ext­HashMap.get­Key
  126. get­Key
    1. Std.HashMap.get­Key
  127. get­Key
    1. Std.TreeMap.get­Key
  128. get­Key?
    1. Std.DHashMap.get­Key?
  129. get­Key?
    1. Std.DTreeMap.get­Key?
  130. get­Key?
    1. Std.Ext­DHashMap.get­Key?
  131. get­Key?
    1. Std.Ext­HashMap.get­Key?
  132. get­Key?
    1. Std.HashMap.get­Key?
  133. get­Key?
    1. Std.TreeMap.get­Key?
  134. get­Key­D
    1. Std.DHashMap.get­Key­D
  135. get­Key­D
    1. Std.DTreeMap.get­Key­D
  136. get­Key­D
    1. Std.Ext­DHashMap.get­Key­D
  137. get­Key­D
    1. Std.Ext­HashMap.get­Key­D
  138. get­Key­D
    1. Std.HashMap.get­Key­D
  139. get­Key­D
    1. Std.TreeMap.get­Key­D
  140. get­Key­GE!
    1. Std.TreeMap.get­Key­GE!
  141. get­Key­GE
    1. Std.TreeMap.get­Key­GE
  142. get­Key­GE?
    1. Std.TreeMap.get­Key­GE?
  143. get­Key­GED
    1. Std.TreeMap.get­Key­GED
  144. get­Key­GT!
    1. Std.TreeMap.get­Key­GT!
  145. get­Key­GT
    1. Std.TreeMap.get­Key­GT
  146. get­Key­GT?
    1. Std.TreeMap.get­Key­GT?
  147. get­Key­GTD
    1. Std.TreeMap.get­Key­GTD
  148. get­Key­LE!
    1. Std.TreeMap.get­Key­LE!
  149. get­Key­LE
    1. Std.TreeMap.get­Key­LE
  150. get­Key­LE?
    1. Std.TreeMap.get­Key­LE?
  151. get­Key­LED
    1. Std.TreeMap.get­Key­LED
  152. get­Key­LT!
    1. Std.TreeMap.get­Key­LT!
  153. get­Key­LT
    1. Std.TreeMap.get­Key­LT
  154. get­Key­LT?
    1. Std.TreeMap.get­Key­LT?
  155. get­Key­LTD
    1. Std.TreeMap.get­Key­LTD
  156. get­Kind
    1. Lean.Syntax.get­Kind
  157. get­LE!
    1. Std.TreeSet.get­LE!
  158. get­LE
    1. Std.TreeSet.get­LE
  159. get­LE?
    1. Std.TreeSet.get­LE?
  160. get­LED
    1. Std.TreeSet.get­LED
  161. get­LT!
    1. Std.TreeSet.get­LT!
  162. get­LT
    1. Std.TreeSet.get­LT
  163. get­LT?
    1. Std.TreeSet.get­LT?
  164. get­LTD
    1. Std.TreeSet.get­LTD
  165. get­Lake
    1. Lake.get­Lake
  166. get­Lake­Env
    1. Lake.get­Lake­Env
  167. get­Lake­Home
    1. Lake.get­Lake­Home
  168. get­Lake­Install
    1. Lake.get­Lake­Install
  169. get­Lake­Lib­Dir
    1. Lake.get­Lake­Lib­Dir
  170. get­Lake­Src­Dir
    1. Lake.get­Lake­Src­Dir
  171. get­Last!
    1. List.get­Last!
  172. get­Last
    1. List.get­Last
  173. get­Last?
    1. List.get­Last?
  174. get­Last­D
    1. List.get­Last­D
  175. get­Lean
    1. Lake.get­Lean
  176. get­Lean­Ar
    1. Lake.get­Lean­Ar
  177. get­Lean­Cc
    1. Lake.get­Lean­Cc
  178. get­Lean­Cc?
    1. Lake.get­Lean­Cc?
  179. get­Lean­Include­Dir
    1. Lake.get­Lean­Include­Dir
  180. get­Lean­Install
    1. Lake.get­Lean­Install
  181. get­Lean­Lib­Dir
    1. Lake.get­Lean­Lib­Dir
  182. get­Lean­Path
    1. Lake.get­Lean­Path
  183. get­Lean­Shared­Lib
    1. Lake.get­Lean­Shared­Lib
  184. get­Lean­Src­Dir
    1. Lake.get­Lean­Src­Dir
  185. get­Lean­Src­Path
    1. Lake.get­Lean­Src­Path
  186. get­Lean­Sysroot
    1. Lake.get­Lean­Sysroot
  187. get­Lean­System­Lib­Dir
    1. Lake.get­Lean­System­Lib­Dir
  188. get­Leanc
    1. Lake.get­Leanc
  189. get­Left
    1. Sum.get­Left
  190. get­Left?
    1. Sum.get­Left?
  191. get­Line
    1. IO.FS.Handle.get­Line
  192. get­Line
    1. IO.FS.Stream.get­Line (structure field)
  193. get­Lsb
    1. BitVec.get­Lsb
  194. get­Lsb?
    1. BitVec.get­Lsb?
  195. get­Lsb­D
    1. BitVec.get­Lsb­D
  196. get­M
    1. Option.get­M
  197. get­Max?
    1. Array.get­Max?
  198. get­Modify
  199. get­Msb
    1. BitVec.get­Msb
  200. get­Msb?
    1. BitVec.get­Msb?
  201. get­Msb­D
    1. BitVec.get­Msb­D
  202. get­Name
    1. Lean.TSyntax.get­Name
  203. get­Nat
    1. Lean.TSyntax.get­Nat
  204. get­No­Cache
    1. Lake.get­No­Cache
  205. get­Num­Heartbeats
    1. IO.get­Num­Heartbeats
  206. get­PID
    1. IO.Process.get­PID
  207. get­Pkg­Url­Map
    1. Lake.get­Pkg­Url­Map
  208. get­Random­Bytes
    1. IO.get­Random­Bytes
  209. get­Right
    1. Sum.get­Right
  210. get­Right?
    1. Sum.get­Right?
  211. get­Root­Package
    1. Lake.get­Root­Package
  212. get­Scientific
    1. Lean.TSyntax.get­Scientific
  213. get­Shared­Lib­Path
    1. Lake.get­Shared­Lib­Path
  214. get­Stderr
    1. IO.get­Stderr
  215. get­Stdin
    1. IO.get­Stdin
  216. get­Stdout
    1. IO.get­Stdout
  217. get­String
    1. Lean.TSyntax.get­String
  218. get­TID
    1. IO.get­TID
  219. get­Task­State
    1. IO.get­Task­State
  220. get­The
  221. get­Then­Insert­If­New?
    1. Std.DHashMap.get­Then­Insert­If­New?
  222. get­Then­Insert­If­New?
    1. Std.DTreeMap.get­Then­Insert­If­New?
  223. get­Then­Insert­If­New?
    1. Std.Ext­DHashMap.get­Then­Insert­If­New?
  224. get­Then­Insert­If­New?
    1. Std.Ext­HashMap.get­Then­Insert­If­New?
  225. get­Then­Insert­If­New?
    1. Std.HashMap.get­Then­Insert­If­New?
  226. get­Then­Insert­If­New?
    1. Std.TreeMap.get­Then­Insert­If­New?
  227. get­Try­Cache
    1. Lake.get­Try­Cache
  228. get­Utf8Byte
    1. String.get­Utf8Byte
  229. get­Workspace
    1. Lake.MonadWorkspace.get­Workspace (class method)
  230. get_elem_tactic
  231. get_elem_tactic_trivial
  232. globs
    1. [anonymous] (structure field)
  233. goal
    1. main
  234. grind
  235. ground
    1. Lean.Meta.Simp.Config.ground (structure field)
  236. group
    1. IO.FileRight.group (structure field)
  237. group­By­Key
    1. Array.group­By­Key
  238. group­By­Key
    1. List.group­By­Key
  239. group­Kind
    1. Lean.group­Kind
  240. guard
  241. guard
    1. Option.guard
  242. guard_expr
  243. guard_hyp
  244. guard_msgs.diff
  245. 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. Hash­Map
    1. Std.Hash­Map
  36. Hash­Set
    1. Std.Hash­Set
  37. Hashable
  38. Hashable.mk
    1. Instance constructor of Hashable
  39. Homogeneous­Pow
  40. HomogeneousPow.mk
    1. Instance constructor of Homogeneous­Pow
  41. Hygiene­Info
    1. Lean.Syntax.Hygiene­Info
  42. h­Add
    1. HAdd.h­Add (class method)
  43. h­And
    1. HAnd.h­And (class method)
  44. h­Append
    1. HAppend.h­Append (class method)
  45. h­Div
    1. HDiv.h­Div (class method)
  46. h­Iterate
    1. Fin.h­Iterate
  47. h­Iterate­From
    1. Fin.h­Iterate­From
  48. h­Mod
    1. HMod.h­Mod (class method)
  49. h­Mul
    1. HMul.h­Mul (class method)
  50. h­Or
    1. HOr.h­Or (class method)
  51. h­Pow
    1. HPow.h­Pow (class method)
  52. h­Shift­Left
    1. HShiftLeft.h­Shift­Left (class method)
  53. h­Shift­Right
    1. HShiftRight.h­Shift­Right (class method)
  54. h­Sub
    1. HSub.h­Sub (class method)
  55. h­Xor
    1. HXor.h­Xor (class method)
  56. has­Decl
    1. Lean.Macro.has­Decl
  57. has­Finished
    1. IO.has­Finished
  58. has­Next
    1. String.Iterator.has­Next
  59. has­Prev
    1. String.Iterator.has­Prev
  60. hash
    1. BitVec.hash
  61. hash
    1. Hashable.hash (class method)
  62. hash
    1. String.hash
  63. hash_eq
  64. hash_eq
    1. LawfulHashable.hash_eq (class method)
  65. have (0) (1)
  66. have'
  67. head!
    1. List.head!
  68. head
    1. List.head
  69. head?
    1. List.head?
  70. head­D
    1. List.head­D
  71. helim
    1. Subsingleton.helim
  72. heq_of_eq
  73. heq_of_eq­Rec_eq
  74. heq_of_heq_of_eq
  75. hrec­On
    1. Quot.hrec­On
  76. hrec­On
    1. Quotient.hrec­On
  77. hygiene
    1. in tactics
  78. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  79. hygienic
    1. tactic.hygienic

I

  1. IO
  2. IO.Access­Right
  3. IO.AccessRight.flags
  4. IO.AccessRight.mk
    1. Constructor of IO.Access­Right
  5. IO.Error
  6. IO.Error.already­Exists
    1. Constructor of IO.Error
  7. IO.Error.hardware­Fault
    1. Constructor of IO.Error
  8. IO.Error.illegal­Operation
    1. Constructor of IO.Error
  9. IO.Error.inappropriate­Type
    1. Constructor of IO.Error
  10. IO.Error.interrupted
    1. Constructor of IO.Error
  11. IO.Error.invalid­Argument
    1. Constructor of IO.Error
  12. IO.Error.no­File­Or­Directory
    1. Constructor of IO.Error
  13. IO.Error.no­Such­Thing
    1. Constructor of IO.Error
  14. IO.Error.other­Error
    1. Constructor of IO.Error
  15. IO.Error.permission­Denied
    1. Constructor of IO.Error
  16. IO.Error.protocol­Error
    1. Constructor of IO.Error
  17. IO.Error.resource­Busy
    1. Constructor of IO.Error
  18. IO.Error.resource­Exhausted
    1. Constructor of IO.Error
  19. IO.Error.resource­Vanished
    1. Constructor of IO.Error
  20. IO.Error.time­Expired
    1. Constructor of IO.Error
  21. IO.Error.to­String
  22. IO.Error.unexpected­Eof
    1. Constructor of IO.Error
  23. IO.Error.unsatisfied­Constraints
    1. Constructor of IO.Error
  24. IO.Error.unsupported­Operation
    1. Constructor of IO.Error
  25. IO.Error.user­Error
    1. Constructor of IO.Error
  26. IO.FS.Dir­Entry
  27. IO.FS.DirEntry.mk
    1. Constructor of IO.FS.Dir­Entry
  28. IO.FS.DirEntry.path
  29. IO.FS.Handle
  30. IO.FS.Handle.flush
  31. IO.FS.Handle.get­Line
  32. IO.FS.Handle.is­Tty
  33. IO.FS.Handle.lock
  34. IO.FS.Handle.mk
  35. IO.FS.Handle.put­Str
  36. IO.FS.Handle.put­Str­Ln
  37. IO.FS.Handle.read
  38. IO.FS.Handle.read­Bin­To­End
  39. IO.FS.Handle.read­Bin­To­End­Into
  40. IO.FS.Handle.read­To­End
  41. IO.FS.Handle.rewind
  42. IO.FS.Handle.truncate
  43. IO.FS.Handle.try­Lock
  44. IO.FS.Handle.unlock
  45. IO.FS.Handle.write
  46. IO.FS.Metadata
  47. IO.FS.Metadata.mk
    1. Constructor of IO.FS.Metadata
  48. IO.FS.Mode
  49. IO.FS.Mode.append
    1. Constructor of IO.FS.Mode
  50. IO.FS.Mode.read
    1. Constructor of IO.FS.Mode
  51. IO.FS.Mode.read­Write
    1. Constructor of IO.FS.Mode
  52. IO.FS.Mode.write
    1. Constructor of IO.FS.Mode
  53. IO.FS.Mode.write­New
    1. Constructor of IO.FS.Mode
  54. IO.FS.Stream
  55. IO.FS.Stream.Buffer
  56. IO.FS.Stream.Buffer.mk
    1. Constructor of IO.FS.Stream.Buffer
  57. IO.FS.Stream.mk
    1. Constructor of IO.FS.Stream
  58. IO.FS.Stream.of­Buffer
  59. IO.FS.Stream.of­Handle
  60. IO.FS.Stream.put­Str­Ln
  61. IO.FS.create­Dir
  62. IO.FS.create­Dir­All
  63. IO.FS.create­Temp­Dir
  64. IO.FS.create­Temp­File
  65. IO.FS.lines
  66. IO.FS.read­Bin­File
  67. IO.FS.read­File
  68. IO.FS.real­Path
  69. IO.FS.remove­Dir
  70. IO.FS.remove­Dir­All
  71. IO.FS.remove­File
  72. IO.FS.rename
  73. IO.FS.with­File
  74. IO.FS.with­Isolated­Streams
  75. IO.FS.with­Temp­Dir
  76. IO.FS.with­Temp­File
  77. IO.FS.write­Bin­File
  78. IO.FS.write­File
  79. IO.File­Right
  80. IO.FileRight.flags
  81. IO.FileRight.mk
    1. Constructor of IO.File­Right
  82. IO.Process.Child
  83. IO.Process.Child.kill
  84. IO.Process.Child.take­Stdin
  85. IO.Process.Child.try­Wait
  86. IO.Process.Child.wait
  87. IO.Process.Output
  88. IO.Process.Output.mk
    1. Constructor of IO.Process.Output
  89. IO.Process.Spawn­Args
  90. IO.Process.SpawnArgs.mk
    1. Constructor of IO.Process.Spawn­Args
  91. IO.Process.Stdio
  92. IO.Process.Stdio.inherit
    1. Constructor of IO.Process.Stdio
  93. IO.Process.Stdio.null
    1. Constructor of IO.Process.Stdio
  94. IO.Process.Stdio.piped
    1. Constructor of IO.Process.Stdio
  95. IO.Process.Stdio.to­Handle­Type
  96. IO.Process.Stdio­Config
  97. IO.Process.StdioConfig.mk
    1. Constructor of IO.Process.Stdio­Config
  98. IO.Process.exit
  99. IO.Process.get­Current­Dir
  100. IO.Process.get­PID
  101. IO.Process.output
  102. IO.Process.run
  103. IO.Process.set­Current­Dir
  104. IO.Process.spawn
  105. IO.Promise
  106. IO.Promise.is­Resolved
  107. IO.Promise.new
  108. IO.Promise.resolve
  109. IO.Promise.result!
  110. IO.Promise.result?
  111. IO.Promise.result­D
  112. IO.Ref
  113. IO.Task­State
  114. IO.TaskState.finished
    1. Constructor of IO.Task­State
  115. IO.TaskState.running
    1. Constructor of IO.Task­State
  116. IO.TaskState.waiting
    1. Constructor of IO.Task­State
  117. IO.add­Heartbeats
  118. IO.app­Dir
  119. IO.app­Path
  120. IO.as­Task
  121. IO.bind­Task
  122. IO.cancel
  123. IO.chain­Task
  124. IO.check­Canceled
  125. IO.current­Dir
  126. IO.eprint
  127. IO.eprintln
  128. IO.get­Env
  129. IO.get­Num­Heartbeats
  130. IO.get­Random­Bytes
  131. IO.get­Stderr
  132. IO.get­Stdin
  133. IO.get­Stdout
  134. IO.get­TID
  135. IO.get­Task­State
  136. IO.has­Finished
  137. IO.iterate
  138. IO.lazy­Pure
  139. IO.map­Task
  140. IO.map­Tasks
  141. IO.mk­Ref
  142. IO.mono­Ms­Now
  143. IO.mono­Nanos­Now
  144. IO.of­Except
  145. IO.print
  146. IO.println
  147. IO.rand
  148. IO.set­Access­Rights
  149. IO.set­Rand­Seed
  150. IO.set­Stderr
  151. IO.set­Stdin
  152. IO.set­Stdout
  153. IO.sleep
  154. IO.to­EIO
  155. IO.user­Error
  156. IO.wait
  157. IO.wait­Any
  158. IO.with­Stderr
  159. IO.with­Stdin
  160. IO.with­Stdout
  161. ISize
  162. ISize.abs
  163. ISize.add
  164. ISize.complement
  165. ISize.dec­Eq
  166. ISize.dec­Le
  167. ISize.dec­Lt
  168. ISize.div
  169. ISize.land
  170. ISize.le
  171. ISize.lor
  172. ISize.lt
  173. ISize.max­Value
  174. ISize.min­Value
  175. ISize.mod
  176. ISize.mul
  177. ISize.neg
  178. ISize.of­Bit­Vec
  179. ISize.of­Int
  180. ISize.of­Int­LE
  181. ISize.of­Int­Truncate
  182. ISize.of­Nat
  183. ISize.shift­Left
  184. ISize.shift­Right
  185. ISize.size
  186. ISize.sub
  187. ISize.to­Bit­Vec
  188. ISize.to­Float
  189. ISize.to­Float32
  190. ISize.to­Int
  191. ISize.to­Int16
  192. ISize.to­Int32
  193. ISize.to­Int64
  194. ISize.to­Int8
  195. ISize.to­Nat­Clamp­Neg
  196. ISize.xor
  197. Id
  198. Id.run
  199. Ident
    1. Lean.Syntax.Ident
  200. Iff
  201. Iff.elim
  202. Iff.intro
    1. Constructor of Iff
  203. Inhabited
  204. Inhabited.mk
    1. Instance constructor of Inhabited
  205. Int
  206. Int.add
  207. Int.bdiv
  208. Int.bmod
  209. Int.cast
  210. Int.dec­Eq
  211. Int.ediv
  212. Int.emod
  213. Int.fdiv
  214. Int.fmod
  215. Int.gcd
  216. Int.lcm
  217. Int.le
  218. Int.lt
  219. Int.mul
  220. Int.nat­Abs
  221. Int.neg
  222. Int.neg­Of­Nat
  223. Int.neg­Succ
    1. Constructor of Int
  224. Int.not
  225. Int.of­Nat
    1. Constructor of Int
  226. Int.pow
  227. Int.repr
  228. Int.shift­Right
  229. Int.sign
  230. Int.sub
  231. Int.sub­Nat­Nat
  232. Int.tdiv
  233. Int.tmod
  234. Int.to­ISize
  235. Int.to­Int16
  236. Int.to­Int32
  237. Int.to­Int64
  238. Int.to­Int8
  239. Int.to­Nat
  240. Int.to­Nat?
  241. Int16
  242. Int16.abs
  243. Int16.add
  244. Int16.complement
  245. Int16.dec­Eq
  246. Int16.dec­Le
  247. Int16.dec­Lt
  248. Int16.div
  249. Int16.land
  250. Int16.le
  251. Int16.lor
  252. Int16.lt
  253. Int16.max­Value
  254. Int16.min­Value
  255. Int16.mod
  256. Int16.mul
  257. Int16.neg
  258. Int16.of­Bit­Vec
  259. Int16.of­Int
  260. Int16.of­Int­LE
  261. Int16.of­Int­Truncate
  262. Int16.of­Nat
  263. Int16.shift­Left
  264. Int16.shift­Right
  265. Int16.size
  266. Int16.sub
  267. Int16.to­Bit­Vec
  268. Int16.to­Float
  269. Int16.to­Float32
  270. Int16.to­ISize
  271. Int16.to­Int
  272. Int16.to­Int32
  273. Int16.to­Int64
  274. Int16.to­Int8
  275. Int16.to­Nat­Clamp­Neg
  276. Int16.xor
  277. Int32
  278. Int32.abs
  279. Int32.add
  280. Int32.complement
  281. Int32.dec­Eq
  282. Int32.dec­Le
  283. Int32.dec­Lt
  284. Int32.div
  285. Int32.land
  286. Int32.le
  287. Int32.lor
  288. Int32.lt
  289. Int32.max­Value
  290. Int32.min­Value
  291. Int32.mod
  292. Int32.mul
  293. Int32.neg
  294. Int32.of­Bit­Vec
  295. Int32.of­Int
  296. Int32.of­Int­LE
  297. Int32.of­Int­Truncate
  298. Int32.of­Nat
  299. Int32.shift­Left
  300. Int32.shift­Right
  301. Int32.size
  302. Int32.sub
  303. Int32.to­Bit­Vec
  304. Int32.to­Float
  305. Int32.to­Float32
  306. Int32.to­ISize
  307. Int32.to­Int
  308. Int32.to­Int16
  309. Int32.to­Int64
  310. Int32.to­Int8
  311. Int32.to­Nat­Clamp­Neg
  312. Int32.xor
  313. Int64
  314. Int64.abs
  315. Int64.add
  316. Int64.complement
  317. Int64.dec­Eq
  318. Int64.dec­Le
  319. Int64.dec­Lt
  320. Int64.div
  321. Int64.land
  322. Int64.le
  323. Int64.lor
  324. Int64.lt
  325. Int64.max­Value
  326. Int64.min­Value
  327. Int64.mod
  328. Int64.mul
  329. Int64.neg
  330. Int64.of­Bit­Vec
  331. Int64.of­Int
  332. Int64.of­Int­LE
  333. Int64.of­Int­Truncate
  334. Int64.of­Nat
  335. Int64.shift­Left
  336. Int64.shift­Right
  337. Int64.size
  338. Int64.sub
  339. Int64.to­Bit­Vec
  340. Int64.to­Float
  341. Int64.to­Float32
  342. Int64.to­ISize
  343. Int64.to­Int
  344. Int64.to­Int16
  345. Int64.to­Int32
  346. Int64.to­Int8
  347. Int64.to­Nat­Clamp­Neg
  348. Int64.xor
  349. Int8
  350. Int8.abs
  351. Int8.add
  352. Int8.complement
  353. Int8.dec­Eq
  354. Int8.dec­Le
  355. Int8.dec­Lt
  356. Int8.div
  357. Int8.land
  358. Int8.le
  359. Int8.lor
  360. Int8.lt
  361. Int8.max­Value
  362. Int8.min­Value
  363. Int8.mod
  364. Int8.mul
  365. Int8.neg
  366. Int8.of­Bit­Vec
  367. Int8.of­Int
  368. Int8.of­Int­LE
  369. Int8.of­Int­Truncate
  370. Int8.of­Nat
  371. Int8.shift­Left
  372. Int8.shift­Right
  373. Int8.size
  374. Int8.sub
  375. Int8.to­Bit­Vec
  376. Int8.to­Float
  377. Int8.to­Float32
  378. Int8.to­ISize
  379. Int8.to­Int
  380. Int8.to­Int16
  381. Int8.to­Int32
  382. Int8.to­Int64
  383. Int8.to­Nat­Clamp­Neg
  384. Int8.xor
  385. Int­Cast
  386. IntCast.mk
    1. Instance constructor of Int­Cast
  387. Int­Interval
    1. Lean.Grind.Int­Interval
  388. Int­Module
    1. Lean.Grind.Int­Module
  389. Is­Char­P
    1. Lean.Grind.Is­Char­P
  390. Is­Infix
    1. List.Is­Infix
  391. Is­Prefix
    1. List.Is­Prefix
  392. Is­Suffix
    1. List.Is­Suffix
  393. Iterator
    1. String.Iterator
  394. i
    1. String.Iterator.i (structure field)
  395. id_map
    1. LawfulFunctor.id_map (class method)
  396. ident­Kind
    1. Lean.ident­Kind
  397. identifier
  398. identifier
    1. raw
  399. idx­Of
    1. Array.idx­Of
  400. idx­Of
    1. List.idx­Of
  401. idx­Of?
    1. Array.idx­Of?
  402. idx­Of?
    1. List.idx­Of?
  403. if ... then ... else ...
  404. if h : ... then ... else ...
  405. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  406. impredicative
  407. inaccessible
  408. ind
    1. Quot.ind
  409. ind
    1. Quotient.ind
  410. ind
    1. Squash.ind
  411. indent­D
    1. Std.Format.indent­D
  412. index
    1. Lean.Meta.DSimp.Config.index (structure field)
  413. index
    1. Lean.Meta.Simp.Config.index (structure field)
  414. index
    1. of inductive type
  415. indexed family
    1. of types
  416. induction
  417. induction
    1. Fin.induction
  418. induction­On
    1. Fin.induction­On
  419. induction­On
    1. Nat.div.induction­On
  420. induction­On
    1. Nat.mod.induction­On
  421. inductive.auto­Promote­Indices
  422. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  423. infer­Instance
  424. infer­Instance­As
  425. infer_instance
  426. inhabited­Left
    1. PSum.inhabited­Left
  427. inhabited­Left
    1. Sum.inhabited­Left
  428. inhabited­Right
    1. PSum.inhabited­Right
  429. inhabited­Right
    1. Sum.inhabited­Right
  430. inherit­Env
    1. IO.Process.SpawnArgs.args (structure field)
  431. init (Lake command)
  432. injection
  433. injections
  434. inner
    1. Std.DHashMap.Equiv.inner (structure field)
  435. inner
    1. Std.DTreeMap.Raw.inner (structure field)
  436. inner
    1. Std.Ext­HashSet.inner (structure field)
  437. inner
    1. Std.HashMap.Equiv.inner (structure field)
  438. inner
    1. Std.HashMap.Raw.inner (structure field)
  439. inner
    1. Std.HashSet.Equiv.inner (structure field)
  440. inner
    1. Std.HashSet.Raw.inner (structure field)
  441. inner
    1. Std.HashSet.inner (structure field)
  442. inner
    1. Std.TreeMap.Raw.inner (structure field)
  443. inner
    1. Std.TreeSet.Raw.inner (structure field)
  444. insert
    1. List.insert
  445. insert
    1. Std.DHashMap.insert
  446. insert
    1. Std.DTreeMap.insert
  447. insert
    1. Std.Ext­DHashMap.insert
  448. insert
    1. Std.Ext­HashMap.insert
  449. insert
    1. Std.Ext­HashSet.insert
  450. insert
    1. Std.HashMap.insert
  451. insert
    1. Std.HashSet.insert
  452. insert
    1. Std.TreeMap.insert
  453. insert
    1. Std.TreeSet.insert
  454. insert­Idx!
    1. Array.insert­Idx!
  455. insert­Idx
    1. Array.insert­Idx
  456. insert­Idx
    1. List.insert­Idx
  457. insert­Idx­If­In­Bounds
    1. Array.insert­Idx­If­In­Bounds
  458. insert­Idx­TR
    1. List.insert­Idx­TR
  459. insert­If­New
    1. Std.DHashMap.insert­If­New
  460. insert­If­New
    1. Std.DTreeMap.insert­If­New
  461. insert­If­New
    1. Std.Ext­DHashMap.insert­If­New
  462. insert­If­New
    1. Std.Ext­HashMap.insert­If­New
  463. insert­If­New
    1. Std.HashMap.insert­If­New
  464. insert­If­New
    1. Std.TreeMap.insert­If­New
  465. insert­Many
    1. Std.DHashMap.insert­Many
  466. insert­Many
    1. Std.DTreeMap.insert­Many
  467. insert­Many
    1. Std.Ext­DHashMap.insert­Many
  468. insert­Many
    1. Std.Ext­HashMap.insert­Many
  469. insert­Many
    1. Std.Ext­HashSet.insert­Many
  470. insert­Many
    1. Std.HashMap.insert­Many
  471. insert­Many
    1. Std.HashSet.insert­Many
  472. insert­Many
    1. Std.TreeMap.insert­Many
  473. insert­Many
    1. Std.TreeSet.insert­Many
  474. insert­Many­If­New­Unit
    1. Std.Ext­HashMap.insert­Many­If­New­Unit
  475. insert­Many­If­New­Unit
    1. Std.HashMap.insert­Many­If­New­Unit
  476. insert­Many­If­New­Unit
    1. Std.TreeMap.insert­Many­If­New­Unit
  477. insertion­Sort
    1. Array.insertion­Sort
  478. instance synthesis
  479. instance
    1. trace.grind.ematch.instance
  480. int­Cast
    1. IntCast.int­Cast (class method)
  481. int­Cast
    1. [anonymous] (class method)
  482. int­Cast_neg
    1. [anonymous] (class method)
  483. int­Cast_of­Nat
    1. [anonymous] (class method)
  484. int­Max
    1. BitVec.int­Max
  485. int­Min
    1. BitVec.int­Min
  486. intercalate
    1. List.intercalate
  487. intercalate
    1. String.intercalate
  488. intercalate­TR
    1. List.intercalate­TR
  489. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  490. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  491. intersperse
    1. List.intersperse
  492. intersperse­TR
    1. List.intersperse­TR
  493. intro (0) (1)
  494. intro | ... => ... | ... => ...
  495. intros
  496. inv­Image
  497. inv_zero
    1. [anonymous] (class method)
  498. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
  499. iota
    1. Lean.Meta.Simp.Config.iota (structure field)
  500. is­Absolute
    1. System.FilePath.is­Absolute
  501. is­Alpha
    1. Char.is­Alpha
  502. is­Alphanum
    1. Char.is­Alphanum
  503. is­Digit
    1. Char.is­Digit
  504. is­Dir
    1. System.FilePath.is­Dir
  505. is­Empty
    1. Array.is­Empty
  506. is­Empty
    1. List.is­Empty
  507. is­Empty
    1. Std.DHashMap.is­Empty
  508. is­Empty
    1. Std.DTreeMap.is­Empty
  509. is­Empty
    1. Std.Ext­DHashMap.is­Empty
  510. is­Empty
    1. Std.Ext­HashMap.is­Empty
  511. is­Empty
    1. Std.Ext­HashSet.is­Empty
  512. is­Empty
    1. Std.Format.is­Empty
  513. is­Empty
    1. Std.HashMap.is­Empty
  514. is­Empty
    1. Std.HashSet.is­Empty
  515. is­Empty
    1. Std.TreeMap.is­Empty
  516. is­Empty
    1. Std.TreeSet.is­Empty
  517. is­Empty
    1. String.is­Empty
  518. is­Empty
    1. Substring.is­Empty
  519. is­Emscripten
    1. System.Platform.is­Emscripten
  520. is­Eq
    1. Ordering.is­Eq
  521. is­Eq­Some
    1. Option.is­Eq­Some
  522. is­Eqv
    1. Array.is­Eqv
  523. is­Eqv
    1. List.is­Eqv
  524. is­Exclusive­Unsafe
  525. is­Finite
    1. Float.is­Finite
  526. is­Finite
    1. Float32.is­Finite
  527. is­GE
    1. Ordering.is­GE
  528. is­GT
    1. Ordering.is­GT
  529. is­Inf
    1. Float.is­Inf
  530. is­Inf
    1. Float32.is­Inf
  531. is­Int
    1. String.is­Int
  532. is­LE
    1. Ordering.is­LE
  533. is­LT
    1. Ordering.is­LT
  534. is­Left
    1. Sum.is­Left
  535. is­Lower
    1. Char.is­Lower
  536. is­Lt
    1. Fin.is­Lt (structure field)
  537. is­Na­N
    1. Float.is­Na­N
  538. is­Na­N
    1. Float32.is­Na­N
  539. is­Nat
    1. String.is­Nat
  540. is­Nat
    1. Substring.is­Nat
  541. is­Ne
    1. Ordering.is­Ne
  542. is­Nil
    1. Std.Format.is­Nil
  543. is­None
    1. Option.is­None
  544. is­OSX
    1. System.Platform.is­OSX
  545. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  546. is­Ok
    1. Except.is­Ok
  547. is­Perm
    1. List.is­Perm
  548. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  549. is­Prefix­Of
    1. Array.is­Prefix­Of
  550. is­Prefix­Of
    1. List.is­Prefix­Of
  551. is­Prefix­Of
    1. String.is­Prefix­Of
  552. is­Prefix­Of?
    1. List.is­Prefix­Of?
  553. is­Relative
    1. System.FilePath.is­Relative
  554. is­Resolved
    1. IO.Promise.is­Resolved
  555. is­Right
    1. Sum.is­Right
  556. is­Some
    1. Option.is­Some
  557. is­Sublist
    1. List.is­Sublist
  558. is­Suffix­Of
    1. List.is­Suffix­Of
  559. is­Suffix­Of?
    1. List.is­Suffix­Of?
  560. is­Tty
    1. IO.FS.Handle.is­Tty
  561. is­Tty
    1. IO.FS.Stream.is­Tty (structure field)
  562. is­Upper
    1. Char.is­Upper
  563. is­Valid
    1. String.Pos.is­Valid
  564. is­Valid­Char
    1. Nat.is­Valid­Char
  565. is­Valid­Char
    1. UInt32.is­Valid­Char
  566. is­Valid­Char­Nat
    1. Char.is­Valid­Char­Nat
  567. is­Whitespace
    1. Char.is­Whitespace
  568. is­Windows
    1. System.Platform.is­Windows
  569. iseqv
    1. Setoid.iseqv (class method)
  570. iter
    1. String.iter
  571. iterate
  572. iterate
    1. IO.iterate
  573. iunfoldr
    1. BitVec.iunfoldr
  574. 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_HOME (environment variable)
  3. LAKE_NO_CACHE (environment variable)
  4. LAKE_OVERRIDE_LEAN (environment variable)
  5. LE
  6. LE.mk
    1. Instance constructor of LE
  7. LEAN (environment variable)
  8. LEAN_AR (environment variable)
  9. LEAN_CC (environment variable)
  10. LEAN_NUM_THREADS (environment variable)
  11. LEAN_SYSROOT (environment variable)
  12. LT
  13. LT.mk
    1. Instance constructor of LT
  14. Lake.Backend
  15. Lake.Backend.c
    1. Constructor of Lake.Backend
  16. Lake.Backend.default
    1. Constructor of Lake.Backend
  17. Lake.Backend.llvm
    1. Constructor of Lake.Backend
  18. Lake.Build­Type
  19. Lake.BuildType.debug
    1. Constructor of Lake.Build­Type
  20. Lake.BuildType.min­Size­Rel
    1. Constructor of Lake.Build­Type
  21. Lake.BuildType.rel­With­Deb­Info
    1. Constructor of Lake.Build­Type
  22. Lake.BuildType.release
    1. Constructor of Lake.Build­Type
  23. Lake.Glob
  24. Lake.Glob.and­Submodules
    1. Constructor of Lake.Glob
  25. Lake.Glob.one
    1. Constructor of Lake.Glob
  26. Lake.Glob.submodules
    1. Constructor of Lake.Glob
  27. Lake.Lean­Exe­Config
  28. Lake.Lean­ExeConfig.mk
    1. Constructor of Lake.Lean­Exe­Config
  29. Lake.Lean­Lib­Config
  30. Lake.Lean­LibConfig.mk
    1. Constructor of Lake.Lean­Lib­Config
  31. Lake.Monad­Lake­Env
  32. Lake.Monad­Workspace
  33. Lake.MonadWorkspace.mk
    1. Instance constructor of Lake.Monad­Workspace
  34. Lake.Script­M (0) (1)
  35. Lake.find­Extern­Lib?
  36. Lake.find­Lean­Exe?
  37. Lake.find­Lean­Lib?
  38. Lake.find­Module?
  39. Lake.find­Package?
  40. Lake.get­Augmented­Env
  41. Lake.get­Augmented­Lean­Path
  42. Lake.get­Augmented­Lean­Src­Path
  43. Lake.get­Augmented­Shared­Lib­Path
  44. Lake.get­Elan?
  45. Lake.get­Elan­Home?
  46. Lake.get­Elan­Install?
  47. Lake.get­Elan­Toolchain
  48. Lake.get­Env­Lean­Path
  49. Lake.get­Env­Lean­Src­Path
  50. Lake.get­Env­Shared­Lib­Path
  51. Lake.get­Lake
  52. Lake.get­Lake­Env
  53. Lake.get­Lake­Home
  54. Lake.get­Lake­Install
  55. Lake.get­Lake­Lib­Dir
  56. Lake.get­Lake­Src­Dir
  57. Lake.get­Lean
  58. Lake.get­Lean­Ar
  59. Lake.get­Lean­Cc
  60. Lake.get­Lean­Cc?
  61. Lake.get­Lean­Include­Dir
  62. Lake.get­Lean­Install
  63. Lake.get­Lean­Lib­Dir
  64. Lake.get­Lean­Path
  65. Lake.get­Lean­Shared­Lib
  66. Lake.get­Lean­Src­Dir
  67. Lake.get­Lean­Src­Path
  68. Lake.get­Lean­Sysroot
  69. Lake.get­Lean­System­Lib­Dir
  70. Lake.get­Leanc
  71. Lake.get­No­Cache
  72. Lake.get­Pkg­Url­Map
  73. Lake.get­Root­Package
  74. Lake.get­Shared­Lib­Path
  75. Lake.get­Try­Cache
  76. Lawful­Applicative
  77. LawfulApplicative.mk
    1. Instance constructor of Lawful­Applicative
  78. Lawful­BEq
  79. LawfulBEq.mk
    1. Instance constructor of Lawful­BEq
  80. Lawful­Functor
  81. LawfulFunctor.mk
    1. Instance constructor of Lawful­Functor
  82. Lawful­Get­Elem
  83. Lawful­GetElem.mk
    1. Instance constructor of Lawful­Get­Elem
  84. Lawful­Hashable
  85. LawfulHashable.mk
    1. Instance constructor of Lawful­Hashable
  86. Lawful­Monad
  87. LawfulMonad.mk'
  88. LawfulMonad.mk
    1. Instance constructor of Lawful­Monad
  89. Leading­Ident­Behavior
    1. Lean.Parser.Leading­Ident­Behavior
  90. Lean.Elab.register­Deriving­Handler
  91. Lean.Grind.Add­Right­Cancel
  92. Lean.Grind.Add­RightCancel.mk
    1. Instance constructor of Lean.Grind.Add­Right­Cancel
  93. Lean.Grind.Comm­Ring
  94. Lean.Grind.CommRing.mk
    1. Instance constructor of Lean.Grind.Comm­Ring
  95. Lean.Grind.Comm­Semiring
  96. Lean.Grind.CommSemiring.mk
    1. Instance constructor of Lean.Grind.Comm­Semiring
  97. Lean.Grind.Field
  98. Lean.Grind.Field.mk
    1. Instance constructor of Lean.Grind.Field
  99. Lean.Grind.Int­Interval
  100. Lean.Grind.IntInterval.ci
    1. Constructor of Lean.Grind.Int­Interval
  101. Lean.Grind.IntInterval.co
    1. Constructor of Lean.Grind.Int­Interval
  102. Lean.Grind.IntInterval.ii
    1. Constructor of Lean.Grind.Int­Interval
  103. Lean.Grind.IntInterval.io
    1. Constructor of Lean.Grind.Int­Interval
  104. Lean.Grind.Int­Module
  105. Lean.Grind.IntModule.mk
    1. Instance constructor of Lean.Grind.Int­Module
  106. Lean.Grind.Is­Char­P
  107. Lean.Grind.Is­CharP.mk
    1. Instance constructor of Lean.Grind.Is­Char­P
  108. Lean.Grind.Nat­Module
  109. Lean.Grind.NatModule.mk
    1. Instance constructor of Lean.Grind.Nat­Module
  110. Lean.Grind.No­Nat­Zero­Divisors
  111. Lean.Grind.No­Nat­ZeroDivisors.mk'
  112. Lean.Grind.No­Nat­ZeroDivisors.mk
    1. Instance constructor of Lean.Grind.No­Nat­Zero­Divisors
  113. Lean.Grind.Ordered­Add
  114. Lean.Grind.OrderedAdd.mk
    1. Instance constructor of Lean.Grind.Ordered­Add
  115. Lean.Grind.Ordered­Ring
  116. Lean.Grind.OrderedRing.mk
    1. Instance constructor of Lean.Grind.Ordered­Ring
  117. Lean.Grind.Ring
  118. Lean.Grind.Ring.mk
    1. Instance constructor of Lean.Grind.Ring
  119. Lean.Grind.Semiring
  120. Lean.Grind.Semiring.mk
    1. Instance constructor of Lean.Grind.Semiring
  121. Lean.Grind.To­Int
  122. Lean.Grind.ToInt.mk
    1. Instance constructor of Lean.Grind.To­Int
  123. Lean.Lean­Option
  124. Lean.LeanOption.mk
    1. Constructor of Lean.Lean­Option
  125. Lean.Macro.Exception.unsupported­Syntax
  126. Lean.Macro.add­Macro­Scope
  127. Lean.Macro.expand­Macro?
  128. Lean.Macro.get­Curr­Namespace
  129. Lean.Macro.has­Decl
  130. Lean.Macro.resolve­Global­Name
  131. Lean.Macro.resolve­Namespace
  132. Lean.Macro.throw­Error
  133. Lean.Macro.throw­Error­At
  134. Lean.Macro.throw­Unsupported
  135. Lean.Macro.trace
  136. Lean.Macro.with­Fresh­Macro­Scope
  137. Lean.Macro­M
  138. Lean.Meta.DSimp.Config
  139. Lean.Meta.DSimp.Config.mk
    1. Constructor of Lean.Meta.DSimp.Config
  140. Lean.Meta.Occurrences
  141. Lean.Meta.Occurrences.all
    1. Constructor of Lean.Meta.Occurrences
  142. Lean.Meta.Occurrences.neg
    1. Constructor of Lean.Meta.Occurrences
  143. Lean.Meta.Occurrences.pos
    1. Constructor of Lean.Meta.Occurrences
  144. Lean.Meta.Rewrite.Config
  145. Lean.Meta.Rewrite.Config.mk
    1. Constructor of Lean.Meta.Rewrite.Config
  146. Lean.Meta.Rewrite.New­Goals
  147. Lean.Meta.Simp.Config
  148. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  149. Lean.Meta.Simp.neutral­Config
  150. Lean.Meta.Simp­Extension
  151. Lean.Meta.Transparency­Mode
  152. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.Transparency­Mode
  153. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.Transparency­Mode
  154. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.Transparency­Mode
  155. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.Transparency­Mode
  156. Lean.Meta.register­Simp­Attr
  157. Lean.Order.CCPO
  158. Lean.Order.CCPO.mk
    1. Instance constructor of Lean.Order.CCPO
  159. Lean.Order.Partial­Order
  160. Lean.Order.PartialOrder.mk
    1. Instance constructor of Lean.Order.Partial­Order
  161. Lean.Order.fix
  162. Lean.Order.fix_eq
  163. Lean.Order.monotone
  164. Lean.Parser.Leading­Ident­Behavior
  165. Lean.Parser.Leading­IdentBehavior.both
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  166. Lean.Parser.Leading­IdentBehavior.default
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  167. Lean.Parser.Leading­IdentBehavior.symbol
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  168. Lean.PrettyPrinter.Unexpand­M
  169. Lean.PrettyPrinter.Unexpander
  170. Lean.Source­Info
  171. Lean.SourceInfo.none
    1. Constructor of Lean.Source­Info
  172. Lean.SourceInfo.original
    1. Constructor of Lean.Source­Info
  173. Lean.SourceInfo.synthetic
    1. Constructor of Lean.Source­Info
  174. Lean.Syntax
  175. Lean.Syntax.Char­Lit
  176. Lean.Syntax.Command
  177. Lean.Syntax.Hygiene­Info
  178. Lean.Syntax.Ident
  179. Lean.Syntax.Level
  180. Lean.Syntax.Name­Lit
  181. Lean.Syntax.Num­Lit
  182. Lean.Syntax.Prec
  183. Lean.Syntax.Preresolved
  184. Lean.Syntax.Preresolved.decl
    1. Constructor of Lean.Syntax.Preresolved
  185. Lean.Syntax.Preresolved.namespace
    1. Constructor of Lean.Syntax.Preresolved
  186. Lean.Syntax.Prio
  187. Lean.Syntax.Scientific­Lit
  188. Lean.Syntax.Str­Lit
  189. Lean.Syntax.TSep­Array
  190. Lean.Syntax.TSepArray.mk
    1. Constructor of Lean.Syntax.TSep­Array
  191. Lean.Syntax.Tactic
  192. Lean.Syntax.Term
  193. Lean.Syntax.atom
    1. Constructor of Lean.Syntax
  194. Lean.Syntax.get­Kind
  195. Lean.Syntax.ident
    1. Constructor of Lean.Syntax
  196. Lean.Syntax.is­Of­Kind
  197. Lean.Syntax.missing
    1. Constructor of Lean.Syntax
  198. Lean.Syntax.node
    1. Constructor of Lean.Syntax
  199. Lean.Syntax.set­Kind
  200. Lean.Syntax­Node­Kind
  201. Lean.Syntax­Node­Kinds
  202. Lean.TSyntax
  203. Lean.TSyntax.get­Char
  204. Lean.TSyntax.get­Hygiene­Info
  205. Lean.TSyntax.get­Id
  206. Lean.TSyntax.get­Name
  207. Lean.TSyntax.get­Nat
  208. Lean.TSyntax.get­Scientific
  209. Lean.TSyntax.get­String
  210. Lean.TSyntax.mk
    1. Constructor of Lean.TSyntax
  211. Lean.TSyntax­Array
  212. Lean.char­Lit­Kind
  213. Lean.choice­Kind
  214. Lean.field­Idx­Kind
  215. Lean.group­Kind
  216. Lean.hygiene­Info­Kind
  217. Lean.ident­Kind
  218. Lean.interpolated­Str­Kind
  219. Lean.interpolated­Str­Lit­Kind
  220. Lean.name­Lit­Kind
  221. Lean.null­Kind
  222. Lean.num­Lit­Kind
  223. Lean.scientific­Lit­Kind
  224. Lean.str­Lit­Kind
  225. Lean­Exe­Config
    1. Lake.Lean­Exe­Config
  226. Lean­Lib­Config
    1. Lake.Lean­Lib­Config
  227. Lean­Option
    1. Lean.Lean­Option
  228. Level
    1. Lean.Syntax.Level
  229. Lex
    1. List.Lex
  230. List
  231. List.Is­Infix
  232. List.Is­Prefix
  233. List.Is­Suffix
  234. List.Lex
  235. List.Lex.cons
    1. Constructor of List.Lex
  236. List.Lex.nil
    1. Constructor of List.Lex
  237. List.Lex.rel
    1. Constructor of List.Lex
  238. List.Mem
  239. List.Mem.head
    1. Constructor of List.Mem
  240. List.Mem.tail
    1. Constructor of List.Mem
  241. List.Nodup
  242. List.Pairwise
  243. List.Pairwise.cons
    1. Constructor of List.Pairwise
  244. List.Pairwise.nil
    1. Constructor of List.Pairwise
  245. List.Perm
  246. List.Perm.cons
    1. Constructor of List.Perm
  247. List.Perm.nil
    1. Constructor of List.Perm
  248. List.Perm.swap
    1. Constructor of List.Perm
  249. List.Perm.trans
    1. Constructor of List.Perm
  250. List.Sublist
  251. List.Sublist.cons
    1. Constructor of List.Sublist
  252. List.Sublist.cons₂
    1. Constructor of List.Sublist
  253. List.Sublist.slnil
    1. Constructor of List.Sublist
  254. List.all
  255. List.all­M
  256. List.and
  257. List.any
  258. List.any­M
  259. List.append
  260. List.append­TR
  261. List.as­String
  262. List.attach
  263. List.attach­With
  264. List.beq
  265. List.concat
  266. List.cons
    1. Constructor of List
  267. List.contains
  268. List.count
  269. List.count­P
  270. List.drop
  271. List.drop­Last
  272. List.drop­Last­TR
  273. List.drop­While
  274. List.elem
  275. List.erase
  276. List.erase­Dups
  277. List.erase­Idx
  278. List.erase­Idx­TR
  279. List.erase­P
  280. List.erase­PTR
  281. List.erase­Reps
  282. List.erase­TR
  283. List.extract
  284. List.filter
  285. List.filter­M
  286. List.filter­Map
  287. List.filter­Map­M
  288. List.filter­Map­TR
  289. List.filter­Rev­M
  290. List.filter­TR
  291. List.fin­Idx­Of?
  292. List.fin­Range
  293. List.find?
  294. List.find­Fin­Idx?
  295. List.find­Idx
  296. List.find­Idx?
  297. List.find­M?
  298. List.find­Some?
  299. List.find­Some­M?
  300. List.first­M
  301. List.flat­Map
  302. List.flat­Map­M
  303. List.flat­Map­TR
  304. List.flatten
  305. List.flatten­TR
  306. List.foldl
  307. List.foldl­M
  308. List.foldl­Rec­On
  309. List.foldr
  310. List.foldr­M
  311. List.foldr­Rec­On
  312. List.foldr­TR
  313. List.for­A
  314. List.for­M
  315. List.get
  316. List.get­D
  317. List.get­Last
  318. List.get­Last!
  319. List.get­Last?
  320. List.get­Last­D
  321. List.group­By­Key
  322. List.head
  323. List.head!
  324. List.head?
  325. List.head­D
  326. List.idx­Of
  327. List.idx­Of?
  328. List.insert
  329. List.insert­Idx
  330. List.insert­Idx­TR
  331. List.intercalate
  332. List.intercalate­TR
  333. List.intersperse
  334. List.intersperse­TR
  335. List.is­Empty
  336. List.is­Eqv
  337. List.is­Perm
  338. List.is­Prefix­Of
  339. List.is­Prefix­Of?
  340. List.is­Sublist
  341. List.is­Suffix­Of
  342. List.is­Suffix­Of?
  343. List.le
  344. List.leftpad
  345. List.leftpad­TR
  346. List.length
  347. List.length­TR
  348. List.lex
  349. List.lookup
  350. List.lt
  351. List.map
  352. List.map­A
  353. List.map­Fin­Idx
  354. List.map­Fin­Idx­M
  355. List.map­Idx
  356. List.map­Idx­M
  357. List.map­M
  358. List.map­M'
  359. List.map­Mono
  360. List.map­Mono­M
  361. List.map­TR
  362. List.max?
  363. List.merge
  364. List.merge­Sort
  365. List.min?
  366. List.modify
  367. List.modify­Head
  368. List.modify­TR
  369. List.modify­Tail­Idx
  370. List.nil
    1. Constructor of List
  371. List.of­Fn
  372. List.or
  373. List.partition
  374. List.partition­M
  375. List.partition­Map
  376. List.pmap
  377. List.range
  378. List.range'
  379. List.range'TR
  380. List.remove­All
  381. List.replace
  382. List.replace­TR
  383. List.replicate
  384. List.replicate­TR
  385. List.reverse
  386. List.rightpad
  387. List.rotate­Left
  388. List.rotate­Right
  389. List.set
  390. List.set­TR
  391. List.singleton
  392. List.span
  393. List.split­At
  394. List.split­By
  395. List.sum
  396. List.tail
  397. List.tail!
  398. List.tail?
  399. List.tail­D
  400. List.take
  401. List.take­TR
  402. List.take­While
  403. List.take­While­TR
  404. List.to­Array
  405. List.to­Array­Impl
  406. List.to­Byte­Array
  407. List.to­Float­Array
  408. List.to­String
  409. List.unattach
  410. List.unzip
  411. List.unzip­TR
  412. List.zip
  413. List.zip­Idx
  414. List.zip­Idx­TR
  415. List.zip­With
  416. List.zip­With­All
  417. List.zip­With­TR
  418. land
    1. Fin.land
  419. land
    1. ISize.land
  420. land
    1. Int16.land
  421. land
    1. Int32.land
  422. land
    1. Int64.land
  423. land
    1. Int8.land
  424. land
    1. Nat.land
  425. land
    1. UInt16.land
  426. land
    1. UInt32.land
  427. land
    1. UInt64.land
  428. land
    1. UInt8.land
  429. land
    1. USize.land
  430. last
    1. Fin.last
  431. last­Cases
    1. Fin.last­Cases
  432. lazy­Pure
    1. IO.lazy­Pure
  433. lcm
    1. Int.lcm
  434. lcm
    1. Nat.lcm
  435. le
    1. Char.le
  436. le
    1. Float.le
  437. le
    1. Float32.le
  438. le
    1. ISize.le
  439. le
    1. Int.le
  440. le
    1. Int16.le
  441. le
    1. Int32.le
  442. le
    1. Int64.le
  443. le
    1. Int8.le
  444. le
    1. LE.le (class method)
  445. le
    1. List.le
  446. le
    1. Nat.le
  447. le
    1. String.le
  448. le
    1. UInt16.le
  449. le
    1. UInt32.le
  450. le
    1. UInt64.le
  451. le
    1. UInt8.le
  452. le
    1. USize.le
  453. le­Of­Ord
  454. lean (Lake command)
  455. lean_is_array
  456. lean_is_string
  457. lean_string_object (0) (1)
  458. lean_to_array
  459. lean_to_string
  460. left (0) (1)
  461. left
    1. And.left (structure field)
  462. left_distrib
    1. Lean.Grind.Semiring.mul_one (class method)
  463. leftpad
    1. Array.leftpad
  464. leftpad
    1. List.leftpad
  465. leftpad­TR
    1. List.leftpad­TR
  466. length
    1. List.length
  467. length
    1. String.length
  468. length­TR
    1. List.length­TR
  469. let
  470. let rec
  471. let'
  472. let­I
  473. let­To­Have
    1. Lean.Meta.Simp.Config.let­To­Have (structure field)
  474. level
    1. of universe
  475. lex'
    1. Ord.lex'
  476. lex
    1. Array.lex
  477. lex
    1. List.lex
  478. lex
    1. Ord.lex
  479. lex­Lt
    1. Prod.lex­Lt
  480. lhs
  481. lib­Name
    1. [anonymous] (structure field)
  482. lib­Prefix­On­Windows
    1. [anonymous] (structure field)
  483. lift
    1. Except­CpsT.lift
  484. lift
    1. ExceptT.lift
  485. lift
    1. OptionT.lift
  486. lift
    1. Quot.lift
  487. lift
    1. Quotient.lift
  488. lift
    1. Squash.lift
  489. lift
    1. State­CpsT.lift
  490. lift
    1. State­RefT'.lift
  491. lift
    1. StateT.lift
  492. lift­On
    1. Quot.lift­On
  493. lift­On
    1. Quotient.lift­On
  494. lift­On₂
    1. Quotient.lift­On₂
  495. lift­With
    1. MonadControl.lift­With (class method)
  496. lift­With
    1. Monad­ControlT.lift­With (class method)
  497. lift₂
    1. Quotient.lift₂
  498. line­Eq
  499. lines
    1. IO.FS.lines
  500. lint (Lake command)
  501. linter.unnecessary­Simpa
  502. literal
    1. raw string
  503. literal
    1. string
  504. lock
    1. IO.FS.Handle.lock
  505. log
    1. Float.log
  506. log
    1. Float32.log
  507. log10
    1. Float.log10
  508. log10
    1. Float32.log10
  509. log2
    1. Fin.log2
  510. log2
    1. Float.log2
  511. log2
    1. Float32.log2
  512. log2
    1. Nat.log2
  513. log2
    1. UInt16.log2
  514. log2
    1. UInt32.log2
  515. log2
    1. UInt64.log2
  516. log2
    1. UInt8.log2
  517. log2
    1. USize.log2
  518. lookup
    1. List.lookup
  519. lor
    1. Fin.lor
  520. lor
    1. ISize.lor
  521. lor
    1. Int16.lor
  522. lor
    1. Int32.lor
  523. lor
    1. Int64.lor
  524. lor
    1. Int8.lor
  525. lor
    1. Nat.lor
  526. lor
    1. UInt16.lor
  527. lor
    1. UInt32.lor
  528. lor
    1. UInt64.lor
  529. lor
    1. UInt8.lor
  530. lor
    1. USize.lor
  531. lt
    1. Char.lt
  532. lt
    1. Float.lt
  533. lt
    1. Float32.lt
  534. lt
    1. ISize.lt
  535. lt
    1. Int.lt
  536. lt
    1. Int16.lt
  537. lt
    1. Int32.lt
  538. lt
    1. Int64.lt
  539. lt
    1. Int8.lt
  540. lt
    1. LT.lt (class method)
  541. lt
    1. List.lt
  542. lt
    1. Nat.lt
  543. lt
    1. Option.lt
  544. lt
    1. UInt16.lt
  545. lt
    1. UInt32.lt
  546. lt
    1. UInt64.lt
  547. lt
    1. UInt8.lt
  548. lt
    1. USize.lt
  549. 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.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. mleft
  201. mod
    1. Fin.mod
  202. mod
    1. ISize.mod
  203. mod
    1. Int16.mod
  204. mod
    1. Int32.mod
  205. mod
    1. Int64.mod
  206. mod
    1. Int8.mod
  207. mod
    1. Mod.mod (class method)
  208. mod
    1. Nat.mod
  209. mod
    1. UInt16.mod
  210. mod
    1. UInt32.mod
  211. mod
    1. UInt64.mod
  212. mod
    1. UInt8.mod
  213. mod
    1. USize.mod
  214. mod­Core
    1. Nat.mod­Core
  215. modified
    1. IO.FS.Metadata.modified (structure field)
  216. modify
  217. modify
    1. Array.modify
  218. modify
    1. List.modify
  219. modify
    1. ST.Ref.modify
  220. modify
    1. Std.DHashMap.modify
  221. modify
    1. Std.DTreeMap.modify
  222. modify
    1. Std.Ext­DHashMap.modify
  223. modify
    1. Std.Ext­HashMap.modify
  224. modify
    1. Std.HashMap.modify
  225. modify
    1. Std.TreeMap.modify
  226. modify
    1. String.modify
  227. modify­Get
    1. EStateM.modify­Get
  228. modify­Get
    1. MonadState.modify­Get
  229. modify­Get
    1. MonadState.modify­Get (class method)
  230. modify­Get
    1. Monad­StateOf.modify­Get (class method)
  231. modify­Get
    1. ST.Ref.modify­Get
  232. modify­Get
    1. State­RefT'.modify­Get
  233. modify­Get
    1. StateT.modify­Get
  234. modify­Get­The
  235. modify­Head
    1. List.modify­Head
  236. modify­M
    1. Array.modify­M
  237. modify­Op
    1. Array.modify­Op
  238. modify­TR
    1. List.modify­TR
  239. modify­Tail­Idx
    1. List.modify­Tail­Idx
  240. modify­The
  241. modn
    1. Fin.modn
  242. monad­Eval
    1. MonadEval.monad­Eval (class method)
  243. monad­Eval
    1. Monad­EvalT.monad­Eval (class method)
  244. monad­Lift
    1. MonadLift.monad­Lift (class method)
  245. monad­Lift
    1. Monad­LiftT.monad­Lift (class method)
  246. monad­Map
    1. MonadFunctor.monad­Map (class method)
  247. monad­Map
    1. Monad­FunctorT.monad­Map (class method)
  248. mono­Ms­Now
    1. IO.mono­Ms­Now
  249. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  250. monotone
    1. Lean.Order.monotone
  251. mp
    1. Eq.mp
  252. mp
    1. Iff.mp (structure field)
  253. mpr
    1. Eq.mpr
  254. mpr
    1. Iff.mpr (structure field)
  255. mpure
  256. mpure_intro
  257. mrefine
  258. mreplace
  259. mright
  260. msb
    1. BitVec.msb
  261. mspec
  262. mspecialize
  263. mspecialize_pure
  264. mstart
  265. mstop
  266. mul
    1. BitVec.mul
  267. mul
    1. Fin.mul
  268. mul
    1. Float.mul
  269. mul
    1. Float32.mul
  270. mul
    1. ISize.mul
  271. mul
    1. Int.mul
  272. mul
    1. Int16.mul
  273. mul
    1. Int32.mul
  274. mul
    1. Int64.mul
  275. mul
    1. Int8.mul
  276. mul
    1. Mul.mul (class method)
  277. mul
    1. Nat.mul
  278. mul
    1. UInt16.mul
  279. mul
    1. UInt32.mul
  280. mul
    1. UInt64.mul
  281. mul
    1. UInt8.mul
  282. mul
    1. USize.mul
  283. mul­Rec
    1. BitVec.mul­Rec
  284. mul_assoc
    1. Lean.Grind.Semiring.add_comm (class method)
  285. mul_comm
    1. [anonymous] (class method) (0) (1)
  286. mul_inv_cancel
    1. [anonymous] (class method)
  287. mul_lt_mul_of_pos_left
    1. Lean.Grind.OrderedRing.zero_lt_one (class method)
  288. mul_lt_mul_of_pos_right
    1. Lean.Grind.OrderedRing.mul_lt_mul_of_pos_left (class method)
  289. mul_one
    1. Lean.Grind.Semiring.add_assoc (class method)
  290. mul_zero
    1. Lean.Grind.Semiring.right_distrib (class method)
  291. mvars
    1. pp.mvars
  292. 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.next'
  141. next
    1. RandomGen.next (class method)
  142. next
    1. String.Iterator.next
  143. next
    1. String.next
  144. next
    1. Substring.next
  145. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  146. next­Until
    1. String.next­Until
  147. next­While
    1. String.next­While
  148. nextn
    1. String.Iterator.nextn
  149. nextn
    1. Substring.nextn
  150. nil
    1. BitVec.nil
  151. no_nat_zero_divisors
    1. Lean.Grind.No­Nat­ZeroDivisors.no_nat_zero_divisors (class method)
  152. nofun
  153. nomatch
  154. non­Backtrackable
    1. EStateM.non­Backtrackable
  155. norm_cast (0) (1)
  156. normalize
    1. System.FilePath.normalize
  157. not
    1. BitVec.not
  158. not
    1. Bool.not
  159. not
    1. Int.not
  160. not­M
  161. notify­All
    1. Std.Condvar.notify­All
  162. notify­One
    1. Std.Condvar.notify­One
  163. npow
    1. Lean.Grind.Semiring.of­Nat (class method)
  164. nsmul
    1. Lean.Grind.Semiring.nat­Cast (class method)
  165. nsmul
    1. [anonymous] (class method) (0) (1)
  166. nsmul_eq_nat­Cast_mul
    1. Lean.Grind.Semiring.of­Nat_succ (class method)
  167. null­Kind
    1. Lean.null­Kind
  168. num­Bits
    1. System.Platform.num­Bits
  169. num­Lit­Kind
    1. Lean.num­Lit­Kind

O

  1. Occurrences
    1. Lean.Meta.Occurrences
  2. Of­Nat
  3. OfNat.mk
    1. Instance constructor of Of­Nat
  4. Of­Scientific
  5. OfScientific.mk
    1. Instance constructor of Of­Scientific
  6. Option
  7. Option.all
  8. Option.any
  9. Option.attach
  10. Option.attach­With
  11. Option.bind
  12. Option.bind­M
  13. Option.choice
  14. Option.decidable­Eq­None
  15. Option.elim
  16. Option.elim­M
  17. Option.filter
  18. Option.for­M
  19. Option.format
  20. Option.get
  21. Option.get!
  22. Option.get­D
  23. Option.get­DM
  24. Option.get­M
  25. Option.guard
  26. Option.is­Eq­Some
  27. Option.is­None
  28. Option.is­Some
  29. Option.join
  30. Option.lt
  31. Option.map
  32. Option.map­A
  33. Option.map­M
  34. Option.max
  35. Option.merge
  36. Option.min
  37. Option.none
    1. Constructor of Option
  38. Option.or
  39. Option.or­Else
  40. Option.pbind
  41. Option.pelim
  42. Option.pmap
  43. Option.repr
  44. Option.sequence
  45. Option.some
    1. Constructor of Option
  46. Option.to­Array
  47. Option.to­List
  48. Option.try­Catch
  49. Option.unattach
  50. Option­T
  51. OptionT.bind
  52. OptionT.fail
  53. OptionT.lift
  54. OptionT.mk
  55. OptionT.or­Else
  56. OptionT.pure
  57. OptionT.run
  58. OptionT.try­Catch
  59. Or
  60. Or.by_cases
  61. Or.by_cases'
  62. Or.inl
    1. Constructor of Or
  63. Or.inr
    1. Constructor of Or
  64. Ord
  65. Ord.lex
  66. Ord.lex'
  67. Ord.mk
    1. Instance constructor of Ord
  68. Ord.on
  69. Ord.opposite
  70. Ord.to­BEq
  71. Ord.to­LE
  72. Ord.to­LT
  73. Ordered­Add
    1. Lean.Grind.Ordered­Add
  74. Ordered­Ring
    1. Lean.Grind.Ordered­Ring
  75. Ordering
  76. Ordering.eq
    1. Constructor of Ordering
  77. Ordering.gt
    1. Constructor of Ordering
  78. Ordering.is­Eq
  79. Ordering.is­GE
  80. Ordering.is­GT
  81. Ordering.is­LE
  82. Ordering.is­LT
  83. Ordering.is­Ne
  84. Ordering.lt
    1. Constructor of Ordering
  85. Ordering.swap
  86. Ordering.then
  87. Output
    1. IO.Process.Output
  88. obtain
  89. occs
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  90. of­Array
    1. Std.Ext­HashSet.of­Array
  91. of­Array
    1. Std.HashSet.of­Array
  92. of­Array
    1. Std.TreeMap.of­Array
  93. of­Array
    1. Std.TreeSet.of­Array
  94. of­Binary­Scientific
    1. Float.of­Binary­Scientific
  95. of­Binary­Scientific
    1. Float32.of­Binary­Scientific
  96. of­Bit­Vec
    1. ISize.of­Bit­Vec
  97. of­Bit­Vec
    1. Int16.of­Bit­Vec
  98. of­Bit­Vec
    1. Int32.of­Bit­Vec
  99. of­Bit­Vec
    1. Int64.of­Bit­Vec
  100. of­Bit­Vec
    1. Int8.of­Bit­Vec
  101. of­Bits
    1. Float.of­Bits
  102. of­Bits
    1. Float32.of­Bits
  103. of­Bool
    1. BitVec.of­Bool
  104. of­Bool­List­BE
    1. BitVec.of­Bool­List­BE
  105. of­Bool­List­LE
    1. BitVec.of­Bool­List­LE
  106. of­Buffer
    1. IO.FS.Stream.of­Buffer
  107. of­Except
    1. IO.of­Except
  108. of­Except
    1. MonadExcept.of­Except
  109. of­Fin
    1. UInt16.of­Fin
  110. of­Fin
    1. UInt32.of­Fin
  111. of­Fin
    1. UInt64.of­Fin
  112. of­Fin
    1. UInt8.of­Fin
  113. of­Fin
    1. USize.of­Fin
  114. of­Fn
    1. Array.of­Fn
  115. of­Fn
    1. List.of­Fn
  116. of­Handle
    1. IO.FS.Stream.of­Handle
  117. of­Int
    1. BitVec.of­Int
  118. of­Int
    1. Float.of­Int
  119. of­Int
    1. Float32.of­Int
  120. of­Int
    1. ISize.of­Int
  121. of­Int
    1. Int16.of­Int
  122. of­Int
    1. Int32.of­Int
  123. of­Int
    1. Int64.of­Int
  124. of­Int
    1. Int8.of­Int
  125. of­Int­LE
    1. ISize.of­Int­LE
  126. of­Int­LE
    1. Int16.of­Int­LE
  127. of­Int­LE
    1. Int32.of­Int­LE
  128. of­Int­LE
    1. Int64.of­Int­LE
  129. of­Int­LE
    1. Int8.of­Int­LE
  130. of­Int­Truncate
    1. ISize.of­Int­Truncate
  131. of­Int­Truncate
    1. Int16.of­Int­Truncate
  132. of­Int­Truncate
    1. Int32.of­Int­Truncate
  133. of­Int­Truncate
    1. Int64.of­Int­Truncate
  134. of­Int­Truncate
    1. Int8.of­Int­Truncate
  135. of­List
    1. Std.DHashMap.of­List
  136. of­List
    1. Std.DTreeMap.of­List
  137. of­List
    1. Std.Ext­DHashMap.of­List
  138. of­List
    1. Std.Ext­HashMap.of­List
  139. of­List
    1. Std.Ext­HashSet.of­List
  140. of­List
    1. Std.HashMap.of­List
  141. of­List
    1. Std.HashSet.of­List
  142. of­List
    1. Std.TreeMap.of­List
  143. of­List
    1. Std.TreeSet.of­List
  144. of­Nat
    1. BitVec.of­Nat
  145. of­Nat
    1. Char.of­Nat
  146. of­Nat
    1. Fin.of­Nat
  147. of­Nat
    1. Float.of­Nat
  148. of­Nat
    1. Float32.of­Nat
  149. of­Nat
    1. ISize.of­Nat
  150. of­Nat
    1. Int16.of­Nat
  151. of­Nat
    1. Int32.of­Nat
  152. of­Nat
    1. Int64.of­Nat
  153. of­Nat
    1. Int8.of­Nat
  154. of­Nat
    1. OfNat.of­Nat (class method)
  155. of­Nat
    1. UInt16.of­Nat
  156. of­Nat
    1. UInt32.of­Nat
  157. of­Nat
    1. UInt64.of­Nat
  158. of­Nat
    1. UInt8.of­Nat
  159. of­Nat
    1. USize.of­Nat
  160. of­Nat
    1. [anonymous] (class method)
  161. of­Nat32
    1. USize.of­Nat32
  162. of­Nat­LT
    1. BitVec.of­Nat­LT
  163. of­Nat­LT
    1. UInt16.of­Nat­LT
  164. of­Nat­LT
    1. UInt32.of­Nat­LT
  165. of­Nat­LT
    1. UInt64.of­Nat­LT
  166. of­Nat­LT
    1. UInt8.of­Nat­LT
  167. of­Nat­LT
    1. USize.of­Nat­LT
  168. of­Nat­Truncate
    1. UInt16.of­Nat­Truncate
  169. of­Nat­Truncate
    1. UInt32.of­Nat­Truncate
  170. of­Nat­Truncate
    1. UInt64.of­Nat­Truncate
  171. of­Nat­Truncate
    1. UInt8.of­Nat­Truncate
  172. of­Nat­Truncate
    1. USize.of­Nat­Truncate
  173. of­Nat_eq_nat­Cast
    1. Lean.Grind.Semiring.pow_succ (class method)
  174. of­Nat_ext_iff
    1. Lean.Grind.Is­CharP.of­Nat_ext_iff (class method)
  175. of­Nat_succ
    1. Lean.Grind.Semiring.pow_zero (class method)
  176. of­Scientific
    1. Float.of­Scientific
  177. of­Scientific
    1. Float32.of­Scientific
  178. of­Scientific
    1. OfScientific.of­Scientific (class method)
  179. of­Subarray
    1. Array.of­Subarray
  180. of­UInt8
    1. Char.of­UInt8
  181. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  182. offset­Of­Pos
    1. String.offset­Of­Pos
  183. omega
  184. on
    1. Ord.on
  185. one_mul
    1. Lean.Grind.Semiring.mul_assoc (class method)
  186. one_zsmul
    1. [anonymous] (class method)
  187. open
  188. opposite
    1. Ord.opposite
  189. opt­Param
  190. optional
  191. or
    1. BitVec.or
  192. or
    1. Bool.or
  193. or
    1. List.or
  194. or
    1. Option.or
  195. or­Else'
    1. EStateM.or­Else'
  196. or­Else
    1. EStateM.or­Else
  197. or­Else
    1. MonadExcept.or­Else
  198. or­Else
    1. Option.or­Else
  199. or­Else
    1. OptionT.or­Else
  200. or­Else
    1. ReaderT.or­Else
  201. or­Else
    1. StateT.or­Else
  202. or­Else
    1. [anonymous] (class method)
  203. or­Else­Lazy
    1. Except.or­Else­Lazy
  204. or­M
  205. orelse'
    1. MonadExcept.orelse'
  206. other
    1. IO.FileRight.other (structure field)
  207. out
    1. NeZero.out (class method)
  208. out
    1. Std.DTreeMap.Raw.WF.out (structure field)
  209. out
    1. Std.HashMap.Raw.WF.out (structure field)
  210. out
    1. Std.HashSet.Raw.WF.out (structure field)
  211. out
    1. Std.TreeMap.Raw.WF.out (structure field)
  212. out
    1. Std.TreeSet.Raw.WF.out (structure field)
  213. out­Param
  214. output
    1. IO.Process.output
  215. override list (Elan command)
  216. override set (Elan command)
  217. override unset (Elan command)

P

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

U

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

V

  1. val
    1. Char.val (structure field)
  2. val
    1. Fin.val (structure field)
  3. val
    1. Subtype.val (structure field)
  4. valid
    1. Char.valid (structure field)
  5. validate­UTF8
    1. String.validate­UTF8
  6. value
    1. For­InStep.value
  7. value
    1. 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
    1. BitVec.xor
  2. xor
    1. Bool.xor
  3. xor
    1. Fin.xor
  4. xor
    1. ISize.xor
  5. xor
    1. Int16.xor
  6. xor
    1. Int32.xor
  7. xor
    1. Int64.xor
  8. xor
    1. Int8.xor
  9. xor
    1. Nat.xor
  10. xor
    1. UInt16.xor
  11. xor
    1. UInt32.xor
  12. xor
    1. UInt64.xor
  13. xor
    1. UInt8.xor
  14. xor
    1. USize.xor

Z

  1. Zero
  2. Zero.mk
    1. Instance constructor of Zero
  3. zero
    1. BitVec.zero
  4. zero
    1. Zero.zero (class method)
  5. zero­Extend
    1. BitVec.zero­Extend
  6. 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)