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. Alternative
  8. Alternative.mk
    1. Instance constructor of Alternative
  9. And
  10. And.elim
  11. And.intro
    1. Constructor of And
  12. Append
  13. Append.mk
    1. Instance constructor of Append
  14. Applicative
  15. Applicative.mk
    1. Instance constructor of Applicative
  16. Array
  17. Array.all
  18. Array.all­Diff
  19. Array.all­M
  20. Array.any
  21. Array.any­M
  22. Array.append
  23. Array.append­List
  24. Array.attach
  25. Array.attach­With
  26. Array.back
  27. Array.back!
  28. Array.back?
  29. Array.bin­Insert
  30. Array.bin­Insert­M
  31. Array.bin­Search
  32. Array.bin­Search­Contains
  33. Array.contains
  34. Array.count
  35. Array.count­P
  36. Array.drop
  37. Array.elem
  38. Array.empty
  39. Array.empty­With­Capacity
  40. Array.erase
  41. Array.erase­Idx
  42. Array.erase­Idx!
  43. Array.erase­Idx­If­In­Bounds
  44. Array.erase­P
  45. Array.erase­Reps
  46. Array.extract
  47. Array.filter
  48. Array.filter­M
  49. Array.filter­Map
  50. Array.filter­Map­M
  51. Array.filter­Rev­M
  52. Array.filter­Sep­Elems
  53. Array.filter­Sep­Elems­M
  54. Array.fin­Idx­Of?
  55. Array.fin­Range
  56. Array.find?
  57. Array.find­Fin­Idx?
  58. Array.find­Idx
  59. Array.find­Idx?
  60. Array.find­Idx­M?
  61. Array.find­M?
  62. Array.find­Rev?
  63. Array.find­Rev­M?
  64. Array.find­Some!
  65. Array.find­Some?
  66. Array.find­Some­M?
  67. Array.find­Some­Rev?
  68. Array.find­Some­Rev­M?
  69. Array.first­M
  70. Array.flat­Map
  71. Array.flat­Map­M
  72. Array.flatten
  73. Array.foldl
  74. Array.foldl­M
  75. Array.foldr
  76. Array.foldr­M
  77. Array.for­M
  78. Array.for­Rev­M
  79. Array.get­D
  80. Array.get­Even­Elems
  81. Array.get­Max?
  82. Array.group­By­Key
  83. Array.idx­Of
  84. Array.idx­Of?
  85. Array.insert­Idx
  86. Array.insert­Idx!
  87. Array.insert­Idx­If­In­Bounds
  88. Array.insertion­Sort
  89. Array.is­Empty
  90. Array.is­Eqv
  91. Array.is­Prefix­Of
  92. Array.leftpad
  93. Array.lex
  94. Array.map
  95. Array.map­Fin­Idx
  96. Array.map­Fin­Idx­M
  97. Array.map­Idx
  98. Array.map­Idx­M
  99. Array.map­M
  100. Array.map­M'
  101. Array.map­Mono
  102. Array.map­Mono­M
  103. Array.mk
    1. Constructor of Array
  104. Array.modify
  105. Array.modify­M
  106. Array.modify­Op
  107. Array.of­Fn
  108. Array.of­Subarray
  109. Array.partition
  110. Array.pmap
  111. Array.pop
  112. Array.pop­While
  113. Array.push
  114. Array.qsort
  115. Array.qsort­Ord
  116. Array.range
  117. Array.range'
  118. Array.replace
  119. Array.replicate
  120. Array.reverse
  121. Array.rightpad
  122. Array.set
  123. Array.set!
  124. Array.set­If­In­Bounds
  125. Array.shrink
  126. Array.singleton
  127. Array.size
  128. Array.sum
  129. Array.swap
  130. Array.swap­At
  131. Array.swap­At!
  132. Array.swap­If­In­Bounds
  133. Array.take
  134. Array.take­While
  135. Array.to­List
  136. Array.to­List­Append
  137. Array.to­List­Rev
  138. Array.to­Subarray
  139. Array.to­Vector
  140. Array.uget
  141. Array.unattach
  142. Array.unzip
  143. Array.uset
  144. Array.usize
  145. Array.zip
  146. Array.zip­Idx
  147. Array.zip­With
  148. Array.zip­With­All
  149. Atomic­T
    1. Std.Atomic­T
  150. abs
    1. BitVec.abs
  151. abs
    1. Float.abs
  152. abs
    1. Float32.abs
  153. abs
    1. ISize.abs
  154. abs
    1. Int16.abs
  155. abs
    1. Int32.abs
  156. abs
    1. Int64.abs
  157. abs
    1. Int8.abs
  158. absurd
  159. ac_nf
  160. ac_nf0
  161. ac_rfl
  162. accessed
    1. IO.FS.Metadata.accessed (structure field)
  163. acos
    1. Float.acos
  164. acos
    1. Float32.acos
  165. acosh
    1. Float.acosh
  166. acosh
    1. Float32.acosh
  167. adapt
    1. ExceptT.adapt
  168. adapt
    1. ReaderT.adapt
  169. adapt­Except
    1. EStateM.adapt­Except
  170. adc
    1. BitVec.adc
  171. adcb
    1. BitVec.adcb
  172. add
    1. Add.add (class method)
  173. add
    1. BitVec.add
  174. add
    1. Fin.add
  175. add
    1. Float.add
  176. add
    1. Float32.add
  177. add
    1. ISize.add
  178. add
    1. Int.add
  179. add
    1. Int16.add
  180. add
    1. Int32.add
  181. add
    1. Int64.add
  182. add
    1. Int8.add
  183. add
    1. Nat.add
  184. add
    1. UInt16.add
  185. add
    1. UInt32.add
  186. add
    1. UInt64.add
  187. add
    1. UInt8.add
  188. add
    1. USize.add
  189. add­App­Paren
    1. Repr.add­App­Paren
  190. add­Cases
    1. Fin.add­Cases
  191. add­Extension
    1. System.FilePath.add­Extension
  192. add­Heartbeats
    1. IO.add­Heartbeats
  193. add­Macro­Scope
    1. Lean.Macro.add­Macro­Scope
  194. add­Nat
    1. Fin.add­Nat
  195. admit
  196. all
    1. Array.all
  197. all
    1. List.all
  198. all
    1. Nat.all
  199. all
    1. Option.all
  200. all
    1. Std.HashSet.all
  201. all
    1. Std.TreeMap.all
  202. all
    1. Std.TreeSet.all
  203. all
    1. String.all
  204. all
    1. Subarray.all
  205. all
    1. Substring.all
  206. all­Diff
    1. Array.all­Diff
  207. all­Eq
    1. Subsingleton.all­Eq (class method)
  208. all­I
    1. Prod.all­I
  209. all­M
    1. Array.all­M
  210. all­M
    1. List.all­M
  211. all­M
    1. Nat.all­M
  212. all­M
    1. Subarray.all­M
  213. all­Ones
    1. BitVec.all­Ones
  214. all­TR
    1. Nat.all­TR
  215. all_goals (0) (1)
  216. allow­Unsafe­Reducibility
  217. alter
    1. Std.DHashMap.alter
  218. alter
    1. Std.DTreeMap.alter
  219. alter
    1. Std.Ext­DHashMap.alter
  220. alter
    1. Std.Ext­HashMap.alter
  221. alter
    1. Std.HashMap.alter
  222. alter
    1. Std.TreeMap.alter
  223. and
    1. BitVec.and
  224. and
    1. Bool.and
  225. and
    1. List.and
  226. and­M
  227. and_intros
  228. any
    1. Array.any
  229. any
    1. List.any
  230. any
    1. Nat.any
  231. any
    1. Option.any
  232. any
    1. Std.HashSet.any
  233. any
    1. Std.TreeMap.any
  234. any
    1. Std.TreeSet.any
  235. any
    1. String.any
  236. any
    1. Subarray.any
  237. any
    1. Substring.any
  238. any­I
    1. Prod.any­I
  239. any­M
    1. Array.any­M
  240. any­M
    1. List.any­M
  241. any­M
    1. Nat.any­M
  242. any­M
    1. Subarray.any­M
  243. any­TR
    1. Nat.any­TR
  244. any_goals (0) (1)
  245. app­Dir
    1. IO.app­Dir
  246. app­Path
    1. IO.app­Path
  247. append
    1. Append.append (class method)
  248. append
    1. Array.append
  249. append
    1. BitVec.append
  250. append
    1. List.append
  251. append
    1. String.append
  252. append­List
    1. Array.append­List
  253. append­TR
    1. List.append­TR
  254. apply (0) (1)
  255. apply?
  256. apply_assumption
  257. apply_ext_theorem
  258. apply_mod_cast
  259. apply_rfl
  260. apply_rules
  261. arg [@]i
  262. args
  263. args
    1. [anonymous] (structure field)
  264. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  265. array
    1. Subarray.array (structure field)
  266. as­String
    1. List.as­String
  267. as­Task
    1. BaseIO.as­Task
  268. as­Task
    1. EIO.as­Task
  269. as­Task
    1. IO.as­Task
  270. as_aux_lemma
  271. asin
    1. Float.asin
  272. asin
    1. Float32.asin
  273. asinh
    1. Float.asinh
  274. asinh
    1. Float32.asinh
  275. assumption
  276. assumption
    1. inaccessible
  277. assumption_mod_cast
  278. at­End
    1. String.Iterator.at­End
  279. at­End
    1. String.at­End
  280. at­End
    1. Substring.at­End
  281. at­Idx!
    1. Std.TreeSet.at­Idx!
  282. at­Idx
    1. Std.TreeSet.at­Idx
  283. at­Idx?
    1. Std.TreeSet.at­Idx?
  284. at­Idx­D
    1. Std.TreeSet.at­Idx­D
  285. atan
    1. Float.atan
  286. atan
    1. Float32.atan
  287. atan2
    1. Float.atan2
  288. atan2
    1. Float32.atan2
  289. atanh
    1. Float.atanh
  290. atanh
    1. Float32.atanh
  291. atomically
    1. Std.Mutex.atomically
  292. atomically­Once
    1. Std.Mutex.atomically­Once
  293. attach
    1. Array.attach
  294. attach
    1. List.attach
  295. attach
    1. Option.attach
  296. attach­With
    1. Array.attach­With
  297. attach­With
    1. List.attach­With
  298. attach­With
    1. Option.attach­With
  299. auto­Implicit
  300. auto­Lift
  301. auto­Param
  302. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  303. auto­Unfold
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
  304. 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. Command
    1. Lean.Syntax.Command
  53. Condvar
    1. Std.Condvar
  54. Config
    1. Lean.Meta.DSimp.Config
  55. Config
    1. Lean.Meta.Rewrite.Config
  56. Config
    1. Lean.Meta.Simp.Config
  57. calc
  58. call-by-need
  59. cancel
    1. IO.cancel
  60. canon­Instances
    1. backward.synthInstance.canon­Instances
  61. capitalize
    1. String.capitalize
  62. carry
    1. BitVec.carry
  63. case
  64. case ... => ...
  65. case'
  66. case' ... => ...
  67. case­Strong­Rec­On
    1. Nat.case­Strong­Rec­On
  68. cases
  69. cases
    1. Fin.cases
  70. cases­Aux­On
    1. Nat.cases­Aux­On
  71. cast
  72. cast
    1. BitVec.cast
  73. cast
    1. Fin.cast
  74. cast
    1. Int.cast
  75. cast
    1. Nat.cast
  76. cast­Add
    1. Fin.cast­Add
  77. cast­LE
    1. Fin.cast­LE
  78. cast­LT
    1. Fin.cast­LT
  79. cast­Succ
    1. Fin.cast­Succ
  80. cast_heq
  81. catch­Exceptions
    1. EIO.catch­Exceptions
  82. catch­Runtime
    1. Lean.Meta.Simp.Config.catch­Runtime (structure field)
  83. cbrt
    1. Float.cbrt
  84. cbrt
    1. Float32.cbrt
  85. ceil
    1. Float.ceil
  86. ceil
    1. Float32.ceil
  87. chain
    1. of coercions
  88. chain­Task
    1. BaseIO.chain­Task
  89. chain­Task
    1. EIO.chain­Task
  90. chain­Task
    1. IO.chain­Task
  91. change (0) (1)
  92. change ... with ...
  93. char­Lit­Kind
    1. Lean.char­Lit­Kind
  94. check-build (Lake command)
  95. check-lint (Lake command)
  96. check-test (Lake command)
  97. check­Canceled
    1. IO.check­Canceled
  98. choice
    1. Option.choice
  99. choice­Kind
    1. Lean.choice­Kind
  100. choose
    1. Exists.choose
  101. classical
  102. clean (Lake command)
  103. clear
  104. cmd
    1. [anonymous] (structure field)
  105. coe
    1. Coe.coe (class method)
  106. coe
    1. CoeDep.coe (class method)
  107. coe
    1. CoeFun.coe (class method)
  108. coe
    1. CoeHTC.coe (class method)
  109. coe
    1. CoeHTCT.coe (class method)
  110. coe
    1. CoeHead.coe (class method)
  111. coe
    1. CoeOTC.coe (class method)
  112. coe
    1. CoeOut.coe (class method)
  113. coe
    1. CoeSort.coe (class method)
  114. coe
    1. CoeT.coe (class method)
  115. coe
    1. CoeTC.coe (class method)
  116. coe
    1. CoeTail.coe (class method)
  117. col­Eq
  118. col­Ge
  119. col­Gt
  120. comment
    1. block
  121. comment
    1. line
  122. common­Prefix
    1. Substring.common­Prefix
  123. common­Suffix
    1. Substring.common­Suffix
  124. comp
    1. Function.comp
  125. comp_map
    1. LawfulFunctor.comp_map (class method)
  126. compare
    1. Ord.compare (class method)
  127. compare­Lex
  128. compare­Of­Less­And­BEq
  129. compare­Of­Less­And­Eq
  130. compare­On
  131. complement
    1. ISize.complement
  132. complement
    1. Int16.complement
  133. complement
    1. Int32.complement
  134. complement
    1. Int64.complement
  135. complement
    1. Int8.complement
  136. complement
    1. UInt16.complement
  137. complement
    1. UInt32.complement
  138. complement
    1. UInt64.complement
  139. complement
    1. UInt8.complement
  140. complement
    1. USize.complement
  141. completions (Elan command)
  142. components
    1. System.FilePath.components
  143. concat
    1. BitVec.concat
  144. concat
    1. List.concat
  145. cond
  146. configuration
    1. of tactics
  147. congr (0) (1) (2)
  148. congr­Arg
  149. congr­Fun
  150. cons
    1. BitVec.cons
  151. const
    1. Function.const
  152. constructor (0) (1)
  153. contains
    1. Array.contains
  154. contains
    1. List.contains
  155. contains
    1. Std.DHashMap.contains
  156. contains
    1. Std.DTreeMap.contains
  157. contains
    1. Std.Ext­DHashMap.contains
  158. contains
    1. Std.Ext­HashMap.contains
  159. contains
    1. Std.Ext­HashSet.contains
  160. contains
    1. Std.HashMap.contains
  161. contains
    1. Std.HashSet.contains
  162. contains
    1. Std.TreeMap.contains
  163. contains
    1. Std.TreeSet.contains
  164. contains
    1. String.contains
  165. contains
    1. Substring.contains
  166. contains­Then­Insert
    1. Std.DHashMap.contains­Then­Insert
  167. contains­Then­Insert
    1. Std.DTreeMap.contains­Then­Insert
  168. contains­Then­Insert
    1. Std.Ext­DHashMap.contains­Then­Insert
  169. contains­Then­Insert
    1. Std.Ext­HashMap.contains­Then­Insert
  170. contains­Then­Insert
    1. Std.Ext­HashSet.contains­Then­Insert
  171. contains­Then­Insert
    1. Std.HashMap.contains­Then­Insert
  172. contains­Then­Insert
    1. Std.HashSet.contains­Then­Insert
  173. contains­Then­Insert
    1. Std.TreeMap.contains­Then­Insert
  174. contains­Then­Insert
    1. Std.TreeSet.contains­Then­Insert
  175. contains­Then­Insert­If­New
    1. Std.DHashMap.contains­Then­Insert­If­New
  176. contains­Then­Insert­If­New
    1. Std.DTreeMap.contains­Then­Insert­If­New
  177. contains­Then­Insert­If­New
    1. Std.Ext­DHashMap.contains­Then­Insert­If­New
  178. contains­Then­Insert­If­New
    1. Std.Ext­HashMap.contains­Then­Insert­If­New
  179. contains­Then­Insert­If­New
    1. Std.HashMap.contains­Then­Insert­If­New
  180. contains­Then­Insert­If­New
    1. Std.TreeMap.contains­Then­Insert­If­New
  181. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  182. contradiction
  183. control
  184. control­At
  185. conv
  186. conv => ...
  187. conv' (0) (1)
  188. cos
    1. Float.cos
  189. cos
    1. Float32.cos
  190. cosh
    1. Float.cosh
  191. cosh
    1. Float32.cosh
  192. count
    1. Array.count
  193. count
    1. List.count
  194. count­P
    1. Array.count­P
  195. count­P
    1. List.count­P
  196. create­Dir
    1. IO.FS.create­Dir
  197. create­Dir­All
    1. IO.FS.create­Dir­All
  198. create­Temp­Dir
    1. IO.FS.create­Temp­Dir
  199. create­Temp­File
    1. IO.FS.create­Temp­File
  200. crlf­To­Lf
    1. String.crlf­To­Lf
  201. csup
    1. [anonymous] (class method)
  202. csup_spec
    1. [anonymous] (class method)
  203. cumulativity
  204. curr
    1. String.Iterator.curr
  205. curr­Column
    1. Std.Format.Monad­PrettyFormat.curr­Column (class method)
  206. current­Dir
    1. IO.current­Dir
  207. curry
    1. Function.curry
  208. custom­Eliminators
    1. tactic.custom­Eliminators
  209. 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. done (0) (1)
  106. down
    1. PLift.down (structure field)
  107. down
    1. ULift.down (structure field)
  108. drop
    1. Array.drop
  109. drop
    1. List.drop
  110. drop
    1. String.drop
  111. drop
    1. Subarray.drop
  112. drop
    1. Substring.drop
  113. drop­Last
    1. List.drop­Last
  114. drop­Last­TR
    1. List.drop­Last­TR
  115. drop­Prefix?
    1. String.drop­Prefix?
  116. drop­Prefix?
    1. Substring.drop­Prefix?
  117. drop­Right
    1. String.drop­Right
  118. drop­Right
    1. Substring.drop­Right
  119. drop­Right­While
    1. String.drop­Right­While
  120. drop­Right­While
    1. Substring.drop­Right­While
  121. drop­Suffix?
    1. String.drop­Suffix?
  122. drop­Suffix?
    1. Substring.drop­Suffix?
  123. drop­While
    1. List.drop­While
  124. drop­While
    1. String.drop­While
  125. drop­While
    1. Substring.drop­While
  126. dsimp (0) (1)
  127. dsimp!
  128. dsimp
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  129. dsimp?
  130. dsimp?!
  131. 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. File­Path
    1. System.File­Path
  4. File­Right
    1. IO.File­Right
  5. Fin
  6. Fin.add
  7. Fin.add­Cases
  8. Fin.add­Nat
  9. Fin.cases
  10. Fin.cast
  11. Fin.cast­Add
  12. Fin.cast­LE
  13. Fin.cast­LT
  14. Fin.cast­Succ
  15. Fin.div
  16. Fin.elim0
  17. Fin.foldl
  18. Fin.foldl­M
  19. Fin.foldr
  20. Fin.foldr­M
  21. Fin.h­Iterate
  22. Fin.h­Iterate­From
  23. Fin.induction
  24. Fin.induction­On
  25. Fin.land
  26. Fin.last
  27. Fin.last­Cases
  28. Fin.log2
  29. Fin.lor
  30. Fin.mk
    1. Constructor of Fin
  31. Fin.mod
  32. Fin.modn
  33. Fin.mul
  34. Fin.nat­Add
  35. Fin.of­Nat
  36. Fin.pred
  37. Fin.rev
  38. Fin.reverse­Induction
  39. Fin.shift­Left
  40. Fin.shift­Right
  41. Fin.sub
  42. Fin.sub­Nat
  43. Fin.succ
  44. Fin.succ­Rec
  45. Fin.succ­Rec­On
  46. Fin.to­Nat
  47. Fin.xor
  48. Flatten­Behavior
    1. Std.Format.Flatten­Behavior
  49. Float
  50. Float.abs
  51. Float.acos
  52. Float.acosh
  53. Float.add
  54. Float.asin
  55. Float.asinh
  56. Float.atan
  57. Float.atan2
  58. Float.atanh
  59. Float.beq
  60. Float.cbrt
  61. Float.ceil
  62. Float.cos
  63. Float.cosh
  64. Float.dec­Le
  65. Float.dec­Lt
  66. Float.div
  67. Float.exp
  68. Float.exp2
  69. Float.floor
  70. Float.fr­Exp
  71. Float.is­Finite
  72. Float.is­Inf
  73. Float.is­Na­N
  74. Float.le
  75. Float.log
  76. Float.log10
  77. Float.log2
  78. Float.lt
  79. Float.mul
  80. Float.neg
  81. Float.of­Binary­Scientific
  82. Float.of­Bits
  83. Float.of­Int
  84. Float.of­Nat
  85. Float.of­Scientific
  86. Float.pow
  87. Float.round
  88. Float.scale­B
  89. Float.sin
  90. Float.sinh
  91. Float.sqrt
  92. Float.sub
  93. Float.tan
  94. Float.tanh
  95. Float.to­Bits
  96. Float.to­Float32
  97. Float.to­ISize
  98. Float.to­Int16
  99. Float.to­Int32
  100. Float.to­Int64
  101. Float.to­Int8
  102. Float.to­String
  103. Float.to­UInt16
  104. Float.to­UInt32
  105. Float.to­UInt64
  106. Float.to­UInt8
  107. Float.to­USize
  108. Float32
  109. Float32.abs
  110. Float32.acos
  111. Float32.acosh
  112. Float32.add
  113. Float32.asin
  114. Float32.asinh
  115. Float32.atan
  116. Float32.atan2
  117. Float32.atanh
  118. Float32.beq
  119. Float32.cbrt
  120. Float32.ceil
  121. Float32.cos
  122. Float32.cosh
  123. Float32.dec­Le
  124. Float32.dec­Lt
  125. Float32.div
  126. Float32.exp
  127. Float32.exp2
  128. Float32.floor
  129. Float32.fr­Exp
  130. Float32.is­Finite
  131. Float32.is­Inf
  132. Float32.is­Na­N
  133. Float32.le
  134. Float32.log
  135. Float32.log10
  136. Float32.log2
  137. Float32.lt
  138. Float32.mul
  139. Float32.neg
  140. Float32.of­Binary­Scientific
  141. Float32.of­Bits
  142. Float32.of­Int
  143. Float32.of­Nat
  144. Float32.of­Scientific
  145. Float32.pow
  146. Float32.round
  147. Float32.scale­B
  148. Float32.sin
  149. Float32.sinh
  150. Float32.sqrt
  151. Float32.sub
  152. Float32.tan
  153. Float32.tanh
  154. Float32.to­Bits
  155. Float32.to­Float
  156. Float32.to­ISize
  157. Float32.to­Int16
  158. Float32.to­Int32
  159. Float32.to­Int64
  160. Float32.to­Int8
  161. Float32.to­String
  162. Float32.to­UInt16
  163. Float32.to­UInt32
  164. Float32.to­UInt64
  165. Float32.to­UInt8
  166. Float32.to­USize
  167. For­In
  168. For­In'
  169. ForIn'.mk
    1. Instance constructor of For­In'
  170. ForIn.mk
    1. Instance constructor of For­In
  171. For­In­Step
  172. For­InStep.done
    1. Constructor of For­In­Step
  173. For­InStep.value
  174. For­InStep.yield
    1. Constructor of For­In­Step
  175. For­M
  176. ForM.for­In
  177. ForM.mk
    1. Instance constructor of For­M
  178. Format
    1. Std.Format
  179. Function.comp
  180. Function.const
  181. Function.curry
  182. Function.uncurry
  183. Functor
  184. Functor.discard
  185. Functor.map­Rev
  186. Functor.mk
    1. Instance constructor of Functor
  187. fail
  188. fail
    1. OptionT.fail
  189. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
  190. fail­If­Unchanged
    1. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  191. fail_if_success (0) (1)
  192. failure
    1. ReaderT.failure
  193. failure
    1. StateT.failure
  194. failure
    1. [anonymous] (class method)
  195. false_or_by_contra
  196. fdiv
    1. Int.fdiv
  197. field­Idx­Kind
    1. Lean.field­Idx­Kind
  198. field­Notation
    1. pp.field­Notation
  199. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
  200. file­Name
    1. System.FilePath.file­Name
  201. file­Stem
    1. System.FilePath.file­Stem
  202. fill
    1. BitVec.fill
  203. fill
    1. Std.Format.fill
  204. filter
    1. Array.filter
  205. filter
    1. List.filter
  206. filter
    1. Option.filter
  207. filter
    1. Std.DHashMap.filter
  208. filter
    1. Std.DTreeMap.filter
  209. filter
    1. Std.Ext­DHashMap.filter
  210. filter
    1. Std.Ext­HashMap.filter
  211. filter
    1. Std.Ext­HashSet.filter
  212. filter
    1. Std.HashMap.filter
  213. filter
    1. Std.HashSet.filter
  214. filter
    1. Std.TreeMap.filter
  215. filter
    1. Std.TreeSet.filter
  216. filter­M
    1. Array.filter­M
  217. filter­M
    1. List.filter­M
  218. filter­Map
    1. Array.filter­Map
  219. filter­Map
    1. List.filter­Map
  220. filter­Map
    1. Std.DHashMap.filter­Map
  221. filter­Map
    1. Std.DTreeMap.filter­Map
  222. filter­Map
    1. Std.Ext­DHashMap.filter­Map
  223. filter­Map
    1. Std.Ext­HashMap.filter­Map
  224. filter­Map
    1. Std.HashMap.filter­Map
  225. filter­Map
    1. Std.TreeMap.filter­Map
  226. filter­Map­M
    1. Array.filter­Map­M
  227. filter­Map­M
    1. List.filter­Map­M
  228. filter­Map­TR
    1. List.filter­Map­TR
  229. filter­Rev­M
    1. Array.filter­Rev­M
  230. filter­Rev­M
    1. List.filter­Rev­M
  231. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  232. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  233. filter­TR
    1. List.filter­TR
  234. fin­Idx­Of?
    1. Array.fin­Idx­Of?
  235. fin­Idx­Of?
    1. List.fin­Idx­Of?
  236. fin­Range
    1. Array.fin­Range
  237. fin­Range
    1. List.fin­Range
  238. find
    1. String.find
  239. find?
    1. Array.find?
  240. find?
    1. List.find?
  241. find­Extern­Lib?
    1. Lake.find­Extern­Lib?
  242. find­Fin­Idx?
    1. Array.find­Fin­Idx?
  243. find­Fin­Idx?
    1. List.find­Fin­Idx?
  244. find­Idx
    1. Array.find­Idx
  245. find­Idx
    1. List.find­Idx
  246. find­Idx?
    1. Array.find­Idx?
  247. find­Idx?
    1. List.find­Idx?
  248. find­Idx­M?
    1. Array.find­Idx­M?
  249. find­Lean­Exe?
    1. Lake.find­Lean­Exe?
  250. find­Lean­Lib?
    1. Lake.find­Lean­Lib?
  251. find­Line­Start
    1. String.find­Line­Start
  252. find­M?
    1. Array.find­M?
  253. find­M?
    1. List.find­M?
  254. find­Module?
    1. Lake.find­Module?
  255. find­Package?
    1. Lake.find­Package?
  256. find­Rev?
    1. Array.find­Rev?
  257. find­Rev?
    1. Subarray.find­Rev?
  258. find­Rev­M?
    1. Array.find­Rev­M?
  259. find­Rev­M?
    1. Subarray.find­Rev­M?
  260. find­Some!
    1. Array.find­Some!
  261. find­Some?
    1. Array.find­Some?
  262. find­Some?
    1. List.find­Some?
  263. find­Some­M?
    1. Array.find­Some­M?
  264. find­Some­M?
    1. List.find­Some­M?
  265. find­Some­Rev?
    1. Array.find­Some­Rev?
  266. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
  267. find­Some­Rev­M?
    1. Subarray.find­Some­Rev­M?
  268. first (0) (1)
  269. first­Diff­Pos
    1. String.first­Diff­Pos
  270. first­M
    1. Array.first­M
  271. first­M
    1. List.first­M
  272. fix
    1. Lean.Order.fix
  273. fix
    1. WellFounded.fix
  274. fix_eq
    1. Lean.Order.fix_eq
  275. flags
    1. IO.AccessRight.flags
  276. flags
    1. IO.FileRight.flags
  277. flat­Map
    1. Array.flat­Map
  278. flat­Map
    1. List.flat­Map
  279. flat­Map­M
    1. Array.flat­Map­M
  280. flat­Map­M
    1. List.flat­Map­M
  281. flat­Map­TR
    1. List.flat­Map­TR
  282. flatten
    1. Array.flatten
  283. flatten
    1. List.flatten
  284. flatten­TR
    1. List.flatten­TR
  285. floor
    1. Float.floor
  286. floor
    1. Float32.floor
  287. flush
    1. IO.FS.Handle.flush
  288. flush
    1. IO.FS.Stream.flush (structure field)
  289. fmod
    1. Int.fmod
  290. focus (0) (1)
  291. fold
    1. Nat.fold
  292. fold
    1. Std.DHashMap.fold
  293. fold
    1. Std.HashMap.fold
  294. fold
    1. Std.HashSet.fold
  295. fold­I
    1. Prod.fold­I
  296. fold­M
    1. Nat.fold­M
  297. fold­M
    1. Std.DHashMap.fold­M
  298. fold­M
    1. Std.HashMap.fold­M
  299. fold­M
    1. Std.HashSet.fold­M
  300. fold­Rev
    1. Nat.fold­Rev
  301. fold­Rev­M
    1. Nat.fold­Rev­M
  302. fold­TR
    1. Nat.fold­TR
  303. foldl
    1. Array.foldl
  304. foldl
    1. Fin.foldl
  305. foldl
    1. List.foldl
  306. foldl
    1. Std.DTreeMap.foldl
  307. foldl
    1. Std.TreeMap.foldl
  308. foldl
    1. Std.TreeSet.foldl
  309. foldl
    1. String.foldl
  310. foldl
    1. Subarray.foldl
  311. foldl
    1. Substring.foldl
  312. foldl­M
    1. Array.foldl­M
  313. foldl­M
    1. Fin.foldl­M
  314. foldl­M
    1. List.foldl­M
  315. foldl­M
    1. Std.DTreeMap.foldl­M
  316. foldl­M
    1. Std.TreeMap.foldl­M
  317. foldl­M
    1. Std.TreeSet.foldl­M
  318. foldl­M
    1. Subarray.foldl­M
  319. foldl­Rec­On
    1. List.foldl­Rec­On
  320. foldr
    1. Array.foldr
  321. foldr
    1. Fin.foldr
  322. foldr
    1. List.foldr
  323. foldr
    1. Std.TreeMap.foldr
  324. foldr
    1. Std.TreeSet.foldr
  325. foldr
    1. String.foldr
  326. foldr
    1. Subarray.foldr
  327. foldr
    1. Substring.foldr
  328. foldr­M
    1. Array.foldr­M
  329. foldr­M
    1. Fin.foldr­M
  330. foldr­M
    1. List.foldr­M
  331. foldr­M
    1. Std.TreeMap.foldr­M
  332. foldr­M
    1. Std.TreeSet.foldr­M
  333. foldr­M
    1. Subarray.foldr­M
  334. foldr­Rec­On
    1. List.foldr­Rec­On
  335. foldr­TR
    1. List.foldr­TR
  336. for­A
    1. List.for­A
  337. for­Async
    1. Std.Channel.for­Async
  338. for­In'
    1. ForIn'.for­In' (class method)
  339. for­In
    1. ForIn.for­In (class method)
  340. for­In
    1. ForM.for­In
  341. for­In
    1. Std.DHashMap.for­In
  342. for­In
    1. Std.DTreeMap.for­In
  343. for­In
    1. Std.HashMap.for­In
  344. for­In
    1. Std.HashSet.for­In
  345. for­In
    1. Std.TreeMap.for­In
  346. for­In
    1. Std.TreeSet.for­In
  347. for­In
    1. Subarray.for­In
  348. for­M
    1. Array.for­M
  349. for­M
    1. ForM.for­M (class method)
  350. for­M
    1. List.for­M
  351. for­M
    1. Nat.for­M
  352. for­M
    1. Option.for­M
  353. for­M
    1. Std.DHashMap.for­M
  354. for­M
    1. Std.DTreeMap.for­M
  355. for­M
    1. Std.HashMap.for­M
  356. for­M
    1. Std.HashSet.for­M
  357. for­M
    1. Std.TreeMap.for­M
  358. for­M
    1. Std.TreeSet.for­M
  359. for­M
    1. Subarray.for­M
  360. for­Rev­M
    1. Array.for­Rev­M
  361. for­Rev­M
    1. Nat.for­Rev­M
  362. for­Rev­M
    1. Subarray.for­Rev­M
  363. format
    1. Option.format
  364. format
    1. Std.ToFormat.format (class method)
  365. forward
    1. String.Iterator.forward
  366. fr­Exp
    1. Float.fr­Exp
  367. fr­Exp
    1. Float32.fr­Exp
  368. from­State­M
    1. EStateM.from­State­M
  369. from­UTF8!
    1. String.from­UTF8!
  370. from­UTF8
    1. String.from­UTF8
  371. from­UTF8?
    1. String.from­UTF8?
  372. front
    1. String.front
  373. front
    1. Substring.front
  374. fst
    1. MProd.fst (structure field)
  375. fst
    1. PProd.fst (structure field)
  376. fst
    1. PSigma.fst (structure field)
  377. fst
    1. Prod.fst (structure field)
  378. fst
    1. Sigma.fst (structure field)
  379. fun
  380. fun_cases
  381. fun_induction
  382. 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.TreeMap.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.TreeMap.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.TreeMap.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.TreeMap.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. ground
    1. Lean.Meta.Simp.Config.ground (structure field)
  235. group
    1. IO.FileRight.group (structure field)
  236. group­By­Key
    1. Array.group­By­Key
  237. group­By­Key
    1. List.group­By­Key
  238. group­Kind
    1. Lean.group­Kind
  239. guard
  240. guard
    1. Option.guard
  241. guard_expr
  242. guard_hyp
  243. guard_msgs.diff
  244. 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
  66. have'
  67. have­I
  68. head!
    1. List.head!
  69. head
    1. List.head
  70. head?
    1. List.head?
  71. head­D
    1. List.head­D
  72. helim
    1. Subsingleton.helim
  73. heq_of_eq
  74. heq_of_eq­Rec_eq
  75. heq_of_heq_of_eq
  76. hrec­On
    1. Quot.hrec­On
  77. hrec­On
    1. Quotient.hrec­On
  78. hygiene
    1. in tactics
  79. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  80. 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. Is­Infix
    1. List.Is­Infix
  388. Is­Prefix
    1. List.Is­Prefix
  389. Is­Suffix
    1. List.Is­Suffix
  390. Iterator
    1. String.Iterator
  391. i
    1. String.Iterator.i (structure field)
  392. id_map
    1. LawfulFunctor.id_map (class method)
  393. ident­Kind
    1. Lean.ident­Kind
  394. identifier
  395. identifier
    1. raw
  396. idx­Of
    1. Array.idx­Of
  397. idx­Of
    1. List.idx­Of
  398. idx­Of?
    1. Array.idx­Of?
  399. idx­Of?
    1. List.idx­Of?
  400. if ... then ... else ...
  401. if h : ... then ... else ...
  402. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  403. impredicative
  404. inaccessible
  405. ind
    1. Quot.ind
  406. ind
    1. Quotient.ind
  407. ind
    1. Squash.ind
  408. indent­D
    1. Std.Format.indent­D
  409. index
    1. Lean.Meta.DSimp.Config.index (structure field)
  410. index
    1. Lean.Meta.Simp.Config.index (structure field)
  411. index
    1. of inductive type
  412. indexed family
    1. of types
  413. induction
  414. induction
    1. Fin.induction
  415. induction­On
    1. Fin.induction­On
  416. induction­On
    1. Nat.div.induction­On
  417. induction­On
    1. Nat.mod.induction­On
  418. inductive.auto­Promote­Indices
  419. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  420. infer­Instance
  421. infer­Instance­As
  422. infer_instance
  423. inhabited­Left
    1. PSum.inhabited­Left
  424. inhabited­Left
    1. Sum.inhabited­Left
  425. inhabited­Right
    1. PSum.inhabited­Right
  426. inhabited­Right
    1. Sum.inhabited­Right
  427. inherit­Env
    1. IO.Process.SpawnArgs.args (structure field)
  428. init (Lake command)
  429. injection
  430. injections
  431. inner
    1. Std.DHashMap.Equiv.inner (structure field)
  432. inner
    1. Std.DTreeMap.Raw.inner (structure field)
  433. inner
    1. Std.Ext­HashSet.inner (structure field)
  434. inner
    1. Std.HashMap.Equiv.inner (structure field)
  435. inner
    1. Std.HashMap.Raw.inner (structure field)
  436. inner
    1. Std.HashSet.Equiv.inner (structure field)
  437. inner
    1. Std.HashSet.Raw.inner (structure field)
  438. inner
    1. Std.HashSet.inner (structure field)
  439. inner
    1. Std.TreeMap.Raw.inner (structure field)
  440. inner
    1. Std.TreeSet.Raw.inner (structure field)
  441. insert
    1. List.insert
  442. insert
    1. Std.DHashMap.insert
  443. insert
    1. Std.DTreeMap.insert
  444. insert
    1. Std.Ext­DHashMap.insert
  445. insert
    1. Std.Ext­HashMap.insert
  446. insert
    1. Std.Ext­HashSet.insert
  447. insert
    1. Std.HashMap.insert
  448. insert
    1. Std.HashSet.insert
  449. insert
    1. Std.TreeMap.insert
  450. insert
    1. Std.TreeSet.insert
  451. insert­Idx!
    1. Array.insert­Idx!
  452. insert­Idx
    1. Array.insert­Idx
  453. insert­Idx
    1. List.insert­Idx
  454. insert­Idx­If­In­Bounds
    1. Array.insert­Idx­If­In­Bounds
  455. insert­Idx­TR
    1. List.insert­Idx­TR
  456. insert­If­New
    1. Std.DHashMap.insert­If­New
  457. insert­If­New
    1. Std.DTreeMap.insert­If­New
  458. insert­If­New
    1. Std.Ext­DHashMap.insert­If­New
  459. insert­If­New
    1. Std.Ext­HashMap.insert­If­New
  460. insert­If­New
    1. Std.HashMap.insert­If­New
  461. insert­If­New
    1. Std.TreeMap.insert­If­New
  462. insert­Many
    1. Std.DHashMap.insert­Many
  463. insert­Many
    1. Std.DTreeMap.insert­Many
  464. insert­Many
    1. Std.Ext­DHashMap.insert­Many
  465. insert­Many
    1. Std.Ext­HashMap.insert­Many
  466. insert­Many
    1. Std.Ext­HashSet.insert­Many
  467. insert­Many
    1. Std.HashMap.insert­Many
  468. insert­Many
    1. Std.HashSet.insert­Many
  469. insert­Many
    1. Std.TreeMap.insert­Many
  470. insert­Many
    1. Std.TreeSet.insert­Many
  471. insert­Many­If­New­Unit
    1. Std.Ext­HashMap.insert­Many­If­New­Unit
  472. insert­Many­If­New­Unit
    1. Std.HashMap.insert­Many­If­New­Unit
  473. insert­Many­If­New­Unit
    1. Std.TreeMap.insert­Many­If­New­Unit
  474. insertion­Sort
    1. Array.insertion­Sort
  475. instance synthesis
  476. int­Cast
    1. IntCast.int­Cast (class method)
  477. int­Max
    1. BitVec.int­Max
  478. int­Min
    1. BitVec.int­Min
  479. intercalate
    1. List.intercalate
  480. intercalate
    1. String.intercalate
  481. intercalate­TR
    1. List.intercalate­TR
  482. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  483. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  484. intersperse
    1. List.intersperse
  485. intersperse­TR
    1. List.intersperse­TR
  486. intro (0) (1)
  487. intro | ... => ... | ... => ...
  488. intros
  489. inv­Image
  490. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
  491. iota
    1. Lean.Meta.Simp.Config.iota (structure field)
  492. is­Absolute
    1. System.FilePath.is­Absolute
  493. is­Alpha
    1. Char.is­Alpha
  494. is­Alphanum
    1. Char.is­Alphanum
  495. is­Digit
    1. Char.is­Digit
  496. is­Dir
    1. System.FilePath.is­Dir
  497. is­Empty
    1. Array.is­Empty
  498. is­Empty
    1. List.is­Empty
  499. is­Empty
    1. Std.DHashMap.is­Empty
  500. is­Empty
    1. Std.DTreeMap.is­Empty
  501. is­Empty
    1. Std.Ext­DHashMap.is­Empty
  502. is­Empty
    1. Std.Ext­HashMap.is­Empty
  503. is­Empty
    1. Std.Ext­HashSet.is­Empty
  504. is­Empty
    1. Std.Format.is­Empty
  505. is­Empty
    1. Std.HashMap.is­Empty
  506. is­Empty
    1. Std.HashSet.is­Empty
  507. is­Empty
    1. Std.TreeMap.is­Empty
  508. is­Empty
    1. Std.TreeSet.is­Empty
  509. is­Empty
    1. String.is­Empty
  510. is­Empty
    1. Substring.is­Empty
  511. is­Emscripten
    1. System.Platform.is­Emscripten
  512. is­Eq
    1. Ordering.is­Eq
  513. is­Eq­Some
    1. Option.is­Eq­Some
  514. is­Eqv
    1. Array.is­Eqv
  515. is­Eqv
    1. List.is­Eqv
  516. is­Exclusive­Unsafe
  517. is­Finite
    1. Float.is­Finite
  518. is­Finite
    1. Float32.is­Finite
  519. is­GE
    1. Ordering.is­GE
  520. is­GT
    1. Ordering.is­GT
  521. is­Inf
    1. Float.is­Inf
  522. is­Inf
    1. Float32.is­Inf
  523. is­Int
    1. String.is­Int
  524. is­LE
    1. Ordering.is­LE
  525. is­LT
    1. Ordering.is­LT
  526. is­Left
    1. Sum.is­Left
  527. is­Lower
    1. Char.is­Lower
  528. is­Lt
    1. Fin.is­Lt (structure field)
  529. is­Na­N
    1. Float.is­Na­N
  530. is­Na­N
    1. Float32.is­Na­N
  531. is­Nat
    1. String.is­Nat
  532. is­Nat
    1. Substring.is­Nat
  533. is­Ne
    1. Ordering.is­Ne
  534. is­Nil
    1. Std.Format.is­Nil
  535. is­None
    1. Option.is­None
  536. is­OSX
    1. System.Platform.is­OSX
  537. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  538. is­Ok
    1. Except.is­Ok
  539. is­Perm
    1. List.is­Perm
  540. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  541. is­Prefix­Of
    1. Array.is­Prefix­Of
  542. is­Prefix­Of
    1. List.is­Prefix­Of
  543. is­Prefix­Of
    1. String.is­Prefix­Of
  544. is­Prefix­Of?
    1. List.is­Prefix­Of?
  545. is­Relative
    1. System.FilePath.is­Relative
  546. is­Resolved
    1. IO.Promise.is­Resolved
  547. is­Right
    1. Sum.is­Right
  548. is­Some
    1. Option.is­Some
  549. is­Sublist
    1. List.is­Sublist
  550. is­Suffix­Of
    1. List.is­Suffix­Of
  551. is­Suffix­Of?
    1. List.is­Suffix­Of?
  552. is­Tty
    1. IO.FS.Handle.is­Tty
  553. is­Tty
    1. IO.FS.Stream.is­Tty (structure field)
  554. is­Upper
    1. Char.is­Upper
  555. is­Valid
    1. String.Pos.is­Valid
  556. is­Valid­Char
    1. Nat.is­Valid­Char
  557. is­Valid­Char
    1. UInt32.is­Valid­Char
  558. is­Valid­Char­Nat
    1. Char.is­Valid­Char­Nat
  559. is­Whitespace
    1. Char.is­Whitespace
  560. is­Windows
    1. System.Platform.is­Windows
  561. iseqv
    1. Setoid.iseqv (class method)
  562. iter
    1. String.iter
  563. iterate
  564. iterate
    1. IO.iterate
  565. iunfoldr
    1. BitVec.iunfoldr
  566. 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.Lean­Option
  32. Lake.LeanOption.mk
    1. Constructor of Lake.Lean­Option
  33. Lake.Monad­Lake­Env
  34. Lake.Monad­Workspace
  35. Lake.MonadWorkspace.mk
    1. Instance constructor of Lake.Monad­Workspace
  36. Lake.Script­M (0) (1)
  37. Lake.find­Extern­Lib?
  38. Lake.find­Lean­Exe?
  39. Lake.find­Lean­Lib?
  40. Lake.find­Module?
  41. Lake.find­Package?
  42. Lake.get­Augmented­Env
  43. Lake.get­Augmented­Lean­Path
  44. Lake.get­Augmented­Lean­Src­Path
  45. Lake.get­Augmented­Shared­Lib­Path
  46. Lake.get­Elan?
  47. Lake.get­Elan­Home?
  48. Lake.get­Elan­Install?
  49. Lake.get­Elan­Toolchain
  50. Lake.get­Env­Lean­Path
  51. Lake.get­Env­Lean­Src­Path
  52. Lake.get­Env­Shared­Lib­Path
  53. Lake.get­Lake
  54. Lake.get­Lake­Env
  55. Lake.get­Lake­Home
  56. Lake.get­Lake­Install
  57. Lake.get­Lake­Lib­Dir
  58. Lake.get­Lake­Src­Dir
  59. Lake.get­Lean
  60. Lake.get­Lean­Ar
  61. Lake.get­Lean­Cc
  62. Lake.get­Lean­Cc?
  63. Lake.get­Lean­Include­Dir
  64. Lake.get­Lean­Install
  65. Lake.get­Lean­Lib­Dir
  66. Lake.get­Lean­Path
  67. Lake.get­Lean­Shared­Lib
  68. Lake.get­Lean­Src­Dir
  69. Lake.get­Lean­Src­Path
  70. Lake.get­Lean­Sysroot
  71. Lake.get­Lean­System­Lib­Dir
  72. Lake.get­Leanc
  73. Lake.get­No­Cache
  74. Lake.get­Pkg­Url­Map
  75. Lake.get­Root­Package
  76. Lake.get­Shared­Lib­Path
  77. Lake.get­Try­Cache
  78. Lawful­Applicative
  79. LawfulApplicative.mk
    1. Instance constructor of Lawful­Applicative
  80. Lawful­BEq
  81. LawfulBEq.mk
    1. Instance constructor of Lawful­BEq
  82. Lawful­Functor
  83. LawfulFunctor.mk
    1. Instance constructor of Lawful­Functor
  84. Lawful­Get­Elem
  85. Lawful­GetElem.mk
    1. Instance constructor of Lawful­Get­Elem
  86. Lawful­Hashable
  87. LawfulHashable.mk
    1. Instance constructor of Lawful­Hashable
  88. Lawful­Monad
  89. LawfulMonad.mk'
  90. LawfulMonad.mk
    1. Instance constructor of Lawful­Monad
  91. Leading­Ident­Behavior
    1. Lean.Parser.Leading­Ident­Behavior
  92. Lean.Elab.register­Deriving­Handler
  93. Lean.Macro.Exception.unsupported­Syntax
  94. Lean.Macro.add­Macro­Scope
  95. Lean.Macro.expand­Macro?
  96. Lean.Macro.get­Curr­Namespace
  97. Lean.Macro.has­Decl
  98. Lean.Macro.resolve­Global­Name
  99. Lean.Macro.resolve­Namespace
  100. Lean.Macro.throw­Error
  101. Lean.Macro.throw­Error­At
  102. Lean.Macro.throw­Unsupported
  103. Lean.Macro.trace
  104. Lean.Macro.with­Fresh­Macro­Scope
  105. Lean.Macro­M
  106. Lean.Meta.DSimp.Config
  107. Lean.Meta.DSimp.Config.mk
    1. Constructor of Lean.Meta.DSimp.Config
  108. Lean.Meta.Occurrences
  109. Lean.Meta.Occurrences.all
    1. Constructor of Lean.Meta.Occurrences
  110. Lean.Meta.Occurrences.neg
    1. Constructor of Lean.Meta.Occurrences
  111. Lean.Meta.Occurrences.pos
    1. Constructor of Lean.Meta.Occurrences
  112. Lean.Meta.Rewrite.Config
  113. Lean.Meta.Rewrite.Config.mk
    1. Constructor of Lean.Meta.Rewrite.Config
  114. Lean.Meta.Rewrite.New­Goals
  115. Lean.Meta.Simp.Config
  116. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  117. Lean.Meta.Simp.neutral­Config
  118. Lean.Meta.Simp­Extension
  119. Lean.Meta.Transparency­Mode
  120. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.Transparency­Mode
  121. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.Transparency­Mode
  122. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.Transparency­Mode
  123. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.Transparency­Mode
  124. Lean.Meta.register­Simp­Attr
  125. Lean.Order.CCPO
  126. Lean.Order.CCPO.mk
    1. Instance constructor of Lean.Order.CCPO
  127. Lean.Order.Partial­Order
  128. Lean.Order.PartialOrder.mk
    1. Instance constructor of Lean.Order.Partial­Order
  129. Lean.Order.fix
  130. Lean.Order.fix_eq
  131. Lean.Order.monotone
  132. Lean.Parser.Leading­Ident­Behavior
  133. Lean.Parser.Leading­IdentBehavior.both
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  134. Lean.Parser.Leading­IdentBehavior.default
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  135. Lean.Parser.Leading­IdentBehavior.symbol
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  136. Lean.PrettyPrinter.Unexpand­M
  137. Lean.PrettyPrinter.Unexpander
  138. Lean.Source­Info
  139. Lean.SourceInfo.none
    1. Constructor of Lean.Source­Info
  140. Lean.SourceInfo.original
    1. Constructor of Lean.Source­Info
  141. Lean.SourceInfo.synthetic
    1. Constructor of Lean.Source­Info
  142. Lean.Syntax
  143. Lean.Syntax.Char­Lit
  144. Lean.Syntax.Command
  145. Lean.Syntax.Hygiene­Info
  146. Lean.Syntax.Ident
  147. Lean.Syntax.Level
  148. Lean.Syntax.Name­Lit
  149. Lean.Syntax.Num­Lit
  150. Lean.Syntax.Prec
  151. Lean.Syntax.Preresolved
  152. Lean.Syntax.Preresolved.decl
    1. Constructor of Lean.Syntax.Preresolved
  153. Lean.Syntax.Preresolved.namespace
    1. Constructor of Lean.Syntax.Preresolved
  154. Lean.Syntax.Prio
  155. Lean.Syntax.Scientific­Lit
  156. Lean.Syntax.Str­Lit
  157. Lean.Syntax.TSep­Array
  158. Lean.Syntax.TSepArray.mk
    1. Constructor of Lean.Syntax.TSep­Array
  159. Lean.Syntax.Tactic
  160. Lean.Syntax.Term
  161. Lean.Syntax.atom
    1. Constructor of Lean.Syntax
  162. Lean.Syntax.get­Kind
  163. Lean.Syntax.ident
    1. Constructor of Lean.Syntax
  164. Lean.Syntax.is­Of­Kind
  165. Lean.Syntax.missing
    1. Constructor of Lean.Syntax
  166. Lean.Syntax.node
    1. Constructor of Lean.Syntax
  167. Lean.Syntax.set­Kind
  168. Lean.Syntax­Node­Kind
  169. Lean.Syntax­Node­Kinds
  170. Lean.TSyntax
  171. Lean.TSyntax.get­Char
  172. Lean.TSyntax.get­Hygiene­Info
  173. Lean.TSyntax.get­Id
  174. Lean.TSyntax.get­Name
  175. Lean.TSyntax.get­Nat
  176. Lean.TSyntax.get­Scientific
  177. Lean.TSyntax.get­String
  178. Lean.TSyntax.mk
    1. Constructor of Lean.TSyntax
  179. Lean.TSyntax­Array
  180. Lean.char­Lit­Kind
  181. Lean.choice­Kind
  182. Lean.field­Idx­Kind
  183. Lean.group­Kind
  184. Lean.hygiene­Info­Kind
  185. Lean.ident­Kind
  186. Lean.interpolated­Str­Kind
  187. Lean.interpolated­Str­Lit­Kind
  188. Lean.name­Lit­Kind
  189. Lean.null­Kind
  190. Lean.num­Lit­Kind
  191. Lean.scientific­Lit­Kind
  192. Lean.str­Lit­Kind
  193. Lean­Exe­Config
    1. Lake.Lean­Exe­Config
  194. Lean­Lib­Config
    1. Lake.Lean­Lib­Config
  195. Lean­Option
    1. Lake.Lean­Option
  196. Level
    1. Lean.Syntax.Level
  197. Lex
    1. List.Lex
  198. List
  199. List.Is­Infix
  200. List.Is­Prefix
  201. List.Is­Suffix
  202. List.Lex
  203. List.Lex.cons
    1. Constructor of List.Lex
  204. List.Lex.nil
    1. Constructor of List.Lex
  205. List.Lex.rel
    1. Constructor of List.Lex
  206. List.Mem
  207. List.Mem.head
    1. Constructor of List.Mem
  208. List.Mem.tail
    1. Constructor of List.Mem
  209. List.Nodup
  210. List.Pairwise
  211. List.Pairwise.cons
    1. Constructor of List.Pairwise
  212. List.Pairwise.nil
    1. Constructor of List.Pairwise
  213. List.Perm
  214. List.Perm.cons
    1. Constructor of List.Perm
  215. List.Perm.nil
    1. Constructor of List.Perm
  216. List.Perm.swap
    1. Constructor of List.Perm
  217. List.Perm.trans
    1. Constructor of List.Perm
  218. List.Sublist
  219. List.Sublist.cons
    1. Constructor of List.Sublist
  220. List.Sublist.cons₂
    1. Constructor of List.Sublist
  221. List.Sublist.slnil
    1. Constructor of List.Sublist
  222. List.all
  223. List.all­M
  224. List.and
  225. List.any
  226. List.any­M
  227. List.append
  228. List.append­TR
  229. List.as­String
  230. List.attach
  231. List.attach­With
  232. List.beq
  233. List.concat
  234. List.cons
    1. Constructor of List
  235. List.contains
  236. List.count
  237. List.count­P
  238. List.drop
  239. List.drop­Last
  240. List.drop­Last­TR
  241. List.drop­While
  242. List.elem
  243. List.erase
  244. List.erase­Dups
  245. List.erase­Idx
  246. List.erase­Idx­TR
  247. List.erase­P
  248. List.erase­PTR
  249. List.erase­Reps
  250. List.erase­TR
  251. List.extract
  252. List.filter
  253. List.filter­M
  254. List.filter­Map
  255. List.filter­Map­M
  256. List.filter­Map­TR
  257. List.filter­Rev­M
  258. List.filter­TR
  259. List.fin­Idx­Of?
  260. List.fin­Range
  261. List.find?
  262. List.find­Fin­Idx?
  263. List.find­Idx
  264. List.find­Idx?
  265. List.find­M?
  266. List.find­Some?
  267. List.find­Some­M?
  268. List.first­M
  269. List.flat­Map
  270. List.flat­Map­M
  271. List.flat­Map­TR
  272. List.flatten
  273. List.flatten­TR
  274. List.foldl
  275. List.foldl­M
  276. List.foldl­Rec­On
  277. List.foldr
  278. List.foldr­M
  279. List.foldr­Rec­On
  280. List.foldr­TR
  281. List.for­A
  282. List.for­M
  283. List.get
  284. List.get­D
  285. List.get­Last
  286. List.get­Last!
  287. List.get­Last?
  288. List.get­Last­D
  289. List.group­By­Key
  290. List.head
  291. List.head!
  292. List.head?
  293. List.head­D
  294. List.idx­Of
  295. List.idx­Of?
  296. List.insert
  297. List.insert­Idx
  298. List.insert­Idx­TR
  299. List.intercalate
  300. List.intercalate­TR
  301. List.intersperse
  302. List.intersperse­TR
  303. List.is­Empty
  304. List.is­Eqv
  305. List.is­Perm
  306. List.is­Prefix­Of
  307. List.is­Prefix­Of?
  308. List.is­Sublist
  309. List.is­Suffix­Of
  310. List.is­Suffix­Of?
  311. List.le
  312. List.leftpad
  313. List.leftpad­TR
  314. List.length
  315. List.length­TR
  316. List.lex
  317. List.lookup
  318. List.lt
  319. List.map
  320. List.map­A
  321. List.map­Fin­Idx
  322. List.map­Fin­Idx­M
  323. List.map­Idx
  324. List.map­Idx­M
  325. List.map­M
  326. List.map­M'
  327. List.map­Mono
  328. List.map­Mono­M
  329. List.map­TR
  330. List.max?
  331. List.merge
  332. List.merge­Sort
  333. List.min?
  334. List.modify
  335. List.modify­Head
  336. List.modify­TR
  337. List.modify­Tail­Idx
  338. List.nil
    1. Constructor of List
  339. List.of­Fn
  340. List.or
  341. List.partition
  342. List.partition­M
  343. List.partition­Map
  344. List.pmap
  345. List.range
  346. List.range'
  347. List.range'TR
  348. List.remove­All
  349. List.replace
  350. List.replace­TR
  351. List.replicate
  352. List.replicate­TR
  353. List.reverse
  354. List.rightpad
  355. List.rotate­Left
  356. List.rotate­Right
  357. List.set
  358. List.set­TR
  359. List.singleton
  360. List.span
  361. List.split­At
  362. List.split­By
  363. List.sum
  364. List.tail
  365. List.tail!
  366. List.tail?
  367. List.tail­D
  368. List.take
  369. List.take­TR
  370. List.take­While
  371. List.take­While­TR
  372. List.to­Array
  373. List.to­Array­Impl
  374. List.to­Byte­Array
  375. List.to­Float­Array
  376. List.to­String
  377. List.unattach
  378. List.unzip
  379. List.unzip­TR
  380. List.zip
  381. List.zip­Idx
  382. List.zip­Idx­TR
  383. List.zip­With
  384. List.zip­With­All
  385. List.zip­With­TR
  386. land
    1. Fin.land
  387. land
    1. ISize.land
  388. land
    1. Int16.land
  389. land
    1. Int32.land
  390. land
    1. Int64.land
  391. land
    1. Int8.land
  392. land
    1. Nat.land
  393. land
    1. UInt16.land
  394. land
    1. UInt32.land
  395. land
    1. UInt64.land
  396. land
    1. UInt8.land
  397. land
    1. USize.land
  398. last
    1. Fin.last
  399. last­Cases
    1. Fin.last­Cases
  400. lazy­Pure
    1. IO.lazy­Pure
  401. lcm
    1. Int.lcm
  402. lcm
    1. Nat.lcm
  403. le
    1. Char.le
  404. le
    1. Float.le
  405. le
    1. Float32.le
  406. le
    1. ISize.le
  407. le
    1. Int.le
  408. le
    1. Int16.le
  409. le
    1. Int32.le
  410. le
    1. Int64.le
  411. le
    1. Int8.le
  412. le
    1. LE.le (class method)
  413. le
    1. List.le
  414. le
    1. Nat.le
  415. le
    1. String.le
  416. le
    1. UInt16.le
  417. le
    1. UInt32.le
  418. le
    1. UInt64.le
  419. le
    1. UInt8.le
  420. le
    1. USize.le
  421. le­Of­Ord
  422. lean (Lake command)
  423. lean_is_array
  424. lean_is_string
  425. lean_string_object (0) (1)
  426. lean_to_array
  427. lean_to_string
  428. left (0) (1)
  429. left
    1. And.left (structure field)
  430. leftpad
    1. Array.leftpad
  431. leftpad
    1. List.leftpad
  432. leftpad­TR
    1. List.leftpad­TR
  433. length
    1. List.length
  434. length
    1. String.length
  435. length­TR
    1. List.length­TR
  436. let
  437. let rec
  438. let'
  439. let­I
  440. level
    1. of universe
  441. lex'
    1. Ord.lex'
  442. lex
    1. Array.lex
  443. lex
    1. List.lex
  444. lex
    1. Ord.lex
  445. lex­Lt
    1. Prod.lex­Lt
  446. lhs
  447. lib­Name
    1. [anonymous] (structure field)
  448. lift
    1. Except­CpsT.lift
  449. lift
    1. ExceptT.lift
  450. lift
    1. OptionT.lift
  451. lift
    1. Quot.lift
  452. lift
    1. Quotient.lift
  453. lift
    1. Squash.lift
  454. lift
    1. State­CpsT.lift
  455. lift
    1. State­RefT'.lift
  456. lift
    1. StateT.lift
  457. lift­On
    1. Quot.lift­On
  458. lift­On
    1. Quotient.lift­On
  459. lift­On₂
    1. Quotient.lift­On₂
  460. lift­With
    1. MonadControl.lift­With (class method)
  461. lift­With
    1. Monad­ControlT.lift­With (class method)
  462. lift₂
    1. Quotient.lift₂
  463. line­Eq
  464. lines
    1. IO.FS.lines
  465. lint (Lake command)
  466. linter.unnecessary­Simpa
  467. literal
    1. raw string
  468. literal
    1. string
  469. lock
    1. IO.FS.Handle.lock
  470. log
    1. Float.log
  471. log
    1. Float32.log
  472. log10
    1. Float.log10
  473. log10
    1. Float32.log10
  474. log2
    1. Fin.log2
  475. log2
    1. Float.log2
  476. log2
    1. Float32.log2
  477. log2
    1. Nat.log2
  478. log2
    1. UInt16.log2
  479. log2
    1. UInt32.log2
  480. log2
    1. UInt64.log2
  481. log2
    1. UInt8.log2
  482. log2
    1. USize.log2
  483. lookup
    1. List.lookup
  484. lor
    1. Fin.lor
  485. lor
    1. ISize.lor
  486. lor
    1. Int16.lor
  487. lor
    1. Int32.lor
  488. lor
    1. Int64.lor
  489. lor
    1. Int8.lor
  490. lor
    1. Nat.lor
  491. lor
    1. UInt16.lor
  492. lor
    1. UInt32.lor
  493. lor
    1. UInt64.lor
  494. lor
    1. UInt8.lor
  495. lor
    1. USize.lor
  496. lt
    1. Char.lt
  497. lt
    1. Float.lt
  498. lt
    1. Float32.lt
  499. lt
    1. ISize.lt
  500. lt
    1. Int.lt
  501. lt
    1. Int16.lt
  502. lt
    1. Int32.lt
  503. lt
    1. Int64.lt
  504. lt
    1. Int8.lt
  505. lt
    1. LT.lt (class method)
  506. lt
    1. List.lt
  507. lt
    1. Nat.lt
  508. lt
    1. Option.lt
  509. lt
    1. UInt16.lt
  510. lt
    1. UInt32.lt
  511. lt
    1. UInt64.lt
  512. lt
    1. UInt8.lt
  513. lt
    1. USize.lt
  514. lt­Of­Ord

