The Lean Language Reference

Index

Symbols

  1. ( ... )
  2. . ...
  3. <;> (0) (1)
  4. { ... }
  5. ·
  6. · ...
  7. Σ-types
  8. ι-reduction

A

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

B

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

C

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

D

  1. DHash­Map
    1. Std.DHash­Map
  2. DTree­Map
    1. Std.DTree­Map
  3. Decidable
  4. Decidable.by­Cases
  5. Decidable.decide
  6. Decidable.is­False
    1. Constructor of Decidable
  7. Decidable.is­True
    1. Constructor of Decidable
  8. Decidable­Eq
  9. Decidable­LE
  10. Decidable­LT
  11. Decidable­Pred
  12. Decidable­Rel
  13. Dir­Entry
    1. IO.FS.Dir­Entry
  14. Div
  15. Div.mk
    1. Instance constructor of Div
  16. Dvd
  17. Dvd.mk
    1. Instance constructor of Dvd
  18. data
    1. IO.FS.Stream.Buffer.data (structure field)
  19. data
    1. String.data (structure field)
  20. dbg­Trace­If­Shared
  21. dbg_trace
  22. dcond
    1. Bool.dcond
  23. dec­Eq
    1. BitVec.dec­Eq
  24. dec­Eq
    1. Bool.dec­Eq
  25. dec­Eq
    1. ISize.dec­Eq
  26. dec­Eq
    1. Int.dec­Eq
  27. dec­Eq
    1. Int16.dec­Eq
  28. dec­Eq
    1. Int32.dec­Eq
  29. dec­Eq
    1. Int64.dec­Eq
  30. dec­Eq
    1. Int8.dec­Eq
  31. dec­Eq
    1. Nat.dec­Eq
  32. dec­Eq
    1. String.dec­Eq
  33. dec­Eq
    1. UInt16.dec­Eq
  34. dec­Eq
    1. UInt32.dec­Eq
  35. dec­Eq
    1. UInt64.dec­Eq
  36. dec­Eq
    1. UInt8.dec­Eq
  37. dec­Eq
    1. USize.dec­Eq
  38. dec­Le
    1. Float.dec­Le
  39. dec­Le
    1. Float32.dec­Le
  40. dec­Le
    1. ISize.dec­Le
  41. dec­Le
    1. Int16.dec­Le
  42. dec­Le
    1. Int32.dec­Le
  43. dec­Le
    1. Int64.dec­Le
  44. dec­Le
    1. Int8.dec­Le
  45. dec­Le
    1. Nat.dec­Le
  46. dec­Le
    1. UInt16.dec­Le
  47. dec­Le
    1. UInt32.dec­Le
  48. dec­Le
    1. UInt64.dec­Le
  49. dec­Le
    1. UInt8.dec­Le
  50. dec­Le
    1. USize.dec­Le
  51. dec­Lt
    1. Float.dec­Lt
  52. dec­Lt
    1. Float32.dec­Lt
  53. dec­Lt
    1. ISize.dec­Lt
  54. dec­Lt
    1. Int16.dec­Lt
  55. dec­Lt
    1. Int32.dec­Lt
  56. dec­Lt
    1. Int64.dec­Lt
  57. dec­Lt
    1. Int8.dec­Lt
  58. dec­Lt
    1. Nat.dec­Lt
  59. dec­Lt
    1. UInt16.dec­Lt
  60. dec­Lt
    1. UInt32.dec­Lt
  61. dec­Lt
    1. UInt64.dec­Lt
  62. dec­Lt
    1. UInt8.dec­Lt
  63. dec­Lt
    1. USize.dec­Lt
  64. decapitalize
    1. String.decapitalize
  65. decidable
  66. decidable­Eq­None
    1. Option.decidable­Eq­None
  67. decide
  68. decide
    1. Decidable.decide
  69. decide
    1. Lean.Meta.DSimp.Config.decide (structure field)
  70. decide
    1. Lean.Meta.Simp.Config.decide (structure field)
  71. decreasing_tactic
  72. decreasing_trivial
  73. decreasing_with
  74. dedicated
    1. Task.Priority.dedicated
  75. deep­Terms
    1. pp.deep­Terms
  76. def­Indent
    1. Std.Format.def­Indent
  77. def­Width
    1. Std.Format.def­Width
  78. default (Elan command)
  79. default
    1. Inhabited.default (class method)
  80. default
    1. Task.Priority.default
  81. default­Facets
    1. [anonymous] (structure field)
  82. delta (0) (1)
  83. diff
    1. guard_msgs.diff
  84. digit­Char
    1. Nat.digit­Char
  85. discard
    1. Functor.discard
  86. discharge
    1. trace.Meta.Tactic.simp.discharge
  87. div
    1. Div.div (class method)
  88. div
    1. Fin.div
  89. div
    1. Float.div
  90. div
    1. Float32.div
  91. div
    1. ISize.div
  92. div
    1. Int16.div
  93. div
    1. Int32.div
  94. div
    1. Int64.div
  95. div
    1. Int8.div
  96. div
    1. Nat.div
  97. div
    1. UInt16.div
  98. div
    1. UInt32.div
  99. div
    1. UInt64.div
  100. div
    1. UInt8.div
  101. div
    1. USize.div
  102. div2Induction
    1. Nat.div2Induction
  103. div­Rec
    1. BitVec.div­Rec
  104. div­Subtract­Shift
    1. BitVec.div­Subtract­Shift
  105. div_eq_mul_inv
    1. [anonymous] (class method)
  106. done (0) (1)
  107. down
    1. PLift.down (structure field)
  108. down
    1. ULift.down (structure field)
  109. drop
    1. Array.drop
  110. drop
    1. List.drop
  111. drop
    1. String.drop
  112. drop
    1. Subarray.drop
  113. drop
    1. Substring.drop
  114. drop­Last
    1. List.drop­Last
  115. drop­Last­TR
    1. List.drop­Last­TR
  116. drop­Prefix?
    1. String.drop­Prefix?
  117. drop­Prefix?
    1. Substring.drop­Prefix?
  118. drop­Right
    1. String.drop­Right
  119. drop­Right
    1. Substring.drop­Right
  120. drop­Right­While
    1. String.drop­Right­While
  121. drop­Right­While
    1. Substring.drop­Right­While
  122. drop­Suffix?
    1. String.drop­Suffix?
  123. drop­Suffix?
    1. Substring.drop­Suffix?
  124. drop­While
    1. List.drop­While
  125. drop­While
    1. String.drop­While
  126. drop­While
    1. Substring.drop­While
  127. dsimp (0) (1)
  128. dsimp!
  129. dsimp
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  130. dsimp?
  131. dsimp?!
  132. dvd
    1. Dvd.dvd (class method)

E

  1. EIO
  2. EIO.as­Task
  3. EIO.bind­Task
  4. EIO.catch­Exceptions
  5. EIO.chain­Task
  6. EIO.map­Task
  7. EIO.map­Tasks
  8. EIO.to­Base­IO
  9. EIO.to­IO
  10. EIO.to­IO'
  11. ELAN (environment variable)
  12. ELAN_HOME (environment variable) (0) (1)
  13. EST
  14. EState­M
  15. EStateM.Backtrackable
  16. EStateM.Backtrackable.mk
    1. Instance constructor of EStateM.Backtrackable
  17. EStateM.Result
  18. EStateM.Result.error
    1. Constructor of EStateM.Result
  19. EStateM.Result.ok
    1. Constructor of EStateM.Result
  20. EStateM.adapt­Except
  21. EStateM.bind
  22. EStateM.from­State­M
  23. EStateM.get
  24. EStateM.map
  25. EStateM.modify­Get
  26. EStateM.non­Backtrackable
  27. EStateM.or­Else
  28. EStateM.or­Else'
  29. EStateM.pure
  30. EStateM.run
  31. EStateM.run'
  32. EStateM.seq­Right
  33. EStateM.set
  34. EStateM.throw
  35. EStateM.try­Catch
  36. Empty
  37. Empty.elim
  38. Eq
  39. Eq.mp
  40. Eq.mpr
  41. Eq.refl
    1. Constructor of Eq
  42. Eq.subst
  43. Eq.symm
  44. Eq.trans
  45. Equiv
    1. HasEquiv.Equiv (class method)
  46. Equiv
    1. Std.DHashMap.Equiv
  47. Equiv
    1. Std.HashMap.Equiv
  48. Equiv
    1. Std.HashSet.Equiv
  49. Equiv­BEq
  50. EquivBEq.mk
    1. Instance constructor of Equiv­BEq
  51. Equivalence
  52. Equivalence.mk
    1. Constructor of Equivalence
  53. Error
    1. IO.Error
  54. Even
  55. Even.plus­Two
    1. Constructor of Even
  56. Even.zero
    1. Constructor of Even
  57. Except
  58. Except.bind
  59. Except.error
    1. Constructor of Except
  60. Except.is­Ok
  61. Except.map
  62. Except.map­Error
  63. Except.ok
    1. Constructor of Except
  64. Except.or­Else­Lazy
  65. Except.pure
  66. Except.to­Bool
  67. Except.to­Option
  68. Except.try­Catch
  69. Except­Cps­T
  70. Except­CpsT.lift
  71. Except­CpsT.run
  72. Except­CpsT.run­Catch
  73. Except­CpsT.run­K
  74. Except­T
  75. ExceptT.adapt
  76. ExceptT.bind
  77. ExceptT.bind­Cont
  78. ExceptT.lift
  79. ExceptT.map
  80. ExceptT.mk
  81. ExceptT.pure
  82. ExceptT.run
  83. ExceptT.try­Catch
  84. Exists
  85. Exists.choose
  86. Exists.intro
    1. Constructor of Exists
  87. Ext­DHash­Map
    1. Std.Ext­DHash­Map
  88. Ext­Hash­Map
    1. Std.Ext­Hash­Map
  89. Ext­Hash­Set
    1. Std.Ext­Hash­Set
  90. ediv
    1. Int.ediv
  91. elem
    1. Array.elem
  92. elem
    1. List.elem
  93. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  94. elim
    1. And.elim
  95. elim
    1. Empty.elim
  96. elim
    1. False.elim
  97. elim
    1. HEq.elim
  98. elim
    1. Iff.elim
  99. elim
    1. Not.elim
  100. elim
    1. Option.elim
  101. elim
    1. PEmpty.elim
  102. elim
    1. Subsingleton.elim
  103. elim
    1. Sum.elim
  104. elim0
    1. Fin.elim0
  105. elim­M
    1. Option.elim­M
  106. emod
    1. Int.emod
  107. empty
    1. Array.empty
  108. empty
    1. Std.DTreeMap.empty
  109. empty
    1. Std.TreeMap.empty
  110. empty
    1. Std.TreeSet.empty
  111. empty
    1. Subarray.empty
  112. empty­With­Capacity
    1. Array.empty­With­Capacity
  113. empty­With­Capacity
    1. Std.DHashMap.empty­With­Capacity
  114. empty­With­Capacity
    1. Std.Ext­DHashMap.empty­With­Capacity
  115. empty­With­Capacity
    1. Std.Ext­HashMap.empty­With­Capacity
  116. empty­With­Capacity
    1. Std.Ext­HashSet.empty­With­Capacity
  117. empty­With­Capacity
    1. Std.HashMap.empty­With­Capacity
  118. empty­With­Capacity
    1. Std.HashSet.empty­With­Capacity
  119. end­Pos
    1. String.end­Pos
  120. end­Tags
    1. Std.Format.Monad­PrettyFormat.end­Tags (class method)
  121. ends­With
    1. String.ends­With
  122. enter
  123. entry­At­Idx!
    1. Std.TreeMap.entry­At­Idx!
  124. entry­At­Idx
    1. Std.TreeMap.entry­At­Idx
  125. entry­At­Idx?
    1. Std.TreeMap.entry­At­Idx?
  126. entry­At­Idx­D
    1. Std.TreeMap.entry­At­Idx­D
  127. env (Lake command)
  128. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  129. environment variables
  130. eprint
    1. IO.eprint
  131. eprintln
    1. IO.eprintln
  132. eq­Rec_heq
  133. eq_of_beq
    1. [anonymous] (class method)
  134. eq_of_heq
  135. eq_refl
  136. erase
    1. Array.erase
  137. erase
    1. List.erase
  138. erase
    1. Std.DHashMap.erase
  139. erase
    1. Std.DTreeMap.erase
  140. erase
    1. Std.Ext­DHashMap.erase
  141. erase
    1. Std.Ext­HashMap.erase
  142. erase
    1. Std.Ext­HashSet.erase
  143. erase
    1. Std.HashMap.erase
  144. erase
    1. Std.HashSet.erase
  145. erase
    1. Std.TreeMap.erase
  146. erase
    1. Std.TreeSet.erase
  147. erase­Dups
    1. List.erase­Dups
  148. erase­Idx!
    1. Array.erase­Idx!
  149. erase­Idx
    1. Array.erase­Idx
  150. erase­Idx
    1. List.erase­Idx
  151. erase­Idx­If­In­Bounds
    1. Array.erase­Idx­If­In­Bounds
  152. erase­Idx­TR
    1. List.erase­Idx­TR
  153. erase­Many
    1. Std.TreeMap.erase­Many
  154. erase­Many
    1. Std.TreeSet.erase­Many
  155. erase­P
    1. Array.erase­P
  156. erase­P
    1. List.erase­P
  157. erase­PTR
    1. List.erase­PTR
  158. erase­Reps
    1. Array.erase­Reps
  159. erase­Reps
    1. List.erase­Reps
  160. erase­TR
    1. List.erase­TR
  161. erw (0) (1)
  162. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
  163. eta
    1. Lean.Meta.Simp.Config.eta (structure field)
  164. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
  165. eta­Struct
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  166. eval.derive.repr
  167. eval.pp
  168. eval.type
  169. exact
  170. exact
    1. Quotient.exact
  171. exact?
  172. exact_mod_cast
  173. exe (Lake command)
  174. exe­Extension
    1. System.FilePath.exe­Extension
  175. exe­Name
    1. [anonymous] (structure field)
  176. execution
    1. IO.AccessRight.execution (structure field)
  177. exfalso
  178. exists
  179. exit
    1. IO.Process.exit
  180. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  181. exp
    1. Float.exp
  182. exp
    1. Float32.exp
  183. exp2
    1. Float.exp2
  184. exp2
    1. Float32.exp2
  185. expand­Macro?
    1. Lean.Macro.expand­Macro?
  186. expose_names
  187. ext (0) (1)
  188. ext1
  189. ext­Separator
    1. System.FilePath.ext­Separator
  190. extension
    1. System.FilePath.extension
  191. extensionality
    1. of propositions
  192. extra­Dep­Targets
    1. [anonymous] (structure field) (0) (1)
  193. extract
    1. Array.extract
  194. extract
    1. List.extract
  195. extract
    1. String.Iterator.extract
  196. extract
    1. String.extract
  197. extract
    1. Substring.extract
  198. extract­Lsb'
    1. BitVec.extract­Lsb'
  199. extract­Lsb
    1. BitVec.extract­Lsb

