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­Cases
    1. Fin.add­Cases
  190. add­Extension
    1. System.FilePath.add­Extension
  191. add­Heartbeats
    1. IO.add­Heartbeats
  192. add­Macro­Scope
    1. Lean.Macro.add­Macro­Scope
  193. add­Nat
    1. Fin.add­Nat
  194. admit
  195. all
    1. Array.all
  196. all
    1. List.all
  197. all
    1. Nat.all
  198. all
    1. Option.all
  199. all
    1. Std.HashSet.all
  200. all
    1. Std.TreeMap.all
  201. all
    1. Std.TreeSet.all
  202. all
    1. String.all
  203. all
    1. Subarray.all
  204. all
    1. Substring.all
  205. all­Diff
    1. Array.all­Diff
  206. all­Eq
    1. Subsingleton.all­Eq (class method)
  207. all­I
    1. Prod.all­I
  208. all­M
    1. Array.all­M
  209. all­M
    1. List.all­M
  210. all­M
    1. Nat.all­M
  211. all­M
    1. Subarray.all­M
  212. all­Ones
    1. BitVec.all­Ones
  213. all­TR
    1. Nat.all­TR
  214. all_goals (0) (1)
  215. allow­Unsafe­Reducibility
  216. alter
    1. Std.DHashMap.alter
  217. alter
    1. Std.DTreeMap.alter
  218. alter
    1. Std.Ext­DHashMap.alter
  219. alter
    1. Std.Ext­HashMap.alter
  220. alter
    1. Std.HashMap.alter
  221. alter
    1. Std.TreeMap.alter
  222. and
    1. BitVec.and
  223. and
    1. Bool.and
  224. and
    1. List.and
  225. and­M
  226. and_intros
  227. any
    1. Array.any
  228. any
    1. List.any
  229. any
    1. Nat.any
  230. any
    1. Option.any
  231. any
    1. Std.HashSet.any
  232. any
    1. Std.TreeMap.any
  233. any
    1. Std.TreeSet.any
  234. any
    1. String.any
  235. any
    1. Subarray.any
  236. any
    1. Substring.any
  237. any­I
    1. Prod.any­I
  238. any­M
    1. Array.any­M
  239. any­M
    1. List.any­M
  240. any­M
    1. Nat.any­M
  241. any­M
    1. Subarray.any­M
  242. any­TR
    1. Nat.any­TR
  243. any_goals (0) (1)
  244. app­Dir
    1. IO.app­Dir
  245. app­Path
    1. IO.app­Path
  246. append
    1. Append.append (class method)
  247. append
    1. Array.append
  248. append
    1. BitVec.append
  249. append
    1. List.append
  250. append
    1. String.append
  251. append­List
    1. Array.append­List
  252. append­TR
    1. List.append­TR
  253. apply (0) (1)
  254. apply?
  255. apply_assumption
  256. apply_ext_theorem
  257. apply_mod_cast
  258. apply_rfl
  259. apply_rules
  260. arg [@]i
  261. args
  262. args
    1. [anonymous] (structure field)
  263. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  264. array
    1. Subarray.array (structure field)
  265. as­String
    1. List.as­String
  266. as­Task
    1. BaseIO.as­Task
  267. as­Task
    1. EIO.as­Task
  268. as­Task
    1. IO.as­Task
  269. as_aux_lemma
  270. asin
    1. Float.asin
  271. asin
    1. Float32.asin
  272. asinh
    1. Float.asinh
  273. asinh
    1. Float32.asinh
  274. assumption
  275. assumption
    1. inaccessible
  276. assumption_mod_cast
  277. at­End
    1. String.Iterator.at­End
  278. at­End
    1. String.at­End
  279. at­End
    1. Substring.at­End
  280. at­Idx!
    1. Std.TreeSet.at­Idx!
  281. at­Idx
    1. Std.TreeSet.at­Idx
  282. at­Idx?
    1. Std.TreeSet.at­Idx?
  283. at­Idx­D
    1. Std.TreeSet.at­Idx­D
  284. atan
    1. Float.atan
  285. atan
    1. Float32.atan
  286. atan2
    1. Float.atan2
  287. atan2
    1. Float32.atan2
  288. atanh
    1. Float.atanh
  289. atanh
    1. Float32.atanh
  290. atomically
    1. Std.Mutex.atomically
  291. atomically­Once
    1. Std.Mutex.atomically­Once
  292. attach
    1. Array.attach
  293. attach
    1. List.attach
  294. attach
    1. Option.attach
  295. attach­With
    1. Array.attach­With
  296. attach­With
    1. List.attach­With
  297. attach­With
    1. Option.attach­With
  298. auto­Implicit
  299. auto­Lift
  300. auto­Param
  301. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  302. auto­Unfold
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
  303. 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. bsize
    1. Substring.bsize
  168. buckets
    1. Std.DHashMap.Raw.buckets (structure field)
  169. build (Lake command)
  170. bv_check
  171. bv_decide
  172. bv_decide?
  173. bv_normalize
  174. bv_omega
  175. by­Cases
    1. Decidable.by­Cases
  176. by_cases
  177. by_cases'
    1. Or.by_cases'
  178. by_cases
    1. Or.by_cases
  179. byte­Idx
    1. String.Pos.byte­Idx (structure field)
  180. 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. current­Dir
    1. IO.current­Dir
  206. curry
    1. Function.curry
  207. custom­Eliminators
    1. tactic.custom­Eliminators
  208. 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. default (Elan command)
  77. default
    1. Inhabited.default (class method)
  78. default
    1. Task.Priority.default
  79. default­Facets
    1. [anonymous] (structure field)
  80. delta (0) (1)
  81. diff
    1. guard_msgs.diff
  82. digit­Char
    1. Nat.digit­Char
  83. discard
    1. Functor.discard
  84. discharge
    1. trace.Meta.Tactic.simp.discharge
  85. div
    1. Div.div (class method)
  86. div
    1. Fin.div
  87. div
    1. Float.div
  88. div
    1. Float32.div
  89. div
    1. ISize.div
  90. div
    1. Int16.div
  91. div
    1. Int32.div
  92. div
    1. Int64.div
  93. div
    1. Int8.div
  94. div
    1. Nat.div
  95. div
    1. UInt16.div
  96. div
    1. UInt32.div
  97. div
    1. UInt64.div
  98. div
    1. UInt8.div
  99. div
    1. USize.div
  100. div2Induction
    1. Nat.div2Induction
  101. div­Rec
    1. BitVec.div­Rec
  102. div­Subtract­Shift
    1. BitVec.div­Subtract­Shift
  103. done (0) (1)
  104. down
    1. PLift.down (structure field)
  105. down
    1. ULift.down (structure field)
  106. drop
    1. Array.drop
  107. drop
    1. List.drop
  108. drop
    1. String.drop
  109. drop
    1. Subarray.drop
  110. drop
    1. Substring.drop
  111. drop­Last
    1. List.drop­Last
  112. drop­Last­TR
    1. List.drop­Last­TR
  113. drop­Prefix?
    1. String.drop­Prefix?
  114. drop­Prefix?
    1. Substring.drop­Prefix?
  115. drop­Right
    1. String.drop­Right
  116. drop­Right
    1. Substring.drop­Right
  117. drop­Right­While
    1. String.drop­Right­While
  118. drop­Right­While
    1. Substring.drop­Right­While
  119. drop­Suffix?
    1. String.drop­Suffix?
  120. drop­Suffix?
    1. Substring.drop­Suffix?
  121. drop­While
    1. List.drop­While
  122. drop­While
    1. String.drop­While
  123. drop­While
    1. Substring.drop­While
  124. dsimp (0) (1)
  125. dsimp!
  126. dsimp
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  127. dsimp?
  128. dsimp?!
  129. 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. ends­With
    1. String.ends­With
  121. enter
  122. entry­At­Idx!
    1. Std.TreeMap.entry­At­Idx!
  123. entry­At­Idx
    1. Std.TreeMap.entry­At­Idx
  124. entry­At­Idx?
    1. Std.TreeMap.entry­At­Idx?
  125. entry­At­Idx­D
    1. Std.TreeMap.entry­At­Idx­D
  126. env (Lake command)
  127. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  128. environment variables
  129. eprint
    1. IO.eprint
  130. eprintln
    1. IO.eprintln
  131. eq­Rec_heq
  132. eq_of_beq
    1. [anonymous] (class method)
  133. eq_of_heq
  134. eq_refl
  135. erase
    1. Array.erase
  136. erase
    1. List.erase
  137. erase
    1. Std.DHashMap.erase
  138. erase
    1. Std.DTreeMap.erase
  139. erase
    1. Std.Ext­DHashMap.erase
  140. erase
    1. Std.Ext­HashMap.erase
  141. erase
    1. Std.Ext­HashSet.erase
  142. erase
    1. Std.HashMap.erase
  143. erase
    1. Std.HashSet.erase
  144. erase
    1. Std.TreeMap.erase
  145. erase
    1. Std.TreeSet.erase
  146. erase­Dups
    1. List.erase­Dups
  147. erase­Idx!
    1. Array.erase­Idx!
  148. erase­Idx
    1. Array.erase­Idx
  149. erase­Idx
    1. List.erase­Idx
  150. erase­Idx­If­In­Bounds
    1. Array.erase­Idx­If­In­Bounds
  151. erase­Idx­TR
    1. List.erase­Idx­TR
  152. erase­Many
    1. Std.TreeMap.erase­Many
  153. erase­Many
    1. Std.TreeSet.erase­Many
  154. erase­P
    1. Array.erase­P
  155. erase­P
    1. List.erase­P
  156. erase­PTR
    1. List.erase­PTR
  157. erase­Reps
    1. Array.erase­Reps
  158. erase­Reps
    1. List.erase­Reps
  159. erase­TR
    1. List.erase­TR
  160. erw (0) (1)
  161. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
  162. eta
    1. Lean.Meta.Simp.Config.eta (structure field)
  163. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
  164. eta­Struct
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  165. eval.derive.repr
  166. eval.pp
  167. eval.type
  168. exact
  169. exact
    1. Quotient.exact
  170. exact?
  171. exact_mod_cast
  172. exe (Lake command)
  173. exe­Extension
    1. System.FilePath.exe­Extension
  174. exe­Name
    1. [anonymous] (structure field)
  175. execution
    1. IO.AccessRight.execution (structure field)
  176. exfalso
  177. exists
  178. exit
    1. IO.Process.exit
  179. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  180. exp
    1. Float.exp
  181. exp
    1. Float32.exp
  182. exp2
    1. Float.exp2
  183. exp2
    1. Float32.exp2
  184. expand­Macro?
    1. Lean.Macro.expand­Macro?
  185. expose_names
  186. ext (0) (1)
  187. ext1
  188. ext­Separator
    1. System.FilePath.ext­Separator
  189. extension
    1. System.FilePath.extension
  190. extensionality
    1. of propositions
  191. extra­Dep­Targets
    1. [anonymous] (structure field) (0) (1)
  192. extract
    1. Array.extract
  193. extract
    1. List.extract
  194. extract
    1. String.Iterator.extract
  195. extract
    1. String.extract
  196. extract
    1. Substring.extract
  197. extract­Lsb'
    1. BitVec.extract­Lsb'
  198. 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. Float
  49. Float.abs
  50. Float.acos
  51. Float.acosh
  52. Float.add
  53. Float.asin
  54. Float.asinh
  55. Float.atan
  56. Float.atan2
  57. Float.atanh
  58. Float.beq
  59. Float.cbrt
  60. Float.ceil
  61. Float.cos
  62. Float.cosh
  63. Float.dec­Le
  64. Float.dec­Lt
  65. Float.div
  66. Float.exp
  67. Float.exp2
  68. Float.floor
  69. Float.fr­Exp
  70. Float.is­Finite
  71. Float.is­Inf
  72. Float.is­Na­N
  73. Float.le
  74. Float.log
  75. Float.log10
  76. Float.log2
  77. Float.lt
  78. Float.mul
  79. Float.neg
  80. Float.of­Binary­Scientific
  81. Float.of­Bits
  82. Float.of­Int
  83. Float.of­Nat
  84. Float.of­Scientific
  85. Float.pow
  86. Float.round
  87. Float.scale­B
  88. Float.sin
  89. Float.sinh
  90. Float.sqrt
  91. Float.sub
  92. Float.tan
  93. Float.tanh
  94. Float.to­Bits
  95. Float.to­Float32
  96. Float.to­ISize
  97. Float.to­Int16
  98. Float.to­Int32
  99. Float.to­Int64
  100. Float.to­Int8
  101. Float.to­String
  102. Float.to­UInt16
  103. Float.to­UInt32
  104. Float.to­UInt64
  105. Float.to­UInt8
  106. Float.to­USize
  107. Float32
  108. Float32.abs
  109. Float32.acos
  110. Float32.acosh
  111. Float32.add
  112. Float32.asin
  113. Float32.asinh
  114. Float32.atan
  115. Float32.atan2
  116. Float32.atanh
  117. Float32.beq
  118. Float32.cbrt
  119. Float32.ceil
  120. Float32.cos
  121. Float32.cosh
  122. Float32.dec­Le
  123. Float32.dec­Lt
  124. Float32.div
  125. Float32.exp
  126. Float32.exp2
  127. Float32.floor
  128. Float32.fr­Exp
  129. Float32.is­Finite
  130. Float32.is­Inf
  131. Float32.is­Na­N
  132. Float32.le
  133. Float32.log
  134. Float32.log10
  135. Float32.log2
  136. Float32.lt
  137. Float32.mul
  138. Float32.neg
  139. Float32.of­Binary­Scientific
  140. Float32.of­Bits
  141. Float32.of­Int
  142. Float32.of­Nat
  143. Float32.of­Scientific
  144. Float32.pow
  145. Float32.round
  146. Float32.scale­B
  147. Float32.sin
  148. Float32.sinh
  149. Float32.sqrt
  150. Float32.sub
  151. Float32.tan
  152. Float32.tanh
  153. Float32.to­Bits
  154. Float32.to­Float
  155. Float32.to­ISize
  156. Float32.to­Int16
  157. Float32.to­Int32
  158. Float32.to­Int64
  159. Float32.to­Int8
  160. Float32.to­String
  161. Float32.to­UInt16
  162. Float32.to­UInt32
  163. Float32.to­UInt64
  164. Float32.to­UInt8
  165. Float32.to­USize
  166. For­In
  167. For­In'
  168. ForIn'.mk
    1. Instance constructor of For­In'
  169. ForIn.mk
    1. Instance constructor of For­In
  170. For­In­Step
  171. For­InStep.done
    1. Constructor of For­In­Step
  172. For­InStep.value
  173. For­InStep.yield
    1. Constructor of For­In­Step
  174. For­M
  175. ForM.for­In
  176. ForM.mk
    1. Instance constructor of For­M
  177. Function.comp
  178. Function.const
  179. Function.curry
  180. Function.uncurry
  181. Functor
  182. Functor.discard
  183. Functor.map­Rev
  184. Functor.mk
    1. Instance constructor of Functor
  185. fail
  186. fail
    1. OptionT.fail
  187. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
  188. fail­If­Unchanged
    1. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  189. fail_if_success (0) (1)
  190. failure
    1. ReaderT.failure
  191. failure
    1. StateT.failure
  192. failure
    1. [anonymous] (class method)
  193. false_or_by_contra
  194. fdiv
    1. Int.fdiv
  195. field­Idx­Kind
    1. Lean.field­Idx­Kind
  196. field­Notation
    1. pp.field­Notation
  197. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
  198. file­Name
    1. System.FilePath.file­Name
  199. file­Stem
    1. System.FilePath.file­Stem
  200. fill
    1. BitVec.fill
  201. filter
    1. Array.filter
  202. filter
    1. List.filter
  203. filter
    1. Option.filter
  204. filter
    1. Std.DHashMap.filter
  205. filter
    1. Std.DTreeMap.filter
  206. filter
    1. Std.Ext­DHashMap.filter
  207. filter
    1. Std.Ext­HashMap.filter
  208. filter
    1. Std.Ext­HashSet.filter
  209. filter
    1. Std.HashMap.filter
  210. filter
    1. Std.HashSet.filter
  211. filter
    1. Std.TreeMap.filter
  212. filter
    1. Std.TreeSet.filter
  213. filter­M
    1. Array.filter­M
  214. filter­M
    1. List.filter­M
  215. filter­Map
    1. Array.filter­Map
  216. filter­Map
    1. List.filter­Map
  217. filter­Map
    1. Std.DHashMap.filter­Map
  218. filter­Map
    1. Std.DTreeMap.filter­Map
  219. filter­Map
    1. Std.Ext­DHashMap.filter­Map
  220. filter­Map
    1. Std.Ext­HashMap.filter­Map
  221. filter­Map
    1. Std.HashMap.filter­Map
  222. filter­Map
    1. Std.TreeMap.filter­Map
  223. filter­Map­M
    1. Array.filter­Map­M
  224. filter­Map­M
    1. List.filter­Map­M
  225. filter­Map­TR
    1. List.filter­Map­TR
  226. filter­Rev­M
    1. Array.filter­Rev­M
  227. filter­Rev­M
    1. List.filter­Rev­M
  228. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  229. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  230. filter­TR
    1. List.filter­TR
  231. fin­Idx­Of?
    1. Array.fin­Idx­Of?
  232. fin­Idx­Of?
    1. List.fin­Idx­Of?
  233. fin­Range
    1. Array.fin­Range
  234. fin­Range
    1. List.fin­Range
  235. find
    1. String.find
  236. find?
    1. Array.find?
  237. find?
    1. List.find?
  238. find­Extern­Lib?
    1. Lake.find­Extern­Lib?
  239. find­Fin­Idx?
    1. Array.find­Fin­Idx?
  240. find­Fin­Idx?
    1. List.find­Fin­Idx?
  241. find­Idx
    1. Array.find­Idx
  242. find­Idx
    1. List.find­Idx
  243. find­Idx?
    1. Array.find­Idx?
  244. find­Idx?
    1. List.find­Idx?
  245. find­Idx­M?
    1. Array.find­Idx­M?
  246. find­Lean­Exe?
    1. Lake.find­Lean­Exe?
  247. find­Lean­Lib?
    1. Lake.find­Lean­Lib?
  248. find­Line­Start
    1. String.find­Line­Start
  249. find­M?
    1. Array.find­M?
  250. find­M?
    1. List.find­M?
  251. find­Module?
    1. Lake.find­Module?
  252. find­Package?
    1. Lake.find­Package?
  253. find­Rev?
    1. Array.find­Rev?
  254. find­Rev?
    1. Subarray.find­Rev?
  255. find­Rev­M?
    1. Array.find­Rev­M?
  256. find­Rev­M?
    1. Subarray.find­Rev­M?
  257. find­Some!
    1. Array.find­Some!
  258. find­Some?
    1. Array.find­Some?
  259. find­Some?
    1. List.find­Some?
  260. find­Some­M?
    1. Array.find­Some­M?
  261. find­Some­M?
    1. List.find­Some­M?
  262. find­Some­Rev?
    1. Array.find­Some­Rev?
  263. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
  264. find­Some­Rev­M?
    1. Subarray.find­Some­Rev­M?
  265. first (0) (1)
  266. first­Diff­Pos
    1. String.first­Diff­Pos
  267. first­M
    1. Array.first­M
  268. first­M
    1. List.first­M
  269. fix
    1. Lean.Order.fix
  270. fix
    1. WellFounded.fix
  271. fix_eq
    1. Lean.Order.fix_eq
  272. flags
    1. IO.AccessRight.flags
  273. flags
    1. IO.FileRight.flags
  274. flat­Map
    1. Array.flat­Map
  275. flat­Map
    1. List.flat­Map
  276. flat­Map­M
    1. Array.flat­Map­M
  277. flat­Map­M
    1. List.flat­Map­M
  278. flat­Map­TR
    1. List.flat­Map­TR
  279. flatten
    1. Array.flatten
  280. flatten
    1. List.flatten
  281. flatten­TR
    1. List.flatten­TR
  282. floor
    1. Float.floor
  283. floor
    1. Float32.floor
  284. flush
    1. IO.FS.Handle.flush
  285. flush
    1. IO.FS.Stream.flush (structure field)
  286. fmod
    1. Int.fmod
  287. focus (0) (1)
  288. fold
    1. Nat.fold
  289. fold
    1. Std.DHashMap.fold
  290. fold
    1. Std.HashMap.fold
  291. fold
    1. Std.HashSet.fold
  292. fold­I
    1. Prod.fold­I
  293. fold­M
    1. Nat.fold­M
  294. fold­M
    1. Std.DHashMap.fold­M
  295. fold­M
    1. Std.HashMap.fold­M
  296. fold­M
    1. Std.HashSet.fold­M
  297. fold­Rev
    1. Nat.fold­Rev
  298. fold­Rev­M
    1. Nat.fold­Rev­M
  299. fold­TR
    1. Nat.fold­TR
  300. foldl
    1. Array.foldl
  301. foldl
    1. Fin.foldl
  302. foldl
    1. List.foldl
  303. foldl
    1. Std.DTreeMap.foldl
  304. foldl
    1. Std.TreeMap.foldl
  305. foldl
    1. Std.TreeSet.foldl
  306. foldl
    1. String.foldl
  307. foldl
    1. Subarray.foldl
  308. foldl
    1. Substring.foldl
  309. foldl­M
    1. Array.foldl­M
  310. foldl­M
    1. Fin.foldl­M
  311. foldl­M
    1. List.foldl­M
  312. foldl­M
    1. Std.DTreeMap.foldl­M
  313. foldl­M
    1. Std.TreeMap.foldl­M
  314. foldl­M
    1. Std.TreeSet.foldl­M
  315. foldl­M
    1. Subarray.foldl­M
  316. foldl­Rec­On
    1. List.foldl­Rec­On
  317. foldr
    1. Array.foldr
  318. foldr
    1. Fin.foldr
  319. foldr
    1. List.foldr
  320. foldr
    1. Std.TreeMap.foldr
  321. foldr
    1. Std.TreeSet.foldr
  322. foldr
    1. String.foldr
  323. foldr
    1. Subarray.foldr
  324. foldr
    1. Substring.foldr
  325. foldr­M
    1. Array.foldr­M
  326. foldr­M
    1. Fin.foldr­M
  327. foldr­M
    1. List.foldr­M
  328. foldr­M
    1. Std.TreeMap.foldr­M
  329. foldr­M
    1. Std.TreeSet.foldr­M
  330. foldr­M
    1. Subarray.foldr­M
  331. foldr­Rec­On
    1. List.foldr­Rec­On
  332. foldr­TR
    1. List.foldr­TR
  333. for­A
    1. List.for­A
  334. for­Async
    1. Std.Channel.for­Async
  335. for­In'
    1. ForIn'.for­In' (class method)
  336. for­In
    1. ForIn.for­In (class method)
  337. for­In
    1. ForM.for­In
  338. for­In
    1. Std.DHashMap.for­In
  339. for­In
    1. Std.DTreeMap.for­In
  340. for­In
    1. Std.HashMap.for­In
  341. for­In
    1. Std.HashSet.for­In
  342. for­In
    1. Std.TreeMap.for­In
  343. for­In
    1. Std.TreeSet.for­In
  344. for­In
    1. Subarray.for­In
  345. for­M
    1. Array.for­M
  346. for­M
    1. ForM.for­M (class method)
  347. for­M
    1. List.for­M
  348. for­M
    1. Nat.for­M
  349. for­M
    1. Option.for­M
  350. for­M
    1. Std.DHashMap.for­M
  351. for­M
    1. Std.DTreeMap.for­M
  352. for­M
    1. Std.HashMap.for­M
  353. for­M
    1. Std.HashSet.for­M
  354. for­M
    1. Std.TreeMap.for­M
  355. for­M
    1. Std.TreeSet.for­M
  356. for­M
    1. Subarray.for­M
  357. for­Rev­M
    1. Array.for­Rev­M
  358. for­Rev­M
    1. Nat.for­Rev­M
  359. for­Rev­M
    1. Subarray.for­Rev­M
  360. format
    1. Option.format
  361. forward
    1. String.Iterator.forward
  362. fr­Exp
    1. Float.fr­Exp
  363. fr­Exp
    1. Float32.fr­Exp
  364. from­State­M
    1. EStateM.from­State­M
  365. from­UTF8!
    1. String.from­UTF8!
  366. from­UTF8
    1. String.from­UTF8
  367. from­UTF8?
    1. String.from­UTF8?
  368. front
    1. String.front
  369. front
    1. Substring.front
  370. fst
    1. MProd.fst (structure field)
  371. fst
    1. PProd.fst (structure field)
  372. fst
    1. PSigma.fst (structure field)
  373. fst
    1. Prod.fst (structure field)
  374. fst
    1. Sigma.fst (structure field)
  375. fun
  376. fun_cases
  377. fun_induction
  378. 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. index
    1. Lean.Meta.DSimp.Config.index (structure field)
  409. index
    1. Lean.Meta.Simp.Config.index (structure field)
  410. index
    1. of inductive type
  411. indexed family
    1. of types
  412. induction
  413. induction
    1. Fin.induction
  414. induction­On
    1. Fin.induction­On
  415. induction­On
    1. Nat.div.induction­On
  416. induction­On
    1. Nat.mod.induction­On
  417. inductive.auto­Promote­Indices
  418. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  419. infer­Instance
  420. infer­Instance­As
  421. infer_instance
  422. inhabited­Left
    1. PSum.inhabited­Left
  423. inhabited­Left
    1. Sum.inhabited­Left
  424. inhabited­Right
    1. PSum.inhabited­Right
  425. inhabited­Right
    1. Sum.inhabited­Right
  426. inherit­Env
    1. IO.Process.SpawnArgs.args (structure field)
  427. init (Lake command)
  428. injection
  429. injections
  430. inner
    1. Std.DHashMap.Equiv.inner (structure field)
  431. inner
    1. Std.DTreeMap.Raw.inner (structure field)
  432. inner
    1. Std.Ext­HashSet.inner (structure field)
  433. inner
    1. Std.HashMap.Equiv.inner (structure field)
  434. inner
    1. Std.HashMap.Raw.inner (structure field)
  435. inner
    1. Std.HashSet.Equiv.inner (structure field)
  436. inner
    1. Std.HashSet.Raw.inner (structure field)
  437. inner
    1. Std.HashSet.inner (structure field)
  438. inner
    1. Std.TreeMap.Raw.inner (structure field)
  439. inner
    1. Std.TreeSet.Raw.inner (structure field)
  440. insert
    1. List.insert
  441. insert
    1. Std.DHashMap.insert
  442. insert
    1. Std.DTreeMap.insert
  443. insert
    1. Std.Ext­DHashMap.insert
  444. insert
    1. Std.Ext­HashMap.insert
  445. insert
    1. Std.Ext­HashSet.insert
  446. insert
    1. Std.HashMap.insert
  447. insert
    1. Std.HashSet.insert
  448. insert
    1. Std.TreeMap.insert
  449. insert
    1. Std.TreeSet.insert
  450. insert­Idx!
    1. Array.insert­Idx!
  451. insert­Idx
    1. Array.insert­Idx
  452. insert­Idx
    1. List.insert­Idx
  453. insert­Idx­If­In­Bounds
    1. Array.insert­Idx­If­In­Bounds
  454. insert­Idx­TR
    1. List.insert­Idx­TR
  455. insert­If­New
    1. Std.DHashMap.insert­If­New
  456. insert­If­New
    1. Std.DTreeMap.insert­If­New
  457. insert­If­New
    1. Std.Ext­DHashMap.insert­If­New
  458. insert­If­New
    1. Std.Ext­HashMap.insert­If­New
  459. insert­If­New
    1. Std.HashMap.insert­If­New
  460. insert­If­New
    1. Std.TreeMap.insert­If­New
  461. insert­Many
    1. Std.DHashMap.insert­Many
  462. insert­Many
    1. Std.DTreeMap.insert­Many
  463. insert­Many
    1. Std.Ext­DHashMap.insert­Many
  464. insert­Many
    1. Std.Ext­HashMap.insert­Many
  465. insert­Many
    1. Std.Ext­HashSet.insert­Many
  466. insert­Many
    1. Std.HashMap.insert­Many
  467. insert­Many
    1. Std.HashSet.insert­Many
  468. insert­Many
    1. Std.TreeMap.insert­Many
  469. insert­Many
    1. Std.TreeSet.insert­Many
  470. insert­Many­If­New­Unit
    1. Std.Ext­HashMap.insert­Many­If­New­Unit
  471. insert­Many­If­New­Unit
    1. Std.HashMap.insert­Many­If­New­Unit
  472. insert­Many­If­New­Unit
    1. Std.TreeMap.insert­Many­If­New­Unit
  473. insertion­Sort
    1. Array.insertion­Sort
  474. instance synthesis
  475. int­Cast
    1. IntCast.int­Cast (class method)
  476. int­Max
    1. BitVec.int­Max
  477. int­Min
    1. BitVec.int­Min
  478. intercalate
    1. List.intercalate
  479. intercalate
    1. String.intercalate
  480. intercalate­TR
    1. List.intercalate­TR
  481. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  482. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  483. intersperse
    1. List.intersperse
  484. intersperse­TR
    1. List.intersperse­TR
  485. intro (0) (1)
  486. intro | ... => ... | ... => ...
  487. intros
  488. inv­Image
  489. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
  490. iota
    1. Lean.Meta.Simp.Config.iota (structure field)
  491. is­Absolute
    1. System.FilePath.is­Absolute
  492. is­Alpha
    1. Char.is­Alpha
  493. is­Alphanum
    1. Char.is­Alphanum
  494. is­Digit
    1. Char.is­Digit
  495. is­Dir
    1. System.FilePath.is­Dir
  496. is­Empty
    1. Array.is­Empty
  497. is­Empty
    1. List.is­Empty
  498. is­Empty
    1. Std.DHashMap.is­Empty
  499. is­Empty
    1. Std.DTreeMap.is­Empty
  500. is­Empty
    1. Std.Ext­DHashMap.is­Empty
  501. is­Empty
    1. Std.Ext­HashMap.is­Empty
  502. is­Empty
    1. Std.Ext­HashSet.is­Empty
  503. is­Empty
    1. Std.HashMap.is­Empty
  504. is­Empty
    1. Std.HashSet.is­Empty
  505. is­Empty
    1. Std.TreeMap.is­Empty
  506. is­Empty
    1. Std.TreeSet.is­Empty
  507. is­Empty
    1. String.is­Empty
  508. is­Empty
    1. Substring.is­Empty
  509. is­Emscripten
    1. System.Platform.is­Emscripten
  510. is­Eq
    1. Ordering.is­Eq
  511. is­Eq­Some
    1. Option.is­Eq­Some
  512. is­Eqv
    1. Array.is­Eqv
  513. is­Eqv
    1. List.is­Eqv
  514. is­Exclusive­Unsafe
  515. is­Finite
    1. Float.is­Finite
  516. is­Finite
    1. Float32.is­Finite
  517. is­GE
    1. Ordering.is­GE
  518. is­GT
    1. Ordering.is­GT
  519. is­Inf
    1. Float.is­Inf
  520. is­Inf
    1. Float32.is­Inf
  521. is­Int
    1. String.is­Int
  522. is­LE
    1. Ordering.is­LE
  523. is­LT
    1. Ordering.is­LT
  524. is­Left
    1. Sum.is­Left
  525. is­Lower
    1. Char.is­Lower
  526. is­Lt
    1. Fin.is­Lt (structure field)
  527. is­Na­N
    1. Float.is­Na­N
  528. is­Na­N
    1. Float32.is­Na­N
  529. is­Nat
    1. String.is­Nat
  530. is­Nat
    1. Substring.is­Nat
  531. is­Ne
    1. Ordering.is­Ne
  532. is­None
    1. Option.is­None
  533. is­OSX
    1. System.Platform.is­OSX
  534. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  535. is­Ok
    1. Except.is­Ok
  536. is­Perm
    1. List.is­Perm
  537. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  538. is­Prefix­Of
    1. Array.is­Prefix­Of
  539. is­Prefix­Of
    1. List.is­Prefix­Of
  540. is­Prefix­Of
    1. String.is­Prefix­Of
  541. is­Prefix­Of?
    1. List.is­Prefix­Of?
  542. is­Relative
    1. System.FilePath.is­Relative
  543. is­Resolved
    1. IO.Promise.is­Resolved
  544. is­Right
    1. Sum.is­Right
  545. is­Some
    1. Option.is­Some
  546. is­Sublist
    1. List.is­Sublist
  547. is­Suffix­Of
    1. List.is­Suffix­Of
  548. is­Suffix­Of?
    1. List.is­Suffix­Of?
  549. is­Tty
    1. IO.FS.Handle.is­Tty
  550. is­Tty
    1. IO.FS.Stream.is­Tty (structure field)
  551. is­Upper
    1. Char.is­Upper
  552. is­Valid
    1. String.Pos.is­Valid
  553. is­Valid­Char
    1. Nat.is­Valid­Char
  554. is­Valid­Char
    1. UInt32.is­Valid­Char
  555. is­Valid­Char­Nat
    1. Char.is­Valid­Char­Nat
  556. is­Whitespace
    1. Char.is­Whitespace
  557. is­Windows
    1. System.Platform.is­Windows
  558. iseqv
    1. Setoid.iseqv (class method)
  559. iter
    1. String.iter
  560. iterate
  561. iterate
    1. IO.iterate
  562. iunfoldr
    1. BitVec.iunfoldr
  563. iunfoldr_replace
    1. BitVec.iunfoldr_replace

J

  1. join
    1. Option.join
  2. join
    1. String.join
  3. join
    1. System.FilePath.join

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