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. Assertion
    1. Std.Do.Assertion
  151. Atomic­T
    1. Std.Atomic­T
  152. abs
    1. BitVec.abs
  153. abs
    1. Float.abs
  154. abs
    1. Float32.abs
  155. abs
    1. ISize.abs
  156. abs
    1. Int16.abs
  157. abs
    1. Int32.abs
  158. abs
    1. Int64.abs
  159. abs
    1. Int8.abs
  160. absurd
  161. ac_nf
  162. ac_nf0
  163. ac_rfl
  164. accessed
    1. IO.FS.Metadata.accessed (structure field)
  165. acos
    1. Float.acos
  166. acos
    1. Float32.acos
  167. acosh
    1. Float.acosh
  168. acosh
    1. Float32.acosh
  169. adapt
    1. ExceptT.adapt
  170. adapt
    1. ReaderT.adapt
  171. adapt­Except
    1. EStateM.adapt­Except
  172. adc
    1. BitVec.adc
  173. adcb
    1. BitVec.adcb
  174. add
    1. Add.add (class method)
  175. add
    1. BitVec.add
  176. add
    1. Fin.add
  177. add
    1. Float.add
  178. add
    1. Float32.add
  179. add
    1. ISize.add
  180. add
    1. Int.add
  181. add
    1. Int16.add
  182. add
    1. Int32.add
  183. add
    1. Int64.add
  184. add
    1. Int8.add
  185. add
    1. Nat.add
  186. add
    1. UInt16.add
  187. add
    1. UInt32.add
  188. add
    1. UInt64.add
  189. add
    1. UInt8.add
  190. add
    1. USize.add
  191. add­App­Paren
    1. Repr.add­App­Paren
  192. add­Cases
    1. Fin.add­Cases
  193. add­Extension
    1. System.FilePath.add­Extension
  194. add­Heartbeats
    1. IO.add­Heartbeats
  195. add­Macro­Scope
    1. Lean.Macro.add­Macro­Scope
  196. add­Nat
    1. Fin.add­Nat
  197. add_assoc
    1. Lean.Grind.Semiring.add_zero (class method)
  198. add_comm
    1. Lean.Grind.Semiring.npow (class method)
  199. add_le_left_iff
    1. Lean.Grind.OrderedAdd.add_le_left_iff (class method)
  200. add_one_nsmul
    1. [anonymous] (class method)
  201. add_right_cancel
    1. Lean.Grind.Add­RightCancel.add_right_cancel (class method)
  202. add_zero
    1. Lean.Grind.Semiring.nsmul (class method)
  203. add_zsmul
    1. [anonymous] (class method)
  204. admit
  205. all
    1. Array.all
  206. all
    1. List.all
  207. all
    1. Nat.all
  208. all
    1. Option.all
  209. all
    1. Std.HashSet.all
  210. all
    1. Std.TreeMap.all
  211. all
    1. Std.TreeSet.all
  212. all
    1. String.all
  213. all
    1. Subarray.all
  214. all
    1. Substring.all
  215. all­Diff
    1. Array.all­Diff
  216. all­Eq
    1. Subsingleton.all­Eq (class method)
  217. all­I
    1. Prod.all­I
  218. all­M
    1. Array.all­M
  219. all­M
    1. List.all­M
  220. all­M
    1. Nat.all­M
  221. all­M
    1. Subarray.all­M
  222. all­Ones
    1. BitVec.all­Ones
  223. all­TR
    1. Nat.all­TR
  224. all_goals (0) (1)
  225. allow­Unsafe­Reducibility
  226. alter
    1. Std.DHashMap.alter
  227. alter
    1. Std.DTreeMap.alter
  228. alter
    1. Std.Ext­DHashMap.alter
  229. alter
    1. Std.Ext­HashMap.alter
  230. alter
    1. Std.HashMap.alter
  231. alter
    1. Std.TreeMap.alter
  232. and
    1. BitVec.and
  233. and
    1. Bool.and
  234. and
    1. List.and
  235. and
    1. Std.Do.Triple.and
  236. and­M
  237. and_intros
  238. any
    1. Array.any
  239. any
    1. List.any
  240. any
    1. Nat.any
  241. any
    1. Option.any
  242. any
    1. Std.HashSet.any
  243. any
    1. Std.TreeMap.any
  244. any
    1. Std.TreeSet.any
  245. any
    1. String.any
  246. any
    1. Subarray.any
  247. any
    1. Substring.any
  248. any­I
    1. Prod.any­I
  249. any­M
    1. Array.any­M
  250. any­M
    1. List.any­M
  251. any­M
    1. Nat.any­M
  252. any­M
    1. Subarray.any­M
  253. any­TR
    1. Nat.any­TR
  254. any_goals (0) (1)
  255. app­Dir
    1. IO.app­Dir
  256. app­Path
    1. IO.app­Path
  257. append
    1. Append.append (class method)
  258. append
    1. Array.append
  259. append
    1. BitVec.append
  260. append
    1. List.append
  261. append
    1. String.append
  262. append­List
    1. Array.append­List
  263. append­TR
    1. List.append­TR
  264. apply (0) (1)
  265. apply
    1. Std.Do.PredTrans.apply (structure field)
  266. apply?
  267. apply_assumption
  268. apply_ext_theorem
  269. apply_mod_cast
  270. apply_rfl
  271. apply_rules
  272. arg [@]i
  273. args
  274. args
    1. [anonymous] (structure field)
  275. arith
    1. Lean.Meta.Simp.Config.arith (structure field)
  276. as­String
    1. List.as­String
  277. as­Task
    1. BaseIO.as­Task
  278. as­Task
    1. EIO.as­Task
  279. as­Task
    1. IO.as­Task
  280. as_aux_lemma
  281. asin
    1. Float.asin
  282. asin
    1. Float32.asin
  283. asinh
    1. Float.asinh
  284. asinh
    1. Float32.asinh
  285. assumption
  286. assumption
    1. inaccessible
  287. assumption_mod_cast
  288. at­End
    1. String.Iterator.at­End
  289. at­End
    1. String.at­End
  290. at­End
    1. Substring.at­End
  291. at­Idx!
    1. Std.TreeSet.at­Idx!
  292. at­Idx
    1. Std.TreeSet.at­Idx
  293. at­Idx?
    1. Std.TreeSet.at­Idx?
  294. at­Idx­D
    1. Std.TreeSet.at­Idx­D
  295. atan
    1. Float.atan
  296. atan
    1. Float32.atan
  297. atan2
    1. Float.atan2
  298. atan2
    1. Float32.atan2
  299. atanh
    1. Float.atanh
  300. atanh
    1. Float32.atanh
  301. atomically
    1. Std.Mutex.atomically
  302. atomically­Once
    1. Std.Mutex.atomically­Once
  303. attach
    1. Array.attach
  304. attach
    1. List.attach
  305. attach
    1. Option.attach
  306. attach­With
    1. Array.attach­With
  307. attach­With
    1. List.attach­With
  308. attach­With
    1. Option.attach­With
  309. auto­Implicit
  310. auto­Lift
  311. auto­Param
  312. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  313. auto­Unfold
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
  314. auto­Unfold
    1. Lean.Meta.Simp.Config.auto­Unfold (structure field)