F

  1. False
  2. False.elim
  3. Field
    1. Lean.Grind.Field
  4. File­Path
    1. System.File­Path
  5. File­Right
    1. IO.File­Right
  6. Fin
  7. Fin.add
  8. Fin.add­Cases
  9. Fin.add­Nat
  10. Fin.cases
  11. Fin.cast
  12. Fin.cast­Add
  13. Fin.cast­LE
  14. Fin.cast­LT
  15. Fin.cast­Succ
  16. Fin.div
  17. Fin.elim0
  18. Fin.foldl
  19. Fin.foldl­M
  20. Fin.foldr
  21. Fin.foldr­M
  22. Fin.h­Iterate
  23. Fin.h­Iterate­From
  24. Fin.induction
  25. Fin.induction­On
  26. Fin.land
  27. Fin.last
  28. Fin.last­Cases
  29. Fin.log2
  30. Fin.lor
  31. Fin.mk
    1. Constructor of Fin
  32. Fin.mod
  33. Fin.modn
  34. Fin.mul
  35. Fin.nat­Add
  36. Fin.of­Nat
  37. Fin.pred
  38. Fin.rev
  39. Fin.reverse­Induction
  40. Fin.shift­Left
  41. Fin.shift­Right
  42. Fin.sub
  43. Fin.sub­Nat
  44. Fin.succ
  45. Fin.succ­Rec
  46. Fin.succ­Rec­On
  47. Fin.to­Nat
  48. Fin.xor
  49. Flatten­Behavior
    1. Std.Format.Flatten­Behavior
  50. Float
  51. Float.abs
  52. Float.acos
  53. Float.acosh
  54. Float.add
  55. Float.asin
  56. Float.asinh
  57. Float.atan
  58. Float.atan2
  59. Float.atanh
  60. Float.beq
  61. Float.cbrt
  62. Float.ceil
  63. Float.cos
  64. Float.cosh
  65. Float.dec­Le
  66. Float.dec­Lt
  67. Float.div
  68. Float.exp
  69. Float.exp2
  70. Float.floor
  71. Float.fr­Exp
  72. Float.is­Finite
  73. Float.is­Inf
  74. Float.is­Na­N
  75. Float.le
  76. Float.log
  77. Float.log10
  78. Float.log2
  79. Float.lt
  80. Float.mul
  81. Float.neg
  82. Float.of­Binary­Scientific
  83. Float.of­Bits
  84. Float.of­Int
  85. Float.of­Nat
  86. Float.of­Scientific
  87. Float.pow
  88. Float.round
  89. Float.scale­B
  90. Float.sin
  91. Float.sinh
  92. Float.sqrt
  93. Float.sub
  94. Float.tan
  95. Float.tanh
  96. Float.to­Bits
  97. Float.to­Float32
  98. Float.to­ISize
  99. Float.to­Int16
  100. Float.to­Int32
  101. Float.to­Int64
  102. Float.to­Int8
  103. Float.to­String
  104. Float.to­UInt16
  105. Float.to­UInt32
  106. Float.to­UInt64
  107. Float.to­UInt8
  108. Float.to­USize
  109. Float32
  110. Float32.abs
  111. Float32.acos
  112. Float32.acosh
  113. Float32.add
  114. Float32.asin
  115. Float32.asinh
  116. Float32.atan
  117. Float32.atan2
  118. Float32.atanh
  119. Float32.beq
  120. Float32.cbrt
  121. Float32.ceil
  122. Float32.cos
  123. Float32.cosh
  124. Float32.dec­Le
  125. Float32.dec­Lt
  126. Float32.div
  127. Float32.exp
  128. Float32.exp2
  129. Float32.floor
  130. Float32.fr­Exp
  131. Float32.is­Finite
  132. Float32.is­Inf
  133. Float32.is­Na­N
  134. Float32.le
  135. Float32.log
  136. Float32.log10
  137. Float32.log2
  138. Float32.lt
  139. Float32.mul
  140. Float32.neg
  141. Float32.of­Binary­Scientific
  142. Float32.of­Bits
  143. Float32.of­Int
  144. Float32.of­Nat
  145. Float32.of­Scientific
  146. Float32.pow
  147. Float32.round
  148. Float32.scale­B
  149. Float32.sin
  150. Float32.sinh
  151. Float32.sqrt
  152. Float32.sub
  153. Float32.tan
  154. Float32.tanh
  155. Float32.to­Bits
  156. Float32.to­Float
  157. Float32.to­ISize
  158. Float32.to­Int16
  159. Float32.to­Int32
  160. Float32.to­Int64
  161. Float32.to­Int8
  162. Float32.to­String
  163. Float32.to­UInt16
  164. Float32.to­UInt32
  165. Float32.to­UInt64
  166. Float32.to­UInt8
  167. Float32.to­USize
  168. For­In
  169. For­In'
  170. ForIn'.mk
    1. Instance constructor of For­In'
  171. ForIn.mk
    1. Instance constructor of For­In
  172. For­In­Step
  173. For­InStep.done
    1. Constructor of For­In­Step
  174. For­InStep.value
  175. For­InStep.yield
    1. Constructor of For­In­Step
  176. For­M
  177. ForM.for­In
  178. ForM.mk
    1. Instance constructor of For­M
  179. Format
    1. Std.Format
  180. Function.comp
  181. Function.const
  182. Function.curry
  183. Function.uncurry
  184. Functor
  185. Functor.discard
  186. Functor.map­Rev
  187. Functor.mk
    1. Instance constructor of Functor
  188. fail
  189. fail
    1. OptionT.fail
  190. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
  191. fail­If­Unchanged
    1. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  192. fail_if_success (0) (1)
  193. failure
    1. ReaderT.failure
  194. failure
    1. StateT.failure
  195. failure
    1. [anonymous] (class method)
  196. false_or_by_contra
  197. fdiv
    1. Int.fdiv
  198. field­Idx­Kind
    1. Lean.field­Idx­Kind
  199. field­Notation
    1. pp.field­Notation
  200. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
  201. file­Name
    1. System.FilePath.file­Name
  202. file­Stem
    1. System.FilePath.file­Stem
  203. fill
    1. BitVec.fill
  204. fill
    1. Std.Format.fill
  205. filter
    1. Array.filter
  206. filter
    1. List.filter
  207. filter
    1. Option.filter
  208. filter
    1. Std.DHashMap.filter
  209. filter
    1. Std.DTreeMap.filter
  210. filter
    1. Std.Ext­DHashMap.filter
  211. filter
    1. Std.Ext­HashMap.filter
  212. filter
    1. Std.Ext­HashSet.filter
  213. filter
    1. Std.HashMap.filter
  214. filter
    1. Std.HashSet.filter
  215. filter
    1. Std.TreeMap.filter
  216. filter
    1. Std.TreeSet.filter
  217. filter­M
    1. Array.filter­M
  218. filter­M
    1. List.filter­M
  219. filter­Map
    1. Array.filter­Map
  220. filter­Map
    1. List.filter­Map
  221. filter­Map
    1. Std.DHashMap.filter­Map
  222. filter­Map
    1. Std.DTreeMap.filter­Map
  223. filter­Map
    1. Std.Ext­DHashMap.filter­Map
  224. filter­Map
    1. Std.Ext­HashMap.filter­Map
  225. filter­Map
    1. Std.HashMap.filter­Map
  226. filter­Map
    1. Std.TreeMap.filter­Map
  227. filter­Map­M
    1. Array.filter­Map­M
  228. filter­Map­M
    1. List.filter­Map­M
  229. filter­Map­TR
    1. List.filter­Map­TR
  230. filter­Rev­M
    1. Array.filter­Rev­M
  231. filter­Rev­M
    1. List.filter­Rev­M
  232. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  233. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  234. filter­TR
    1. List.filter­TR
  235. fin­Idx­Of?
    1. Array.fin­Idx­Of?
  236. fin­Idx­Of?
    1. List.fin­Idx­Of?
  237. fin­Range
    1. Array.fin­Range
  238. fin­Range
    1. List.fin­Range
  239. find
    1. String.find
  240. find?
    1. Array.find?
  241. find?
    1. List.find?
  242. find­Extern­Lib?
    1. Lake.find­Extern­Lib?
  243. find­Fin­Idx?
    1. Array.find­Fin­Idx?
  244. find­Fin­Idx?
    1. List.find­Fin­Idx?
  245. find­Idx
    1. Array.find­Idx
  246. find­Idx
    1. List.find­Idx
  247. find­Idx?
    1. Array.find­Idx?
  248. find­Idx?
    1. List.find­Idx?
  249. find­Idx­M?
    1. Array.find­Idx­M?
  250. find­Lean­Exe?
    1. Lake.find­Lean­Exe?
  251. find­Lean­Lib?
    1. Lake.find­Lean­Lib?
  252. find­Line­Start
    1. String.find­Line­Start
  253. find­M?
    1. Array.find­M?
  254. find­M?
    1. List.find­M?
  255. find­Module?
    1. Lake.find­Module?
  256. find­Package?
    1. Lake.find­Package?
  257. find­Rev?
    1. Array.find­Rev?
  258. find­Rev?
    1. Subarray.find­Rev?
  259. find­Rev­M?
    1. Array.find­Rev­M?
  260. find­Rev­M?
    1. Subarray.find­Rev­M?
  261. find­Some!
    1. Array.find­Some!
  262. find­Some?
    1. Array.find­Some?
  263. find­Some?
    1. List.find­Some?
  264. find­Some­M?
    1. Array.find­Some­M?
  265. find­Some­M?
    1. List.find­Some­M?
  266. find­Some­Rev?
    1. Array.find­Some­Rev?
  267. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
  268. find­Some­Rev­M?
    1. Subarray.find­Some­Rev­M?
  269. first (0) (1)
  270. first­Diff­Pos
    1. String.first­Diff­Pos
  271. first­M
    1. Array.first­M
  272. first­M
    1. List.first­M
  273. fix
    1. Lean.Order.fix
  274. fix
    1. WellFounded.fix
  275. fix_eq
    1. Lean.Order.fix_eq
  276. flags
    1. IO.AccessRight.flags
  277. flags
    1. IO.FileRight.flags
  278. flat­Map
    1. Array.flat­Map
  279. flat­Map
    1. List.flat­Map
  280. flat­Map­M
    1. Array.flat­Map­M
  281. flat­Map­M
    1. List.flat­Map­M
  282. flat­Map­TR
    1. List.flat­Map­TR
  283. flatten
    1. Array.flatten
  284. flatten
    1. List.flatten
  285. flatten­TR
    1. List.flatten­TR
  286. floor
    1. Float.floor
  287. floor
    1. Float32.floor
  288. flush
    1. IO.FS.Handle.flush
  289. flush
    1. IO.FS.Stream.flush (structure field)
  290. fmod
    1. Int.fmod
  291. fn
    1. Thunk.fn (structure field)
  292. focus (0) (1)
  293. fold
    1. Nat.fold
  294. fold
    1. Std.DHashMap.fold
  295. fold
    1. Std.HashMap.fold
  296. fold
    1. Std.HashSet.fold
  297. fold­I
    1. Prod.fold­I
  298. fold­M
    1. Nat.fold­M
  299. fold­M
    1. Std.DHashMap.fold­M
  300. fold­M
    1. Std.HashMap.fold­M
  301. fold­M
    1. Std.HashSet.fold­M
  302. fold­Rev
    1. Nat.fold­Rev
  303. fold­Rev­M
    1. Nat.fold­Rev­M
  304. fold­TR
    1. Nat.fold­TR
  305. foldl
    1. Array.foldl
  306. foldl
    1. Fin.foldl
  307. foldl
    1. List.foldl
  308. foldl
    1. Std.DTreeMap.foldl
  309. foldl
    1. Std.TreeMap.foldl
  310. foldl
    1. Std.TreeSet.foldl
  311. foldl
    1. String.foldl
  312. foldl
    1. Subarray.foldl
  313. foldl
    1. Substring.foldl
  314. foldl­M
    1. Array.foldl­M
  315. foldl­M
    1. Fin.foldl­M
  316. foldl­M
    1. List.foldl­M
  317. foldl­M
    1. Std.DTreeMap.foldl­M
  318. foldl­M
    1. Std.TreeMap.foldl­M
  319. foldl­M
    1. Std.TreeSet.foldl­M
  320. foldl­M
    1. Subarray.foldl­M
  321. foldl­Rec­On
    1. List.foldl­Rec­On
  322. foldr
    1. Array.foldr
  323. foldr
    1. Fin.foldr
  324. foldr
    1. List.foldr
  325. foldr
    1. Std.TreeMap.foldr
  326. foldr
    1. Std.TreeSet.foldr
  327. foldr
    1. String.foldr
  328. foldr
    1. Subarray.foldr
  329. foldr
    1. Substring.foldr
  330. foldr­M
    1. Array.foldr­M
  331. foldr­M
    1. Fin.foldr­M
  332. foldr­M
    1. List.foldr­M
  333. foldr­M
    1. Std.TreeMap.foldr­M
  334. foldr­M
    1. Std.TreeSet.foldr­M
  335. foldr­M
    1. Subarray.foldr­M
  336. foldr­Rec­On
    1. List.foldr­Rec­On
  337. foldr­TR
    1. List.foldr­TR
  338. for­A
    1. List.for­A
  339. for­Async
    1. Std.Channel.for­Async
  340. for­In'
    1. ForIn'.for­In' (class method)
  341. for­In
    1. ForIn.for­In (class method)
  342. for­In
    1. ForM.for­In
  343. for­In
    1. Std.DHashMap.for­In
  344. for­In
    1. Std.DTreeMap.for­In
  345. for­In
    1. Std.HashMap.for­In
  346. for­In
    1. Std.HashSet.for­In
  347. for­In
    1. Std.TreeMap.for­In
  348. for­In
    1. Std.TreeSet.for­In
  349. for­In
    1. Subarray.for­In
  350. for­M
    1. Array.for­M
  351. for­M
    1. ForM.for­M (class method)
  352. for­M
    1. List.for­M
  353. for­M
    1. Nat.for­M
  354. for­M
    1. Option.for­M
  355. for­M
    1. Std.DHashMap.for­M
  356. for­M
    1. Std.DTreeMap.for­M
  357. for­M
    1. Std.HashMap.for­M
  358. for­M
    1. Std.HashSet.for­M
  359. for­M
    1. Std.TreeMap.for­M
  360. for­M
    1. Std.TreeSet.for­M
  361. for­M
    1. Subarray.for­M
  362. for­Rev­M
    1. Array.for­Rev­M
  363. for­Rev­M
    1. Nat.for­Rev­M
  364. for­Rev­M
    1. Subarray.for­Rev­M
  365. format
    1. Option.format
  366. format
    1. Std.ToFormat.format (class method)
  367. forward
    1. String.Iterator.forward
  368. fr­Exp
    1. Float.fr­Exp
  369. fr­Exp
    1. Float32.fr­Exp
  370. from­State­M
    1. EStateM.from­State­M
  371. from­UTF8!
    1. String.from­UTF8!
  372. from­UTF8
    1. String.from­UTF8
  373. from­UTF8?
    1. String.from­UTF8?
  374. front
    1. String.front
  375. front
    1. Substring.front
  376. fst
    1. MProd.fst (structure field)
  377. fst
    1. PProd.fst (structure field)
  378. fst
    1. PSigma.fst (structure field)
  379. fst
    1. Prod.fst (structure field)
  380. fst
    1. Sigma.fst (structure field)
  381. fun
  382. fun_cases
  383. fun_induction
  384. funext (0) (1)