M

  1. MProd
  2. MProd.mk
    1. Constructor of MProd
  3. Macro­M
    1. Lean.Macro­M
  4. Max
  5. Max.mk
    1. Instance constructor of Max
  6. Mem
    1. List.Mem
  7. Metadata
    1. IO.FS.Metadata
  8. Min
  9. Min.mk
    1. Instance constructor of Min
  10. Mod
  11. Mod.mk
    1. Instance constructor of Mod
  12. Mode
    1. IO.FS.Mode
  13. Monad
  14. Monad.mk
    1. Instance constructor of Monad
  15. Monad­Control
  16. MonadControl.mk
    1. Instance constructor of Monad­Control
  17. Monad­Control­T
  18. Monad­ControlT.mk
    1. Instance constructor of Monad­Control­T
  19. Monad­Eval
  20. MonadEval.mk
    1. Instance constructor of Monad­Eval
  21. Monad­Eval­T
  22. Monad­EvalT.mk
    1. Instance constructor of Monad­Eval­T
  23. Monad­Except
  24. MonadExcept.mk
    1. Instance constructor of Monad­Except
  25. MonadExcept.of­Except
  26. MonadExcept.or­Else
  27. MonadExcept.orelse'
  28. Monad­Except­Of
  29. Monad­ExceptOf.mk
    1. Instance constructor of Monad­Except­Of
  30. Monad­Finally
  31. MonadFinally.mk
    1. Instance constructor of Monad­Finally
  32. Monad­Functor
  33. MonadFunctor.mk
    1. Instance constructor of Monad­Functor
  34. Monad­Functor­T
  35. Monad­FunctorT.mk
    1. Instance constructor of Monad­Functor­T
  36. Monad­Lake­Env
    1. Lake.Monad­Lake­Env
  37. Monad­Lift
  38. MonadLift.mk
    1. Instance constructor of Monad­Lift
  39. Monad­Lift­T
  40. Monad­LiftT.mk
    1. Instance constructor of Monad­Lift­T
  41. Monad­Pretty­Format
    1. Std.Format.Monad­Pretty­Format
  42. Monad­Reader
  43. MonadReader.mk
    1. Instance constructor of Monad­Reader
  44. Monad­Reader­Of
  45. Monad­ReaderOf.mk
    1. Instance constructor of Monad­Reader­Of
  46. Monad­State
  47. MonadState.get
  48. MonadState.mk
    1. Instance constructor of Monad­State
  49. MonadState.modify­Get
  50. Monad­State­Of
  51. Monad­StateOf.mk
    1. Instance constructor of Monad­State­Of
  52. Monad­With­Reader
  53. Monad­WithReader.mk
    1. Instance constructor of Monad­With­Reader
  54. Monad­With­Reader­Of
  55. Monad­With­ReaderOf.mk
    1. Instance constructor of Monad­With­Reader­Of
  56. Monad­Workspace
    1. Lake.Monad­Workspace
  57. Mul
  58. Mul.mk
    1. Instance constructor of Mul
  59. Mutex
    1. Std.Mutex
  60. main goal
  61. map
    1. Array.map
  62. map
    1. EStateM.map
  63. map
    1. Except.map
  64. map
    1. ExceptT.map
  65. map
    1. Functor.map (class method)
  66. map
    1. List.map
  67. map
    1. Option.map
  68. map
    1. Prod.map
  69. map
    1. StateT.map
  70. map
    1. Std.DHashMap.map
  71. map
    1. Std.DTreeMap.map
  72. map
    1. Std.Ext­DHashMap.map
  73. map
    1. Std.Ext­HashMap.map
  74. map
    1. Std.HashMap.map
  75. map
    1. Std.TreeMap.map
  76. map
    1. String.map
  77. map
    1. Sum.map
  78. map
    1. Task.map
  79. map
    1. Thunk.map
  80. map
    1. dependent
  81. map
    1. extensional
  82. map­A
    1. List.map­A
  83. map­A
    1. Option.map­A
  84. map­Const
    1. Functor.map­Const (class method)
  85. map­Error
    1. Except.map­Error
  86. map­Fin­Idx
    1. Array.map­Fin­Idx
  87. map­Fin­Idx
    1. List.map­Fin­Idx
  88. map­Fin­Idx­M
    1. Array.map­Fin­Idx­M
  89. map­Fin­Idx­M
    1. List.map­Fin­Idx­M
  90. map­Idx
    1. Array.map­Idx
  91. map­Idx
    1. List.map­Idx
  92. map­Idx­M
    1. Array.map­Idx­M
  93. map­Idx­M
    1. List.map­Idx­M
  94. map­List
    1. Task.map­List
  95. map­M'
    1. Array.map­M'
  96. map­M'
    1. List.map­M'
  97. map­M
    1. Array.map­M
  98. map­M
    1. List.map­M
  99. map­M
    1. Option.map­M
  100. map­Mono
    1. Array.map­Mono
  101. map­Mono
    1. List.map­Mono
  102. map­Mono­M
    1. Array.map­Mono­M
  103. map­Mono­M
    1. List.map­Mono­M
  104. map­Rev
    1. Functor.map­Rev
  105. map­TR
    1. List.map­TR
  106. map­Task
    1. BaseIO.map­Task
  107. map­Task
    1. EIO.map­Task
  108. map­Task
    1. IO.map­Task
  109. map­Tasks
    1. BaseIO.map­Tasks
  110. map­Tasks
    1. EIO.map­Tasks
  111. map­Tasks
    1. IO.map­Tasks
  112. map_const
    1. LawfulFunctor.map_const (class method)
  113. map_pure
    1. LawfulApplicative.seq­Left_eq (class method)
  114. 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. Quotient.mk'
  177. mk
    1. ExceptT.mk
  178. mk
    1. IO.FS.Handle.mk
  179. mk
    1. OptionT.mk
  180. mk
    1. Quot.mk
  181. mk
    1. Quotient.mk
  182. mk
    1. Squash.mk
  183. mk­File­Path
    1. System.mk­File­Path
  184. mk­Iterator
    1. String.mk­Iterator
  185. mk­Ref
    1. IO.mk­Ref
  186. mk­Ref
    1. ST.mk­Ref
  187. mk­Std­Gen
  188. mod
    1. Fin.mod
  189. mod
    1. ISize.mod
  190. mod
    1. Int16.mod
  191. mod
    1. Int32.mod
  192. mod
    1. Int64.mod
  193. mod
    1. Int8.mod
  194. mod
    1. Mod.mod (class method)
  195. mod
    1. Nat.mod
  196. mod
    1. UInt16.mod
  197. mod
    1. UInt32.mod
  198. mod
    1. UInt64.mod
  199. mod
    1. UInt8.mod
  200. mod
    1. USize.mod
  201. mod­Core
    1. Nat.mod­Core
  202. modified
    1. IO.FS.Metadata.modified (structure field)
  203. modify
  204. modify
    1. Array.modify
  205. modify
    1. List.modify
  206. modify
    1. ST.Ref.modify
  207. modify
    1. Std.DHashMap.modify
  208. modify
    1. Std.DTreeMap.modify
  209. modify
    1. Std.Ext­DHashMap.modify
  210. modify
    1. Std.Ext­HashMap.modify
  211. modify
    1. Std.HashMap.modify
  212. modify
    1. Std.TreeMap.modify
  213. modify
    1. String.modify
  214. modify­Get
    1. EStateM.modify­Get
  215. modify­Get
    1. MonadState.modify­Get
  216. modify­Get
    1. MonadState.modify­Get (class method)
  217. modify­Get
    1. Monad­StateOf.modify­Get (class method)
  218. modify­Get
    1. ST.Ref.modify­Get
  219. modify­Get
    1. State­RefT'.modify­Get
  220. modify­Get
    1. StateT.modify­Get
  221. modify­Get­The
  222. modify­Head
    1. List.modify­Head
  223. modify­M
    1. Array.modify­M
  224. modify­Op
    1. Array.modify­Op
  225. modify­TR
    1. List.modify­TR
  226. modify­Tail­Idx
    1. List.modify­Tail­Idx
  227. modify­The
  228. modn
    1. Fin.modn
  229. monad­Eval
    1. MonadEval.monad­Eval (class method)
  230. monad­Eval
    1. Monad­EvalT.monad­Eval (class method)
  231. monad­Lift
    1. MonadLift.monad­Lift (class method)
  232. monad­Lift
    1. Monad­LiftT.monad­Lift (class method)
  233. monad­Map
    1. MonadFunctor.monad­Map (class method)
  234. monad­Map
    1. Monad­FunctorT.monad­Map (class method)
  235. mono­Ms­Now
    1. IO.mono­Ms­Now
  236. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  237. monotone
    1. Lean.Order.monotone
  238. mp
    1. Eq.mp
  239. mp
    1. Iff.mp (structure field)
  240. mpr
    1. Eq.mpr
  241. mpr
    1. Iff.mpr (structure field)
  242. msb
    1. BitVec.msb
  243. mul
    1. BitVec.mul
  244. mul
    1. Fin.mul
  245. mul
    1. Float.mul
  246. mul
    1. Float32.mul
  247. mul
    1. ISize.mul
  248. mul
    1. Int.mul
  249. mul
    1. Int16.mul
  250. mul
    1. Int32.mul
  251. mul
    1. Int64.mul
  252. mul
    1. Int8.mul
  253. mul
    1. Mul.mul (class method)
  254. mul
    1. Nat.mul
  255. mul
    1. UInt16.mul
  256. mul
    1. UInt32.mul
  257. mul
    1. UInt64.mul
  258. mul
    1. UInt8.mul
  259. mul
    1. USize.mul
  260. mul­Rec
    1. BitVec.mul­Rec
  261. 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­Pow
  85. NatPow.mk
    1. Instance constructor of Nat­Pow
  86. Ne­Zero
  87. NeZero.mk
    1. Instance constructor of Ne­Zero
  88. Neg
  89. Neg.mk
    1. Instance constructor of Neg
  90. New­Goals
    1. Lean.Meta.Rewrite.New­Goals
  91. Nodup
    1. List.Nodup
  92. Nonempty
  93. Nonempty.intro
    1. Constructor of Nonempty
  94. Not
  95. Not.elim
  96. Num­Lit
    1. Lean.Syntax.Num­Lit
  97. name
    1. Lake.LeanOption.name (structure field)
  98. name­Lit­Kind
    1. Lean.name­Lit­Kind
  99. namespace
    1. of inductive type
  100. nat­Abs
    1. Int.nat­Abs
  101. nat­Add
    1. Fin.nat­Add
  102. nat­Cast
    1. NatCast.nat­Cast (class method)
  103. native­Facets
    1. [anonymous] (structure field) (0) (1)
  104. native_decide
  105. ndrec
    1. HEq.ndrec
  106. ndrec­On
    1. HEq.ndrec­On
  107. needs
    1. [anonymous] (structure field) (0) (1)
  108. neg
    1. BitVec.neg
  109. neg
    1. Float.neg
  110. neg
    1. Float32.neg
  111. neg
    1. ISize.neg
  112. neg
    1. Int.neg
  113. neg
    1. Int16.neg
  114. neg
    1. Int32.neg
  115. neg
    1. Int64.neg
  116. neg
    1. Int8.neg
  117. neg
    1. Neg.neg (class method)
  118. neg
    1. UInt16.neg
  119. neg
    1. UInt32.neg
  120. neg
    1. UInt64.neg
  121. neg
    1. UInt8.neg
  122. neg
    1. USize.neg
  123. neg­Of­Nat
    1. Int.neg­Of­Nat
  124. nest­D
    1. Std.Format.nest­D
  125. neutral­Config
    1. Lean.Meta.Simp.neutral­Config
  126. new (Lake command)
  127. new
    1. IO.Promise.new
  128. new
    1. Std.Channel.new
  129. new
    1. Std.CloseableChannel.new
  130. new
    1. Std.Condvar.new
  131. new
    1. Std.Mutex.new
  132. new­Goals
    1. Lean.Meta.Rewrite.Config.new­Goals (structure field)
  133. next
  134. next ... => ...
  135. next'
    1. String.next'
  136. next
    1. RandomGen.next (class method)
  137. next
    1. String.Iterator.next
  138. next
    1. String.next
  139. next
    1. Substring.next
  140. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  141. next­Until
    1. String.next­Until
  142. next­While
    1. String.next­While
  143. nextn
    1. String.Iterator.nextn
  144. nextn
    1. Substring.nextn
  145. nil
    1. BitVec.nil
  146. nofun
  147. nomatch
  148. non­Backtrackable
    1. EStateM.non­Backtrackable
  149. norm_cast (0) (1)
  150. normalize
    1. System.FilePath.normalize
  151. not
    1. BitVec.not
  152. not
    1. Bool.not
  153. not
    1. Int.not
  154. not­M
  155. notify­All
    1. Std.Condvar.notify­All
  156. notify­One
    1. Std.Condvar.notify­One
  157. null­Kind
    1. Lean.null­Kind
  158. num­Bits
    1. System.Platform.num­Bits
  159. 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. Ordering
  74. Ordering.eq
    1. Constructor of Ordering
  75. Ordering.gt
    1. Constructor of Ordering
  76. Ordering.is­Eq
  77. Ordering.is­GE
  78. Ordering.is­GT
  79. Ordering.is­LE
  80. Ordering.is­LT
  81. Ordering.is­Ne
  82. Ordering.lt
    1. Constructor of Ordering
  83. Ordering.swap
  84. Ordering.then
  85. Output
    1. IO.Process.Output
  86. obtain
  87. occs
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  88. of­Array
    1. Std.Ext­HashSet.of­Array
  89. of­Array
    1. Std.HashSet.of­Array
  90. of­Array
    1. Std.TreeMap.of­Array
  91. of­Array
    1. Std.TreeSet.of­Array
  92. of­Binary­Scientific
    1. Float.of­Binary­Scientific
  93. of­Binary­Scientific
    1. Float32.of­Binary­Scientific
  94. of­Bit­Vec
    1. ISize.of­Bit­Vec
  95. of­Bit­Vec
    1. Int16.of­Bit­Vec
  96. of­Bit­Vec
    1. Int32.of­Bit­Vec
  97. of­Bit­Vec
    1. Int64.of­Bit­Vec
  98. of­Bit­Vec
    1. Int8.of­Bit­Vec
  99. of­Bits
    1. Float.of­Bits
  100. of­Bits
    1. Float32.of­Bits
  101. of­Bool
    1. BitVec.of­Bool
  102. of­Bool­List­BE
    1. BitVec.of­Bool­List­BE
  103. of­Bool­List­LE
    1. BitVec.of­Bool­List­LE
  104. of­Buffer
    1. IO.FS.Stream.of­Buffer
  105. of­Except
    1. IO.of­Except
  106. of­Except
    1. MonadExcept.of­Except
  107. of­Fin
    1. UInt16.of­Fin
  108. of­Fin
    1. UInt32.of­Fin
  109. of­Fin
    1. UInt64.of­Fin
  110. of­Fin
    1. UInt8.of­Fin
  111. of­Fin
    1. USize.of­Fin
  112. of­Fn
    1. Array.of­Fn
  113. of­Fn
    1. List.of­Fn
  114. of­Handle
    1. IO.FS.Stream.of­Handle
  115. of­Int
    1. BitVec.of­Int
  116. of­Int
    1. Float.of­Int
  117. of­Int
    1. Float32.of­Int
  118. of­Int
    1. ISize.of­Int
  119. of­Int
    1. Int16.of­Int
  120. of­Int
    1. Int32.of­Int
  121. of­Int
    1. Int64.of­Int
  122. of­Int
    1. Int8.of­Int
  123. of­Int­LE
    1. ISize.of­Int­LE
  124. of­Int­LE
    1. Int16.of­Int­LE
  125. of­Int­LE
    1. Int32.of­Int­LE
  126. of­Int­LE
    1. Int64.of­Int­LE
  127. of­Int­LE
    1. Int8.of­Int­LE
  128. of­Int­Truncate
    1. ISize.of­Int­Truncate
  129. of­Int­Truncate
    1. Int16.of­Int­Truncate
  130. of­Int­Truncate
    1. Int32.of­Int­Truncate
  131. of­Int­Truncate
    1. Int64.of­Int­Truncate
  132. of­Int­Truncate
    1. Int8.of­Int­Truncate
  133. of­List
    1. Std.DHashMap.of­List
  134. of­List
    1. Std.DTreeMap.of­List
  135. of­List
    1. Std.Ext­DHashMap.of­List
  136. of­List
    1. Std.Ext­HashMap.of­List
  137. of­List
    1. Std.Ext­HashSet.of­List
  138. of­List
    1. Std.HashMap.of­List
  139. of­List
    1. Std.HashSet.of­List
  140. of­List
    1. Std.TreeMap.of­List
  141. of­List
    1. Std.TreeSet.of­List
  142. of­Nat
    1. BitVec.of­Nat
  143. of­Nat
    1. Char.of­Nat
  144. of­Nat
    1. Fin.of­Nat
  145. of­Nat
    1. Float.of­Nat
  146. of­Nat
    1. Float32.of­Nat
  147. of­Nat
    1. ISize.of­Nat
  148. of­Nat
    1. Int16.of­Nat
  149. of­Nat
    1. Int32.of­Nat
  150. of­Nat
    1. Int64.of­Nat
  151. of­Nat
    1. Int8.of­Nat
  152. of­Nat
    1. OfNat.of­Nat (class method)
  153. of­Nat
    1. UInt16.of­Nat
  154. of­Nat
    1. UInt32.of­Nat
  155. of­Nat
    1. UInt64.of­Nat
  156. of­Nat
    1. UInt8.of­Nat
  157. of­Nat
    1. USize.of­Nat
  158. of­Nat32
    1. USize.of­Nat32
  159. of­Nat­LT
    1. BitVec.of­Nat­LT
  160. of­Nat­LT
    1. UInt16.of­Nat­LT
  161. of­Nat­LT
    1. UInt32.of­Nat­LT
  162. of­Nat­LT
    1. UInt64.of­Nat­LT
  163. of­Nat­LT
    1. UInt8.of­Nat­LT
  164. of­Nat­LT
    1. USize.of­Nat­LT
  165. of­Nat­Truncate
    1. UInt16.of­Nat­Truncate
  166. of­Nat­Truncate
    1. UInt32.of­Nat­Truncate
  167. of­Nat­Truncate
    1. UInt64.of­Nat­Truncate
  168. of­Nat­Truncate
    1. UInt8.of­Nat­Truncate
  169. of­Nat­Truncate
    1. USize.of­Nat­Truncate
  170. of­Scientific
    1. Float.of­Scientific
  171. of­Scientific
    1. Float32.of­Scientific
  172. of­Scientific
    1. OfScientific.of­Scientific (class method)
  173. of­Subarray
    1. Array.of­Subarray
  174. of­UInt8
    1. Char.of­UInt8
  175. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  176. offset­Of­Pos
    1. String.offset­Of­Pos
  177. omega
  178. on
    1. Ord.on
  179. open
  180. opposite
    1. Ord.opposite
  181. opt­Param
  182. optional
  183. or
    1. BitVec.or
  184. or
    1. Bool.or
  185. or
    1. List.or
  186. or
    1. Option.or
  187. or­Else'
    1. EStateM.or­Else'
  188. or­Else
    1. EStateM.or­Else
  189. or­Else
    1. MonadExcept.or­Else
  190. or­Else
    1. Option.or­Else
  191. or­Else
    1. OptionT.or­Else
  192. or­Else
    1. ReaderT.or­Else
  193. or­Else
    1. StateT.or­Else
  194. or­Else
    1. [anonymous] (class method)
  195. or­Else­Lazy
    1. Except.or­Else­Lazy
  196. or­M
  197. orelse'
    1. MonadExcept.orelse'
  198. other
    1. IO.FileRight.other (structure field)
  199. out
    1. NeZero.out (class method)
  200. out
    1. Std.DTreeMap.Raw.WF.out (structure field)
  201. out
    1. Std.HashMap.Raw.WF.out (structure field)
  202. out
    1. Std.HashSet.Raw.WF.out (structure field)
  203. out
    1. Std.TreeMap.Raw.WF.out (structure field)
  204. out
    1. Std.TreeSet.Raw.WF.out (structure field)
  205. out­Param
  206. output
    1. IO.Process.output
  207. override list (Elan command)
  208. override set (Elan command)
  209. override unset (Elan command)