B

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

C

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

F

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

G

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

H

  1. HAdd
  2. HAdd.mk
    1. Instance constructor of HAdd
  3. HAnd
  4. HAnd.mk
    1. Instance constructor of HAnd
  5. HAppend
  6. HAppend.mk
    1. Instance constructor of HAppend
  7. HDiv
  8. HDiv.mk
    1. Instance constructor of HDiv
  9. HEq
  10. HEq.elim
  11. HEq.ndrec
  12. HEq.ndrec­On
  13. HEq.refl
    1. Constructor of HEq
  14. HEq.rfl
  15. HEq.subst
  16. HMod
  17. HMod.mk
    1. Instance constructor of HMod
  18. HMul
  19. HMul.mk
    1. Instance constructor of HMul
  20. HOr
  21. HOr.mk
    1. Instance constructor of HOr
  22. HPow
  23. HPow.mk
    1. Instance constructor of HPow
  24. HShift­Left
  25. HShiftLeft.mk
    1. Instance constructor of HShift­Left
  26. HShift­Right
  27. HShiftRight.mk
    1. Instance constructor of HShift­Right
  28. HSub
  29. HSub.mk
    1. Instance constructor of HSub
  30. HXor
  31. HXor.mk
    1. Instance constructor of HXor
  32. Handle
    1. IO.FS.Handle
  33. Has­Equiv
  34. HasEquiv.mk
    1. Instance constructor of Has­Equiv
  35. Hash­Map
    1. Std.Hash­Map
  36. Hash­Set
    1. Std.Hash­Set
  37. Hashable
  38. Hashable.mk
    1. Instance constructor of Hashable
  39. Homogeneous­Pow
  40. HomogeneousPow.mk
    1. Instance constructor of Homogeneous­Pow
  41. Hygiene­Info
    1. Lean.Syntax.Hygiene­Info
  42. h­Add
    1. HAdd.h­Add (class method)
  43. h­And
    1. HAnd.h­And (class method)
  44. h­Append
    1. HAppend.h­Append (class method)
  45. h­Div
    1. HDiv.h­Div (class method)
  46. h­Iterate
    1. Fin.h­Iterate
  47. h­Iterate­From
    1. Fin.h­Iterate­From
  48. h­Mod
    1. HMod.h­Mod (class method)
  49. h­Mul
    1. HMul.h­Mul (class method)
  50. h­Or
    1. HOr.h­Or (class method)
  51. h­Pow
    1. HPow.h­Pow (class method)
  52. h­Shift­Left
    1. HShiftLeft.h­Shift­Left (class method)
  53. h­Shift­Right
    1. HShiftRight.h­Shift­Right (class method)
  54. h­Sub
    1. HSub.h­Sub (class method)
  55. h­Xor
    1. HXor.h­Xor (class method)
  56. has­Decl
    1. Lean.Macro.has­Decl
  57. has­Finished
    1. IO.has­Finished
  58. has­Next
    1. String.Iterator.has­Next
  59. has­Prev
    1. String.Iterator.has­Prev
  60. hash
    1. BitVec.hash
  61. hash
    1. Hashable.hash (class method)
  62. hash
    1. String.hash
  63. hash_eq
  64. hash_eq
    1. LawfulHashable.hash_eq (class method)
  65. have (0) (1)
  66. have'
  67. head!
    1. List.head!
  68. head
    1. List.head
  69. head?
    1. List.head?
  70. head­D
    1. List.head­D
  71. helim
    1. Subsingleton.helim
  72. heq_of_eq
  73. heq_of_eq­Rec_eq
  74. heq_of_heq_of_eq
  75. hrec­On
    1. Quot.hrec­On
  76. hrec­On
    1. Quotient.hrec­On
  77. hygiene
    1. in tactics
  78. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  79. hygienic
    1. tactic.hygienic