G

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

I

  1. IO
  2. IO.Access­Right
  3. IO.AccessRight.flags
  4. IO.AccessRight.mk
    1. Constructor of IO.Access­Right
  5. IO.Error
  6. IO.Error.already­Exists
    1. Constructor of IO.Error
  7. IO.Error.hardware­Fault
    1. Constructor of IO.Error
  8. IO.Error.illegal­Operation
    1. Constructor of IO.Error
  9. IO.Error.inappropriate­Type
    1. Constructor of IO.Error
  10. IO.Error.interrupted
    1. Constructor of IO.Error
  11. IO.Error.invalid­Argument
    1. Constructor of IO.Error
  12. IO.Error.no­File­Or­Directory
    1. Constructor of IO.Error
  13. IO.Error.no­Such­Thing
    1. Constructor of IO.Error
  14. IO.Error.other­Error
    1. Constructor of IO.Error
  15. IO.Error.permission­Denied
    1. Constructor of IO.Error
  16. IO.Error.protocol­Error
    1. Constructor of IO.Error
  17. IO.Error.resource­Busy
    1. Constructor of IO.Error
  18. IO.Error.resource­Exhausted
    1. Constructor of IO.Error
  19. IO.Error.resource­Vanished
    1. Constructor of IO.Error
  20. IO.Error.time­Expired
    1. Constructor of IO.Error
  21. IO.Error.to­String
  22. IO.Error.unexpected­Eof
    1. Constructor of IO.Error
  23. IO.Error.unsatisfied­Constraints
    1. Constructor of IO.Error
  24. IO.Error.unsupported­Operation
    1. Constructor of IO.Error
  25. IO.Error.user­Error
    1. Constructor of IO.Error
  26. IO.FS.Dir­Entry
  27. IO.FS.DirEntry.mk
    1. Constructor of IO.FS.Dir­Entry
  28. IO.FS.DirEntry.path
  29. IO.FS.Handle
  30. IO.FS.Handle.flush
  31. IO.FS.Handle.get­Line
  32. IO.FS.Handle.is­Tty
  33. IO.FS.Handle.lock
  34. IO.FS.Handle.mk
  35. IO.FS.Handle.put­Str
  36. IO.FS.Handle.put­Str­Ln
  37. IO.FS.Handle.read
  38. IO.FS.Handle.read­Bin­To­End
  39. IO.FS.Handle.read­Bin­To­End­Into
  40. IO.FS.Handle.read­To­End
  41. IO.FS.Handle.rewind
  42. IO.FS.Handle.truncate
  43. IO.FS.Handle.try­Lock
  44. IO.FS.Handle.unlock
  45. IO.FS.Handle.write
  46. IO.FS.Metadata
  47. IO.FS.Metadata.mk
    1. Constructor of IO.FS.Metadata
  48. IO.FS.Mode
  49. IO.FS.Mode.append
    1. Constructor of IO.FS.Mode
  50. IO.FS.Mode.read
    1. Constructor of IO.FS.Mode
  51. IO.FS.Mode.read­Write
    1. Constructor of IO.FS.Mode
  52. IO.FS.Mode.write
    1. Constructor of IO.FS.Mode
  53. IO.FS.Mode.write­New
    1. Constructor of IO.FS.Mode
  54. IO.FS.Stream
  55. IO.FS.Stream.Buffer
  56. IO.FS.Stream.Buffer.mk
    1. Constructor of IO.FS.Stream.Buffer
  57. IO.FS.Stream.mk
    1. Constructor of IO.FS.Stream
  58. IO.FS.Stream.of­Buffer
  59. IO.FS.Stream.of­Handle
  60. IO.FS.Stream.put­Str­Ln
  61. IO.FS.create­Dir
  62. IO.FS.create­Dir­All
  63. IO.FS.create­Temp­Dir
  64. IO.FS.create­Temp­File
  65. IO.FS.lines
  66. IO.FS.read­Bin­File
  67. IO.FS.read­File
  68. IO.FS.real­Path
  69. IO.FS.remove­Dir
  70. IO.FS.remove­Dir­All
  71. IO.FS.remove­File
  72. IO.FS.rename
  73. IO.FS.with­File
  74. IO.FS.with­Isolated­Streams
  75. IO.FS.with­Temp­Dir
  76. IO.FS.with­Temp­File
  77. IO.FS.write­Bin­File
  78. IO.FS.write­File
  79. IO.File­Right
  80. IO.FileRight.flags
  81. IO.FileRight.mk
    1. Constructor of IO.File­Right
  82. IO.Process.Child
  83. IO.Process.Child.kill
  84. IO.Process.Child.take­Stdin
  85. IO.Process.Child.try­Wait
  86. IO.Process.Child.wait
  87. IO.Process.Output
  88. IO.Process.Output.mk
    1. Constructor of IO.Process.Output
  89. IO.Process.Spawn­Args
  90. IO.Process.SpawnArgs.mk
    1. Constructor of IO.Process.Spawn­Args
  91. IO.Process.Stdio
  92. IO.Process.Stdio.inherit
    1. Constructor of IO.Process.Stdio
  93. IO.Process.Stdio.null
    1. Constructor of IO.Process.Stdio
  94. IO.Process.Stdio.piped
    1. Constructor of IO.Process.Stdio
  95. IO.Process.Stdio.to­Handle­Type
  96. IO.Process.Stdio­Config
  97. IO.Process.StdioConfig.mk
    1. Constructor of IO.Process.Stdio­Config
  98. IO.Process.exit
  99. IO.Process.get­Current­Dir
  100. IO.Process.get­PID
  101. IO.Process.output
  102. IO.Process.run
  103. IO.Process.set­Current­Dir
  104. IO.Process.spawn
  105. IO.Promise
  106. IO.Promise.is­Resolved
  107. IO.Promise.new
  108. IO.Promise.resolve
  109. IO.Promise.result!
  110. IO.Promise.result?
  111. IO.Promise.result­D
  112. IO.Ref
  113. IO.Task­State
  114. IO.TaskState.finished
    1. Constructor of IO.Task­State
  115. IO.TaskState.running
    1. Constructor of IO.Task­State
  116. IO.TaskState.waiting
    1. Constructor of IO.Task­State
  117. IO.add­Heartbeats
  118. IO.app­Dir
  119. IO.app­Path
  120. IO.as­Task
  121. IO.bind­Task
  122. IO.cancel
  123. IO.chain­Task
  124. IO.check­Canceled
  125. IO.current­Dir
  126. IO.eprint
  127. IO.eprintln
  128. IO.get­Env
  129. IO.get­Num­Heartbeats
  130. IO.get­Random­Bytes
  131. IO.get­Stderr
  132. IO.get­Stdin
  133. IO.get­Stdout
  134. IO.get­TID
  135. IO.get­Task­State
  136. IO.has­Finished
  137. IO.iterate
  138. IO.lazy­Pure
  139. IO.map­Task
  140. IO.map­Tasks
  141. IO.mk­Ref
  142. IO.mono­Ms­Now
  143. IO.mono­Nanos­Now
  144. IO.of­Except
  145. IO.print
  146. IO.println
  147. IO.rand
  148. IO.set­Access­Rights
  149. IO.set­Rand­Seed
  150. IO.set­Stderr
  151. IO.set­Stdin
  152. IO.set­Stdout
  153. IO.sleep
  154. IO.to­EIO
  155. IO.user­Error
  156. IO.wait
  157. IO.wait­Any
  158. IO.with­Stderr
  159. IO.with­Stdin
  160. IO.with­Stdout
  161. ISize
  162. ISize.abs
  163. ISize.add
  164. ISize.complement
  165. ISize.dec­Eq
  166. ISize.dec­Le
  167. ISize.dec­Lt
  168. ISize.div
  169. ISize.land
  170. ISize.le
  171. ISize.lor
  172. ISize.lt
  173. ISize.max­Value
  174. ISize.min­Value
  175. ISize.mod
  176. ISize.mul
  177. ISize.neg
  178. ISize.of­Bit­Vec
  179. ISize.of­Int
  180. ISize.of­Int­LE
  181. ISize.of­Int­Truncate
  182. ISize.of­Nat
  183. ISize.shift­Left
  184. ISize.shift­Right
  185. ISize.size
  186. ISize.sub
  187. ISize.to­Bit­Vec
  188. ISize.to­Float
  189. ISize.to­Float32
  190. ISize.to­Int
  191. ISize.to­Int16
  192. ISize.to­Int32
  193. ISize.to­Int64
  194. ISize.to­Int8
  195. ISize.to­Nat­Clamp­Neg
  196. ISize.xor
  197. Id
  198. Id.run
  199. Ident
    1. Lean.Syntax.Ident
  200. Iff
  201. Iff.elim
  202. Iff.intro
    1. Constructor of Iff
  203. Inhabited
  204. Inhabited.mk
    1. Instance constructor of Inhabited
  205. Int
  206. Int.add
  207. Int.bdiv
  208. Int.bmod
  209. Int.cast
  210. Int.dec­Eq
  211. Int.ediv
  212. Int.emod
  213. Int.fdiv
  214. Int.fmod
  215. Int.gcd
  216. Int.lcm
  217. Int.le
  218. Int.lt
  219. Int.mul
  220. Int.nat­Abs
  221. Int.neg
  222. Int.neg­Of­Nat
  223. Int.neg­Succ
    1. Constructor of Int
  224. Int.not
  225. Int.of­Nat
    1. Constructor of Int
  226. Int.pow
  227. Int.repr
  228. Int.shift­Right
  229. Int.sign
  230. Int.sub
  231. Int.sub­Nat­Nat
  232. Int.tdiv
  233. Int.tmod
  234. Int.to­ISize
  235. Int.to­Int16
  236. Int.to­Int32
  237. Int.to­Int64
  238. Int.to­Int8
  239. Int.to­Nat
  240. Int.to­Nat?
  241. Int16
  242. Int16.abs
  243. Int16.add
  244. Int16.complement
  245. Int16.dec­Eq
  246. Int16.dec­Le
  247. Int16.dec­Lt
  248. Int16.div
  249. Int16.land
  250. Int16.le
  251. Int16.lor
  252. Int16.lt
  253. Int16.max­Value
  254. Int16.min­Value
  255. Int16.mod
  256. Int16.mul
  257. Int16.neg
  258. Int16.of­Bit­Vec
  259. Int16.of­Int
  260. Int16.of­Int­LE
  261. Int16.of­Int­Truncate
  262. Int16.of­Nat
  263. Int16.shift­Left
  264. Int16.shift­Right
  265. Int16.size
  266. Int16.sub
  267. Int16.to­Bit­Vec
  268. Int16.to­Float
  269. Int16.to­Float32
  270. Int16.to­ISize
  271. Int16.to­Int
  272. Int16.to­Int32
  273. Int16.to­Int64
  274. Int16.to­Int8
  275. Int16.to­Nat­Clamp­Neg
  276. Int16.xor
  277. Int32
  278. Int32.abs
  279. Int32.add
  280. Int32.complement
  281. Int32.dec­Eq
  282. Int32.dec­Le
  283. Int32.dec­Lt
  284. Int32.div
  285. Int32.land
  286. Int32.le
  287. Int32.lor
  288. Int32.lt
  289. Int32.max­Value
  290. Int32.min­Value
  291. Int32.mod
  292. Int32.mul
  293. Int32.neg
  294. Int32.of­Bit­Vec
  295. Int32.of­Int
  296. Int32.of­Int­LE
  297. Int32.of­Int­Truncate
  298. Int32.of­Nat
  299. Int32.shift­Left
  300. Int32.shift­Right
  301. Int32.size
  302. Int32.sub
  303. Int32.to­Bit­Vec
  304. Int32.to­Float
  305. Int32.to­Float32
  306. Int32.to­ISize
  307. Int32.to­Int
  308. Int32.to­Int16
  309. Int32.to­Int64
  310. Int32.to­Int8
  311. Int32.to­Nat­Clamp­Neg
  312. Int32.xor
  313. Int64
  314. Int64.abs
  315. Int64.add
  316. Int64.complement
  317. Int64.dec­Eq
  318. Int64.dec­Le
  319. Int64.dec­Lt
  320. Int64.div
  321. Int64.land
  322. Int64.le
  323. Int64.lor
  324. Int64.lt
  325. Int64.max­Value
  326. Int64.min­Value
  327. Int64.mod
  328. Int64.mul
  329. Int64.neg
  330. Int64.of­Bit­Vec
  331. Int64.of­Int
  332. Int64.of­Int­LE
  333. Int64.of­Int­Truncate
  334. Int64.of­Nat
  335. Int64.shift­Left
  336. Int64.shift­Right
  337. Int64.size
  338. Int64.sub
  339. Int64.to­Bit­Vec
  340. Int64.to­Float
  341. Int64.to­Float32
  342. Int64.to­ISize
  343. Int64.to­Int
  344. Int64.to­Int16
  345. Int64.to­Int32
  346. Int64.to­Int8
  347. Int64.to­Nat­Clamp­Neg
  348. Int64.xor
  349. Int8
  350. Int8.abs
  351. Int8.add
  352. Int8.complement
  353. Int8.dec­Eq
  354. Int8.dec­Le
  355. Int8.dec­Lt
  356. Int8.div
  357. Int8.land
  358. Int8.le
  359. Int8.lor
  360. Int8.lt
  361. Int8.max­Value
  362. Int8.min­Value
  363. Int8.mod
  364. Int8.mul
  365. Int8.neg
  366. Int8.of­Bit­Vec
  367. Int8.of­Int
  368. Int8.of­Int­LE
  369. Int8.of­Int­Truncate
  370. Int8.of­Nat
  371. Int8.shift­Left
  372. Int8.shift­Right
  373. Int8.size
  374. Int8.sub
  375. Int8.to­Bit­Vec
  376. Int8.to­Float
  377. Int8.to­Float32
  378. Int8.to­ISize
  379. Int8.to­Int
  380. Int8.to­Int16
  381. Int8.to­Int32
  382. Int8.to­Int64
  383. Int8.to­Nat­Clamp­Neg
  384. Int8.xor
  385. Int­Cast
  386. IntCast.mk
    1. Instance constructor of Int­Cast
  387. Int­Module
    1. Lean.Grind.Int­Module
  388. Is­Char­P
    1. Lean.Grind.Is­Char­P
  389. Is­Infix
    1. List.Is­Infix
  390. Is­Prefix
    1. List.Is­Prefix
  391. Is­Suffix
    1. List.Is­Suffix
  392. Iterator
    1. String.Iterator
  393. i
    1. String.Iterator.i (structure field)
  394. id_map
    1. LawfulFunctor.id_map (class method)
  395. ident­Kind
    1. Lean.ident­Kind
  396. identifier
  397. identifier
    1. raw
  398. idx­Of
    1. Array.idx­Of
  399. idx­Of
    1. List.idx­Of
  400. idx­Of?
    1. Array.idx­Of?
  401. idx­Of?
    1. List.idx­Of?
  402. if ... then ... else ...
  403. if h : ... then ... else ...
  404. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  405. impredicative
  406. inaccessible
  407. ind
    1. Quot.ind
  408. ind
    1. Quotient.ind
  409. ind
    1. Squash.ind
  410. indent­D
    1. Std.Format.indent­D
  411. index
    1. Lean.Meta.DSimp.Config.index (structure field)
  412. index
    1. Lean.Meta.Simp.Config.index (structure field)
  413. index
    1. of inductive type
  414. indexed family
    1. of types
  415. induction
  416. induction
    1. Fin.induction
  417. induction­On
    1. Fin.induction­On
  418. induction­On
    1. Nat.div.induction­On
  419. induction­On
    1. Nat.mod.induction­On
  420. inductive.auto­Promote­Indices
  421. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  422. infer­Instance
  423. infer­Instance­As
  424. infer_instance
  425. inhabited­Left
    1. PSum.inhabited­Left
  426. inhabited­Left
    1. Sum.inhabited­Left
  427. inhabited­Right
    1. PSum.inhabited­Right
  428. inhabited­Right
    1. Sum.inhabited­Right
  429. inherit­Env
    1. IO.Process.SpawnArgs.args (structure field)
  430. init (Lake command)
  431. injection
  432. injections
  433. inner
    1. Std.DHashMap.Equiv.inner (structure field)
  434. inner
    1. Std.DTreeMap.Raw.inner (structure field)
  435. inner
    1. Std.Ext­HashSet.inner (structure field)
  436. inner
    1. Std.HashMap.Equiv.inner (structure field)
  437. inner
    1. Std.HashMap.Raw.inner (structure field)
  438. inner
    1. Std.HashSet.Equiv.inner (structure field)
  439. inner
    1. Std.HashSet.Raw.inner (structure field)
  440. inner
    1. Std.HashSet.inner (structure field)
  441. inner
    1. Std.TreeMap.Raw.inner (structure field)
  442. inner
    1. Std.TreeSet.Raw.inner (structure field)
  443. insert
    1. List.insert
  444. insert
    1. Std.DHashMap.insert
  445. insert
    1. Std.DTreeMap.insert
  446. insert
    1. Std.Ext­DHashMap.insert
  447. insert
    1. Std.Ext­HashMap.insert
  448. insert
    1. Std.Ext­HashSet.insert
  449. insert
    1. Std.HashMap.insert
  450. insert
    1. Std.HashSet.insert
  451. insert
    1. Std.TreeMap.insert
  452. insert
    1. Std.TreeSet.insert
  453. insert­Idx!
    1. Array.insert­Idx!
  454. insert­Idx
    1. Array.insert­Idx
  455. insert­Idx
    1. List.insert­Idx
  456. insert­Idx­If­In­Bounds
    1. Array.insert­Idx­If­In­Bounds
  457. insert­Idx­TR
    1. List.insert­Idx­TR
  458. insert­If­New
    1. Std.DHashMap.insert­If­New
  459. insert­If­New
    1. Std.DTreeMap.insert­If­New
  460. insert­If­New
    1. Std.Ext­DHashMap.insert­If­New
  461. insert­If­New
    1. Std.Ext­HashMap.insert­If­New
  462. insert­If­New
    1. Std.HashMap.insert­If­New
  463. insert­If­New
    1. Std.TreeMap.insert­If­New
  464. insert­Many
    1. Std.DHashMap.insert­Many
  465. insert­Many
    1. Std.DTreeMap.insert­Many
  466. insert­Many
    1. Std.Ext­DHashMap.insert­Many
  467. insert­Many
    1. Std.Ext­HashMap.insert­Many
  468. insert­Many
    1. Std.Ext­HashSet.insert­Many
  469. insert­Many
    1. Std.HashMap.insert­Many
  470. insert­Many
    1. Std.HashSet.insert­Many
  471. insert­Many
    1. Std.TreeMap.insert­Many
  472. insert­Many
    1. Std.TreeSet.insert­Many
  473. insert­Many­If­New­Unit
    1. Std.Ext­HashMap.insert­Many­If­New­Unit
  474. insert­Many­If­New­Unit
    1. Std.HashMap.insert­Many­If­New­Unit
  475. insert­Many­If­New­Unit
    1. Std.TreeMap.insert­Many­If­New­Unit
  476. insertion­Sort
    1. Array.insertion­Sort
  477. instance synthesis
  478. int­Cast
    1. IntCast.int­Cast (class method)
  479. int­Cast
    1. [anonymous] (class method)
  480. int­Cast_neg
    1. [anonymous] (class method)
  481. int­Cast_of­Nat
    1. [anonymous] (class method)
  482. int­Max
    1. BitVec.int­Max
  483. int­Min
    1. BitVec.int­Min
  484. intercalate
    1. List.intercalate
  485. intercalate
    1. String.intercalate
  486. intercalate­TR
    1. List.intercalate­TR
  487. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  488. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  489. intersperse
    1. List.intersperse
  490. intersperse­TR
    1. List.intersperse­TR
  491. intro (0) (1)
  492. intro | ... => ... | ... => ...
  493. intros
  494. inv­Image
  495. inv_zero
    1. [anonymous] (class method)
  496. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
  497. iota
    1. Lean.Meta.Simp.Config.iota (structure field)
  498. is­Absolute
    1. System.FilePath.is­Absolute
  499. is­Alpha
    1. Char.is­Alpha
  500. is­Alphanum
    1. Char.is­Alphanum
  501. is­Digit
    1. Char.is­Digit
  502. is­Dir
    1. System.FilePath.is­Dir
  503. is­Empty
    1. Array.is­Empty
  504. is­Empty
    1. List.is­Empty
  505. is­Empty
    1. Std.DHashMap.is­Empty
  506. is­Empty
    1. Std.DTreeMap.is­Empty
  507. is­Empty
    1. Std.Ext­DHashMap.is­Empty
  508. is­Empty
    1. Std.Ext­HashMap.is­Empty
  509. is­Empty
    1. Std.Ext­HashSet.is­Empty
  510. is­Empty
    1. Std.Format.is­Empty
  511. is­Empty
    1. Std.HashMap.is­Empty
  512. is­Empty
    1. Std.HashSet.is­Empty
  513. is­Empty
    1. Std.TreeMap.is­Empty
  514. is­Empty
    1. Std.TreeSet.is­Empty
  515. is­Empty
    1. String.is­Empty
  516. is­Empty
    1. Substring.is­Empty
  517. is­Emscripten
    1. System.Platform.is­Emscripten
  518. is­Eq
    1. Ordering.is­Eq
  519. is­Eq­Some
    1. Option.is­Eq­Some
  520. is­Eqv
    1. Array.is­Eqv
  521. is­Eqv
    1. List.is­Eqv
  522. is­Exclusive­Unsafe
  523. is­Finite
    1. Float.is­Finite
  524. is­Finite
    1. Float32.is­Finite
  525. is­GE
    1. Ordering.is­GE
  526. is­GT
    1. Ordering.is­GT
  527. is­Inf
    1. Float.is­Inf
  528. is­Inf
    1. Float32.is­Inf
  529. is­Int
    1. String.is­Int
  530. is­LE
    1. Ordering.is­LE
  531. is­LT
    1. Ordering.is­LT
  532. is­Left
    1. Sum.is­Left
  533. is­Lower
    1. Char.is­Lower
  534. is­Lt
    1. Fin.is­Lt (structure field)
  535. is­Na­N
    1. Float.is­Na­N
  536. is­Na­N
    1. Float32.is­Na­N
  537. is­Nat
    1. String.is­Nat
  538. is­Nat
    1. Substring.is­Nat
  539. is­Ne
    1. Ordering.is­Ne
  540. is­Nil
    1. Std.Format.is­Nil
  541. is­None
    1. Option.is­None
  542. is­OSX
    1. System.Platform.is­OSX
  543. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  544. is­Ok
    1. Except.is­Ok
  545. is­Perm
    1. List.is­Perm
  546. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  547. is­Prefix­Of
    1. Array.is­Prefix­Of
  548. is­Prefix­Of
    1. List.is­Prefix­Of
  549. is­Prefix­Of
    1. String.is­Prefix­Of
  550. is­Prefix­Of?
    1. List.is­Prefix­Of?
  551. is­Relative
    1. System.FilePath.is­Relative
  552. is­Resolved
    1. IO.Promise.is­Resolved
  553. is­Right
    1. Sum.is­Right
  554. is­Some
    1. Option.is­Some
  555. is­Sublist
    1. List.is­Sublist
  556. is­Suffix­Of
    1. List.is­Suffix­Of
  557. is­Suffix­Of?
    1. List.is­Suffix­Of?
  558. is­Tty
    1. IO.FS.Handle.is­Tty
  559. is­Tty
    1. IO.FS.Stream.is­Tty (structure field)
  560. is­Upper
    1. Char.is­Upper
  561. is­Valid
    1. String.Pos.is­Valid
  562. is­Valid­Char
    1. Nat.is­Valid­Char
  563. is­Valid­Char
    1. UInt32.is­Valid­Char
  564. is­Valid­Char­Nat
    1. Char.is­Valid­Char­Nat
  565. is­Whitespace
    1. Char.is­Whitespace
  566. is­Windows
    1. System.Platform.is­Windows
  567. iseqv
    1. Setoid.iseqv (class method)
  568. iter
    1. String.iter
  569. iterate
  570. iterate
    1. IO.iterate
  571. iunfoldr
    1. BitVec.iunfoldr
  572. iunfoldr_replace
    1. BitVec.iunfoldr_replace

