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.nsmul (class method)
  197. add_comm
    1. Lean.Grind.Semiring.of­Nat (class method)
  198. add_le_left_iff
    1. Lean.Grind.OrderedAdd.add_le_left_iff (class method)
  199. add_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.nat­Cast (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. bitwise
    1. Nat.bitwise
  163. ble
    1. Nat.ble
  164. blt
    1. Nat.blt
  165. bmod
    1. Int.bmod
  166. bootstrap.inductive­Check­Resulting­Universe
  167. bracket
    1. Std.Format.bracket
  168. bracket­Fill
    1. Std.Format.bracket­Fill
  169. bsize
    1. Substring.bsize
  170. buckets
    1. Std.DHashMap.Raw.buckets (structure field)
  171. build (Lake command)
  172. bv_check
  173. bv_decide
  174. bv_decide?
  175. bv_normalize
  176. bv_omega
  177. by­Cases
    1. Decidable.by­Cases
  178. by_cases
  179. by_cases'
    1. Or.by_cases'
  180. by_cases
    1. Or.by_cases
  181. byte­Idx
    1. String.Pos.byte­Idx (structure field)
  182. 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­Fun
  152. cons
    1. BitVec.cons
  153. const
    1. Function.const
  154. constructor (0) (1)
  155. contains
    1. Array.contains
  156. contains
    1. List.contains
  157. contains
    1. Std.DHashMap.contains
  158. contains
    1. Std.DTreeMap.contains
  159. contains
    1. Std.Ext­DHashMap.contains
  160. contains
    1. Std.Ext­HashMap.contains
  161. contains
    1. Std.Ext­HashSet.contains
  162. contains
    1. Std.HashMap.contains
  163. contains
    1. Std.HashSet.contains
  164. contains
    1. Std.TreeMap.contains
  165. contains
    1. Std.TreeSet.contains
  166. contains
    1. String.contains
  167. contains
    1. Substring.contains
  168. contains­Then­Insert
    1. Std.DHashMap.contains­Then­Insert
  169. contains­Then­Insert
    1. Std.DTreeMap.contains­Then­Insert
  170. contains­Then­Insert
    1. Std.Ext­DHashMap.contains­Then­Insert
  171. contains­Then­Insert
    1. Std.Ext­HashMap.contains­Then­Insert
  172. contains­Then­Insert
    1. Std.Ext­HashSet.contains­Then­Insert
  173. contains­Then­Insert
    1. Std.HashMap.contains­Then­Insert
  174. contains­Then­Insert
    1. Std.HashSet.contains­Then­Insert
  175. contains­Then­Insert
    1. Std.TreeMap.contains­Then­Insert
  176. contains­Then­Insert
    1. Std.TreeSet.contains­Then­Insert
  177. contains­Then­Insert­If­New
    1. Std.DHashMap.contains­Then­Insert­If­New
  178. contains­Then­Insert­If­New
    1. Std.DTreeMap.contains­Then­Insert­If­New
  179. contains­Then­Insert­If­New
    1. Std.Ext­DHashMap.contains­Then­Insert­If­New
  180. contains­Then­Insert­If­New
    1. Std.Ext­HashMap.contains­Then­Insert­If­New
  181. contains­Then­Insert­If­New
    1. Std.HashMap.contains­Then­Insert­If­New
  182. contains­Then­Insert­If­New
    1. Std.TreeMap.contains­Then­Insert­If­New
  183. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  184. contradiction
  185. control
  186. control­At
  187. conv
  188. conv => ...
  189. conv' (0) (1)
  190. cos
    1. Float.cos
  191. cos
    1. Float32.cos
  192. cosh
    1. Float.cosh
  193. cosh
    1. Float32.cosh
  194. count
    1. Array.count
  195. count
    1. List.count
  196. count­P
    1. Array.count­P
  197. count­P
    1. List.count­P
  198. create­Dir
    1. IO.FS.create­Dir
  199. create­Dir­All
    1. IO.FS.create­Dir­All
  200. create­Temp­Dir
    1. IO.FS.create­Temp­Dir
  201. create­Temp­File
    1. IO.FS.create­Temp­File
  202. crlf­To­Lf
    1. String.crlf­To­Lf
  203. csup
    1. [anonymous] (class method)
  204. csup_spec
    1. [anonymous] (class method)
  205. cumulativity
  206. curr
    1. String.Iterator.curr
  207. curr­Column
    1. Std.Format.Monad­PrettyFormat.curr­Column (class method)
  208. current­Dir
    1. IO.current­Dir
  209. curry
    1. Function.curry
  210. custom­Eliminators
    1. tactic.custom­Eliminators
  211. 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.Linear­Order
  109. Lean.Grind.LinearOrder.mk
    1. Instance constructor of Lean.Grind.Linear­Order
  110. Lean.Grind.Nat­Module
  111. Lean.Grind.NatModule.mk
    1. Instance constructor of Lean.Grind.Nat­Module
  112. Lean.Grind.No­Nat­Zero­Divisors
  113. Lean.Grind.No­Nat­ZeroDivisors.mk'
  114. Lean.Grind.No­Nat­ZeroDivisors.mk
    1. Instance constructor of Lean.Grind.No­Nat­Zero­Divisors
  115. Lean.Grind.Ordered­Add
  116. Lean.Grind.OrderedAdd.mk
    1. Instance constructor of Lean.Grind.Ordered­Add
  117. Lean.Grind.Ordered­Ring
  118. Lean.Grind.OrderedRing.mk
    1. Instance constructor of Lean.Grind.Ordered­Ring
  119. Lean.Grind.Partial­Order
  120. Lean.Grind.PartialOrder.mk
    1. Instance constructor of Lean.Grind.Partial­Order
  121. Lean.Grind.Preorder
  122. Lean.Grind.Preorder.mk
    1. Instance constructor of Lean.Grind.Preorder
  123. Lean.Grind.Ring
  124. Lean.Grind.Ring.mk
    1. Instance constructor of Lean.Grind.Ring
  125. Lean.Grind.Semiring
  126. Lean.Grind.Semiring.mk
    1. Instance constructor of Lean.Grind.Semiring
  127. Lean.Grind.To­Int
  128. Lean.Grind.ToInt.mk
    1. Instance constructor of Lean.Grind.To­Int
  129. Lean.Lean­Option
  130. Lean.LeanOption.mk
    1. Constructor of Lean.Lean­Option
  131. Lean.Macro.Exception.unsupported­Syntax
  132. Lean.Macro.add­Macro­Scope
  133. Lean.Macro.expand­Macro?
  134. Lean.Macro.get­Curr­Namespace
  135. Lean.Macro.has­Decl
  136. Lean.Macro.resolve­Global­Name
  137. Lean.Macro.resolve­Namespace
  138. Lean.Macro.throw­Error
  139. Lean.Macro.throw­Error­At
  140. Lean.Macro.throw­Unsupported
  141. Lean.Macro.trace
  142. Lean.Macro.with­Fresh­Macro­Scope
  143. Lean.Macro­M
  144. Lean.Meta.DSimp.Config
  145. Lean.Meta.DSimp.Config.mk
    1. Constructor of Lean.Meta.DSimp.Config
  146. Lean.Meta.Occurrences
  147. Lean.Meta.Occurrences.all
    1. Constructor of Lean.Meta.Occurrences
  148. Lean.Meta.Occurrences.neg
    1. Constructor of Lean.Meta.Occurrences
  149. Lean.Meta.Occurrences.pos
    1. Constructor of Lean.Meta.Occurrences
  150. Lean.Meta.Rewrite.Config
  151. Lean.Meta.Rewrite.Config.mk
    1. Constructor of Lean.Meta.Rewrite.Config
  152. Lean.Meta.Rewrite.New­Goals
  153. Lean.Meta.Simp.Config
  154. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  155. Lean.Meta.Simp.neutral­Config
  156. Lean.Meta.Simp­Extension
  157. Lean.Meta.Transparency­Mode
  158. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.Transparency­Mode
  159. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.Transparency­Mode
  160. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.Transparency­Mode
  161. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.Transparency­Mode
  162. Lean.Meta.register­Simp­Attr
  163. Lean.Order.CCPO
  164. Lean.Order.CCPO.mk
    1. Instance constructor of Lean.Order.CCPO
  165. Lean.Order.Partial­Order
  166. Lean.Order.PartialOrder.mk
    1. Instance constructor of Lean.Order.Partial­Order
  167. Lean.Order.fix
  168. Lean.Order.fix_eq
  169. Lean.Order.monotone
  170. Lean.Parser.Leading­Ident­Behavior
  171. Lean.Parser.Leading­IdentBehavior.both
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  172. Lean.Parser.Leading­IdentBehavior.default
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  173. Lean.Parser.Leading­IdentBehavior.symbol
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  174. Lean.PrettyPrinter.Unexpand­M
  175. Lean.PrettyPrinter.Unexpander
  176. Lean.Source­Info
  177. Lean.SourceInfo.none
    1. Constructor of Lean.Source­Info
  178. Lean.SourceInfo.original
    1. Constructor of Lean.Source­Info
  179. Lean.SourceInfo.synthetic
    1. Constructor of Lean.Source­Info
  180. Lean.Syntax
  181. Lean.Syntax.Char­Lit
  182. Lean.Syntax.Command
  183. Lean.Syntax.Hygiene­Info
  184. Lean.Syntax.Ident
  185. Lean.Syntax.Level
  186. Lean.Syntax.Name­Lit
  187. Lean.Syntax.Num­Lit
  188. Lean.Syntax.Prec
  189. Lean.Syntax.Preresolved
  190. Lean.Syntax.Preresolved.decl
    1. Constructor of Lean.Syntax.Preresolved
  191. Lean.Syntax.Preresolved.namespace
    1. Constructor of Lean.Syntax.Preresolved
  192. Lean.Syntax.Prio
  193. Lean.Syntax.Scientific­Lit
  194. Lean.Syntax.Str­Lit
  195. Lean.Syntax.TSep­Array
  196. Lean.Syntax.TSepArray.mk
    1. Constructor of Lean.Syntax.TSep­Array
  197. Lean.Syntax.Tactic
  198. Lean.Syntax.Term
  199. Lean.Syntax.atom
    1. Constructor of Lean.Syntax
  200. Lean.Syntax.get­Kind
  201. Lean.Syntax.ident
    1. Constructor of Lean.Syntax
  202. Lean.Syntax.is­Of­Kind
  203. Lean.Syntax.missing
    1. Constructor of Lean.Syntax
  204. Lean.Syntax.node
    1. Constructor of Lean.Syntax
  205. Lean.Syntax.set­Kind
  206. Lean.Syntax­Node­Kind
  207. Lean.Syntax­Node­Kinds
  208. Lean.TSyntax
  209. Lean.TSyntax.get­Char
  210. Lean.TSyntax.get­Hygiene­Info
  211. Lean.TSyntax.get­Id
  212. Lean.TSyntax.get­Name
  213. Lean.TSyntax.get­Nat
  214. Lean.TSyntax.get­Scientific
  215. Lean.TSyntax.get­String
  216. Lean.TSyntax.mk
    1. Constructor of Lean.TSyntax
  217. Lean.TSyntax­Array
  218. Lean.char­Lit­Kind
  219. Lean.choice­Kind
  220. Lean.field­Idx­Kind
  221. Lean.group­Kind
  222. Lean.hygiene­Info­Kind
  223. Lean.ident­Kind
  224. Lean.interpolated­Str­Kind
  225. Lean.interpolated­Str­Lit­Kind
  226. Lean.name­Lit­Kind
  227. Lean.null­Kind
  228. Lean.num­Lit­Kind
  229. Lean.scientific­Lit­Kind
  230. Lean.str­Lit­Kind
  231. Lean­Exe­Config
    1. Lake.Lean­Exe­Config
  232. Lean­Lib­Config
    1. Lake.Lean­Lib­Config
  233. Lean­Option
    1. Lean.Lean­Option
  234. Level
    1. Lean.Syntax.Level
  235. Lex
    1. List.Lex
  236. Linear­Order
    1. Lean.Grind.Linear­Order
  237. List
  238. List.Is­Infix
  239. List.Is­Prefix
  240. List.Is­Suffix
  241. List.Lex
  242. List.Lex.cons
    1. Constructor of List.Lex
  243. List.Lex.nil
    1. Constructor of List.Lex
  244. List.Lex.rel
    1. Constructor of List.Lex
  245. List.Mem
  246. List.Mem.head
    1. Constructor of List.Mem
  247. List.Mem.tail
    1. Constructor of List.Mem
  248. List.Nodup
  249. List.Pairwise
  250. List.Pairwise.cons
    1. Constructor of List.Pairwise
  251. List.Pairwise.nil
    1. Constructor of List.Pairwise
  252. List.Perm
  253. List.Perm.cons
    1. Constructor of List.Perm
  254. List.Perm.nil
    1. Constructor of List.Perm
  255. List.Perm.swap
    1. Constructor of List.Perm
  256. List.Perm.trans
    1. Constructor of List.Perm
  257. List.Sublist
  258. List.Sublist.cons
    1. Constructor of List.Sublist
  259. List.Sublist.cons₂
    1. Constructor of List.Sublist
  260. List.Sublist.slnil
    1. Constructor of List.Sublist
  261. List.all
  262. List.all­M
  263. List.and
  264. List.any
  265. List.any­M
  266. List.append
  267. List.append­TR
  268. List.as­String
  269. List.attach
  270. List.attach­With
  271. List.beq
  272. List.concat
  273. List.cons
    1. Constructor of List
  274. List.contains
  275. List.count
  276. List.count­P
  277. List.drop
  278. List.drop­Last
  279. List.drop­Last­TR
  280. List.drop­While
  281. List.elem
  282. List.erase
  283. List.erase­Dups
  284. List.erase­Idx
  285. List.erase­Idx­TR
  286. List.erase­P
  287. List.erase­PTR
  288. List.erase­Reps
  289. List.erase­TR
  290. List.extract
  291. List.filter
  292. List.filter­M
  293. List.filter­Map
  294. List.filter­Map­M
  295. List.filter­Map­TR
  296. List.filter­Rev­M
  297. List.filter­TR
  298. List.fin­Idx­Of?
  299. List.fin­Range
  300. List.find?
  301. List.find­Fin­Idx?
  302. List.find­Idx
  303. List.find­Idx?
  304. List.find­M?
  305. List.find­Some?
  306. List.find­Some­M?
  307. List.first­M
  308. List.flat­Map
  309. List.flat­Map­M
  310. List.flat­Map­TR
  311. List.flatten
  312. List.flatten­TR
  313. List.foldl
  314. List.foldl­M
  315. List.foldl­Rec­On
  316. List.foldr
  317. List.foldr­M
  318. List.foldr­Rec­On
  319. List.foldr­TR
  320. List.for­A
  321. List.for­M
  322. List.get
  323. List.get­D
  324. List.get­Last
  325. List.get­Last!
  326. List.get­Last?
  327. List.get­Last­D
  328. List.group­By­Key
  329. List.head
  330. List.head!
  331. List.head?
  332. List.head­D
  333. List.idx­Of
  334. List.idx­Of?
  335. List.insert
  336. List.insert­Idx
  337. List.insert­Idx­TR
  338. List.intercalate
  339. List.intercalate­TR
  340. List.intersperse
  341. List.intersperse­TR
  342. List.is­Empty
  343. List.is­Eqv
  344. List.is­Perm
  345. List.is­Prefix­Of
  346. List.is­Prefix­Of?
  347. List.is­Sublist
  348. List.is­Suffix­Of
  349. List.is­Suffix­Of?
  350. List.le
  351. List.leftpad
  352. List.leftpad­TR
  353. List.length
  354. List.length­TR
  355. List.lex
  356. List.lookup
  357. List.lt
  358. List.map
  359. List.map­A
  360. List.map­Fin­Idx
  361. List.map­Fin­Idx­M
  362. List.map­Idx
  363. List.map­Idx­M
  364. List.map­M
  365. List.map­M'
  366. List.map­Mono
  367. List.map­Mono­M
  368. List.map­TR
  369. List.max?
  370. List.merge
  371. List.merge­Sort
  372. List.min?
  373. List.modify
  374. List.modify­Head
  375. List.modify­TR
  376. List.modify­Tail­Idx
  377. List.nil
    1. Constructor of List
  378. List.of­Fn
  379. List.or
  380. List.partition
  381. List.partition­M
  382. List.partition­Map
  383. List.pmap
  384. List.range
  385. List.range'
  386. List.range'TR
  387. List.remove­All
  388. List.replace
  389. List.replace­TR
  390. List.replicate
  391. List.replicate­TR
  392. List.reverse
  393. List.rightpad
  394. List.rotate­Left
  395. List.rotate­Right
  396. List.set
  397. List.set­TR
  398. List.singleton
  399. List.span
  400. List.split­At
  401. List.split­By
  402. List.sum
  403. List.tail
  404. List.tail!
  405. List.tail?
  406. List.tail­D
  407. List.take
  408. List.take­TR
  409. List.take­While
  410. List.take­While­TR
  411. List.to­Array
  412. List.to­Array­Impl
  413. List.to­Byte­Array
  414. List.to­Float­Array
  415. List.to­String
  416. List.unattach
  417. List.unzip
  418. List.unzip­TR
  419. List.zip
  420. List.zip­Idx
  421. List.zip­Idx­TR
  422. List.zip­With
  423. List.zip­With­All
  424. List.zip­With­TR
  425. land
    1. Fin.land
  426. land
    1. ISize.land
  427. land
    1. Int16.land
  428. land
    1. Int32.land
  429. land
    1. Int64.land
  430. land
    1. Int8.land
  431. land
    1. Nat.land
  432. land
    1. UInt16.land
  433. land
    1. UInt32.land
  434. land
    1. UInt64.land
  435. land
    1. UInt8.land
  436. land
    1. USize.land
  437. last
    1. Fin.last
  438. last­Cases
    1. Fin.last­Cases
  439. lazy­Pure
    1. IO.lazy­Pure
  440. lcm
    1. Int.lcm
  441. lcm
    1. Nat.lcm
  442. le
    1. Char.le
  443. le
    1. Float.le
  444. le
    1. Float32.le
  445. le
    1. ISize.le
  446. le
    1. Int.le
  447. le
    1. Int16.le
  448. le
    1. Int32.le
  449. le
    1. Int64.le
  450. le
    1. Int8.le
  451. le
    1. LE.le (class method)
  452. le
    1. List.le
  453. le
    1. Nat.le
  454. le
    1. String.le
  455. le
    1. UInt16.le
  456. le
    1. UInt32.le
  457. le
    1. UInt64.le
  458. le
    1. UInt8.le
  459. le
    1. USize.le
  460. le­Of­Ord
  461. le_antisymm
    1. [anonymous] (class method)
  462. le_refl
    1. Lean.Grind.Preorder.to­LT (class method)
  463. le_total
    1. [anonymous] (class method)
  464. le_trans
    1. [anonymous] (class method)
  465. lean (Lake command)
  466. lean_is_array
  467. lean_is_string
  468. lean_string_object (0) (1)
  469. lean_to_array
  470. lean_to_string
  471. left (0) (1)
  472. left
    1. And.left (structure field)
  473. left_distrib
    1. Lean.Grind.Semiring.mul_assoc (class method)
  474. leftpad
    1. Array.leftpad
  475. leftpad
    1. List.leftpad
  476. leftpad­TR
    1. List.leftpad­TR
  477. length
    1. List.length
  478. length
    1. String.length
  479. length­TR
    1. List.length­TR
  480. let
  481. let rec
  482. let'
  483. let­I
  484. let­To­Have
    1. Lean.Meta.Simp.Config.let­To­Have (structure field)
  485. level
    1. of universe
  486. lex'
    1. Ord.lex'
  487. lex
    1. Array.lex
  488. lex
    1. List.lex
  489. lex
    1. Ord.lex
  490. lex­Lt
    1. Prod.lex­Lt
  491. lhs
  492. lib­Name
    1. [anonymous] (structure field)
  493. lift
    1. Except­CpsT.lift
  494. lift
    1. ExceptT.lift
  495. lift
    1. OptionT.lift
  496. lift
    1. Quot.lift
  497. lift
    1. Quotient.lift
  498. lift
    1. Squash.lift
  499. lift
    1. State­CpsT.lift
  500. lift
    1. State­RefT'.lift
  501. lift
    1. StateT.lift
  502. lift­On
    1. Quot.lift­On
  503. lift­On
    1. Quotient.lift­On
  504. lift­On₂
    1. Quotient.lift­On₂
  505. lift­With
    1. MonadControl.lift­With (class method)
  506. lift­With
    1. Monad­ControlT.lift­With (class method)
  507. lift₂
    1. Quotient.lift₂
  508. line­Eq
  509. lines
    1. IO.FS.lines
  510. lint (Lake command)
  511. linter.unnecessary­Simpa
  512. literal
    1. raw string
  513. literal
    1. string
  514. lock
    1. IO.FS.Handle.lock
  515. log
    1. Float.log
  516. log
    1. Float32.log
  517. log10
    1. Float.log10
  518. log10
    1. Float32.log10
  519. log2
    1. Fin.log2
  520. log2
    1. Float.log2
  521. log2
    1. Float32.log2
  522. log2
    1. Nat.log2
  523. log2
    1. UInt16.log2
  524. log2
    1. UInt32.log2
  525. log2
    1. UInt64.log2
  526. log2
    1. UInt8.log2
  527. log2
    1. USize.log2
  528. lookup
    1. List.lookup
  529. lor
    1. Fin.lor
  530. lor
    1. ISize.lor
  531. lor
    1. Int16.lor
  532. lor
    1. Int32.lor
  533. lor
    1. Int64.lor
  534. lor
    1. Int8.lor
  535. lor
    1. Nat.lor
  536. lor
    1. UInt16.lor
  537. lor
    1. UInt32.lor
  538. lor
    1. UInt64.lor
  539. lor
    1. UInt8.lor
  540. lor
    1. USize.lor
  541. lt
    1. Char.lt
  542. lt
    1. Float.lt
  543. lt
    1. Float32.lt
  544. lt
    1. ISize.lt
  545. lt
    1. Int.lt
  546. lt
    1. Int16.lt
  547. lt
    1. Int32.lt
  548. lt
    1. Int64.lt
  549. lt
    1. Int8.lt
  550. lt
    1. LT.lt (class method)
  551. lt
    1. List.lt
  552. lt
    1. Nat.lt
  553. lt
    1. Option.lt
  554. lt
    1. UInt16.lt
  555. lt
    1. UInt32.lt
  556. lt
    1. UInt64.lt
  557. lt
    1. UInt8.lt
  558. lt
    1. USize.lt
  559. lt­Of­Ord
  560. lt_iff_le_not_le
    1. Lean.Grind.Preorder.le_refl (class method)

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. match
  115. match
    1. pp.match
  116. max!
    1. Std.TreeSet.max!
  117. max
    1. Max.max (class method)
  118. max
    1. Nat.max
  119. max
    1. Option.max
  120. max
    1. Std.TreeSet.max
  121. max
    1. Task.Priority.max
  122. max?
    1. List.max?
  123. max?
    1. Std.TreeSet.max?
  124. max­D
    1. Std.TreeSet.max­D
  125. max­Discharge­Depth
    1. Lean.Meta.Simp.Config.max­Discharge­Depth (structure field)
  126. max­Entry!
    1. Std.TreeMap.max­Entry!
  127. max­Entry
    1. Std.TreeMap.max­Entry
  128. max­Entry?
    1. Std.TreeMap.max­Entry?
  129. max­Entry­D
    1. Std.TreeMap.max­Entry­D
  130. max­Heartbeats
    1. synthInstance.max­Heartbeats
  131. max­Key!
    1. Std.TreeMap.max­Key!
  132. max­Key
    1. Std.TreeMap.max­Key
  133. max­Key?
    1. Std.TreeMap.max­Key?
  134. max­Key­D
    1. Std.TreeMap.max­Key­D
  135. max­Of­Le
  136. max­Size
    1. synthInstance.max­Size
  137. max­Steps
    1. Lean.Meta.Simp.Config.max­Steps (structure field)
  138. max­Steps
    1. pp.max­Steps
  139. max­Value
    1. ISize.max­Value
  140. max­Value
    1. Int16.max­Value
  141. max­Value
    1. Int32.max­Value
  142. max­Value
    1. Int64.max­Value
  143. max­Value
    1. Int8.max­Value
  144. memoize
    1. Lean.Meta.Simp.Config.memoize (structure field)
  145. merge
    1. List.merge
  146. merge
    1. Option.merge
  147. merge
    1. Std.TreeSet.merge
  148. merge­Sort
    1. List.merge­Sort
  149. merge­With
    1. Std.TreeMap.merge­With
  150. metadata
    1. System.FilePath.metadata
  151. min!
    1. Std.TreeSet.min!
  152. min
    1. Min.min (class method)
  153. min
    1. Nat.min
  154. min
    1. Option.min
  155. min
    1. Std.TreeSet.min
  156. min
    1. String.Pos.min
  157. min?
    1. List.min?
  158. min?
    1. Std.TreeSet.min?
  159. min­D
    1. Std.TreeSet.min­D
  160. min­Entry!
    1. Std.TreeMap.min­Entry!
  161. min­Entry
    1. Std.TreeMap.min­Entry
  162. min­Entry?
    1. Std.TreeMap.min­Entry?
  163. min­Entry­D
    1. Std.TreeMap.min­Entry­D
  164. min­Key!
    1. Std.TreeMap.min­Key!
  165. min­Key
    1. Std.TreeMap.min­Key
  166. min­Key?
    1. Std.TreeMap.min­Key?
  167. min­Key­D
    1. Std.TreeMap.min­Key­D
  168. min­Of­Le
  169. min­Value
    1. ISize.min­Value
  170. min­Value
    1. Int16.min­Value
  171. min­Value
    1. Int32.min­Value
  172. min­Value
    1. Int64.min­Value
  173. min­Value
    1. Int8.min­Value
  174. mix­Hash
  175. mk'
    1. LawfulMonad.mk'
  176. mk'
    1. Lean.Grind.No­Nat­ZeroDivisors.mk'
  177. mk'
    1. Quotient.mk'
  178. mk
    1. ExceptT.mk
  179. mk
    1. IO.FS.Handle.mk
  180. mk
    1. OptionT.mk
  181. mk
    1. Quot.mk
  182. mk
    1. Quotient.mk
  183. mk
    1. Squash.mk
  184. mk­File­Path
    1. System.mk­File­Path
  185. mk­Iterator
    1. String.mk­Iterator
  186. mk­Ref
    1. IO.mk­Ref
  187. mk­Ref
    1. ST.mk­Ref
  188. mk­Std­Gen
  189. mod
    1. Fin.mod
  190. mod
    1. ISize.mod
  191. mod
    1. Int16.mod
  192. mod
    1. Int32.mod
  193. mod
    1. Int64.mod
  194. mod
    1. Int8.mod
  195. mod
    1. Mod.mod (class method)
  196. mod
    1. Nat.mod
  197. mod
    1. UInt16.mod
  198. mod
    1. UInt32.mod
  199. mod
    1. UInt64.mod
  200. mod
    1. UInt8.mod
  201. mod
    1. USize.mod
  202. mod­Core
    1. Nat.mod­Core
  203. modified
    1. IO.FS.Metadata.modified (structure field)
  204. modify
  205. modify
    1. Array.modify
  206. modify
    1. List.modify
  207. modify
    1. ST.Ref.modify
  208. modify
    1. Std.DHashMap.modify
  209. modify
    1. Std.DTreeMap.modify
  210. modify
    1. Std.Ext­DHashMap.modify
  211. modify
    1. Std.Ext­HashMap.modify
  212. modify
    1. Std.HashMap.modify
  213. modify
    1. Std.TreeMap.modify
  214. modify
    1. String.modify
  215. modify­Get
    1. EStateM.modify­Get
  216. modify­Get
    1. MonadState.modify­Get
  217. modify­Get
    1. MonadState.modify­Get (class method)
  218. modify­Get
    1. Monad­StateOf.modify­Get (class method)
  219. modify­Get
    1. ST.Ref.modify­Get
  220. modify­Get
    1. State­RefT'.modify­Get
  221. modify­Get
    1. StateT.modify­Get
  222. modify­Get­The
  223. modify­Head
    1. List.modify­Head
  224. modify­M
    1. Array.modify­M
  225. modify­Op
    1. Array.modify­Op
  226. modify­TR
    1. List.modify­TR
  227. modify­Tail­Idx
    1. List.modify­Tail­Idx
  228. modify­The
  229. modn
    1. Fin.modn
  230. monad­Eval
    1. MonadEval.monad­Eval (class method)
  231. monad­Eval
    1. Monad­EvalT.monad­Eval (class method)
  232. monad­Lift
    1. MonadLift.monad­Lift (class method)
  233. monad­Lift
    1. Monad­LiftT.monad­Lift (class method)
  234. monad­Map
    1. MonadFunctor.monad­Map (class method)
  235. monad­Map
    1. Monad­FunctorT.monad­Map (class method)
  236. mono­Ms­Now
    1. IO.mono­Ms­Now
  237. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  238. monotone
    1. Lean.Order.monotone
  239. mp
    1. Eq.mp
  240. mp
    1. Iff.mp (structure field)
  241. mpr
    1. Eq.mpr
  242. mpr
    1. Iff.mpr (structure field)
  243. msb
    1. BitVec.msb
  244. mul
    1. BitVec.mul
  245. mul
    1. Fin.mul
  246. mul
    1. Float.mul
  247. mul
    1. Float32.mul
  248. mul
    1. ISize.mul
  249. mul
    1. Int.mul
  250. mul
    1. Int16.mul
  251. mul
    1. Int32.mul
  252. mul
    1. Int64.mul
  253. mul
    1. Int8.mul
  254. mul
    1. Mul.mul (class method)
  255. mul
    1. Nat.mul
  256. mul
    1. UInt16.mul
  257. mul
    1. UInt32.mul
  258. mul
    1. UInt64.mul
  259. mul
    1. UInt8.mul
  260. mul
    1. USize.mul
  261. mul­Rec
    1. BitVec.mul­Rec
  262. mul_assoc
    1. Lean.Grind.Semiring.add_zero (class method)
  263. mul_comm
    1. [anonymous] (class method) (0) (1)
  264. mul_inv_cancel
    1. [anonymous] (class method)
  265. mul_lt_mul_of_pos_left
    1. Lean.Grind.OrderedRing.zero_lt_one (class method)
  266. mul_lt_mul_of_pos_right
    1. Lean.Grind.OrderedRing.mul_lt_mul_of_pos_left (class method)
  267. mul_one
    1. Lean.Grind.Semiring.add_comm (class method)
  268. mul_zero
    1. Lean.Grind.Semiring.left_distrib (class method)
  269. mvars
    1. pp.mvars

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