I

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

J

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

K

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

L

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

M

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

N

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

O

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

P

  1. PEmpty
  2. PEmpty.elim
  3. PLift
  4. PLift.up
    1. Constructor of PLift
  5. PProd
  6. PProd.mk
    1. Constructor of PProd
  7. PSigma
  8. PSigma.mk
    1. Constructor of PSigma
  9. PSum
  10. PSum.inhabited­Left
  11. PSum.inhabited­Right
  12. PSum.inl
    1. Constructor of PSum
  13. PSum.inr
    1. Constructor of PSum
  14. PUnit
  15. PUnit.unit
    1. Constructor of PUnit
  16. Pairwise
    1. List.Pairwise
  17. Partial­Order
    1. Lean.Order.Partial­Order
  18. Perm
    1. List.Perm
  19. Pos
    1. String.Pos
  20. Post­Cond
    1. Std.Do.Post­Cond
  21. Pow
  22. Pow.mk
    1. Instance constructor of Pow
  23. Prec
    1. Lean.Syntax.Prec
  24. Pred­Trans
    1. Std.Do.Pred­Trans
  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.mul_zero (class method)
  82. pow_zero
    1. Lean.Grind.Semiring.zero_mul (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.one_mul (class method)
  138. rightpad
    1. Array.rightpad
  139. rightpad
    1. List.rightpad
  140. rintro
  141. root
    1. IO.FS.DirEntry.root (structure field)
  142. root
    1. [anonymous] (structure field)
  143. roots
    1. [anonymous] (structure field)
  144. rotate­Left
    1. BitVec.rotate­Left
  145. rotate­Left
    1. List.rotate­Left
  146. rotate­Right
    1. BitVec.rotate­Right
  147. rotate­Right
    1. List.rotate­Right
  148. rotate_left
  149. rotate_right
  150. round
    1. Float.round
  151. round
    1. Float32.round
  152. run (Elan command)
  153. run'
    1. EStateM.run'
  154. run'
    1. State­CpsT.run'
  155. run'
    1. State­RefT'.run'
  156. run'
    1. StateT.run'
  157. run
    1. EStateM.run
  158. run
    1. Except­CpsT.run
  159. run
    1. ExceptT.run
  160. run
    1. IO.Process.run
  161. run
    1. Id.run
  162. run
    1. OptionT.run
  163. run
    1. ReaderT.run
  164. run
    1. State­CpsT.run
  165. run
    1. State­RefT'.run
  166. run
    1. StateT.run
  167. run­Catch
    1. Except­CpsT.run­Catch
  168. run­EST
  169. run­K
    1. Except­CpsT.run­K
  170. run­K
    1. State­CpsT.run­K
  171. run­ST
  172. run_tac
  173. rw (0) (1)
  174. rw?
  175. rw_mod_cast
  176. rwa

S

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

T

  1. TSep­Array
    1. Lean.Syntax.TSep­Array
  2. TSyntax
    1. Lean.TSyntax
  3. TSyntax­Array
    1. Lean.TSyntax­Array
  4. Tactic
    1. Lean.Syntax.Tactic
  5. Task
  6. Task.Priority
  7. Task.Priority.dedicated
  8. Task.Priority.default
  9. Task.Priority.max
  10. Task.bind
  11. Task.get
  12. Task.map
  13. Task.map­List
  14. Task.pure
  15. Task.spawn
  16. Task­State
    1. IO.Task­State
  17. Term
    1. Lean.Syntax.Term
  18. Thunk
  19. Thunk.bind
  20. Thunk.get
  21. Thunk.map
  22. Thunk.mk
    1. Constructor of Thunk
  23. Thunk.pure
  24. To­Format
    1. Std.To­Format
  25. To­Int
    1. Lean.Grind.To­Int
  26. Trans
  27. Trans.mk
    1. Instance constructor of Trans
  28. Transparency­Mode
    1. Lean.Meta.Transparency­Mode
  29. Tree­Map
    1. Std.Tree­Map
  30. Tree­Set
    1. Std.Tree­Set
  31. Triple
    1. Std.Do.Triple
  32. True
  33. True.intro
    1. Constructor of True
  34. Type
  35. tactic
  36. tactic'
  37. tactic.custom­Eliminators
  38. tactic.hygienic
  39. tactic.simp.trace (0) (1)
  40. tactic.skip­Assigned­Instances
  41. tail!
    1. List.tail!
  42. tail
    1. List.tail
  43. tail?
    1. List.tail?
  44. tail­D
    1. List.tail­D
  45. take
    1. Array.take
  46. take
    1. List.take
  47. take
    1. ST.Ref.take
  48. take
    1. String.take
  49. take
    1. Subarray.take
  50. take
    1. Substring.take
  51. take­Right
    1. String.take­Right
  52. take­Right
    1. Substring.take­Right
  53. take­Right­While
    1. String.take­Right­While
  54. take­Right­While
    1. Substring.take­Right­While
  55. take­Stdin
    1. IO.Process.Child.take­Stdin
  56. take­TR
    1. List.take­TR
  57. take­While
    1. Array.take­While
  58. take­While
    1. List.take­While
  59. take­While
    1. String.take­While
  60. take­While
    1. Substring.take­While
  61. take­While­TR
    1. List.take­While­TR
  62. tan
    1. Float.tan
  63. tan
    1. Float32.tan
  64. tanh
    1. Float.tanh
  65. tanh
    1. Float32.tanh
  66. target
    1. System.Platform.target
  67. tdiv
    1. Int.tdiv
  68. term
    1. placeholder
  69. test (Lake command)
  70. test­Bit
    1. Nat.test­Bit
  71. then
    1. Ordering.then
  72. threshold
    1. pp.deepTerms.threshold
  73. threshold
    1. pp.proofs.threshold
  74. throw
    1. EStateM.throw
  75. throw
    1. MonadExcept.throw (class method)
  76. throw
    1. Monad­ExceptOf.throw (class method)
  77. throw­Error
    1. Lean.Macro.throw­Error
  78. throw­Error­At
    1. Lean.Macro.throw­Error­At
  79. throw­The
  80. throw­Unsupported
    1. Lean.Macro.throw­Unsupported
  81. tmod
    1. Int.tmod
  82. to­Add
    1. Lean.Grind.Semiring.to­Add (class method)
  83. to­Add­Comm­Group
    1. Lean.Grind.IntModule.to­Add­Comm­Group (class method)
  84. to­Add­Comm­Monoid
    1. Lean.Grind.NatModule.to­Add­Comm­Monoid (class method)
  85. to­Applicative
    1. Alternative.to­Applicative (class method)
  86. to­Applicative
    1. Monad.to­Applicative (class method)
  87. to­Array
    1. List.to­Array
  88. to­Array
    1. Option.to­Array
  89. to­Array
    1. Std.DHashMap.to­Array
  90. to­Array
    1. Std.DTreeMap.to­Array
  91. to­Array
    1. Std.HashMap.to­Array
  92. to­Array
    1. Std.HashSet.to­Array
  93. to­Array
    1. Std.TreeMap.to­Array
  94. to­Array
    1. Std.TreeSet.to­Array
  95. to­Array
    1. Subarray.to­Array
  96. to­Array­Impl
    1. List.to­Array­Impl
  97. to­BEq
    1. Ord.to­BEq
  98. to­Base­IO
    1. EIO.to­Base­IO
  99. to­Bind
    1. [anonymous] (class method)
  100. to­Bit­Vec
    1. ISize.to­Bit­Vec
  101. to­Bit­Vec
    1. Int16.to­Bit­Vec
  102. to­Bit­Vec
    1. Int32.to­Bit­Vec
  103. to­Bit­Vec
    1. Int64.to­Bit­Vec
  104. to­Bit­Vec
    1. Int8.to­Bit­Vec
  105. to­Bit­Vec
    1. UInt16.to­Bit­Vec (structure field)
  106. to­Bit­Vec
    1. UInt32.to­Bit­Vec (structure field)
  107. to­Bit­Vec
    1. UInt64.to­Bit­Vec (structure field)
  108. to­Bit­Vec
    1. UInt8.to­Bit­Vec (structure field)
  109. to­Bit­Vec
    1. USize.to­Bit­Vec (structure field)
  110. to­Bits
    1. Float.to­Bits
  111. to­Bits
    1. Float32.to­Bits
  112. to­Bool
    1. Except.to­Bool
  113. to­Byte­Array
    1. List.to­Byte­Array
  114. to­Comm­Ring
    1. Lean.Grind.Field.to­Comm­Ring (class method)
  115. to­Digits
    1. Nat.to­Digits
  116. to­Div
    1. [anonymous] (class method)
  117. to­EIO
    1. BaseIO.to­EIO
  118. to­EIO
    1. IO.to­EIO
  119. to­End
    1. String.Iterator.to­End
  120. to­Fin
    1. BitVec.to­Fin (structure field)
  121. to­Fin
    1. UInt16.to­Fin
  122. to­Fin
    1. UInt32.to­Fin
  123. to­Fin
    1. UInt64.to­Fin
  124. to­Fin
    1. UInt8.to­Fin
  125. to­Fin
    1. USize.to­Fin
  126. to­Float
    1. Float32.to­Float
  127. to­Float
    1. ISize.to­Float
  128. to­Float
    1. Int16.to­Float
  129. to­Float
    1. Int32.to­Float
  130. to­Float
    1. Int64.to­Float
  131. to­Float
    1. Int8.to­Float
  132. to­Float
    1. Nat.to­Float
  133. to­Float
    1. UInt16.to­Float
  134. to­Float
    1. UInt32.to­Float
  135. to­Float
    1. UInt64.to­Float
  136. to­Float
    1. UInt8.to­Float
  137. to­Float
    1. USize.to­Float
  138. to­Float32
    1. Float.to­Float32
  139. to­Float32
    1. ISize.to­Float32
  140. to­Float32
    1. Int16.to­Float32
  141. to­Float32
    1. Int32.to­Float32
  142. to­Float32
    1. Int64.to­Float32
  143. to­Float32
    1. Int8.to­Float32
  144. to­Float32
    1. Nat.to­Float32
  145. to­Float32
    1. UInt16.to­Float32
  146. to­Float32
    1. UInt32.to­Float32
  147. to­Float32
    1. UInt64.to­Float32
  148. to­Float32
    1. UInt8.to­Float32
  149. to­Float32
    1. USize.to­Float32
  150. to­Float­Array
    1. List.to­Float­Array
  151. to­Format
    1. String.to­Format
  152. to­Functor
    1. Applicative.to­Functor (class method)
  153. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  154. to­Handle­Type
    1. IO.Process.Stdio.to­Handle­Type
  155. to­Hex
    1. BitVec.to­Hex
  156. to­IO'
    1. EIO.to­IO'
  157. to­IO
    1. BaseIO.to­IO
  158. to­IO
    1. EIO.to­IO
  159. to­ISize
    1. Bool.to­ISize
  160. to­ISize
    1. Float.to­ISize
  161. to­ISize
    1. Float32.to­ISize
  162. to­ISize
    1. Int.to­ISize
  163. to­ISize
    1. Int16.to­ISize
  164. to­ISize
    1. Int32.to­ISize
  165. to­ISize
    1. Int64.to­ISize
  166. to­ISize
    1. Int8.to­ISize
  167. to­ISize
    1. Nat.to­ISize
  168. to­ISize
    1. USize.to­ISize
  169. to­Int!
    1. String.to­Int!
  170. to­Int
    1. BitVec.to­Int
  171. to­Int
    1. Bool.to­Int
  172. to­Int
    1. ISize.to­Int
  173. to­Int
    1. Int16.to­Int
  174. to­Int
    1. Int32.to­Int
  175. to­Int
    1. Int64.to­Int
  176. to­Int
    1. Int8.to­Int
  177. to­Int
    1. Lean.Grind.ToInt.to­Int (class method)
  178. to­Int16
    1. Bool.to­Int16
  179. to­Int16
    1. Float.to­Int16
  180. to­Int16
    1. Float32.to­Int16
  181. to­Int16
    1. ISize.to­Int16
  182. to­Int16
    1. Int.to­Int16
  183. to­Int16
    1. Int32.to­Int16
  184. to­Int16
    1. Int64.to­Int16
  185. to­Int16
    1. Int8.to­Int16
  186. to­Int16
    1. Nat.to­Int16
  187. to­Int16
    1. UInt16.to­Int16
  188. to­Int32
    1. Bool.to­Int32
  189. to­Int32
    1. Float.to­Int32
  190. to­Int32
    1. Float32.to­Int32
  191. to­Int32
    1. ISize.to­Int32
  192. to­Int32
    1. Int.to­Int32
  193. to­Int32
    1. Int16.to­Int32
  194. to­Int32
    1. Int64.to­Int32
  195. to­Int32
    1. Int8.to­Int32
  196. to­Int32
    1. Nat.to­Int32
  197. to­Int32
    1. UInt32.to­Int32
  198. to­Int64
    1. Bool.to­Int64
  199. to­Int64
    1. Float.to­Int64
  200. to­Int64
    1. Float32.to­Int64
  201. to­Int64
    1. ISize.to­Int64
  202. to­Int64
    1. Int.to­Int64
  203. to­Int64
    1. Int16.to­Int64
  204. to­Int64
    1. Int32.to­Int64
  205. to­Int64
    1. Int8.to­Int64
  206. to­Int64
    1. Nat.to­Int64
  207. to­Int64
    1. UInt64.to­Int64
  208. to­Int8
    1. Bool.to­Int8
  209. to­Int8
    1. Float.to­Int8
  210. to­Int8
    1. Float32.to­Int8
  211. to­Int8
    1. ISize.to­Int8
  212. to­Int8
    1. Int.to­Int8
  213. to­Int8
    1. Int16.to­Int8
  214. to­Int8
    1. Int32.to­Int8
  215. to­Int8
    1. Int64.to­Int8
  216. to­Int8
    1. Nat.to­Int8
  217. to­Int8
    1. UInt8.to­Int8
  218. to­Int?
    1. String.to­Int?
  219. to­Int_inj
    1. Lean.Grind.ToInt.to­Int_inj (class method)
  220. to­Int_mem
    1. Lean.Grind.ToInt.to­Int_mem (class method)
  221. to­Inv
    1. [anonymous] (class method)
  222. to­Iterator
    1. Substring.to­Iterator
  223. to­LE
    1. Ord.to­LE
  224. to­LT
    1. Ord.to­LT
  225. to­Lawful­Applicative
    1. LawfulMonad.to­Lawful­Applicative (class method)
  226. to­Lawful­Functor
    1. LawfulApplicative.to­Lawful­Functor (class method)
  227. to­Lawful­Monad
    1. Std.Do.WPMonad.to­Lawful­Monad (class method)
  228. to­Lean­Config
    1. Lake.Lean­ExeConfig.to­Lean­Config (structure field)
  229. to­Lean­Config
    1. Lake.Lean­LibConfig.to­Lean­Config (structure field)
  230. to­List
    1. Array.to­List
  231. to­List
    1. Array.to­List (structure field)
  232. to­List
    1. Option.to­List
  233. to­List
    1. Std.DHashMap.to­List
  234. to­List
    1. Std.DTreeMap.to­List
  235. to­List
    1. Std.HashMap.to­List
  236. to­List
    1. Std.HashSet.to­List
  237. to­List
    1. Std.TreeMap.to­List
  238. to­List
    1. Std.TreeSet.to­List
  239. to­List
    1. String.to­List
  240. to­List­Append
    1. Array.to­List­Append
  241. to­List­Rev
    1. Array.to­List­Rev
  242. to­Lower
    1. Char.to­Lower
  243. to­Lower
    1. String.to­Lower
  244. to­Monad­State­Of
    1. ST.Ref.to­Monad­State­Of
  245. to­Mul
    1. [anonymous] (class method)
  246. to­Name
    1. String.to­Name
  247. to­Name
    1. Substring.to­Name
  248. to­Nat!
    1. String.to­Nat!
  249. to­Nat
    1. BitVec.to­Nat
  250. to­Nat
    1. Bool.to­Nat
  251. to­Nat
    1. Char.to­Nat
  252. to­Nat
    1. Fin.to­Nat
  253. to­Nat
    1. Int.to­Nat
  254. to­Nat
    1. UInt16.to­Nat
  255. to­Nat
    1. UInt32.to­Nat
  256. to­Nat
    1. UInt64.to­Nat
  257. to­Nat
    1. UInt8.to­Nat
  258. to­Nat
    1. USize.to­Nat
  259. to­Nat?
    1. Int.to­Nat?
  260. to­Nat?
    1. String.to­Nat?
  261. to­Nat?
    1. Substring.to­Nat?
  262. to­Nat­Clamp­Neg
    1. ISize.to­Nat­Clamp­Neg
  263. to­Nat­Clamp­Neg
    1. Int16.to­Nat­Clamp­Neg
  264. to­Nat­Clamp­Neg
    1. Int32.to­Nat­Clamp­Neg
  265. to­Nat­Clamp­Neg
    1. Int64.to­Nat­Clamp­Neg
  266. to­Nat­Clamp­Neg
    1. Int8.to­Nat­Clamp­Neg
  267. to­Neg
    1. [anonymous] (class method)
  268. to­Option
    1. Except.to­Option
  269. to­Ordered­Add
    1. Lean.Grind.OrderedRing.to­Ordered­Add (class method)
  270. to­Partial­Equiv­BEq
    1. EquivBEq.to­Partial­Equiv­BEq (class method)
  271. to­Partial­Order
    1. Lean.Order.CCPO.to­Partial­Order (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)
  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­WP
    1. [anonymous] (class method)
  348. toolchain gc (Elan command)
  349. toolchain install (Elan command)
  350. toolchain link (Elan command)
  351. toolchain list (Elan command)
  352. toolchain uninstall (Elan command)
  353. trace
  354. trace
    1. Lean.Macro.trace
  355. trace
    1. tactic.simp.trace (0) (1)
  356. trace.Elab.definition.wf
  357. trace.Meta.Tactic.simp.discharge
  358. trace.Meta.Tactic.simp.rewrite
  359. trace.compiler.ir.result
  360. trace.grind.ematch.instance
  361. trace.grind.split
  362. trace_state (0) (1)
  363. trans
    1. Eq.trans
  364. trans
    1. Equivalence.trans (structure field)
  365. trans
    1. Setoid.trans
  366. trans
    1. Trans.trans (class method)
  367. translate-config (Lake command)
  368. transparency
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  369. trim
    1. String.trim
  370. trim
    1. Substring.trim
  371. trim­Left
    1. String.trim­Left
  372. trim­Left
    1. Substring.trim­Left
  373. trim­Right
    1. String.trim­Right
  374. trim­Right
    1. Substring.trim­Right
  375. trivial
  376. truncate
    1. BitVec.truncate
  377. truncate
    1. IO.FS.Handle.truncate
  378. try (0) (1)
  379. try­Catch
    1. EStateM.try­Catch
  380. try­Catch
    1. Except.try­Catch
  381. try­Catch
    1. ExceptT.try­Catch
  382. try­Catch
    1. MonadExcept.try­Catch (class method)
  383. try­Catch
    1. Monad­ExceptOf.try­Catch (class method)
  384. try­Catch
    1. Option.try­Catch
  385. try­Catch
    1. OptionT.try­Catch
  386. try­Catch­The
  387. try­Finally'
    1. MonadFinally.try­Finally' (class method)
  388. try­Lock
    1. IO.FS.Handle.try­Lock
  389. try­Wait
    1. IO.Process.Child.try­Wait
  390. two­Pow
    1. BitVec.two­Pow
  391. type constructor
  392. type
    1. IO.FS.Metadata.type (structure field)
  393. type
    1. eval.type
  394. 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. WP
    1. Std.Do.WP
  8. WPMonad
    1. Std.Do.WPMonad
  9. Well­Founded
  10. WellFounded.fix
  11. WellFounded.intro
    1. Constructor of Well­Founded
  12. Well­Founded­Relation
  13. Well­FoundedRelation.mk
    1. Instance constructor of Well­Founded­Relation
  14. wait
    1. IO.Process.Child.wait
  15. wait
    1. IO.wait
  16. wait
    1. Std.Condvar.wait
  17. wait­Any
    1. IO.wait­Any
  18. wait­Until
    1. Std.Condvar.wait­Until
  19. walk­Dir
    1. System.FilePath.walk­Dir
  20. warn­Exponents
    1. Lean.Meta.Simp.Config.warn­Exponents (structure field)
  21. wf
    1. Well­FoundedRelation.wf (class method)
  22. wf
    1. trace.Elab.definition.wf
  23. wf­Param
  24. which (Elan command)
  25. whnf
  26. with­Extension
    1. System.FilePath.with­Extension
  27. with­File
    1. IO.FS.with­File
  28. with­File­Name
    1. System.FilePath.with­File­Name
  29. with­Fresh­Macro­Scope
    1. Lean.Macro.with­Fresh­Macro­Scope
  30. with­Isolated­Streams
    1. IO.FS.with­Isolated­Streams
  31. with­Position
  32. with­Position­After­Linebreak
  33. with­Reader
    1. Monad­WithReader.with­Reader (class method)
  34. with­Reader
    1. Monad­With­ReaderOf.with­Reader (class method)
  35. with­Stderr
    1. IO.with­Stderr
  36. with­Stdin
    1. IO.with­Stdin
  37. with­Stdout
    1. IO.with­Stdout
  38. with­Temp­Dir
    1. IO.FS.with­Temp­Dir
  39. with­Temp­File
    1. IO.FS.with­Temp­File
  40. with­The­Reader
  41. with_reducible (0) (1)
  42. with_reducible_and_instances (0) (1)
  43. with_unfolding_all (0) (1)
  44. without­Position
  45. wp
    1. Std.Do.WP.wp (class method)
  46. wp_bind
    1. [anonymous] (class method)
  47. wp_pure
    1. [anonymous] (class method)
  48. write
    1. IO.AccessRight.write (structure field)
  49. write
    1. IO.FS.Handle.write
  50. write
    1. IO.FS.Stream.write (structure field)
  51. write­Bin­File
    1. IO.FS.write­Bin­File
  52. write­File
    1. IO.FS.write­File

X

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

Z

  1. Zero
  2. Zero.mk
    1. Instance constructor of Zero
  3. zero
    1. BitVec.zero
  4. zero
    1. Zero.zero (class method)
  5. zero­Extend
    1. BitVec.zero­Extend
  6. zero_lt_one
    1. [anonymous] (class method)
  7. zero_mul
    1. Lean.Grind.Semiring.left_distrib (class method)
  8. zero_ne_one
    1. [anonymous] (class method)
  9. zero_nsmul
    1. [anonymous] (class method)
  10. zero_zsmul
    1. [anonymous] (class method)
  11. zeta
  12. zeta
    1. Lean.Meta.DSimp.Config.zeta (structure field)
  13. zeta
    1. Lean.Meta.Simp.Config.zeta (structure field)
  14. zeta­Delta
    1. Lean.Meta.DSimp.Config.zeta­Delta (structure field)
  15. zeta­Delta
    1. Lean.Meta.Simp.Config.zeta­Delta (structure field)
  16. zeta­Have
    1. Lean.Meta.DSimp.Config.zeta­Have (structure field)
  17. zeta­Have
    1. Lean.Meta.Simp.Config.zeta­Have (structure field)
  18. zeta­Unused
    1. Lean.Meta.DSimp.Config.zeta­Unused (structure field)
  19. zeta­Unused
    1. Lean.Meta.Simp.Config.zeta­Unused (structure field)
  20. zip
    1. Array.zip
  21. zip
    1. List.zip
  22. zip­Idx
    1. Array.zip­Idx
  23. zip­Idx
    1. List.zip­Idx
  24. zip­Idx­TR
    1. List.zip­Idx­TR
  25. zip­With
    1. Array.zip­With
  26. zip­With
    1. List.zip­With
  27. zip­With­All
    1. Array.zip­With­All
  28. zip­With­All
    1. List.zip­With­All
  29. zip­With­TR
    1. List.zip­With­TR
  30. zpow
    1. [anonymous] (class method)
  31. zpow_neg
    1. [anonymous] (class method)
  32. zpow_succ
    1. [anonymous] (class method)
  33. zpow_zero
    1. [anonymous] (class method)
  34. zsmul
    1. [anonymous] (class method) (0) (1)
  35. zsmul_nat­Cast_eq_nsmul
    1. [anonymous] (class method) (0) (1)