J

  1. join
    1. Option.join
  2. join
    1. Std.Format.join
  3. join
    1. String.join
  4. join
    1. System.FilePath.join
  5. join­Sep
    1. Std.Format.join­Sep
  6. join­Suffix
    1. Std.Format.join­Suffix

K

  1. key­At­Idx!
    1. Std.TreeMap.key­At­Idx!
  2. key­At­Idx
    1. Std.TreeMap.key­At­Idx
  3. key­At­Idx?
    1. Std.TreeMap.key­At­Idx?
  4. key­At­Idx­D
    1. Std.TreeMap.key­At­Idx­D
  5. keys
    1. Std.DHashMap.keys
  6. keys
    1. Std.DTreeMap.keys
  7. keys
    1. Std.HashMap.keys
  8. keys
    1. Std.TreeMap.keys
  9. keys­Array
    1. Std.DHashMap.keys­Array
  10. keys­Array
    1. Std.DTreeMap.keys­Array
  11. keys­Array
    1. Std.HashMap.keys­Array
  12. keys­Array
    1. Std.TreeMap.keys­Array
  13. kill
    1. IO.Process.Child.kill
  14. kleisli­Left
    1. Bind.kleisli­Left
  15. kleisli­Right
    1. Bind.kleisli­Right

L

  1. LAKE (environment variable)
  2. LAKE_HOME (environment variable)
  3. LAKE_NO_CACHE (environment variable)
  4. LAKE_OVERRIDE_LEAN (environment variable)
  5. LE
  6. LE.mk
    1. Instance constructor of LE
  7. LEAN (environment variable)
  8. LEAN_AR (environment variable)
  9. LEAN_CC (environment variable)
  10. LEAN_NUM_THREADS (environment variable)
  11. LEAN_SYSROOT (environment variable)
  12. LT
  13. LT.mk
    1. Instance constructor of LT
  14. Lake.Backend
  15. Lake.Backend.c
    1. Constructor of Lake.Backend
  16. Lake.Backend.default
    1. Constructor of Lake.Backend
  17. Lake.Backend.llvm
    1. Constructor of Lake.Backend
  18. Lake.Build­Type
  19. Lake.BuildType.debug
    1. Constructor of Lake.Build­Type
  20. Lake.BuildType.min­Size­Rel
    1. Constructor of Lake.Build­Type
  21. Lake.BuildType.rel­With­Deb­Info
    1. Constructor of Lake.Build­Type
  22. Lake.BuildType.release
    1. Constructor of Lake.Build­Type
  23. Lake.Glob
  24. Lake.Glob.and­Submodules
    1. Constructor of Lake.Glob
  25. Lake.Glob.one
    1. Constructor of Lake.Glob
  26. Lake.Glob.submodules
    1. Constructor of Lake.Glob
  27. Lake.Lean­Exe­Config
  28. Lake.Lean­ExeConfig.mk
    1. Constructor of Lake.Lean­Exe­Config
  29. Lake.Lean­Lib­Config
  30. Lake.Lean­LibConfig.mk
    1. Constructor of Lake.Lean­Lib­Config
  31. Lake.Monad­Lake­Env
  32. Lake.Monad­Workspace
  33. Lake.MonadWorkspace.mk
    1. Instance constructor of Lake.Monad­Workspace
  34. Lake.Script­M (0) (1)
  35. Lake.find­Extern­Lib?
  36. Lake.find­Lean­Exe?
  37. Lake.find­Lean­Lib?
  38. Lake.find­Module?
  39. Lake.find­Package?
  40. Lake.get­Augmented­Env
  41. Lake.get­Augmented­Lean­Path
  42. Lake.get­Augmented­Lean­Src­Path
  43. Lake.get­Augmented­Shared­Lib­Path
  44. Lake.get­Elan?
  45. Lake.get­Elan­Home?
  46. Lake.get­Elan­Install?
  47. Lake.get­Elan­Toolchain
  48. Lake.get­Env­Lean­Path
  49. Lake.get­Env­Lean­Src­Path
  50. Lake.get­Env­Shared­Lib­Path
  51. Lake.get­Lake
  52. Lake.get­Lake­Env
  53. Lake.get­Lake­Home
  54. Lake.get­Lake­Install
  55. Lake.get­Lake­Lib­Dir
  56. Lake.get­Lake­Src­Dir
  57. Lake.get­Lean
  58. Lake.get­Lean­Ar
  59. Lake.get­Lean­Cc
  60. Lake.get­Lean­Cc?
  61. Lake.get­Lean­Include­Dir
  62. Lake.get­Lean­Install
  63. Lake.get­Lean­Lib­Dir
  64. Lake.get­Lean­Path
  65. Lake.get­Lean­Shared­Lib
  66. Lake.get­Lean­Src­Dir
  67. Lake.get­Lean­Src­Path
  68. Lake.get­Lean­Sysroot
  69. Lake.get­Lean­System­Lib­Dir
  70. Lake.get­Leanc
  71. Lake.get­No­Cache
  72. Lake.get­Pkg­Url­Map
  73. Lake.get­Root­Package
  74. Lake.get­Shared­Lib­Path
  75. Lake.get­Try­Cache
  76. Lawful­Applicative
  77. LawfulApplicative.mk
    1. Instance constructor of Lawful­Applicative
  78. Lawful­BEq
  79. LawfulBEq.mk
    1. Instance constructor of Lawful­BEq
  80. Lawful­Functor
  81. LawfulFunctor.mk
    1. Instance constructor of Lawful­Functor
  82. Lawful­Get­Elem
  83. Lawful­GetElem.mk
    1. Instance constructor of Lawful­Get­Elem
  84. Lawful­Hashable
  85. LawfulHashable.mk
    1. Instance constructor of Lawful­Hashable
  86. Lawful­Monad
  87. LawfulMonad.mk'
  88. LawfulMonad.mk
    1. Instance constructor of Lawful­Monad
  89. Leading­Ident­Behavior
    1. Lean.Parser.Leading­Ident­Behavior
  90. Lean.Elab.register­Deriving­Handler
  91. Lean.Grind.Add­Right­Cancel
  92. Lean.Grind.Add­RightCancel.mk
    1. Instance constructor of Lean.Grind.Add­Right­Cancel
  93. Lean.Grind.Comm­Ring
  94. Lean.Grind.CommRing.mk
    1. Instance constructor of Lean.Grind.Comm­Ring
  95. Lean.Grind.Comm­Semiring
  96. Lean.Grind.CommSemiring.mk
    1. Instance constructor of Lean.Grind.Comm­Semiring
  97. Lean.Grind.Field
  98. Lean.Grind.Field.mk
    1. Instance constructor of Lean.Grind.Field
  99. Lean.Grind.Int­Module
  100. Lean.Grind.IntModule.mk
    1. Instance constructor of Lean.Grind.Int­Module
  101. Lean.Grind.Is­Char­P
  102. Lean.Grind.Is­CharP.mk
    1. Instance constructor of Lean.Grind.Is­Char­P
  103. Lean.Grind.Linear­Order
  104. Lean.Grind.LinearOrder.mk
    1. Instance constructor of Lean.Grind.Linear­Order
  105. Lean.Grind.Nat­Module
  106. Lean.Grind.NatModule.mk
    1. Instance constructor of Lean.Grind.Nat­Module
  107. Lean.Grind.No­Nat­Zero­Divisors
  108. Lean.Grind.No­Nat­ZeroDivisors.mk
    1. Instance constructor of Lean.Grind.No­Nat­Zero­Divisors
  109. Lean.Grind.Ordered­Add
  110. Lean.Grind.OrderedAdd.mk
    1. Instance constructor of Lean.Grind.Ordered­Add
  111. Lean.Grind.Ordered­Ring
  112. Lean.Grind.OrderedRing.mk
    1. Instance constructor of Lean.Grind.Ordered­Ring
  113. Lean.Grind.Partial­Order
  114. Lean.Grind.PartialOrder.mk
    1. Instance constructor of Lean.Grind.Partial­Order
  115. Lean.Grind.Preorder
  116. Lean.Grind.Preorder.mk
    1. Instance constructor of Lean.Grind.Preorder
  117. Lean.Grind.Ring
  118. Lean.Grind.Ring.mk
    1. Instance constructor of Lean.Grind.Ring
  119. Lean.Grind.Semiring
  120. Lean.Grind.Semiring.mk
    1. Instance constructor of Lean.Grind.Semiring
  121. Lean.Lean­Option
  122. Lean.LeanOption.mk
    1. Constructor of Lean.Lean­Option
  123. Lean.Macro.Exception.unsupported­Syntax
  124. Lean.Macro.add­Macro­Scope
  125. Lean.Macro.expand­Macro?
  126. Lean.Macro.get­Curr­Namespace
  127. Lean.Macro.has­Decl
  128. Lean.Macro.resolve­Global­Name
  129. Lean.Macro.resolve­Namespace
  130. Lean.Macro.throw­Error
  131. Lean.Macro.throw­Error­At
  132. Lean.Macro.throw­Unsupported
  133. Lean.Macro.trace
  134. Lean.Macro.with­Fresh­Macro­Scope
  135. Lean.Macro­M
  136. Lean.Meta.DSimp.Config
  137. Lean.Meta.DSimp.Config.mk
    1. Constructor of Lean.Meta.DSimp.Config
  138. Lean.Meta.Occurrences
  139. Lean.Meta.Occurrences.all
    1. Constructor of Lean.Meta.Occurrences
  140. Lean.Meta.Occurrences.neg
    1. Constructor of Lean.Meta.Occurrences
  141. Lean.Meta.Occurrences.pos
    1. Constructor of Lean.Meta.Occurrences
  142. Lean.Meta.Rewrite.Config
  143. Lean.Meta.Rewrite.Config.mk
    1. Constructor of Lean.Meta.Rewrite.Config
  144. Lean.Meta.Rewrite.New­Goals
  145. Lean.Meta.Simp.Config
  146. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  147. Lean.Meta.Simp.neutral­Config
  148. Lean.Meta.Simp­Extension
  149. Lean.Meta.Transparency­Mode
  150. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.Transparency­Mode
  151. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.Transparency­Mode
  152. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.Transparency­Mode
  153. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.Transparency­Mode
  154. Lean.Meta.register­Simp­Attr
  155. Lean.Order.CCPO
  156. Lean.Order.CCPO.mk
    1. Instance constructor of Lean.Order.CCPO
  157. Lean.Order.Partial­Order
  158. Lean.Order.PartialOrder.mk
    1. Instance constructor of Lean.Order.Partial­Order
  159. Lean.Order.fix
  160. Lean.Order.fix_eq
  161. Lean.Order.monotone
  162. Lean.Parser.Leading­Ident­Behavior
  163. Lean.Parser.Leading­IdentBehavior.both
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  164. Lean.Parser.Leading­IdentBehavior.default
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  165. Lean.Parser.Leading­IdentBehavior.symbol
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  166. Lean.PrettyPrinter.Unexpand­M
  167. Lean.PrettyPrinter.Unexpander
  168. Lean.Source­Info
  169. Lean.SourceInfo.none
    1. Constructor of Lean.Source­Info
  170. Lean.SourceInfo.original
    1. Constructor of Lean.Source­Info
  171. Lean.SourceInfo.synthetic
    1. Constructor of Lean.Source­Info
  172. Lean.Syntax
  173. Lean.Syntax.Char­Lit
  174. Lean.Syntax.Command
  175. Lean.Syntax.Hygiene­Info
  176. Lean.Syntax.Ident
  177. Lean.Syntax.Level
  178. Lean.Syntax.Name­Lit
  179. Lean.Syntax.Num­Lit
  180. Lean.Syntax.Prec
  181. Lean.Syntax.Preresolved
  182. Lean.Syntax.Preresolved.decl
    1. Constructor of Lean.Syntax.Preresolved
  183. Lean.Syntax.Preresolved.namespace
    1. Constructor of Lean.Syntax.Preresolved
  184. Lean.Syntax.Prio
  185. Lean.Syntax.Scientific­Lit
  186. Lean.Syntax.Str­Lit
  187. Lean.Syntax.TSep­Array
  188. Lean.Syntax.TSepArray.mk
    1. Constructor of Lean.Syntax.TSep­Array
  189. Lean.Syntax.Tactic
  190. Lean.Syntax.Term
  191. Lean.Syntax.atom
    1. Constructor of Lean.Syntax
  192. Lean.Syntax.get­Kind
  193. Lean.Syntax.ident
    1. Constructor of Lean.Syntax
  194. Lean.Syntax.is­Of­Kind
  195. Lean.Syntax.missing
    1. Constructor of Lean.Syntax
  196. Lean.Syntax.node
    1. Constructor of Lean.Syntax
  197. Lean.Syntax.set­Kind
  198. Lean.Syntax­Node­Kind
  199. Lean.Syntax­Node­Kinds
  200. Lean.TSyntax
  201. Lean.TSyntax.get­Char
  202. Lean.TSyntax.get­Hygiene­Info
  203. Lean.TSyntax.get­Id
  204. Lean.TSyntax.get­Name
  205. Lean.TSyntax.get­Nat
  206. Lean.TSyntax.get­Scientific
  207. Lean.TSyntax.get­String
  208. Lean.TSyntax.mk
    1. Constructor of Lean.TSyntax
  209. Lean.TSyntax­Array
  210. Lean.char­Lit­Kind
  211. Lean.choice­Kind
  212. Lean.field­Idx­Kind
  213. Lean.group­Kind
  214. Lean.hygiene­Info­Kind
  215. Lean.ident­Kind
  216. Lean.interpolated­Str­Kind
  217. Lean.interpolated­Str­Lit­Kind
  218. Lean.name­Lit­Kind
  219. Lean.null­Kind
  220. Lean.num­Lit­Kind
  221. Lean.scientific­Lit­Kind
  222. Lean.str­Lit­Kind
  223. Lean­Exe­Config
    1. Lake.Lean­Exe­Config
  224. Lean­Lib­Config
    1. Lake.Lean­Lib­Config
  225. Lean­Option
    1. Lean.Lean­Option
  226. Level
    1. Lean.Syntax.Level
  227. Lex
    1. List.Lex
  228. Linear­Order
    1. Lean.Grind.Linear­Order
  229. List
  230. List.Is­Infix
  231. List.Is­Prefix
  232. List.Is­Suffix
  233. List.Lex
  234. List.Lex.cons
    1. Constructor of List.Lex
  235. List.Lex.nil
    1. Constructor of List.Lex
  236. List.Lex.rel
    1. Constructor of List.Lex
  237. List.Mem
  238. List.Mem.head
    1. Constructor of List.Mem
  239. List.Mem.tail
    1. Constructor of List.Mem
  240. List.Nodup
  241. List.Pairwise
  242. List.Pairwise.cons
    1. Constructor of List.Pairwise
  243. List.Pairwise.nil
    1. Constructor of List.Pairwise
  244. List.Perm
  245. List.Perm.cons
    1. Constructor of List.Perm
  246. List.Perm.nil
    1. Constructor of List.Perm
  247. List.Perm.swap
    1. Constructor of List.Perm
  248. List.Perm.trans
    1. Constructor of List.Perm
  249. List.Sublist
  250. List.Sublist.cons
    1. Constructor of List.Sublist
  251. List.Sublist.cons₂
    1. Constructor of List.Sublist
  252. List.Sublist.slnil
    1. Constructor of List.Sublist
  253. List.all
  254. List.all­M
  255. List.and
  256. List.any
  257. List.any­M
  258. List.append
  259. List.append­TR
  260. List.as­String
  261. List.attach
  262. List.attach­With
  263. List.beq
  264. List.concat
  265. List.cons
    1. Constructor of List
  266. List.contains
  267. List.count
  268. List.count­P
  269. List.drop
  270. List.drop­Last
  271. List.drop­Last­TR
  272. List.drop­While
  273. List.elem
  274. List.erase
  275. List.erase­Dups
  276. List.erase­Idx
  277. List.erase­Idx­TR
  278. List.erase­P
  279. List.erase­PTR
  280. List.erase­Reps
  281. List.erase­TR
  282. List.extract
  283. List.filter
  284. List.filter­M
  285. List.filter­Map
  286. List.filter­Map­M
  287. List.filter­Map­TR
  288. List.filter­Rev­M
  289. List.filter­TR
  290. List.fin­Idx­Of?
  291. List.fin­Range
  292. List.find?
  293. List.find­Fin­Idx?
  294. List.find­Idx
  295. List.find­Idx?
  296. List.find­M?
  297. List.find­Some?
  298. List.find­Some­M?
  299. List.first­M
  300. List.flat­Map
  301. List.flat­Map­M
  302. List.flat­Map­TR
  303. List.flatten
  304. List.flatten­TR
  305. List.foldl
  306. List.foldl­M
  307. List.foldl­Rec­On
  308. List.foldr
  309. List.foldr­M
  310. List.foldr­Rec­On
  311. List.foldr­TR
  312. List.for­A
  313. List.for­M
  314. List.get
  315. List.get­D
  316. List.get­Last
  317. List.get­Last!
  318. List.get­Last?
  319. List.get­Last­D
  320. List.group­By­Key
  321. List.head
  322. List.head!
  323. List.head?
  324. List.head­D
  325. List.idx­Of
  326. List.idx­Of?
  327. List.insert
  328. List.insert­Idx
  329. List.insert­Idx­TR
  330. List.intercalate
  331. List.intercalate­TR
  332. List.intersperse
  333. List.intersperse­TR
  334. List.is­Empty
  335. List.is­Eqv
  336. List.is­Perm
  337. List.is­Prefix­Of
  338. List.is­Prefix­Of?
  339. List.is­Sublist
  340. List.is­Suffix­Of
  341. List.is­Suffix­Of?
  342. List.le
  343. List.leftpad
  344. List.leftpad­TR
  345. List.length
  346. List.length­TR
  347. List.lex
  348. List.lookup
  349. List.lt
  350. List.map
  351. List.map­A
  352. List.map­Fin­Idx
  353. List.map­Fin­Idx­M
  354. List.map­Idx
  355. List.map­Idx­M
  356. List.map­M
  357. List.map­M'
  358. List.map­Mono
  359. List.map­Mono­M
  360. List.map­TR
  361. List.max?
  362. List.merge
  363. List.merge­Sort
  364. List.min?
  365. List.modify
  366. List.modify­Head
  367. List.modify­TR
  368. List.modify­Tail­Idx
  369. List.nil
    1. Constructor of List
  370. List.of­Fn
  371. List.or
  372. List.partition
  373. List.partition­M
  374. List.partition­Map
  375. List.pmap
  376. List.range
  377. List.range'
  378. List.range'TR
  379. List.remove­All
  380. List.replace
  381. List.replace­TR
  382. List.replicate
  383. List.replicate­TR
  384. List.reverse
  385. List.rightpad
  386. List.rotate­Left
  387. List.rotate­Right
  388. List.set
  389. List.set­TR
  390. List.singleton
  391. List.span
  392. List.split­At
  393. List.split­By
  394. List.sum
  395. List.tail
  396. List.tail!
  397. List.tail?
  398. List.tail­D
  399. List.take
  400. List.take­TR
  401. List.take­While
  402. List.take­While­TR
  403. List.to­Array
  404. List.to­Array­Impl
  405. List.to­Byte­Array
  406. List.to­Float­Array
  407. List.to­String
  408. List.unattach
  409. List.unzip
  410. List.unzip­TR
  411. List.zip
  412. List.zip­Idx
  413. List.zip­Idx­TR
  414. List.zip­With
  415. List.zip­With­All
  416. List.zip­With­TR
  417. land
    1. Fin.land
  418. land
    1. ISize.land
  419. land
    1. Int16.land
  420. land
    1. Int32.land
  421. land
    1. Int64.land
  422. land
    1. Int8.land
  423. land
    1. Nat.land
  424. land
    1. UInt16.land
  425. land
    1. UInt32.land
  426. land
    1. UInt64.land
  427. land
    1. UInt8.land
  428. land
    1. USize.land
  429. last
    1. Fin.last
  430. last­Cases
    1. Fin.last­Cases
  431. lazy­Pure
    1. IO.lazy­Pure
  432. lcm
    1. Int.lcm
  433. lcm
    1. Nat.lcm
  434. le
    1. Char.le
  435. le
    1. Float.le
  436. le
    1. Float32.le
  437. le
    1. ISize.le
  438. le
    1. Int.le
  439. le
    1. Int16.le
  440. le
    1. Int32.le
  441. le
    1. Int64.le
  442. le
    1. Int8.le
  443. le
    1. LE.le (class method)
  444. le
    1. List.le
  445. le
    1. Nat.le
  446. le
    1. String.le
  447. le
    1. UInt16.le
  448. le
    1. UInt32.le
  449. le
    1. UInt64.le
  450. le
    1. UInt8.le
  451. le
    1. USize.le
  452. le­Of­Ord
  453. le_antisymm
    1. [anonymous] (class method)
  454. le_refl
    1. Lean.Grind.Preorder.to­LT (class method)
  455. le_total
    1. [anonymous] (class method)
  456. le_trans
    1. [anonymous] (class method)
  457. lean (Lake command)
  458. lean_is_array
  459. lean_is_string
  460. lean_string_object (0) (1)
  461. lean_to_array
  462. lean_to_string
  463. left (0) (1)
  464. left
    1. And.left (structure field)
  465. left_distrib
    1. Lean.Grind.Semiring.mul_assoc (class method)
  466. leftpad
    1. Array.leftpad
  467. leftpad
    1. List.leftpad
  468. leftpad­TR
    1. List.leftpad­TR
  469. length
    1. List.length
  470. length
    1. String.length
  471. length­TR
    1. List.length­TR
  472. let
  473. let rec
  474. let'
  475. let­I
  476. let­To­Have
    1. Lean.Meta.Simp.Config.let­To­Have (structure field)
  477. level
    1. of universe
  478. lex'
    1. Ord.lex'
  479. lex
    1. Array.lex
  480. lex
    1. List.lex
  481. lex
    1. Ord.lex
  482. lex­Lt
    1. Prod.lex­Lt
  483. lhs
  484. lib­Name
    1. [anonymous] (structure field)
  485. lift
    1. Except­CpsT.lift
  486. lift
    1. ExceptT.lift
  487. lift
    1. OptionT.lift
  488. lift
    1. Quot.lift
  489. lift
    1. Quotient.lift
  490. lift
    1. Squash.lift
  491. lift
    1. State­CpsT.lift
  492. lift
    1. State­RefT'.lift
  493. lift
    1. StateT.lift
  494. lift­On
    1. Quot.lift­On
  495. lift­On
    1. Quotient.lift­On
  496. lift­On₂
    1. Quotient.lift­On₂
  497. lift­With
    1. MonadControl.lift­With (class method)
  498. lift­With
    1. Monad­ControlT.lift­With (class method)
  499. lift₂
    1. Quotient.lift₂
  500. line­Eq
  501. lines
    1. IO.FS.lines
  502. lint (Lake command)
  503. linter.unnecessary­Simpa
  504. literal
    1. raw string
  505. literal
    1. string
  506. lock
    1. IO.FS.Handle.lock
  507. log
    1. Float.log
  508. log
    1. Float32.log
  509. log10
    1. Float.log10
  510. log10
    1. Float32.log10
  511. log2
    1. Fin.log2
  512. log2
    1. Float.log2
  513. log2
    1. Float32.log2
  514. log2
    1. Nat.log2
  515. log2
    1. UInt16.log2
  516. log2
    1. UInt32.log2
  517. log2
    1. UInt64.log2
  518. log2
    1. UInt8.log2
  519. log2
    1. USize.log2
  520. lookup
    1. List.lookup
  521. lor
    1. Fin.lor
  522. lor
    1. ISize.lor
  523. lor
    1. Int16.lor
  524. lor
    1. Int32.lor
  525. lor
    1. Int64.lor
  526. lor
    1. Int8.lor
  527. lor
    1. Nat.lor
  528. lor
    1. UInt16.lor
  529. lor
    1. UInt32.lor
  530. lor
    1. UInt64.lor
  531. lor
    1. UInt8.lor
  532. lor
    1. USize.lor
  533. lt
    1. Char.lt
  534. lt
    1. Float.lt
  535. lt
    1. Float32.lt
  536. lt
    1. ISize.lt
  537. lt
    1. Int.lt
  538. lt
    1. Int16.lt
  539. lt
    1. Int32.lt
  540. lt
    1. Int64.lt
  541. lt
    1. Int8.lt
  542. lt
    1. LT.lt (class method)
  543. lt
    1. List.lt
  544. lt
    1. Nat.lt
  545. lt
    1. Option.lt
  546. lt
    1. UInt16.lt
  547. lt
    1. UInt32.lt
  548. lt
    1. UInt64.lt
  549. lt
    1. UInt8.lt
  550. lt
    1. USize.lt
  551. lt­Of­Ord
  552. lt_iff_le_not_le
    1. Lean.Grind.Preorder.le_refl (class method)