P

  1. PEmpty
  2. PEmpty.elim
  3. PLift
  4. PLift.up
    1. Constructor of PLift
  5. PProd
  6. PProd.mk
    1. Constructor of PProd
  7. PSigma
  8. PSigma.mk
    1. Constructor of PSigma
  9. PSum
  10. PSum.inhabited­Left
  11. PSum.inhabited­Right
  12. PSum.inl
    1. Constructor of PSum
  13. PSum.inr
    1. Constructor of PSum
  14. PUnit
  15. PUnit.unit
    1. Constructor of PUnit
  16. Pairwise
    1. List.Pairwise
  17. Partial­Order
    1. Lean.Order.Partial­Order
  18. Perm
    1. List.Perm
  19. Pos
    1. String.Pos
  20. Pow
  21. Pow.mk
    1. Instance constructor of Pow
  22. Prec
    1. Lean.Syntax.Prec
  23. Preresolved
    1. Lean.Syntax.Preresolved
  24. Prio
    1. Lean.Syntax.Prio
  25. Priority
    1. Task.Priority
  26. Prod
  27. Prod.all­I
  28. Prod.any­I
  29. Prod.fold­I
  30. Prod.lex­Lt
  31. Prod.map
  32. Prod.mk
    1. Constructor of Prod
  33. Prod.swap
  34. Promise
    1. IO.Promise
  35. Prop
  36. Pure
  37. Pure.mk
    1. Instance constructor of Pure
  38. pack (Lake command)
  39. parameter
    1. of inductive type
  40. paren
    1. Std.Format.paren
  41. parent
    1. System.FilePath.parent
  42. parser
  43. partition
    1. Array.partition
  44. partition
    1. List.partition
  45. partition
    1. Std.DHashMap.partition
  46. partition
    1. Std.DTreeMap.partition
  47. partition
    1. Std.HashMap.partition
  48. partition
    1. Std.HashSet.partition
  49. partition
    1. Std.TreeMap.partition
  50. partition
    1. Std.TreeSet.partition
  51. partition­M
    1. List.partition­M
  52. partition­Map
    1. List.partition­Map
  53. path
    1. IO.FS.DirEntry.path
  54. path­Exists
    1. System.FilePath.path­Exists
  55. path­Separator
    1. System.FilePath.path­Separator
  56. path­Separators
    1. System.FilePath.path­Separators
  57. pattern
  58. pbind
    1. Option.pbind
  59. pelim
    1. Option.pelim
  60. placeholder term
  61. pmap
    1. Array.pmap
  62. pmap
    1. List.pmap
  63. pmap
    1. Option.pmap
  64. polymorphism
    1. universe
  65. pop
    1. Array.pop
  66. pop­Front
    1. Subarray.pop­Front
  67. pop­While
    1. Array.pop­While
  68. pos
    1. IO.FS.Stream.Buffer.pos (structure field)
  69. pos
    1. String.Iterator.pos
  70. pos­Of
    1. String.pos­Of
  71. pos­Of
    1. Substring.pos­Of
  72. pow
    1. Float.pow
  73. pow
    1. Float32.pow
  74. pow
    1. HomogeneousPow.pow (class method)
  75. pow
    1. Int.pow
  76. pow
    1. Nat.pow
  77. pow
    1. NatPow.pow (class method)
  78. pow
    1. Pow.pow (class method)
  79. pp
    1. eval.pp
  80. pp.deep­Terms
  81. pp.deepTerms.threshold
  82. pp.field­Notation
  83. pp.match
  84. pp.max­Steps
  85. pp.mvars
  86. pp.proofs
  87. pp.proofs.threshold
  88. precompile­Modules
    1. [anonymous] (structure field)
  89. pred
    1. Fin.pred
  90. pred
    1. Nat.pred
  91. predicative
  92. prefix­Join
    1. Std.Format.prefix­Join
  93. pretty
    1. Std.Format.pretty
  94. pretty­M
    1. Std.Format.pretty­M
  95. prev
    1. String.Iterator.prev
  96. prev
    1. String.prev
  97. prev
    1. Substring.prev
  98. prevn
    1. String.Iterator.prevn
  99. prevn
    1. Substring.prevn
  100. print
    1. IO.print
  101. println
    1. IO.println
  102. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
  103. proj
    1. Lean.Meta.Simp.Config.proj (structure field)
  104. proof state
  105. proofs
    1. pp.proofs
  106. property
    1. Subtype.property (structure field)
  107. propext
  108. proposition
  109. proposition
    1. decidable
  110. ptr­Addr­Unsafe
  111. ptr­Eq
  112. ptr­Eq
    1. ST.Ref.ptr­Eq
  113. ptr­Eq­List
  114. pure
    1. EStateM.pure
  115. pure
    1. Except.pure
  116. pure
    1. ExceptT.pure
  117. pure
    1. OptionT.pure
  118. pure
    1. Pure.pure (class method)
  119. pure
    1. ReaderT.pure
  120. pure
    1. StateT.pure
  121. pure
    1. Task.pure
  122. pure
    1. Thunk.pure
  123. pure_bind
    1. [anonymous] (class method)
  124. pure_seq
    1. [anonymous] (class method)
  125. push
    1. Array.push
  126. push
    1. String.push
  127. push­Newline
    1. Std.Format.Monad­PrettyFormat.push­Newline (class method)
  128. push­Output
    1. Std.Format.Monad­PrettyFormat.push­Output (class method)
  129. push_cast
  130. pushn
    1. String.pushn
  131. put­Str
    1. IO.FS.Handle.put­Str
  132. put­Str
    1. IO.FS.Stream.put­Str (structure field)
  133. put­Str­Ln
    1. IO.FS.Handle.put­Str­Ln
  134. 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. r
    1. Setoid.r (class method)
  27. rand
    1. IO.rand
  28. rand­Bool
  29. rand­Nat
  30. range'
    1. Array.range'
  31. range'
    1. List.range'
  32. range'TR
    1. List.range'TR
  33. range
    1. Array.range
  34. range
    1. List.range
  35. range
    1. RandomGen.range (class method)
  36. raw
    1. Lean.TSyntax.raw (structure field)
  37. rcases
  38. read
    1. IO.AccessRight.read (structure field)
  39. read
    1. IO.FS.Handle.read
  40. read
    1. IO.FS.Stream.read (structure field)
  41. read
    1. MonadReader.read (class method)
  42. read
    1. Monad­ReaderOf.read (class method)
  43. read
    1. ReaderT.read
  44. read­Bin­File
    1. IO.FS.read­Bin­File
  45. read­Bin­To­End
    1. IO.FS.Handle.read­Bin­To­End
  46. read­Bin­To­End­Into
    1. IO.FS.Handle.read­Bin­To­End­Into
  47. read­Dir
    1. System.FilePath.read­Dir
  48. read­File
    1. IO.FS.read­File
  49. read­The
  50. read­To­End
    1. IO.FS.Handle.read­To­End
  51. real­Path
    1. IO.FS.real­Path
  52. rec
    1. Quot.rec
  53. rec
    1. Quotient.rec
  54. rec­Aux
    1. Nat.rec­Aux
  55. rec­On
    1. Quot.rec­On
  56. rec­On
    1. Quotient.rec­On
  57. rec­On­Subsingleton
    1. Quot.rec­On­Subsingleton
  58. rec­On­Subsingleton
    1. Quotient.rec­On­Subsingleton
  59. rec­On­Subsingleton₂
    1. Quotient.rec­On­Subsingleton₂
  60. recursor
  61. recv
    1. Std.Channel.recv
  62. reduce
  63. reduction
    1. ι (iota)
  64. refine
  65. refine'
  66. refl
    1. Equivalence.refl (structure field)
  67. refl
    1. Setoid.refl
  68. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  69. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  70. rel
    1. Lean.Order.PartialOrder.rel (class method)
  71. rel
    1. Well­FoundedRelation.rel (class method)
  72. rel_antisymm
    1. Lean.Order.PartialOrder.rel_antisymm (class method)
  73. rel_refl
    1. Lean.Order.PartialOrder.rel_refl (class method)
  74. rel_trans
    1. Lean.Order.PartialOrder.rel_trans (class method)
  75. relaxed­Auto­Implicit
  76. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  77. remaining­To­String
    1. String.Iterator.remaining­To­String
  78. remove­All
    1. List.remove­All
  79. remove­Dir
    1. IO.FS.remove­Dir
  80. remove­Dir­All
    1. IO.FS.remove­Dir­All
  81. remove­File
    1. IO.FS.remove­File
  82. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  83. rename
  84. rename
    1. IO.FS.rename
  85. rename_i
  86. repeat (0) (1)
  87. repeat'
  88. repeat
    1. Nat.repeat
  89. repeat1'
  90. repeat­TR
    1. Nat.repeat­TR
  91. replace
  92. replace
    1. Array.replace
  93. replace
    1. List.replace
  94. replace
    1. String.replace
  95. replace­TR
    1. List.replace­TR
  96. replicate
    1. Array.replicate
  97. replicate
    1. BitVec.replicate
  98. replicate
    1. List.replicate
  99. replicate­TR
    1. List.replicate­TR
  100. repr
  101. repr
    1. Int.repr
  102. repr
    1. Nat.repr
  103. repr
    1. Option.repr
  104. repr
    1. USize.repr
  105. repr
    1. eval.derive.repr
  106. repr­Arg
  107. repr­Prec
    1. Repr.repr­Prec (class method)
  108. repr­Str
  109. resolve
    1. IO.Promise.resolve
  110. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  111. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  112. restore
    1. EStateM.Backtrackable.restore (class method)
  113. restore­M
    1. MonadControl.restore­M (class method)
  114. restore­M
    1. Monad­ControlT.restore­M (class method)
  115. result!
    1. IO.Promise.result!
  116. result
    1. trace.compiler.ir.result
  117. result?
    1. IO.Promise.result?
  118. result­D
    1. IO.Promise.result­D
  119. rev
    1. Fin.rev
  120. rev­Find
    1. String.rev­Find
  121. rev­Pos­Of
    1. String.rev­Pos­Of
  122. reverse
    1. Array.reverse
  123. reverse
    1. BitVec.reverse
  124. reverse
    1. List.reverse
  125. reverse­Induction
    1. Fin.reverse­Induction
  126. revert
  127. rewind
    1. IO.FS.Handle.rewind
  128. rewrite (0) (1)
  129. rewrite
    1. trace.Meta.Tactic.simp.rewrite
  130. rfl (0) (1) (2)
  131. rfl'
  132. rfl
    1. HEq.rfl
  133. rhs
  134. right (0) (1)
  135. right
    1. And.right (structure field)
  136. rightpad
    1. Array.rightpad
  137. rightpad
    1. List.rightpad
  138. rintro
  139. root
    1. IO.FS.DirEntry.root (structure field)
  140. root
    1. [anonymous] (structure field)
  141. roots
    1. [anonymous] (structure field)
  142. rotate­Left
    1. BitVec.rotate­Left
  143. rotate­Left
    1. List.rotate­Left
  144. rotate­Right
    1. BitVec.rotate­Right
  145. rotate­Right
    1. List.rotate­Right
  146. rotate_left
  147. rotate_right
  148. round
    1. Float.round
  149. round
    1. Float32.round
  150. run (Elan command)
  151. run'
    1. EStateM.run'
  152. run'
    1. State­CpsT.run'
  153. run'
    1. State­RefT'.run'
  154. run'
    1. StateT.run'
  155. run
    1. EStateM.run
  156. run
    1. Except­CpsT.run
  157. run
    1. ExceptT.run
  158. run
    1. IO.Process.run
  159. run
    1. Id.run
  160. run
    1. OptionT.run
  161. run
    1. ReaderT.run
  162. run
    1. State­CpsT.run
  163. run
    1. State­RefT'.run
  164. run
    1. StateT.run
  165. run­Catch
    1. Except­CpsT.run­Catch
  166. run­EST
  167. run­K
    1. Except­CpsT.run­K
  168. run­K
    1. State­CpsT.run­K
  169. run­ST
  170. run_tac
  171. rw (0) (1)
  172. rw?
  173. rw_mod_cast
  174. 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. Seq
  18. Seq.mk
    1. Instance constructor of Seq
  19. Seq­Left
  20. SeqLeft.mk
    1. Instance constructor of Seq­Left
  21. Seq­Right
  22. SeqRight.mk
    1. Instance constructor of Seq­Right
  23. Setoid
  24. Setoid.mk
    1. Instance constructor of Setoid
  25. Setoid.refl
  26. Setoid.symm
  27. Setoid.trans
  28. Shift­Left
  29. ShiftLeft.mk
    1. Instance constructor of Shift­Left
  30. Shift­Right
  31. ShiftRight.mk
    1. Instance constructor of Shift­Right
  32. Sigma
  33. Sigma.mk
    1. Constructor of Sigma
  34. Simp­Extension
    1. Lean.Meta.Simp­Extension
  35. Size­Of
  36. SizeOf.mk
    1. Instance constructor of Size­Of
  37. Sort
  38. Source­Info
    1. Lean.Source­Info
  39. Spawn­Args
    1. IO.Process.Spawn­Args
  40. Squash
  41. Squash.ind
  42. Squash.lift
  43. Squash.mk
  44. State­Cps­T
  45. State­CpsT.lift
  46. State­CpsT.run
  47. State­CpsT.run'
  48. State­CpsT.run­K
  49. State­M
  50. State­Ref­T'
  51. State­RefT'.get
  52. State­RefT'.lift
  53. State­RefT'.modify­Get
  54. State­RefT'.run
  55. State­RefT'.run'
  56. State­RefT'.set
  57. State­T
  58. StateT.bind
  59. StateT.failure
  60. StateT.get
  61. StateT.lift
  62. StateT.map
  63. StateT.modify­Get
  64. StateT.or­Else
  65. StateT.pure
  66. StateT.run
  67. StateT.run'
  68. StateT.set
  69. Std.Atomic­T
  70. Std.Channel
  71. Std.Channel.Sync
  72. Std.Channel.for­Async
  73. Std.Channel.new
  74. Std.Channel.recv
  75. Std.Channel.send
  76. Std.Channel.sync
  77. Std.Closeable­Channel
  78. Std.CloseableChannel.new
  79. Std.Condvar
  80. Std.Condvar.new
  81. Std.Condvar.notify­All
  82. Std.Condvar.notify­One
  83. Std.Condvar.wait
  84. Std.Condvar.wait­Until
  85. Std.DHash­Map
  86. Std.DHashMap.Equiv
  87. Std.DHashMap.Equiv.mk
    1. Constructor of Std.DHashMap.Equiv
  88. Std.DHashMap.Raw
  89. Std.DHashMap.Raw.WF
  90. Std.DHashMap.Raw.WF.alter₀
    1. Constructor of Std.DHashMap.Raw.WF
  91. Std.DHashMap.Raw.WF.const­Alter₀
    1. Constructor of Std.DHashMap.Raw.WF
  92. Std.DHashMap.Raw.WF.const­Get­Then­Insert­If­New?₀
    1. Constructor of Std.DHashMap.Raw.WF
  93. Std.DHashMap.Raw.WF.const­Modify₀
    1. Constructor of Std.DHashMap.Raw.WF
  94. Std.DHashMap.Raw.WF.contains­Then­Insert­If­New₀
    1. Constructor of Std.DHashMap.Raw.WF
  95. Std.DHashMap.Raw.WF.contains­Then­Insert₀
    1. Constructor of Std.DHashMap.Raw.WF
  96. Std.DHashMap.Raw.WF.empty­With­Capacity₀
    1. Constructor of Std.DHashMap.Raw.WF
  97. Std.DHashMap.Raw.WF.erase₀
    1. Constructor of Std.DHashMap.Raw.WF
  98. Std.DHashMap.Raw.WF.filter₀
    1. Constructor of Std.DHashMap.Raw.WF
  99. Std.DHashMap.Raw.WF.get­Then­Insert­If­New?₀
    1. Constructor of Std.DHashMap.Raw.WF
  100. Std.DHashMap.Raw.WF.insert­If­New₀
    1. Constructor of Std.DHashMap.Raw.WF
  101. Std.DHashMap.Raw.WF.insert₀
    1. Constructor of Std.DHashMap.Raw.WF
  102. Std.DHashMap.Raw.WF.modify₀
    1. Constructor of Std.DHashMap.Raw.WF
  103. Std.DHashMap.Raw.WF.wf
    1. Constructor of Std.DHashMap.Raw.WF
  104. Std.DHashMap.Raw.mk
    1. Constructor of Std.DHashMap.Raw
  105. Std.DHashMap.alter
  106. Std.DHashMap.contains
  107. Std.DHashMap.contains­Then­Insert
  108. Std.DHashMap.contains­Then­Insert­If­New
  109. Std.DHashMap.empty­With­Capacity
  110. Std.DHashMap.erase
  111. Std.DHashMap.filter
  112. Std.DHashMap.filter­Map
  113. Std.DHashMap.fold
  114. Std.DHashMap.fold­M
  115. Std.DHashMap.for­In
  116. Std.DHashMap.for­M
  117. Std.DHashMap.get
  118. Std.DHashMap.get!
  119. Std.DHashMap.get?
  120. Std.DHashMap.get­D
  121. Std.DHashMap.get­Key
  122. Std.DHashMap.get­Key!
  123. Std.DHashMap.get­Key?
  124. Std.DHashMap.get­Key­D
  125. Std.DHashMap.get­Then­Insert­If­New?
  126. Std.DHashMap.insert
  127. Std.DHashMap.insert­If­New
  128. Std.DHashMap.insert­Many
  129. Std.DHashMap.is­Empty
  130. Std.DHashMap.keys
  131. Std.DHashMap.keys­Array
  132. Std.DHashMap.map
  133. Std.DHashMap.modify
  134. Std.DHashMap.of­List
  135. Std.DHashMap.partition
  136. Std.DHashMap.size
  137. Std.DHashMap.to­Array
  138. Std.DHashMap.to­List
  139. Std.DHashMap.union
  140. Std.DHashMap.values
  141. Std.DHashMap.values­Array
  142. Std.DTree­Map
  143. Std.DTreeMap.Raw
  144. Std.DTreeMap.Raw.WF
  145. Std.DTreeMap.Raw.WF.mk
    1. Constructor of Std.DTreeMap.Raw.WF
  146. Std.DTreeMap.Raw.mk
    1. Constructor of Std.DTreeMap.Raw
  147. Std.DTreeMap.alter
  148. Std.DTreeMap.contains
  149. Std.DTreeMap.contains­Then­Insert
  150. Std.DTreeMap.contains­Then­Insert­If­New
  151. Std.DTreeMap.empty
  152. Std.DTreeMap.erase
  153. Std.DTreeMap.filter
  154. Std.DTreeMap.filter­Map
  155. Std.DTreeMap.foldl
  156. Std.DTreeMap.foldl­M
  157. Std.DTreeMap.for­In
  158. Std.DTreeMap.for­M
  159. Std.DTreeMap.get
  160. Std.DTreeMap.get!
  161. Std.DTreeMap.get?
  162. Std.DTreeMap.get­D
  163. Std.DTreeMap.get­Key
  164. Std.DTreeMap.get­Key!
  165. Std.DTreeMap.get­Key?
  166. Std.DTreeMap.get­Key­D
  167. Std.DTreeMap.get­Then­Insert­If­New?
  168. Std.DTreeMap.insert
  169. Std.DTreeMap.insert­If­New
  170. Std.DTreeMap.insert­Many
  171. Std.DTreeMap.is­Empty
  172. Std.DTreeMap.keys
  173. Std.DTreeMap.keys­Array
  174. Std.DTreeMap.map
  175. Std.DTreeMap.modify
  176. Std.DTreeMap.of­List
  177. Std.DTreeMap.partition
  178. Std.DTreeMap.size
  179. Std.DTreeMap.to­Array
  180. Std.DTreeMap.to­List
  181. Std.DTreeMap.values
  182. Std.DTreeMap.values­Array
  183. Std.Ext­DHash­Map
  184. Std.Ext­DHashMap.alter
  185. Std.Ext­DHashMap.contains
  186. Std.Ext­DHashMap.contains­Then­Insert
  187. Std.Ext­DHashMap.contains­Then­Insert­If­New
  188. Std.Ext­DHashMap.empty­With­Capacity
  189. Std.Ext­DHashMap.erase
  190. Std.Ext­DHashMap.filter
  191. Std.Ext­DHashMap.filter­Map
  192. Std.Ext­DHashMap.get
  193. Std.Ext­DHashMap.get!
  194. Std.Ext­DHashMap.get?
  195. Std.Ext­DHashMap.get­D
  196. Std.Ext­DHashMap.get­Key
  197. Std.Ext­DHashMap.get­Key!
  198. Std.Ext­DHashMap.get­Key?
  199. Std.Ext­DHashMap.get­Key­D
  200. Std.Ext­DHashMap.get­Then­Insert­If­New?
  201. Std.Ext­DHashMap.insert
  202. Std.Ext­DHashMap.insert­If­New
  203. Std.Ext­DHashMap.insert­Many
  204. Std.Ext­DHashMap.is­Empty
  205. Std.Ext­DHashMap.map
  206. Std.Ext­DHashMap.modify
  207. Std.Ext­DHashMap.of­List
  208. Std.Ext­DHashMap.size
  209. Std.Ext­Hash­Map
  210. Std.Ext­HashMap.alter
  211. Std.Ext­HashMap.contains
  212. Std.Ext­HashMap.contains­Then­Insert
  213. Std.Ext­HashMap.contains­Then­Insert­If­New
  214. Std.Ext­HashMap.empty­With­Capacity
  215. Std.Ext­HashMap.erase
  216. Std.Ext­HashMap.filter
  217. Std.Ext­HashMap.filter­Map
  218. Std.Ext­HashMap.get
  219. Std.Ext­HashMap.get!
  220. Std.Ext­HashMap.get?
  221. Std.Ext­HashMap.get­D
  222. Std.Ext­HashMap.get­Key
  223. Std.Ext­HashMap.get­Key!
  224. Std.Ext­HashMap.get­Key?
  225. Std.Ext­HashMap.get­Key­D
  226. Std.Ext­HashMap.get­Then­Insert­If­New?
  227. Std.Ext­HashMap.insert
  228. Std.Ext­HashMap.insert­If­New
  229. Std.Ext­HashMap.insert­Many
  230. Std.Ext­HashMap.insert­Many­If­New­Unit
  231. Std.Ext­HashMap.is­Empty
  232. Std.Ext­HashMap.map
  233. Std.Ext­HashMap.modify
  234. Std.Ext­HashMap.of­List
  235. Std.Ext­HashMap.size
  236. Std.Ext­HashMap.unit­Of­Array
  237. Std.Ext­HashMap.unit­Of­List
  238. Std.Ext­Hash­Set
  239. Std.Ext­HashSet.contains
  240. Std.Ext­HashSet.contains­Then­Insert
  241. Std.Ext­HashSet.empty­With­Capacity
  242. Std.Ext­HashSet.erase
  243. Std.Ext­HashSet.filter
  244. Std.Ext­HashSet.get
  245. Std.Ext­HashSet.get!
  246. Std.Ext­HashSet.get?
  247. Std.Ext­HashSet.get­D
  248. Std.Ext­HashSet.insert
  249. Std.Ext­HashSet.insert­Many
  250. Std.Ext­HashSet.is­Empty
  251. Std.Ext­HashSet.mk
    1. Constructor of Std.Ext­Hash­Set
  252. Std.Ext­HashSet.of­Array
  253. Std.Ext­HashSet.of­List
  254. Std.Ext­HashSet.size
  255. Std.Format
  256. Std.Format.Flatten­Behavior
  257. Std.Format.FlattenBehavior.all­Or­None
    1. Constructor of Std.Format.Flatten­Behavior
  258. Std.Format.FlattenBehavior.fill
    1. Constructor of Std.Format.Flatten­Behavior
  259. Std.Format.Monad­Pretty­Format
  260. Std.Format.Monad­PrettyFormat.mk
    1. Instance constructor of Std.Format.Monad­Pretty­Format
  261. Std.Format.align
    1. Constructor of Std.Format
  262. Std.Format.append
    1. Constructor of Std.Format
  263. Std.Format.bracket
  264. Std.Format.bracket­Fill
  265. Std.Format.def­Indent
  266. Std.Format.def­Width
  267. Std.Format.fill
  268. Std.Format.group
    1. Constructor of Std.Format
  269. Std.Format.indent­D
  270. Std.Format.is­Empty
  271. Std.Format.is­Nil
  272. Std.Format.join
  273. Std.Format.join­Sep
  274. Std.Format.join­Suffix
  275. Std.Format.line
    1. Constructor of Std.Format
  276. Std.Format.nest
    1. Constructor of Std.Format
  277. Std.Format.nest­D
  278. Std.Format.nil
    1. Constructor of Std.Format
  279. Std.Format.paren
  280. Std.Format.prefix­Join
  281. Std.Format.pretty
  282. Std.Format.pretty­M
  283. Std.Format.sbracket
  284. Std.Format.tag
    1. Constructor of Std.Format
  285. Std.Format.text
    1. Constructor of Std.Format
  286. Std.Hash­Map
  287. Std.HashMap.Equiv
  288. Std.HashMap.Equiv.mk
    1. Constructor of Std.HashMap.Equiv
  289. Std.HashMap.Raw
  290. Std.HashMap.Raw.WF
  291. Std.HashMap.Raw.WF.mk
    1. Constructor of Std.HashMap.Raw.WF
  292. Std.HashMap.Raw.mk
    1. Constructor of Std.HashMap.Raw
  293. Std.HashMap.alter
  294. Std.HashMap.contains
  295. Std.HashMap.contains­Then­Insert
  296. Std.HashMap.contains­Then­Insert­If­New
  297. Std.HashMap.empty­With­Capacity
  298. Std.HashMap.erase
  299. Std.HashMap.filter
  300. Std.HashMap.filter­Map
  301. Std.HashMap.fold
  302. Std.HashMap.fold­M
  303. Std.HashMap.for­In
  304. Std.HashMap.for­M
  305. Std.HashMap.get
  306. Std.HashMap.get!
  307. Std.HashMap.get?
  308. Std.HashMap.get­D
  309. Std.HashMap.get­Key
  310. Std.HashMap.get­Key!
  311. Std.HashMap.get­Key?
  312. Std.HashMap.get­Key­D
  313. Std.HashMap.get­Then­Insert­If­New?
  314. Std.HashMap.insert
  315. Std.HashMap.insert­If­New
  316. Std.HashMap.insert­Many
  317. Std.HashMap.insert­Many­If­New­Unit
  318. Std.HashMap.is­Empty
  319. Std.HashMap.keys
  320. Std.HashMap.keys­Array
  321. Std.HashMap.map
  322. Std.HashMap.modify
  323. Std.HashMap.of­List
  324. Std.HashMap.partition
  325. Std.HashMap.size
  326. Std.HashMap.to­Array
  327. Std.HashMap.to­List
  328. Std.HashMap.union
  329. Std.HashMap.unit­Of­Array
  330. Std.HashMap.unit­Of­List
  331. Std.HashMap.values
  332. Std.HashMap.values­Array
  333. Std.Hash­Set
  334. Std.HashSet.Equiv
  335. Std.HashSet.Equiv.mk
    1. Constructor of Std.HashSet.Equiv
  336. Std.HashSet.Raw
  337. Std.HashSet.Raw.WF
  338. Std.HashSet.Raw.WF.mk
    1. Constructor of Std.HashSet.Raw.WF
  339. Std.HashSet.Raw.mk
    1. Constructor of Std.HashSet.Raw
  340. Std.HashSet.all
  341. Std.HashSet.any
  342. Std.HashSet.contains
  343. Std.HashSet.contains­Then­Insert
  344. Std.HashSet.empty­With­Capacity
  345. Std.HashSet.erase
  346. Std.HashSet.filter
  347. Std.HashSet.fold
  348. Std.HashSet.fold­M
  349. Std.HashSet.for­In
  350. Std.HashSet.for­M
  351. Std.HashSet.get
  352. Std.HashSet.get!
  353. Std.HashSet.get?
  354. Std.HashSet.get­D
  355. Std.HashSet.insert
  356. Std.HashSet.insert­Many
  357. Std.HashSet.is­Empty
  358. Std.HashSet.mk
    1. Constructor of Std.Hash­Set
  359. Std.HashSet.of­Array
  360. Std.HashSet.of­List
  361. Std.HashSet.partition
  362. Std.HashSet.size
  363. Std.HashSet.to­Array
  364. Std.HashSet.to­List
  365. Std.HashSet.union
  366. Std.Mutex
  367. Std.Mutex.atomically
  368. Std.Mutex.atomically­Once
  369. Std.Mutex.new
  370. Std.To­Format
  371. Std.ToFormat.mk
    1. Instance constructor of Std.To­Format
  372. Std.Tree­Map
  373. Std.TreeMap.Raw
  374. Std.TreeMap.Raw.WF
  375. Std.TreeMap.Raw.WF.mk
    1. Constructor of Std.TreeMap.Raw.WF
  376. Std.TreeMap.Raw.mk
    1. Constructor of Std.TreeMap.Raw
  377. Std.TreeMap.all
  378. Std.TreeMap.alter
  379. Std.TreeMap.any
  380. Std.TreeMap.contains
  381. Std.TreeMap.contains­Then­Insert
  382. Std.TreeMap.contains­Then­Insert­If­New
  383. Std.TreeMap.empty
  384. Std.TreeMap.entry­At­Idx
  385. Std.TreeMap.entry­At­Idx!
  386. Std.TreeMap.entry­At­Idx?
  387. Std.TreeMap.entry­At­Idx­D
  388. Std.TreeMap.erase
  389. Std.TreeMap.erase­Many
  390. Std.TreeMap.filter
  391. Std.TreeMap.filter­Map
  392. Std.TreeMap.foldl
  393. Std.TreeMap.foldl­M
  394. Std.TreeMap.foldr
  395. Std.TreeMap.foldr­M
  396. Std.TreeMap.for­In
  397. Std.TreeMap.for­M
  398. Std.TreeMap.get
  399. Std.TreeMap.get!
  400. Std.TreeMap.get?
  401. Std.TreeMap.get­D
  402. Std.TreeMap.get­Entry­GE
  403. Std.TreeMap.get­Entry­GE!
  404. Std.TreeMap.get­Entry­GE?
  405. Std.TreeMap.get­Entry­GED
  406. Std.TreeMap.get­Entry­GT
  407. Std.TreeMap.get­Entry­GT!
  408. Std.TreeMap.get­Entry­GT?
  409. Std.TreeMap.get­Entry­GTD
  410. Std.TreeMap.get­Entry­LE
  411. Std.TreeMap.get­Entry­LE!
  412. Std.TreeMap.get­Entry­LE?
  413. Std.TreeMap.get­Entry­LED
  414. Std.TreeMap.get­Entry­LT
  415. Std.TreeMap.get­Entry­LT!
  416. Std.TreeMap.get­Entry­LT?
  417. Std.TreeMap.get­Entry­LTD
  418. Std.TreeMap.get­GE
  419. Std.TreeMap.get­GT
  420. Std.TreeMap.get­Key
  421. Std.TreeMap.get­Key!
  422. Std.TreeMap.get­Key?
  423. Std.TreeMap.get­Key­D
  424. Std.TreeMap.get­Key­GE
  425. Std.TreeMap.get­Key­GE!
  426. Std.TreeMap.get­Key­GE?
  427. Std.TreeMap.get­Key­GED
  428. Std.TreeMap.get­Key­GT
  429. Std.TreeMap.get­Key­GT!
  430. Std.TreeMap.get­Key­GT?
  431. Std.TreeMap.get­Key­GTD
  432. Std.TreeMap.get­Key­LE
  433. Std.TreeMap.get­Key­LE!
  434. Std.TreeMap.get­Key­LE?
  435. Std.TreeMap.get­Key­LED
  436. Std.TreeMap.get­Key­LT
  437. Std.TreeMap.get­Key­LT!
  438. Std.TreeMap.get­Key­LT?
  439. Std.TreeMap.get­Key­LTD
  440. Std.TreeMap.get­LE
  441. Std.TreeMap.get­LT
  442. Std.TreeMap.get­Then­Insert­If­New?
  443. Std.TreeMap.insert
  444. Std.TreeMap.insert­If­New
  445. Std.TreeMap.insert­Many
  446. Std.TreeMap.insert­Many­If­New­Unit
  447. Std.TreeMap.is­Empty
  448. Std.TreeMap.key­At­Idx
  449. Std.TreeMap.key­At­Idx!
  450. Std.TreeMap.key­At­Idx?
  451. Std.TreeMap.key­At­Idx­D
  452. Std.TreeMap.keys
  453. Std.TreeMap.keys­Array
  454. Std.TreeMap.map
  455. Std.TreeMap.max­Entry
  456. Std.TreeMap.max­Entry!
  457. Std.TreeMap.max­Entry?
  458. Std.TreeMap.max­Entry­D
  459. Std.TreeMap.max­Key
  460. Std.TreeMap.max­Key!
  461. Std.TreeMap.max­Key?
  462. Std.TreeMap.max­Key­D
  463. Std.TreeMap.merge­With
  464. Std.TreeMap.min­Entry
  465. Std.TreeMap.min­Entry!
  466. Std.TreeMap.min­Entry?
  467. Std.TreeMap.min­Entry­D
  468. Std.TreeMap.min­Key
  469. Std.TreeMap.min­Key!
  470. Std.TreeMap.min­Key?
  471. Std.TreeMap.min­Key­D
  472. Std.TreeMap.modify
  473. Std.TreeMap.of­Array
  474. Std.TreeMap.of­List
  475. Std.TreeMap.partition
  476. Std.TreeMap.size
  477. Std.TreeMap.to­Array
  478. Std.TreeMap.to­List
  479. Std.TreeMap.unit­Of­Array
  480. Std.TreeMap.unit­Of­List
  481. Std.TreeMap.values
  482. Std.TreeMap.values­Array
  483. Std.Tree­Set
  484. Std.TreeSet.Raw
  485. Std.TreeSet.Raw.WF
  486. Std.TreeSet.Raw.WF.mk
    1. Constructor of Std.TreeSet.Raw.WF
  487. Std.TreeSet.Raw.mk
    1. Constructor of Std.TreeSet.Raw
  488. Std.TreeSet.all
  489. Std.TreeSet.any
  490. Std.TreeSet.at­Idx
  491. Std.TreeSet.at­Idx!
  492. Std.TreeSet.at­Idx?
  493. Std.TreeSet.at­Idx­D
  494. Std.TreeSet.contains
  495. Std.TreeSet.contains­Then­Insert
  496. Std.TreeSet.empty
  497. Std.TreeSet.erase
  498. Std.TreeSet.erase­Many
  499. Std.TreeSet.filter
  500. Std.TreeSet.foldl
  501. Std.TreeSet.foldl­M
  502. Std.TreeSet.foldr
  503. Std.TreeSet.foldr­M
  504. Std.TreeSet.for­In
  505. Std.TreeSet.for­M
  506. Std.TreeSet.get
  507. Std.TreeSet.get!
  508. Std.TreeSet.get?
  509. Std.TreeSet.get­D
  510. Std.TreeSet.get­GE!
  511. Std.TreeSet.get­GE?
  512. Std.TreeSet.get­GED
  513. Std.TreeSet.get­GT!
  514. Std.TreeSet.get­GT?
  515. Std.TreeSet.get­GTD
  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­LTD
  522. Std.TreeSet.insert
  523. Std.TreeSet.insert­Many
  524. Std.TreeSet.is­Empty
  525. Std.TreeSet.max
  526. Std.TreeSet.max!
  527. Std.TreeSet.max?
  528. Std.TreeSet.max­D
  529. Std.TreeSet.merge
  530. Std.TreeSet.min
  531. Std.TreeSet.min!
  532. Std.TreeSet.min?
  533. Std.TreeSet.min­D
  534. Std.TreeSet.of­Array
  535. Std.TreeSet.of­List
  536. Std.TreeSet.partition
  537. Std.TreeSet.size
  538. Std.TreeSet.to­Array
  539. Std.TreeSet.to­List
  540. Std­Gen
  541. Stdio
    1. IO.Process.Stdio
  542. Stdio­Config
    1. IO.Process.Stdio­Config
  543. Str­Lit
    1. Lean.Syntax.Str­Lit
  544. Stream
    1. IO.FS.Stream
  545. String
  546. String.Iterator
  547. String.Iterator.at­End
  548. String.Iterator.curr
  549. String.Iterator.extract
  550. String.Iterator.forward
  551. String.Iterator.has­Next
  552. String.Iterator.has­Prev
  553. String.Iterator.mk
    1. Constructor of String.Iterator
  554. String.Iterator.next
  555. String.Iterator.nextn
  556. String.Iterator.pos
  557. String.Iterator.prev
  558. String.Iterator.prevn
  559. String.Iterator.remaining­Bytes
  560. String.Iterator.remaining­To­String
  561. String.Iterator.set­Curr
  562. String.Iterator.to­End
  563. String.Pos
  564. String.Pos.is­Valid
  565. String.Pos.min
  566. String.Pos.mk
    1. Constructor of String.Pos
  567. String.all
  568. String.any
  569. String.append
  570. String.at­End
  571. String.back
  572. String.capitalize
  573. String.contains
  574. String.crlf­To­Lf
  575. String.dec­Eq
  576. String.decapitalize
  577. String.drop
  578. String.drop­Prefix?
  579. String.drop­Right
  580. String.drop­Right­While
  581. String.drop­Suffix?
  582. String.drop­While
  583. String.end­Pos
  584. String.ends­With
  585. String.extract
  586. String.find
  587. String.find­Line­Start
  588. String.first­Diff­Pos
  589. String.foldl
  590. String.foldr
  591. String.from­UTF8
  592. String.from­UTF8!
  593. String.from­UTF8?
  594. String.front
  595. String.get
  596. String.get!
  597. String.get'
  598. String.get?
  599. String.get­Utf8Byte
  600. String.hash
  601. String.intercalate
  602. String.is­Empty
  603. String.is­Int
  604. String.is­Nat
  605. String.is­Prefix­Of
  606. String.iter
  607. String.join
  608. String.le
  609. String.length
  610. String.map
  611. String.mk
    1. Constructor of String
  612. String.mk­Iterator
  613. String.modify
  614. String.next
  615. String.next'
  616. String.next­Until
  617. String.next­While
  618. String.offset­Of­Pos
  619. String.pos­Of
  620. String.prev
  621. String.push
  622. String.pushn
  623. String.quote
  624. String.remove­Leading­Spaces
  625. String.replace
  626. String.rev­Find
  627. String.rev­Pos­Of
  628. String.set
  629. String.singleton
  630. String.split
  631. String.split­On
  632. String.starts­With
  633. String.strip­Prefix
  634. String.strip­Suffix
  635. String.substr­Eq
  636. String.take
  637. String.take­Right
  638. String.take­Right­While
  639. String.take­While
  640. String.to­Format
  641. String.to­Int!
  642. String.to­Int?
  643. String.to­List
  644. String.to­Lower
  645. String.to­Name
  646. String.to­Nat!
  647. String.to­Nat?
  648. String.to­Substring
  649. String.to­Substring'
  650. String.to­UTF8
  651. String.to­Upper
  652. String.trim
  653. String.trim­Left
  654. String.trim­Right
  655. String.utf8Byte­Size
  656. String.utf8Decode­Char?
  657. String.utf8Encode­Char
  658. String.validate­UTF8
  659. Sub
  660. Sub.mk
    1. Instance constructor of Sub
  661. Subarray
  662. Subarray.all
  663. Subarray.all­M
  664. Subarray.any
  665. Subarray.any­M
  666. Subarray.drop
  667. Subarray.empty
  668. Subarray.find­Rev?
  669. Subarray.find­Rev­M?
  670. Subarray.find­Some­Rev­M?
  671. Subarray.foldl
  672. Subarray.foldl­M
  673. Subarray.foldr
  674. Subarray.foldr­M
  675. Subarray.for­In
  676. Subarray.for­M
  677. Subarray.for­Rev­M
  678. Subarray.get
  679. Subarray.get!
  680. Subarray.get­D
  681. Subarray.mk
    1. Constructor of Subarray
  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­At
    1. List.split­At
  947. split­By
    1. List.split­By
  948. split­On
    1. String.split­On
  949. split­On
    1. Substring.split­On
  950. sqrt
    1. Float.sqrt
  951. sqrt
    1. Float32.sqrt
  952. src­Dir
    1. [anonymous] (structure field) (0) (1)
  953. srem
    1. BitVec.srem
  954. sshift­Right'
    1. BitVec.sshift­Right'
  955. sshift­Right
    1. BitVec.sshift­Right
  956. sshift­Right­Rec
    1. BitVec.sshift­Right­Rec
  957. ssub­Overflow
    1. BitVec.ssub­Overflow
  958. st­M
    1. MonadControl.st­M (class method)
  959. st­M
    1. Monad­ControlT.st­M (class method)
  960. start
    1. Subarray.start (structure field)
  961. start­Pos
    1. Substring.start­Pos (structure field)
  962. start­Tag
    1. Std.Format.Monad­PrettyFormat.start­Tag (class method)
  963. start_le_stop
    1. Subarray.start_le_stop (structure field)
  964. starts­With
    1. String.starts­With
  965. std­Next
  966. std­Range
  967. std­Split
  968. stderr
    1. IO.Process.Child.stderr (structure field)
  969. stderr
    1. IO.Process.Output.stderr (structure field)
  970. stderr
    1. IO.Process.StdioConfig.stderr (structure field)
  971. stdin
    1. IO.Process.Child.stdin (structure field)
  972. stdin
    1. IO.Process.StdioConfig.stdin (structure field)
  973. stdout
    1. IO.Process.Child.stdout (structure field)
  974. stdout
    1. IO.Process.Output.stdout (structure field)
  975. stdout
    1. IO.Process.StdioConfig.stdout (structure field)
  976. stop
  977. stop
    1. Subarray.stop (structure field)
  978. stop­Pos
    1. Substring.stop­Pos (structure field)
  979. stop_le_array_size
    1. Subarray.stop_le_array_size (structure field)
  980. str
    1. Substring.str (structure field)
  981. str­Lit­Kind
    1. Lean.str­Lit­Kind
  982. strip­Prefix
    1. String.strip­Prefix
  983. strip­Suffix
    1. String.strip­Suffix
  984. strong­Rec­On
    1. Nat.strong­Rec­On
  985. sub
    1. BitVec.sub
  986. sub
    1. Fin.sub
  987. sub
    1. Float.sub
  988. sub
    1. Float32.sub
  989. sub
    1. ISize.sub
  990. sub
    1. Int.sub
  991. sub
    1. Int16.sub
  992. sub
    1. Int32.sub
  993. sub
    1. Int64.sub
  994. sub
    1. Int8.sub
  995. sub
    1. Nat.sub
  996. sub
    1. Sub.sub (class method)
  997. sub
    1. UInt16.sub
  998. sub
    1. UInt32.sub
  999. sub
    1. UInt64.sub
  1000. sub
    1. UInt8.sub
  1001. sub
    1. USize.sub
  1002. sub­Digit­Char
    1. Nat.sub­Digit­Char
  1003. sub­Nat
    1. Fin.sub­Nat
  1004. sub­Nat­Nat
    1. Int.sub­Nat­Nat
  1005. subst
  1006. subst
    1. Eq.subst
  1007. subst
    1. HEq.subst
  1008. subst_eqs
  1009. subst_vars
  1010. substr­Eq
    1. String.substr­Eq
  1011. succ
    1. Fin.succ
  1012. succ­Rec
    1. Fin.succ­Rec
  1013. succ­Rec­On
    1. Fin.succ­Rec­On
  1014. suffices
  1015. sum
    1. Array.sum
  1016. sum
    1. List.sum
  1017. super­Digit­Char
    1. Nat.super­Digit­Char
  1018. support­Interpreter
    1. [anonymous] (structure field)
  1019. swap
    1. Array.swap
  1020. swap
    1. Ordering.swap
  1021. swap
    1. Prod.swap
  1022. swap
    1. ST.Ref.swap
  1023. swap
    1. Sum.swap
  1024. swap­At!
    1. Array.swap­At!
  1025. swap­At
    1. Array.swap­At
  1026. swap­If­In­Bounds
    1. Array.swap­If­In­Bounds
  1027. symm
  1028. symm
    1. Eq.symm
  1029. symm
    1. Equivalence.symm (structure field)
  1030. symm
    1. Setoid.symm
  1031. symm_saturate
  1032. sync
    1. Std.Channel.sync
  1033. synthInstance.max­Heartbeats
  1034. synthInstance.max­Size
  1035. 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. Trans
  26. Trans.mk
    1. Instance constructor of Trans
  27. Transparency­Mode
    1. Lean.Meta.Transparency­Mode
  28. Tree­Map
    1. Std.Tree­Map
  29. Tree­Set
    1. Std.Tree­Set
  30. True
  31. True.intro
    1. Constructor of True
  32. Type
  33. tactic
  34. tactic'
  35. tactic.custom­Eliminators
  36. tactic.hygienic
  37. tactic.simp.trace (0) (1)
  38. tactic.skip­Assigned­Instances
  39. tail!
    1. List.tail!
  40. tail
    1. List.tail
  41. tail?
    1. List.tail?
  42. tail­D
    1. List.tail­D
  43. take
    1. Array.take
  44. take
    1. List.take
  45. take
    1. ST.Ref.take
  46. take
    1. String.take
  47. take
    1. Subarray.take
  48. take
    1. Substring.take
  49. take­Right
    1. String.take­Right
  50. take­Right
    1. Substring.take­Right
  51. take­Right­While
    1. String.take­Right­While
  52. take­Right­While
    1. Substring.take­Right­While
  53. take­Stdin
    1. IO.Process.Child.take­Stdin
  54. take­TR
    1. List.take­TR
  55. take­While
    1. Array.take­While
  56. take­While
    1. List.take­While
  57. take­While
    1. String.take­While
  58. take­While
    1. Substring.take­While
  59. take­While­TR
    1. List.take­While­TR
  60. tan
    1. Float.tan
  61. tan
    1. Float32.tan
  62. tanh
    1. Float.tanh
  63. tanh
    1. Float32.tanh
  64. target
    1. System.Platform.target
  65. tdiv
    1. Int.tdiv
  66. term
    1. placeholder
  67. test (Lake command)
  68. test­Bit
    1. Nat.test­Bit
  69. then
    1. Ordering.then
  70. threshold
    1. pp.deepTerms.threshold
  71. threshold
    1. pp.proofs.threshold
  72. throw
    1. EStateM.throw
  73. throw
    1. MonadExcept.throw (class method)
  74. throw
    1. Monad­ExceptOf.throw (class method)
  75. throw­Error
    1. Lean.Macro.throw­Error
  76. throw­Error­At
    1. Lean.Macro.throw­Error­At
  77. throw­The
  78. throw­Unsupported
    1. Lean.Macro.throw­Unsupported
  79. tmod
    1. Int.tmod
  80. to­Applicative
    1. Alternative.to­Applicative (class method)
  81. to­Applicative
    1. Monad.to­Applicative (class method)
  82. to­Array
    1. List.to­Array
  83. to­Array
    1. Option.to­Array
  84. to­Array
    1. Std.DHashMap.to­Array
  85. to­Array
    1. Std.DTreeMap.to­Array
  86. to­Array
    1. Std.HashMap.to­Array
  87. to­Array
    1. Std.HashSet.to­Array
  88. to­Array
    1. Std.TreeMap.to­Array
  89. to­Array
    1. Std.TreeSet.to­Array
  90. to­Array
    1. Subarray.to­Array
  91. to­Array­Impl
    1. List.to­Array­Impl
  92. to­BEq
    1. Ord.to­BEq
  93. to­Base­IO
    1. EIO.to­Base­IO
  94. to­Bind
    1. [anonymous] (class method)
  95. to­Bit­Vec
    1. ISize.to­Bit­Vec
  96. to­Bit­Vec
    1. Int16.to­Bit­Vec
  97. to­Bit­Vec
    1. Int32.to­Bit­Vec
  98. to­Bit­Vec
    1. Int64.to­Bit­Vec
  99. to­Bit­Vec
    1. Int8.to­Bit­Vec
  100. to­Bit­Vec
    1. UInt16.to­Bit­Vec (structure field)
  101. to­Bit­Vec
    1. UInt32.to­Bit­Vec (structure field)
  102. to­Bit­Vec
    1. UInt64.to­Bit­Vec (structure field)
  103. to­Bit­Vec
    1. UInt8.to­Bit­Vec (structure field)
  104. to­Bit­Vec
    1. USize.to­Bit­Vec (structure field)
  105. to­Bits
    1. Float.to­Bits
  106. to­Bits
    1. Float32.to­Bits
  107. to­Bool
    1. Except.to­Bool
  108. to­Byte­Array
    1. List.to­Byte­Array
  109. to­Digits
    1. Nat.to­Digits
  110. to­EIO
    1. BaseIO.to­EIO
  111. to­EIO
    1. IO.to­EIO
  112. to­End
    1. String.Iterator.to­End
  113. to­Fin
    1. BitVec.to­Fin (structure field)
  114. to­Fin
    1. UInt16.to­Fin
  115. to­Fin
    1. UInt32.to­Fin
  116. to­Fin
    1. UInt64.to­Fin
  117. to­Fin
    1. UInt8.to­Fin
  118. to­Fin
    1. USize.to­Fin
  119. to­Float
    1. Float32.to­Float
  120. to­Float
    1. ISize.to­Float
  121. to­Float
    1. Int16.to­Float
  122. to­Float
    1. Int32.to­Float
  123. to­Float
    1. Int64.to­Float
  124. to­Float
    1. Int8.to­Float
  125. to­Float
    1. Nat.to­Float
  126. to­Float
    1. UInt16.to­Float
  127. to­Float
    1. UInt32.to­Float
  128. to­Float
    1. UInt64.to­Float
  129. to­Float
    1. UInt8.to­Float
  130. to­Float
    1. USize.to­Float
  131. to­Float32
    1. Float.to­Float32
  132. to­Float32
    1. ISize.to­Float32
  133. to­Float32
    1. Int16.to­Float32
  134. to­Float32
    1. Int32.to­Float32
  135. to­Float32
    1. Int64.to­Float32
  136. to­Float32
    1. Int8.to­Float32
  137. to­Float32
    1. Nat.to­Float32
  138. to­Float32
    1. UInt16.to­Float32
  139. to­Float32
    1. UInt32.to­Float32
  140. to­Float32
    1. UInt64.to­Float32
  141. to­Float32
    1. UInt8.to­Float32
  142. to­Float32
    1. USize.to­Float32
  143. to­Float­Array
    1. List.to­Float­Array
  144. to­Format
    1. String.to­Format
  145. to­Functor
    1. Applicative.to­Functor (class method)
  146. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  147. to­Handle­Type
    1. IO.Process.Stdio.to­Handle­Type
  148. to­Hex
    1. BitVec.to­Hex
  149. to­IO'
    1. EIO.to­IO'
  150. to­IO
    1. BaseIO.to­IO
  151. to­IO
    1. EIO.to­IO
  152. to­ISize
    1. Bool.to­ISize
  153. to­ISize
    1. Float.to­ISize
  154. to­ISize
    1. Float32.to­ISize
  155. to­ISize
    1. Int.to­ISize
  156. to­ISize
    1. Int16.to­ISize
  157. to­ISize
    1. Int32.to­ISize
  158. to­ISize
    1. Int64.to­ISize
  159. to­ISize
    1. Int8.to­ISize
  160. to­ISize
    1. Nat.to­ISize
  161. to­ISize
    1. USize.to­ISize
  162. to­Int!
    1. String.to­Int!
  163. to­Int
    1. BitVec.to­Int
  164. to­Int
    1. Bool.to­Int
  165. to­Int
    1. ISize.to­Int
  166. to­Int
    1. Int16.to­Int
  167. to­Int
    1. Int32.to­Int
  168. to­Int
    1. Int64.to­Int
  169. to­Int
    1. Int8.to­Int
  170. to­Int16
    1. Bool.to­Int16
  171. to­Int16
    1. Float.to­Int16
  172. to­Int16
    1. Float32.to­Int16
  173. to­Int16
    1. ISize.to­Int16
  174. to­Int16
    1. Int.to­Int16
  175. to­Int16
    1. Int32.to­Int16
  176. to­Int16
    1. Int64.to­Int16
  177. to­Int16
    1. Int8.to­Int16
  178. to­Int16
    1. Nat.to­Int16
  179. to­Int16
    1. UInt16.to­Int16
  180. to­Int32
    1. Bool.to­Int32
  181. to­Int32
    1. Float.to­Int32
  182. to­Int32
    1. Float32.to­Int32
  183. to­Int32
    1. ISize.to­Int32
  184. to­Int32
    1. Int.to­Int32
  185. to­Int32
    1. Int16.to­Int32
  186. to­Int32
    1. Int64.to­Int32
  187. to­Int32
    1. Int8.to­Int32
  188. to­Int32
    1. Nat.to­Int32
  189. to­Int32
    1. UInt32.to­Int32
  190. to­Int64
    1. Bool.to­Int64
  191. to­Int64
    1. Float.to­Int64
  192. to­Int64
    1. Float32.to­Int64
  193. to­Int64
    1. ISize.to­Int64
  194. to­Int64
    1. Int.to­Int64
  195. to­Int64
    1. Int16.to­Int64
  196. to­Int64
    1. Int32.to­Int64
  197. to­Int64
    1. Int8.to­Int64
  198. to­Int64
    1. Nat.to­Int64
  199. to­Int64
    1. UInt64.to­Int64
  200. to­Int8
    1. Bool.to­Int8
  201. to­Int8
    1. Float.to­Int8
  202. to­Int8
    1. Float32.to­Int8
  203. to­Int8
    1. ISize.to­Int8
  204. to­Int8
    1. Int.to­Int8
  205. to­Int8
    1. Int16.to­Int8
  206. to­Int8
    1. Int32.to­Int8
  207. to­Int8
    1. Int64.to­Int8
  208. to­Int8
    1. Nat.to­Int8
  209. to­Int8
    1. UInt8.to­Int8
  210. to­Int?
    1. String.to­Int?
  211. to­Iterator
    1. Substring.to­Iterator
  212. to­LE
    1. Ord.to­LE
  213. to­LT
    1. Ord.to­LT
  214. to­Lawful­Applicative
    1. LawfulMonad.to­Lawful­Applicative (class method)
  215. to­Lawful­Functor
    1. LawfulApplicative.to­Lawful­Functor (class method)
  216. to­Lean­Config
    1. Lake.Lean­ExeConfig.to­Lean­Config (structure field)
  217. to­Lean­Config
    1. Lake.Lean­LibConfig.to­Lean­Config (structure field)
  218. to­List
    1. Array.to­List
  219. to­List
    1. Array.to­List (structure field)
  220. to­List
    1. Option.to­List
  221. to­List
    1. Std.DHashMap.to­List
  222. to­List
    1. Std.DTreeMap.to­List
  223. to­List
    1. Std.HashMap.to­List
  224. to­List
    1. Std.HashSet.to­List
  225. to­List
    1. Std.TreeMap.to­List
  226. to­List
    1. Std.TreeSet.to­List
  227. to­List
    1. String.to­List
  228. to­List­Append
    1. Array.to­List­Append
  229. to­List­Rev
    1. Array.to­List­Rev
  230. to­Lower
    1. Char.to­Lower
  231. to­Lower
    1. String.to­Lower
  232. to­Monad­State­Of
    1. ST.Ref.to­Monad­State­Of
  233. to­Name
    1. String.to­Name
  234. to­Name
    1. Substring.to­Name
  235. to­Nat!
    1. String.to­Nat!
  236. to­Nat
    1. BitVec.to­Nat
  237. to­Nat
    1. Bool.to­Nat
  238. to­Nat
    1. Char.to­Nat
  239. to­Nat
    1. Fin.to­Nat
  240. to­Nat
    1. Int.to­Nat
  241. to­Nat
    1. UInt16.to­Nat
  242. to­Nat
    1. UInt32.to­Nat
  243. to­Nat
    1. UInt64.to­Nat
  244. to­Nat
    1. UInt8.to­Nat
  245. to­Nat
    1. USize.to­Nat
  246. to­Nat?
    1. Int.to­Nat?
  247. to­Nat?
    1. String.to­Nat?
  248. to­Nat?
    1. Substring.to­Nat?
  249. to­Nat­Clamp­Neg
    1. ISize.to­Nat­Clamp­Neg
  250. to­Nat­Clamp­Neg
    1. Int16.to­Nat­Clamp­Neg
  251. to­Nat­Clamp­Neg
    1. Int32.to­Nat­Clamp­Neg
  252. to­Nat­Clamp­Neg
    1. Int64.to­Nat­Clamp­Neg
  253. to­Nat­Clamp­Neg
    1. Int8.to­Nat­Clamp­Neg
  254. to­Option
    1. Except.to­Option
  255. to­Partial­Equiv­BEq
    1. EquivBEq.to­Partial­Equiv­BEq (class method)
  256. to­Partial­Order
    1. Lean.Order.CCPO.to­Partial­Order (class method)
  257. to­Pure
    1. [anonymous] (class method)
  258. to­Refl­BEq
    1. LawfulBEq.to­Refl­BEq (class method)
  259. to­Refl­BEq
    1. [anonymous] (class method)
  260. to­Seq
    1. [anonymous] (class method)
  261. to­Seq­Left
    1. Applicative.to­Pure (class method)
  262. to­Seq­Right
    1. [anonymous] (class method)
  263. to­Stdio­Config
    1. IO.Process.SpawnArgs.to­Stdio­Config (structure field)
  264. to­String
    1. Char.to­String
  265. to­String
    1. Float.to­String
  266. to­String
    1. Float32.to­String
  267. to­String
    1. IO.Error.to­String
  268. to­String
    1. List.to­String
  269. to­String
    1. Substring.to­String
  270. to­String
    1. System.FilePath.to­String (structure field)
  271. to­Sub­Digits
    1. Nat.to­Sub­Digits
  272. to­Subarray
    1. Array.to­Subarray
  273. to­Subscript­String
    1. Nat.to­Subscript­String
  274. to­Substring'
    1. String.to­Substring'
  275. to­Substring
    1. String.to­Substring
  276. to­Super­Digits
    1. Nat.to­Super­Digits
  277. to­Superscript­String
    1. Nat.to­Superscript­String
  278. to­UInt16
    1. Bool.to­UInt16
  279. to­UInt16
    1. Float.to­UInt16
  280. to­UInt16
    1. Float32.to­UInt16
  281. to­UInt16
    1. Int16.to­UInt16 (structure field)
  282. to­UInt16
    1. Nat.to­UInt16
  283. to­UInt16
    1. UInt32.to­UInt16
  284. to­UInt16
    1. UInt64.to­UInt16
  285. to­UInt16
    1. UInt8.to­UInt16
  286. to­UInt16
    1. USize.to­UInt16
  287. to­UInt32
    1. Bool.to­UInt32
  288. to­UInt32
    1. Float.to­UInt32
  289. to­UInt32
    1. Float32.to­UInt32
  290. to­UInt32
    1. Int32.to­UInt32 (structure field)
  291. to­UInt32
    1. Nat.to­UInt32
  292. to­UInt32
    1. UInt16.to­UInt32
  293. to­UInt32
    1. UInt64.to­UInt32
  294. to­UInt32
    1. UInt8.to­UInt32
  295. to­UInt32
    1. USize.to­UInt32
  296. to­UInt64
    1. Bool.to­UInt64
  297. to­UInt64
    1. Float.to­UInt64
  298. to­UInt64
    1. Float32.to­UInt64
  299. to­UInt64
    1. Int64.to­UInt64 (structure field)
  300. to­UInt64
    1. Nat.to­UInt64
  301. to­UInt64
    1. UInt16.to­UInt64
  302. to­UInt64
    1. UInt32.to­UInt64
  303. to­UInt64
    1. UInt8.to­UInt64
  304. to­UInt64
    1. USize.to­UInt64
  305. to­UInt8
    1. Bool.to­UInt8
  306. to­UInt8
    1. Char.to­UInt8
  307. to­UInt8
    1. Float.to­UInt8
  308. to­UInt8
    1. Float32.to­UInt8
  309. to­UInt8
    1. Int8.to­UInt8 (structure field)
  310. to­UInt8
    1. Nat.to­UInt8
  311. to­UInt8
    1. UInt16.to­UInt8
  312. to­UInt8
    1. UInt32.to­UInt8
  313. to­UInt8
    1. UInt64.to­UInt8
  314. to­UInt8
    1. USize.to­UInt8
  315. to­USize
    1. Bool.to­USize
  316. to­USize
    1. Float.to­USize
  317. to­USize
    1. Float32.to­USize
  318. to­USize
    1. ISize.to­USize (structure field)
  319. to­USize
    1. Nat.to­USize
  320. to­USize
    1. UInt16.to­USize
  321. to­USize
    1. UInt32.to­USize
  322. to­USize
    1. UInt64.to­USize
  323. to­USize
    1. UInt8.to­USize
  324. to­UTF8
    1. String.to­UTF8
  325. to­Upper
    1. Char.to­Upper
  326. to­Upper
    1. String.to­Upper
  327. to­Vector
    1. Array.to­Vector
  328. toolchain gc (Elan command)
  329. toolchain install (Elan command)
  330. toolchain link (Elan command)
  331. toolchain list (Elan command)
  332. toolchain uninstall (Elan command)
  333. trace
  334. trace
    1. Lean.Macro.trace
  335. trace
    1. tactic.simp.trace (0) (1)
  336. trace.Elab.definition.wf
  337. trace.Meta.Tactic.simp.discharge
  338. trace.Meta.Tactic.simp.rewrite
  339. trace.compiler.ir.result
  340. trace_state (0) (1)
  341. trans
    1. Eq.trans
  342. trans
    1. Equivalence.trans (structure field)
  343. trans
    1. Setoid.trans
  344. trans
    1. Trans.trans (class method)
  345. translate-config (Lake command)
  346. transparency
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  347. trim
    1. String.trim
  348. trim
    1. Substring.trim
  349. trim­Left
    1. String.trim­Left
  350. trim­Left
    1. Substring.trim­Left
  351. trim­Right
    1. String.trim­Right
  352. trim­Right
    1. Substring.trim­Right
  353. trivial
  354. truncate
    1. BitVec.truncate
  355. truncate
    1. IO.FS.Handle.truncate
  356. try (0) (1)
  357. try­Catch
    1. EStateM.try­Catch
  358. try­Catch
    1. Except.try­Catch
  359. try­Catch
    1. ExceptT.try­Catch
  360. try­Catch
    1. MonadExcept.try­Catch (class method)
  361. try­Catch
    1. Monad­ExceptOf.try­Catch (class method)
  362. try­Catch
    1. Option.try­Catch
  363. try­Catch
    1. OptionT.try­Catch
  364. try­Catch­The
  365. try­Finally'
    1. MonadFinally.try­Finally' (class method)
  366. try­Lock
    1. IO.FS.Handle.try­Lock
  367. try­Wait
    1. IO.Process.Child.try­Wait
  368. two­Pow
    1. BitVec.two­Pow
  369. type constructor
  370. type
    1. IO.FS.Metadata.type (structure field)
  371. type
    1. eval.type
  372. 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. Lake.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. zeta
  7. zeta
    1. Lean.Meta.DSimp.Config.zeta (structure field)
  8. zeta
    1. Lean.Meta.Simp.Config.zeta (structure field)
  9. zeta­Delta
    1. Lean.Meta.DSimp.Config.zeta­Delta (structure field)
  10. zeta­Delta
    1. Lean.Meta.Simp.Config.zeta­Delta (structure field)
  11. zeta­Unused
    1. Lean.Meta.DSimp.Config.zeta­Unused (structure field)
  12. zeta­Unused
    1. Lean.Meta.Simp.Config.zeta­Unused (structure field)
  13. zip
    1. Array.zip
  14. zip
    1. List.zip
  15. zip­Idx
    1. Array.zip­Idx
  16. zip­Idx
    1. List.zip­Idx
  17. zip­Idx­TR
    1. List.zip­Idx­TR
  18. zip­With
    1. Array.zip­With
  19. zip­With
    1. List.zip­With
  20. zip­With­All
    1. Array.zip­With­All
  21. zip­With­All
    1. List.zip­With­All
  22. zip­With­TR
    1. List.zip­With­TR