M

  1. MProd
  2. MProd.mk
    1. Constructor of MProd
  3. Macro­M
    1. Lean.Macro­M
  4. Max
  5. Max.mk
    1. Instance constructor of Max
  6. Mem
    1. List.Mem
  7. Metadata
    1. IO.FS.Metadata
  8. Min
  9. Min.mk
    1. Instance constructor of Min
  10. Mod
  11. Mod.mk
    1. Instance constructor of Mod
  12. Mode
    1. IO.FS.Mode
  13. Monad
  14. Monad.mk
    1. Instance constructor of Monad
  15. Monad­Control
  16. MonadControl.mk
    1. Instance constructor of Monad­Control
  17. Monad­Control­T
  18. Monad­ControlT.mk
    1. Instance constructor of Monad­Control­T
  19. Monad­Eval
  20. MonadEval.mk
    1. Instance constructor of Monad­Eval
  21. Monad­Eval­T
  22. Monad­EvalT.mk
    1. Instance constructor of Monad­Eval­T
  23. Monad­Except
  24. MonadExcept.mk
    1. Instance constructor of Monad­Except
  25. MonadExcept.of­Except
  26. MonadExcept.or­Else
  27. MonadExcept.orelse'
  28. Monad­Except­Of
  29. Monad­ExceptOf.mk
    1. Instance constructor of Monad­Except­Of
  30. Monad­Finally
  31. MonadFinally.mk
    1. Instance constructor of Monad­Finally
  32. Monad­Functor
  33. MonadFunctor.mk
    1. Instance constructor of Monad­Functor
  34. Monad­Functor­T
  35. Monad­FunctorT.mk
    1. Instance constructor of Monad­Functor­T
  36. Monad­Lake­Env
    1. Lake.Monad­Lake­Env
  37. Monad­Lift
  38. MonadLift.mk
    1. Instance constructor of Monad­Lift
  39. Monad­Lift­T
  40. Monad­LiftT.mk
    1. Instance constructor of Monad­Lift­T
  41. Monad­Pretty­Format
    1. Std.Format.Monad­Pretty­Format
  42. Monad­Reader
  43. MonadReader.mk
    1. Instance constructor of Monad­Reader
  44. Monad­Reader­Of
  45. Monad­ReaderOf.mk
    1. Instance constructor of Monad­Reader­Of
  46. Monad­State
  47. MonadState.get
  48. MonadState.mk
    1. Instance constructor of Monad­State
  49. MonadState.modify­Get
  50. Monad­State­Of
  51. Monad­StateOf.mk
    1. Instance constructor of Monad­State­Of
  52. Monad­With­Reader
  53. Monad­WithReader.mk
    1. Instance constructor of Monad­With­Reader
  54. Monad­With­Reader­Of
  55. Monad­With­ReaderOf.mk
    1. Instance constructor of Monad­With­Reader­Of
  56. Monad­Workspace
    1. Lake.Monad­Workspace
  57. Mul
  58. Mul.mk
    1. Instance constructor of Mul
  59. Mutex
    1. Std.Mutex
  60. main goal
  61. map
    1. Array.map
  62. map
    1. EStateM.map
  63. map
    1. Except.map
  64. map
    1. ExceptT.map
  65. map
    1. Functor.map (class method)
  66. map
    1. List.map
  67. map
    1. Option.map
  68. map
    1. Prod.map
  69. map
    1. StateT.map
  70. map
    1. Std.DHashMap.map
  71. map
    1. Std.DTreeMap.map
  72. map
    1. Std.Ext­DHashMap.map
  73. map
    1. Std.Ext­HashMap.map
  74. map
    1. Std.HashMap.map
  75. map
    1. Std.TreeMap.map
  76. map
    1. String.map
  77. map
    1. Sum.map
  78. map
    1. Task.map
  79. map
    1. Thunk.map
  80. map
    1. dependent
  81. map
    1. extensional
  82. map­A
    1. List.map­A
  83. map­A
    1. Option.map­A
  84. map­Const
    1. Functor.map­Const (class method)
  85. map­Error
    1. Except.map­Error
  86. map­Fin­Idx
    1. Array.map­Fin­Idx
  87. map­Fin­Idx
    1. List.map­Fin­Idx
  88. map­Fin­Idx­M
    1. Array.map­Fin­Idx­M
  89. map­Fin­Idx­M
    1. List.map­Fin­Idx­M
  90. map­Idx
    1. Array.map­Idx
  91. map­Idx
    1. List.map­Idx
  92. map­Idx­M
    1. Array.map­Idx­M
  93. map­Idx­M
    1. List.map­Idx­M
  94. map­List
    1. Task.map­List
  95. map­M'
    1. Array.map­M'
  96. map­M'
    1. List.map­M'
  97. map­M
    1. Array.map­M
  98. map­M
    1. List.map­M
  99. map­M
    1. Option.map­M
  100. map­Mono
    1. Array.map­Mono
  101. map­Mono
    1. List.map­Mono
  102. map­Mono­M
    1. Array.map­Mono­M
  103. map­Mono­M
    1. List.map­Mono­M
  104. map­Rev
    1. Functor.map­Rev
  105. map­TR
    1. List.map­TR
  106. map­Task
    1. BaseIO.map­Task
  107. map­Task
    1. EIO.map­Task
  108. map­Task
    1. IO.map­Task
  109. map­Tasks
    1. BaseIO.map­Tasks
  110. map­Tasks
    1. EIO.map­Tasks
  111. map­Tasks
    1. IO.map­Tasks
  112. map_const
    1. LawfulFunctor.map_const (class method)
  113. map_pure
    1. LawfulApplicative.seq­Left_eq (class method)
  114. match
  115. match
    1. pp.match
  116. max!
    1. Std.TreeSet.max!
  117. max
    1. Max.max (class method)
  118. max
    1. Nat.max
  119. max
    1. Option.max
  120. max
    1. Std.TreeSet.max
  121. max
    1. Task.Priority.max
  122. max?
    1. List.max?
  123. max?
    1. Std.TreeSet.max?
  124. max­D
    1. Std.TreeSet.max­D
  125. max­Discharge­Depth
    1. Lean.Meta.Simp.Config.max­Discharge­Depth (structure field)
  126. max­Entry!
    1. Std.TreeMap.max­Entry!
  127. max­Entry
    1. Std.TreeMap.max­Entry
  128. max­Entry?
    1. Std.TreeMap.max­Entry?
  129. max­Entry­D
    1. Std.TreeMap.max­Entry­D
  130. max­Heartbeats
    1. synthInstance.max­Heartbeats
  131. max­Key!
    1. Std.TreeMap.max­Key!
  132. max­Key
    1. Std.TreeMap.max­Key
  133. max­Key?
    1. Std.TreeMap.max­Key?
  134. max­Key­D
    1. Std.TreeMap.max­Key­D
  135. max­Of­Le
  136. max­Size
    1. synthInstance.max­Size
  137. max­Steps
    1. Lean.Meta.Simp.Config.max­Steps (structure field)
  138. max­Steps
    1. pp.max­Steps
  139. max­Value
    1. ISize.max­Value
  140. max­Value
    1. Int16.max­Value
  141. max­Value
    1. Int32.max­Value
  142. max­Value
    1. Int64.max­Value
  143. max­Value
    1. Int8.max­Value
  144. memoize
    1. Lean.Meta.Simp.Config.memoize (structure field)
  145. merge
    1. List.merge
  146. merge
    1. Option.merge
  147. merge
    1. Std.TreeSet.merge
  148. merge­Sort
    1. List.merge­Sort
  149. merge­With
    1. Std.TreeMap.merge­With
  150. metadata
    1. System.FilePath.metadata
  151. min!
    1. Std.TreeSet.min!
  152. min
    1. Min.min (class method)
  153. min
    1. Nat.min
  154. min
    1. Option.min
  155. min
    1. Std.TreeSet.min
  156. min
    1. String.Pos.min
  157. min?
    1. List.min?
  158. min?
    1. Std.TreeSet.min?
  159. min­D
    1. Std.TreeSet.min­D
  160. min­Entry!
    1. Std.TreeMap.min­Entry!
  161. min­Entry
    1. Std.TreeMap.min­Entry
  162. min­Entry?
    1. Std.TreeMap.min­Entry?
  163. min­Entry­D
    1. Std.TreeMap.min­Entry­D
  164. min­Key!
    1. Std.TreeMap.min­Key!
  165. min­Key
    1. Std.TreeMap.min­Key
  166. min­Key?
    1. Std.TreeMap.min­Key?
  167. min­Key­D
    1. Std.TreeMap.min­Key­D
  168. min­Of­Le
  169. min­Value
    1. ISize.min­Value
  170. min­Value
    1. Int16.min­Value
  171. min­Value
    1. Int32.min­Value
  172. min­Value
    1. Int64.min­Value
  173. min­Value
    1. Int8.min­Value
  174. mix­Hash
  175. mk'
    1. LawfulMonad.mk'
  176. mk'
    1. Quotient.mk'
  177. mk
    1. ExceptT.mk
  178. mk
    1. IO.FS.Handle.mk
  179. mk
    1. OptionT.mk
  180. mk
    1. Quot.mk
  181. mk
    1. Quotient.mk
  182. mk
    1. Squash.mk
  183. mk­File­Path
    1. System.mk­File­Path
  184. mk­Iterator
    1. String.mk­Iterator
  185. mk­Ref
    1. IO.mk­Ref
  186. mk­Ref
    1. ST.mk­Ref
  187. mk­Std­Gen
  188. mod
    1. Fin.mod
  189. mod
    1. ISize.mod
  190. mod
    1. Int16.mod
  191. mod
    1. Int32.mod
  192. mod
    1. Int64.mod
  193. mod
    1. Int8.mod
  194. mod
    1. Mod.mod (class method)
  195. mod
    1. Nat.mod
  196. mod
    1. UInt16.mod
  197. mod
    1. UInt32.mod
  198. mod
    1. UInt64.mod
  199. mod
    1. UInt8.mod
  200. mod
    1. USize.mod
  201. mod­Core
    1. Nat.mod­Core
  202. modified
    1. IO.FS.Metadata.modified (structure field)
  203. modify
  204. modify
    1. Array.modify
  205. modify
    1. List.modify
  206. modify
    1. ST.Ref.modify
  207. modify
    1. Std.DHashMap.modify
  208. modify
    1. Std.DTreeMap.modify
  209. modify
    1. Std.Ext­DHashMap.modify
  210. modify
    1. Std.Ext­HashMap.modify
  211. modify
    1. Std.HashMap.modify
  212. modify
    1. Std.TreeMap.modify
  213. modify
    1. String.modify
  214. modify­Get
    1. EStateM.modify­Get
  215. modify­Get
    1. MonadState.modify­Get
  216. modify­Get
    1. MonadState.modify­Get (class method)
  217. modify­Get
    1. Monad­StateOf.modify­Get (class method)
  218. modify­Get
    1. ST.Ref.modify­Get
  219. modify­Get
    1. State­RefT'.modify­Get
  220. modify­Get
    1. StateT.modify­Get
  221. modify­Get­The
  222. modify­Head
    1. List.modify­Head
  223. modify­M
    1. Array.modify­M
  224. modify­Op
    1. Array.modify­Op
  225. modify­TR
    1. List.modify­TR
  226. modify­Tail­Idx
    1. List.modify­Tail­Idx
  227. modify­The
  228. modn
    1. Fin.modn
  229. monad­Eval
    1. MonadEval.monad­Eval (class method)
  230. monad­Eval
    1. Monad­EvalT.monad­Eval (class method)
  231. monad­Lift
    1. MonadLift.monad­Lift (class method)
  232. monad­Lift
    1. Monad­LiftT.monad­Lift (class method)
  233. monad­Map
    1. MonadFunctor.monad­Map (class method)
  234. monad­Map
    1. Monad­FunctorT.monad­Map (class method)
  235. mono­Ms­Now
    1. IO.mono­Ms­Now
  236. mono­Nanos­Now
    1. IO.mono­Nanos­Now
  237. monotone
    1. Lean.Order.monotone
  238. mp
    1. Eq.mp
  239. mp
    1. Iff.mp (structure field)
  240. mpr
    1. Eq.mpr
  241. mpr
    1. Iff.mpr (structure field)
  242. msb
    1. BitVec.msb
  243. mul
    1. BitVec.mul
  244. mul
    1. Fin.mul
  245. mul
    1. Float.mul
  246. mul
    1. Float32.mul
  247. mul
    1. ISize.mul
  248. mul
    1. Int.mul
  249. mul
    1. Int16.mul
  250. mul
    1. Int32.mul
  251. mul
    1. Int64.mul
  252. mul
    1. Int8.mul
  253. mul
    1. Mul.mul (class method)
  254. mul
    1. Nat.mul
  255. mul
    1. UInt16.mul
  256. mul
    1. UInt32.mul
  257. mul
    1. UInt64.mul
  258. mul
    1. UInt8.mul
  259. mul
    1. USize.mul
  260. mul­Rec
    1. BitVec.mul­Rec
  261. mul_assoc
    1. Lean.Grind.Semiring.add_assoc (class method)
  262. mul_comm
    1. [anonymous] (class method) (0) (1)
  263. mul_inv_cancel
    1. [anonymous] (class method)
  264. mul_lt_mul_of_pos_left
    1. Lean.Grind.OrderedRing.zero_lt_one (class method)
  265. mul_lt_mul_of_pos_right
    1. Lean.Grind.OrderedRing.mul_lt_mul_of_pos_left (class method)
  266. mul_one
    1. Lean.Grind.Semiring.add_comm (class method)
  267. mul_zero
    1. Lean.Grind.Semiring.left_distrib (class method)
  268. mvars
    1. pp.mvars

N

  1. Name­Lit
    1. Lean.Syntax.Name­Lit
  2. Nat
  3. Nat.add
  4. Nat.all
  5. Nat.all­M
  6. Nat.all­TR
  7. Nat.any
  8. Nat.any­M
  9. Nat.any­TR
  10. Nat.beq
  11. Nat.bitwise
  12. Nat.ble
  13. Nat.blt
  14. Nat.case­Strong­Rec­On
  15. Nat.cases­Aux­On
  16. Nat.cast
  17. Nat.dec­Eq
  18. Nat.dec­Le
  19. Nat.dec­Lt
  20. Nat.digit­Char
  21. Nat.div
  22. Nat.div.induction­On
  23. Nat.div2Induction
  24. Nat.fold
  25. Nat.fold­M
  26. Nat.fold­Rev
  27. Nat.fold­Rev­M
  28. Nat.fold­TR
  29. Nat.for­M
  30. Nat.for­Rev­M
  31. Nat.gcd
  32. Nat.is­Power­Of­Two
  33. Nat.is­Valid­Char
  34. Nat.land
  35. Nat.lcm
  36. Nat.le
  37. Nat.le.refl
    1. Constructor of Nat.le
  38. Nat.le.step
    1. Constructor of Nat.le
  39. Nat.log2
  40. Nat.lor
  41. Nat.lt
  42. Nat.max
  43. Nat.min
  44. Nat.mod
  45. Nat.mod.induction­On
  46. Nat.mod­Core
  47. Nat.mul
  48. Nat.next­Power­Of­Two
  49. Nat.pow
  50. Nat.pred
  51. Nat.rec­Aux
  52. Nat.repeat
  53. Nat.repeat­TR
  54. Nat.repr
  55. Nat.shift­Left
  56. Nat.shift­Right
  57. Nat.strong­Rec­On
  58. Nat.sub
  59. Nat.sub­Digit­Char
  60. Nat.succ
    1. Constructor of Nat
  61. Nat.super­Digit­Char
  62. Nat.test­Bit
  63. Nat.to­Digits
  64. Nat.to­Float
  65. Nat.to­Float32
  66. Nat.to­ISize
  67. Nat.to­Int16
  68. Nat.to­Int32
  69. Nat.to­Int64
  70. Nat.to­Int8
  71. Nat.to­Sub­Digits
  72. Nat.to­Subscript­String
  73. Nat.to­Super­Digits
  74. Nat.to­Superscript­String
  75. Nat.to­UInt16
  76. Nat.to­UInt32
  77. Nat.to­UInt64
  78. Nat.to­UInt8
  79. Nat.to­USize
  80. Nat.xor
  81. Nat.zero
    1. Constructor of Nat
  82. Nat­Cast
  83. NatCast.mk
    1. Instance constructor of Nat­Cast
  84. Nat­Module
    1. Lean.Grind.Nat­Module
  85. Nat­Pow
  86. NatPow.mk
    1. Instance constructor of Nat­Pow
  87. Ne­Zero
  88. NeZero.mk
    1. Instance constructor of Ne­Zero
  89. Neg
  90. Neg.mk
    1. Instance constructor of Neg
  91. New­Goals
    1. Lean.Meta.Rewrite.New­Goals
  92. No­Nat­Zero­Divisors
    1. Lean.Grind.No­Nat­Zero­Divisors
  93. Nodup
    1. List.Nodup
  94. Nonempty
  95. Nonempty.intro
    1. Constructor of Nonempty
  96. Not
  97. Not.elim
  98. Num­Lit
    1. Lean.Syntax.Num­Lit
  99. name
    1. Lean.LeanOption.name (structure field)
  100. name­Lit­Kind
    1. Lean.name­Lit­Kind
  101. namespace
    1. of inductive type
  102. nat­Abs
    1. Int.nat­Abs
  103. nat­Add
    1. Fin.nat­Add
  104. nat­Cast
    1. NatCast.nat­Cast (class method)
  105. nat­Cast
    1. [anonymous] (class method)
  106. native­Facets
    1. [anonymous] (structure field) (0) (1)
  107. native_decide
  108. ndrec
    1. HEq.ndrec
  109. ndrec­On
    1. HEq.ndrec­On
  110. needs
    1. [anonymous] (structure field) (0) (1)
  111. neg
    1. BitVec.neg
  112. neg
    1. Float.neg
  113. neg
    1. Float32.neg
  114. neg
    1. ISize.neg
  115. neg
    1. Int.neg
  116. neg
    1. Int16.neg
  117. neg
    1. Int32.neg
  118. neg
    1. Int64.neg
  119. neg
    1. Int8.neg
  120. neg
    1. Neg.neg (class method)
  121. neg
    1. UInt16.neg
  122. neg
    1. UInt32.neg
  123. neg
    1. UInt64.neg
  124. neg
    1. UInt8.neg
  125. neg
    1. USize.neg
  126. neg­Of­Nat
    1. Int.neg­Of­Nat
  127. neg_add_cancel
    1. Lean.Grind.IntModule.one_hmul (class method)
  128. neg_add_cancel
    1. [anonymous] (class method)
  129. nest­D
    1. Std.Format.nest­D
  130. neutral­Config
    1. Lean.Meta.Simp.neutral­Config
  131. new (Lake command)
  132. new
    1. IO.Promise.new
  133. new
    1. Std.Channel.new
  134. new
    1. Std.CloseableChannel.new
  135. new
    1. Std.Condvar.new
  136. new
    1. Std.Mutex.new
  137. new­Goals
    1. Lean.Meta.Rewrite.Config.new­Goals (structure field)
  138. next
  139. next ... => ...
  140. next'
    1. String.next'
  141. next
    1. RandomGen.next (class method)
  142. next
    1. String.Iterator.next
  143. next
    1. String.next
  144. next
    1. Substring.next
  145. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  146. next­Until
    1. String.next­Until
  147. next­While
    1. String.next­While
  148. nextn
    1. String.Iterator.nextn
  149. nextn
    1. Substring.nextn
  150. nil
    1. BitVec.nil
  151. no_nat_zero_divisors
    1. Lean.Grind.No­Nat­ZeroDivisors.no_nat_zero_divisors (class method)
  152. nofun
  153. nomatch
  154. non­Backtrackable
    1. EStateM.non­Backtrackable
  155. norm_cast (0) (1)
  156. normalize
    1. System.FilePath.normalize
  157. not
    1. BitVec.not
  158. not
    1. Bool.not
  159. not
    1. Int.not
  160. not­M
  161. notify­All
    1. Std.Condvar.notify­All
  162. notify­One
    1. Std.Condvar.notify­One
  163. null­Kind
    1. Lean.null­Kind
  164. num­Bits
    1. System.Platform.num­Bits
  165. num­Lit­Kind
    1. Lean.num­Lit­Kind

O

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

P

  1. PEmpty
  2. PEmpty.elim
  3. PLift
  4. PLift.up
    1. Constructor of PLift
  5. PProd
  6. PProd.mk
    1. Constructor of PProd
  7. PSigma
  8. PSigma.mk
    1. Constructor of PSigma
  9. PSum
  10. PSum.inhabited­Left
  11. PSum.inhabited­Right
  12. PSum.inl
    1. Constructor of PSum
  13. PSum.inr
    1. Constructor of PSum
  14. PUnit
  15. PUnit.unit
    1. Constructor of PUnit
  16. Pairwise
    1. List.Pairwise
  17. Partial­Order
    1. Lean.Grind.Partial­Order
  18. Partial­Order
    1. Lean.Order.Partial­Order
  19. Perm
    1. List.Perm
  20. Pos
    1. String.Pos
  21. Pow
  22. Pow.mk
    1. Instance constructor of Pow
  23. Prec
    1. Lean.Syntax.Prec
  24. Preorder
    1. Lean.Grind.Preorder
  25. Preresolved
    1. Lean.Syntax.Preresolved
  26. Prio
    1. Lean.Syntax.Prio
  27. Priority
    1. Task.Priority
  28. Prod
  29. Prod.all­I
  30. Prod.any­I
  31. Prod.fold­I
  32. Prod.lex­Lt
  33. Prod.map
  34. Prod.mk
    1. Constructor of Prod
  35. Prod.swap
  36. Promise
    1. IO.Promise
  37. Prop
  38. Pure
  39. Pure.mk
    1. Instance constructor of Pure
  40. pack (Lake command)
  41. parameter
    1. of inductive type
  42. paren
    1. Std.Format.paren
  43. parent
    1. System.FilePath.parent
  44. parser
  45. partition
    1. Array.partition
  46. partition
    1. List.partition
  47. partition
    1. Std.DHashMap.partition
  48. partition
    1. Std.DTreeMap.partition
  49. partition
    1. Std.HashMap.partition
  50. partition
    1. Std.HashSet.partition
  51. partition
    1. Std.TreeMap.partition
  52. partition
    1. Std.TreeSet.partition
  53. partition­M
    1. List.partition­M
  54. partition­Map
    1. List.partition­Map
  55. path
    1. IO.FS.DirEntry.path
  56. path­Exists
    1. System.FilePath.path­Exists
  57. path­Separator
    1. System.FilePath.path­Separator
  58. path­Separators
    1. System.FilePath.path­Separators
  59. pattern
  60. pbind
    1. Option.pbind
  61. pelim
    1. Option.pelim
  62. placeholder term
  63. pmap
    1. Array.pmap
  64. pmap
    1. List.pmap
  65. pmap
    1. Option.pmap
  66. polymorphism
    1. universe
  67. pop
    1. Array.pop
  68. pop­Front
    1. Subarray.pop­Front
  69. pop­While
    1. Array.pop­While
  70. pos
    1. IO.FS.Stream.Buffer.pos (structure field)
  71. pos
    1. String.Iterator.pos
  72. pos­Of
    1. String.pos­Of
  73. pos­Of
    1. Substring.pos­Of
  74. pow
    1. Float.pow
  75. pow
    1. Float32.pow
  76. pow
    1. HomogeneousPow.pow (class method)
  77. pow
    1. Int.pow
  78. pow
    1. Nat.pow
  79. pow
    1. NatPow.pow (class method)
  80. pow
    1. Pow.pow (class method)
  81. pow_succ
    1. Lean.Grind.Semiring.zero_mul (class method)
  82. pow_zero
    1. Lean.Grind.Semiring.right_distrib (class method)
  83. pp
    1. eval.pp
  84. pp.deep­Terms
  85. pp.deepTerms.threshold
  86. pp.field­Notation
  87. pp.match
  88. pp.max­Steps
  89. pp.mvars
  90. pp.proofs
  91. pp.proofs.threshold
  92. precompile­Modules
    1. [anonymous] (structure field)
  93. pred
    1. Fin.pred
  94. pred
    1. Nat.pred
  95. predicative
  96. prefix­Join
    1. Std.Format.prefix­Join
  97. pretty
    1. Std.Format.pretty
  98. pretty­M
    1. Std.Format.pretty­M
  99. prev
    1. String.Iterator.prev
  100. prev
    1. String.prev
  101. prev
    1. Substring.prev
  102. prevn
    1. String.Iterator.prevn
  103. prevn
    1. Substring.prevn
  104. print
    1. IO.print
  105. println
    1. IO.println
  106. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
  107. proj
    1. Lean.Meta.Simp.Config.proj (structure field)
  108. proof state
  109. proofs
    1. pp.proofs
  110. property
    1. Subtype.property (structure field)
  111. propext
  112. proposition
  113. proposition
    1. decidable
  114. ptr­Addr­Unsafe
  115. ptr­Eq
  116. ptr­Eq
    1. ST.Ref.ptr­Eq
  117. ptr­Eq­List
  118. pure
    1. EStateM.pure
  119. pure
    1. Except.pure
  120. pure
    1. ExceptT.pure
  121. pure
    1. OptionT.pure
  122. pure
    1. Pure.pure (class method)
  123. pure
    1. ReaderT.pure
  124. pure
    1. StateT.pure
  125. pure
    1. Task.pure
  126. pure
    1. Thunk.pure
  127. pure_bind
    1. [anonymous] (class method)
  128. pure_seq
    1. [anonymous] (class method)
  129. push
    1. Array.push
  130. push
    1. String.push
  131. push­Newline
    1. Std.Format.Monad­PrettyFormat.push­Newline (class method)
  132. push­Output
    1. Std.Format.Monad­PrettyFormat.push­Output (class method)
  133. push_cast
  134. pushn
    1. String.pushn
  135. put­Str
    1. IO.FS.Handle.put­Str
  136. put­Str
    1. IO.FS.Stream.put­Str (structure field)
  137. put­Str­Ln
    1. IO.FS.Handle.put­Str­Ln
  138. put­Str­Ln
    1. IO.FS.Stream.put­Str­Ln

Q

  1. Quot
  2. Quot.hrec­On
  3. Quot.ind
  4. Quot.lift
  5. Quot.lift­On
  6. Quot.mk
  7. Quot.rec
  8. Quot.rec­On
  9. Quot.rec­On­Subsingleton
  10. Quot.sound
  11. Quotient
  12. Quotient.exact
  13. Quotient.hrec­On
  14. Quotient.ind
  15. Quotient.lift
  16. Quotient.lift­On
  17. Quotient.lift­On₂
  18. Quotient.lift₂
  19. Quotient.mk
  20. Quotient.mk'
  21. Quotient.rec
  22. Quotient.rec­On
  23. Quotient.rec­On­Subsingleton
  24. Quotient.rec­On­Subsingleton₂
  25. Quotient.sound
  26. qsort
    1. Array.qsort
  27. qsort­Ord
    1. Array.qsort­Ord
  28. quantification
    1. impredicative
  29. quantification
    1. predicative
  30. query (Lake command)
  31. quote
    1. Char.quote
  32. quote
    1. String.quote

R

  1. Random­Gen
  2. RandomGen.mk
    1. Instance constructor of Random­Gen
  3. Raw
    1. Std.DHashMap.Raw
  4. Raw
    1. Std.DTreeMap.Raw
  5. Raw
    1. Std.HashMap.Raw
  6. Raw
    1. Std.HashSet.Raw
  7. Raw
    1. Std.TreeMap.Raw
  8. Raw
    1. Std.TreeSet.Raw
  9. Reader­M
  10. Reader­T
  11. ReaderT.adapt
  12. ReaderT.bind
  13. ReaderT.failure
  14. ReaderT.or­Else
  15. ReaderT.pure
  16. ReaderT.read
  17. ReaderT.run
  18. Ref
    1. IO.Ref
  19. Ref
    1. ST.Ref
  20. Repr
  21. Repr.add­App­Paren
  22. Repr.mk
    1. Instance constructor of Repr
  23. Repr­Atom
  24. ReprAtom.mk
    1. Instance constructor of Repr­Atom
  25. Result
    1. EStateM.Result
  26. Ring
    1. Lean.Grind.Ring
  27. r
    1. Setoid.r (class method)
  28. rand
    1. IO.rand
  29. rand­Bool
  30. rand­Nat
  31. range'
    1. Array.range'
  32. range'
    1. List.range'
  33. range'TR
    1. List.range'TR
  34. range
    1. Array.range
  35. range
    1. List.range
  36. range
    1. RandomGen.range (class method)
  37. raw
    1. Lean.TSyntax.raw (structure field)
  38. rcases
  39. read
    1. IO.AccessRight.read (structure field)
  40. read
    1. IO.FS.Handle.read
  41. read
    1. IO.FS.Stream.read (structure field)
  42. read
    1. MonadReader.read (class method)
  43. read
    1. Monad­ReaderOf.read (class method)
  44. read
    1. ReaderT.read
  45. read­Bin­File
    1. IO.FS.read­Bin­File
  46. read­Bin­To­End
    1. IO.FS.Handle.read­Bin­To­End
  47. read­Bin­To­End­Into
    1. IO.FS.Handle.read­Bin­To­End­Into
  48. read­Dir
    1. System.FilePath.read­Dir
  49. read­File
    1. IO.FS.read­File
  50. read­The
  51. read­To­End
    1. IO.FS.Handle.read­To­End
  52. real­Path
    1. IO.FS.real­Path
  53. rec
    1. Quot.rec
  54. rec
    1. Quotient.rec
  55. rec­Aux
    1. Nat.rec­Aux
  56. rec­On
    1. Quot.rec­On
  57. rec­On
    1. Quotient.rec­On
  58. rec­On­Subsingleton
    1. Quot.rec­On­Subsingleton
  59. rec­On­Subsingleton
    1. Quotient.rec­On­Subsingleton
  60. rec­On­Subsingleton₂
    1. Quotient.rec­On­Subsingleton₂
  61. recursor
  62. recv
    1. Std.Channel.recv
  63. reduce
  64. reduction
    1. ι (iota)
  65. refine
  66. refine'
  67. refl
    1. Equivalence.refl (structure field)
  68. refl
    1. Setoid.refl
  69. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  70. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  71. rel
    1. Lean.Order.PartialOrder.rel (class method)
  72. rel
    1. Well­FoundedRelation.rel (class method)
  73. rel_antisymm
    1. Lean.Order.PartialOrder.rel_antisymm (class method)
  74. rel_refl
    1. Lean.Order.PartialOrder.rel_refl (class method)
  75. rel_trans
    1. Lean.Order.PartialOrder.rel_trans (class method)
  76. relaxed­Auto­Implicit
  77. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  78. remaining­To­String
    1. String.Iterator.remaining­To­String
  79. remove­All
    1. List.remove­All
  80. remove­Dir
    1. IO.FS.remove­Dir
  81. remove­Dir­All
    1. IO.FS.remove­Dir­All
  82. remove­File
    1. IO.FS.remove­File
  83. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  84. rename
  85. rename
    1. IO.FS.rename
  86. rename_i
  87. repeat (0) (1)
  88. repeat'
  89. repeat
    1. Nat.repeat
  90. repeat1'
  91. repeat­TR
    1. Nat.repeat­TR
  92. replace
  93. replace
    1. Array.replace
  94. replace
    1. List.replace
  95. replace
    1. String.replace
  96. replace­TR
    1. List.replace­TR
  97. replicate
    1. Array.replicate
  98. replicate
    1. BitVec.replicate
  99. replicate
    1. List.replicate
  100. replicate­TR
    1. List.replicate­TR
  101. repr
  102. repr
    1. Int.repr
  103. repr
    1. Nat.repr
  104. repr
    1. Option.repr
  105. repr
    1. USize.repr
  106. repr
    1. eval.derive.repr
  107. repr­Arg
  108. repr­Prec
    1. Repr.repr­Prec (class method)
  109. repr­Str
  110. resolve
    1. IO.Promise.resolve
  111. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  112. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  113. restore
    1. EStateM.Backtrackable.restore (class method)
  114. restore­M
    1. MonadControl.restore­M (class method)
  115. restore­M
    1. Monad­ControlT.restore­M (class method)
  116. result!
    1. IO.Promise.result!
  117. result
    1. trace.compiler.ir.result
  118. result?
    1. IO.Promise.result?
  119. result­D
    1. IO.Promise.result­D
  120. rev
    1. Fin.rev
  121. rev­Find
    1. String.rev­Find
  122. rev­Pos­Of
    1. String.rev­Pos­Of
  123. reverse
    1. Array.reverse
  124. reverse
    1. BitVec.reverse
  125. reverse
    1. List.reverse
  126. reverse­Induction
    1. Fin.reverse­Induction
  127. revert
  128. rewind
    1. IO.FS.Handle.rewind
  129. rewrite (0) (1)
  130. rewrite
    1. trace.Meta.Tactic.simp.rewrite
  131. rfl (0) (1) (2)
  132. rfl'
  133. rfl
    1. HEq.rfl
  134. rhs
  135. right (0) (1)
  136. right
    1. And.right (structure field)
  137. right_distrib
    1. Lean.Grind.Semiring.mul_one (class method)
  138. rightpad
    1. Array.rightpad
  139. rightpad
    1. List.rightpad
  140. rintro
  141. root
    1. IO.FS.DirEntry.root (structure field)
  142. root
    1. [anonymous] (structure field)
  143. roots
    1. [anonymous] (structure field)
  144. rotate­Left
    1. BitVec.rotate­Left
  145. rotate­Left
    1. List.rotate­Left
  146. rotate­Right
    1. BitVec.rotate­Right
  147. rotate­Right
    1. List.rotate­Right
  148. rotate_left
  149. rotate_right
  150. round
    1. Float.round
  151. round
    1. Float32.round
  152. run (Elan command)
  153. run'
    1. EStateM.run'
  154. run'
    1. State­CpsT.run'
  155. run'
    1. State­RefT'.run'
  156. run'
    1. StateT.run'
  157. run
    1. EStateM.run
  158. run
    1. Except­CpsT.run
  159. run
    1. ExceptT.run
  160. run
    1. IO.Process.run
  161. run
    1. Id.run
  162. run
    1. OptionT.run
  163. run
    1. ReaderT.run
  164. run
    1. State­CpsT.run
  165. run
    1. State­RefT'.run
  166. run
    1. StateT.run
  167. run­Catch
    1. Except­CpsT.run­Catch
  168. run­EST
  169. run­K
    1. Except­CpsT.run­K
  170. run­K
    1. State­CpsT.run­K
  171. run­ST
  172. run_tac
  173. rw (0) (1)
  174. rw?
  175. rw_mod_cast
  176. rwa

S

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

T

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

U

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

V

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

W

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

X

  1. xor
    1. BitVec.xor
  2. xor
    1. Bool.xor
  3. xor
    1. Fin.xor
  4. xor
    1. ISize.xor
  5. xor
    1. Int16.xor
  6. xor
    1. Int32.xor
  7. xor
    1. Int64.xor
  8. xor
    1. Int8.xor
  9. xor
    1. Nat.xor
  10. xor
    1. UInt16.xor
  11. xor
    1. UInt32.xor
  12. xor
    1. UInt64.xor
  13. xor
    1. UInt8.xor
  14. xor
    1. USize.xor

Z

  1. Zero
  2. Zero.mk
    1. Instance constructor of Zero
  3. zero
    1. BitVec.zero
  4. zero
    1. Zero.zero (class method)
  5. zero­Extend
    1. BitVec.zero­Extend
  6. zero_hmul
    1. Lean.Grind.IntModule.hmul­Int (class method)
  7. zero_hmul
    1. Lean.Grind.NatModule.add_zero (class method)
  8. zero_lt_one
    1. [anonymous] (class method)
  9. zero_mul
    1. Lean.Grind.Semiring.one_mul (class method)
  10. zero_ne_one
    1. [anonymous] (class method)
  11. zeta
  12. zeta
    1. Lean.Meta.DSimp.Config.zeta (structure field)
  13. zeta
    1. Lean.Meta.Simp.Config.zeta (structure field)
  14. zeta­Delta
    1. Lean.Meta.DSimp.Config.zeta­Delta (structure field)
  15. zeta­Delta
    1. Lean.Meta.Simp.Config.zeta­Delta (structure field)
  16. zeta­Have
    1. Lean.Meta.DSimp.Config.zeta­Have (structure field)
  17. zeta­Have
    1. Lean.Meta.Simp.Config.zeta­Have (structure field)
  18. zeta­Unused
    1. Lean.Meta.DSimp.Config.zeta­Unused (structure field)
  19. zeta­Unused
    1. Lean.Meta.Simp.Config.zeta­Unused (structure field)
  20. zip
    1. Array.zip
  21. zip
    1. List.zip
  22. zip­Idx
    1. Array.zip­Idx
  23. zip­Idx
    1. List.zip­Idx
  24. zip­Idx­TR
    1. List.zip­Idx­TR
  25. zip­With
    1. Array.zip­With
  26. zip­With
    1. List.zip­With
  27. zip­With­All
    1. Array.zip­With­All
  28. zip­With­All
    1. List.zip­With­All
  29. zip­With­TR
    1. List.zip­With­TR