The Lean Language Reference

Index

Symbols

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

A

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

B

  1. BEq
  2. BEq.mk
    1. Instance constructor of BEq
  3. Backend
    1. Lake.Backend
  4. Backtrackable
    1. EStateM.Backtrackable
  5. Base­IO
  6. BaseIO.as­Task
  7. BaseIO.bind­Task
  8. BaseIO.chain­Task
  9. BaseIO.map­Task
  10. BaseIO.map­Tasks
  11. BaseIO.to­EIO
  12. BaseIO.to­IO
  13. Bind
  14. Bind.bind­Left
  15. Bind.kleisli­Left
  16. Bind.kleisli­Right
  17. Bind.mk
    1. Instance constructor of Bind
  18. Bit­Vec
  19. BitVec.abs
  20. BitVec.adc
  21. BitVec.adcb
  22. BitVec.add
  23. BitVec.all­Ones
  24. BitVec.and
  25. BitVec.append
  26. BitVec.carry
  27. BitVec.cast
  28. BitVec.concat
  29. BitVec.cons
  30. BitVec.dec­Eq
  31. BitVec.div­Rec
  32. BitVec.div­Subtract­Shift
  33. BitVec.extract­Lsb
  34. BitVec.extract­Lsb'
  35. BitVec.fill
  36. BitVec.get­Lsb'
  37. BitVec.get­Lsb?
  38. BitVec.get­Lsb­D
  39. BitVec.get­Msb'
  40. BitVec.get­Msb?
  41. BitVec.get­Msb­D
  42. BitVec.hash
  43. BitVec.int­Max
  44. BitVec.int­Min
  45. BitVec.iunfoldr
  46. BitVec.iunfoldr_replace
  47. BitVec.msb
  48. BitVec.mul
  49. BitVec.mul­Rec
  50. BitVec.neg
  51. BitVec.nil
  52. BitVec.not
  53. BitVec.of­Bool
  54. BitVec.of­Bool­List­BE
  55. BitVec.of­Bool­List­LE
  56. BitVec.of­Fin
    1. Constructor of Bit­Vec
  57. BitVec.of­Int
  58. BitVec.of­Nat
  59. BitVec.of­Nat­LT
  60. BitVec.or
  61. BitVec.replicate
  62. BitVec.reverse
  63. BitVec.rotate­Left
  64. BitVec.rotate­Right
  65. BitVec.sadd­Overflow
  66. BitVec.sdiv
  67. BitVec.set­Width
  68. BitVec.set­Width'
  69. BitVec.shift­Concat
  70. BitVec.shift­Left
  71. BitVec.shift­Left­Rec
  72. BitVec.shift­Left­Zero­Extend
  73. BitVec.sign­Extend
  74. BitVec.sle
  75. BitVec.slt
  76. BitVec.smod
  77. BitVec.smt­SDiv
  78. BitVec.smt­UDiv
  79. BitVec.srem
  80. BitVec.sshift­Right
  81. BitVec.sshift­Right'
  82. BitVec.sshift­Right­Rec
  83. BitVec.ssub­Overflow
  84. BitVec.sub
  85. BitVec.to­Hex
  86. BitVec.to­Int
  87. BitVec.to­Nat
  88. BitVec.truncate
  89. BitVec.two­Pow
  90. BitVec.uadd­Overflow
  91. BitVec.udiv
  92. BitVec.ule
  93. BitVec.ult
  94. BitVec.umod
  95. BitVec.ushift­Right
  96. BitVec.ushift­Right­Rec
  97. BitVec.usub­Overflow
  98. BitVec.xor
  99. BitVec.zero
  100. BitVec.zero­Extend
  101. Bool
  102. Bool.and
  103. Bool.dcond
  104. Bool.dec­Eq
  105. Bool.false
    1. Constructor of Bool
  106. Bool.not
  107. Bool.or
  108. Bool.to­ISize
  109. Bool.to­Int
  110. Bool.to­Int16
  111. Bool.to­Int32
  112. Bool.to­Int64
  113. Bool.to­Int8
  114. Bool.to­Nat
  115. Bool.to­UInt16
  116. Bool.to­UInt32
  117. Bool.to­UInt64
  118. Bool.to­UInt8
  119. Bool.to­USize
  120. Bool.true
    1. Constructor of Bool
  121. Bool.xor
  122. Buffer
    1. IO.FS.Stream.Buffer
  123. Build­Type
    1. Lake.Build­Type
  124. back!
    1. Array.back!
  125. back
    1. Array.back
  126. back
    1. String.back
  127. back?
    1. Array.back?
  128. backward.synthInstance.canon­Instances
  129. bdiv
    1. Int.bdiv
  130. beq
    1. BEq.beq (class method)
  131. beq
    1. Float.beq
  132. beq
    1. Float32.beq
  133. beq
    1. List.beq
  134. beq
    1. Nat.beq
  135. beq
    1. Substring.beq
  136. beta
    1. Lean.Meta.DSimp.Config.beta (structure field)
  137. beta
    1. Lean.Meta.Simp.Config.beta (structure field)
  138. bin­Insert
    1. Array.bin­Insert
  139. bin­Insert­M
    1. Array.bin­Insert­M
  140. bin­Search
    1. Array.bin­Search
  141. bin­Search­Contains
    1. Array.bin­Search­Contains
  142. bind
    1. Bind.bind (class method)
  143. bind
    1. EStateM.bind
  144. bind
    1. Except.bind
  145. bind
    1. ExceptT.bind
  146. bind
    1. Option.bind
  147. bind
    1. OptionT.bind
  148. bind
    1. ReaderT.bind
  149. bind
    1. StateT.bind
  150. bind
    1. Task.bind
  151. bind
    1. Thunk.bind
  152. bind­Cont
    1. ExceptT.bind­Cont
  153. bind­Left
    1. Bind.bind­Left
  154. bind­M
    1. Option.bind­M
  155. bind­Task
    1. BaseIO.bind­Task
  156. bind­Task
    1. EIO.bind­Task
  157. bind­Task
    1. IO.bind­Task
  158. bind_assoc
    1. [anonymous] (class method)
  159. bind_map
    1. [anonymous] (class method)
  160. bind_pure_comp
    1. [anonymous] (class method)
  161. binder­Name­Hint
  162. bitwise
    1. Nat.bitwise
  163. ble
    1. Nat.ble
  164. blt
    1. Nat.blt
  165. bmod
    1. Int.bmod
  166. bootstrap.inductive­Check­Resulting­Universe
  167. bsize
    1. Substring.bsize
  168. build (Lake command)
  169. bv_check
  170. bv_decide
  171. bv_decide?
  172. bv_normalize
  173. bv_omega
  174. by­Cases
    1. Decidable.by­Cases
  175. by_cases
  176. by_cases'
    1. Or.by_cases'
  177. by_cases
    1. Or.by_cases
  178. byte­Idx
    1. String.Pos.byte­Idx (structure field)
  179. 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. Coe
  28. Coe.mk
    1. Instance constructor of Coe
  29. Coe­Dep
  30. CoeDep.mk
    1. Instance constructor of Coe­Dep
  31. Coe­Fun
  32. CoeFun.mk
    1. Instance constructor of Coe­Fun
  33. Coe­HTC
  34. CoeHTC.mk
    1. Instance constructor of Coe­HTC
  35. Coe­HTCT
  36. CoeHTCT.mk
    1. Instance constructor of Coe­HTCT
  37. Coe­Head
  38. CoeHead.mk
    1. Instance constructor of Coe­Head
  39. Coe­OTC
  40. CoeOTC.mk
    1. Instance constructor of Coe­OTC
  41. Coe­Out
  42. CoeOut.mk
    1. Instance constructor of Coe­Out
  43. Coe­Sort
  44. CoeSort.mk
    1. Instance constructor of Coe­Sort
  45. Coe­T
  46. CoeT.mk
    1. Instance constructor of Coe­T
  47. Coe­TC
  48. CoeTC.mk
    1. Instance constructor of Coe­TC
  49. Coe­Tail
  50. CoeTail.mk
    1. Instance constructor of Coe­Tail
  51. Command
    1. Lean.Syntax.Command
  52. Condvar
    1. Std.Condvar
  53. Config
    1. Lean.Meta.DSimp.Config
  54. Config
    1. Lean.Meta.Rewrite.Config
  55. Config
    1. Lean.Meta.Simp.Config
  56. calc
  57. call-by-need
  58. cancel
    1. IO.cancel
  59. canon­Instances
    1. backward.synthInstance.canon­Instances
  60. capitalize
    1. String.capitalize
  61. carry
    1. BitVec.carry
  62. case
  63. case ... => ...
  64. case'
  65. case' ... => ...
  66. case­Strong­Rec­On
    1. Nat.case­Strong­Rec­On
  67. cases
  68. cases
    1. Fin.cases
  69. cases­Aux­On
    1. Nat.cases­Aux­On
  70. cast
  71. cast
    1. BitVec.cast
  72. cast
    1. Fin.cast
  73. cast
    1. Int.cast
  74. cast
    1. Nat.cast
  75. cast­Add
    1. Fin.cast­Add
  76. cast­LE
    1. Fin.cast­LE
  77. cast­LT
    1. Fin.cast­LT
  78. cast­Succ
    1. Fin.cast­Succ
  79. cast_heq
  80. catch­Exceptions
    1. EIO.catch­Exceptions
  81. cbrt
    1. Float.cbrt
  82. cbrt
    1. Float32.cbrt
  83. ceil
    1. Float.ceil
  84. ceil
    1. Float32.ceil
  85. chain
    1. of coercions
  86. chain­Task
    1. BaseIO.chain­Task
  87. chain­Task
    1. EIO.chain­Task
  88. chain­Task
    1. IO.chain­Task
  89. change (0) (1)
  90. change ... with ...
  91. char­Lit­Kind
    1. Lean.char­Lit­Kind
  92. check-build (Lake command)
  93. check-lint (Lake command)
  94. check-test (Lake command)
  95. check­Canceled
    1. IO.check­Canceled
  96. choice
    1. Option.choice
  97. choice­Kind
    1. Lean.choice­Kind
  98. choose
    1. Exists.choose
  99. classical
  100. clean (Lake command)
  101. clear
  102. close
    1. Std.Channel.close
  103. cmd
    1. [anonymous] (structure field)
  104. coe
    1. Coe.coe (class method)
  105. coe
    1. CoeDep.coe (class method)
  106. coe
    1. CoeFun.coe (class method)
  107. coe
    1. CoeHTC.coe (class method)
  108. coe
    1. CoeHTCT.coe (class method)
  109. coe
    1. CoeHead.coe (class method)
  110. coe
    1. CoeOTC.coe (class method)
  111. coe
    1. CoeOut.coe (class method)
  112. coe
    1. CoeSort.coe (class method)
  113. coe
    1. CoeT.coe (class method)
  114. coe
    1. CoeTC.coe (class method)
  115. coe
    1. CoeTail.coe (class method)
  116. col­Eq
  117. col­Ge
  118. col­Gt
  119. comment
    1. block
  120. comment
    1. line
  121. common­Prefix
    1. Substring.common­Prefix
  122. common­Suffix
    1. Substring.common­Suffix
  123. comp
    1. Function.comp
  124. comp_map
    1. LawfulFunctor.comp_map (class method)
  125. compare
    1. Ord.compare (class method)
  126. compare­Lex
  127. compare­Of­Less­And­BEq
  128. compare­Of­Less­And­Eq
  129. compare­On
  130. complement
    1. ISize.complement
  131. complement
    1. Int16.complement
  132. complement
    1. Int32.complement
  133. complement
    1. Int64.complement
  134. complement
    1. Int8.complement
  135. complement
    1. UInt16.complement
  136. complement
    1. UInt32.complement
  137. complement
    1. UInt64.complement
  138. complement
    1. UInt8.complement
  139. complement
    1. USize.complement
  140. completions (Elan command)
  141. components
    1. System.FilePath.components
  142. concat
    1. BitVec.concat
  143. concat
    1. List.concat
  144. cond
  145. configuration
    1. of tactics
  146. congr (0) (1) (2)
  147. congr­Arg
  148. congr­Fun
  149. cons
    1. BitVec.cons
  150. const
    1. Function.const
  151. constructor (0) (1)
  152. contains
    1. Array.contains
  153. contains
    1. List.contains
  154. contains
    1. String.contains
  155. contains
    1. Substring.contains
  156. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  157. contradiction
  158. control
  159. control­At
  160. conv
  161. conv => ...
  162. conv' (0) (1)
  163. cos
    1. Float.cos
  164. cos
    1. Float32.cos
  165. cosh
    1. Float.cosh
  166. cosh
    1. Float32.cosh
  167. count
    1. Array.count
  168. count
    1. List.count
  169. count­P
    1. Array.count­P
  170. count­P
    1. List.count­P
  171. create­Dir
    1. IO.FS.create­Dir
  172. create­Dir­All
    1. IO.FS.create­Dir­All
  173. create­Temp­Dir
    1. IO.FS.create­Temp­Dir
  174. create­Temp­File
    1. IO.FS.create­Temp­File
  175. crlf­To­Lf
    1. String.crlf­To­Lf
  176. csup
    1. [anonymous] (class method)
  177. csup_spec
    1. [anonymous] (class method)
  178. cumulativity
  179. curr
    1. String.Iterator.curr
  180. current­Dir
    1. IO.current­Dir
  181. curry
    1. Function.curry
  182. custom­Eliminators
    1. tactic.custom­Eliminators
  183. cwd
    1. [anonymous] (structure field)

D

  1. Decidable
  2. Decidable.by­Cases
  3. Decidable.decide
  4. Decidable.is­False
    1. Constructor of Decidable
  5. Decidable.is­True
    1. Constructor of Decidable
  6. Decidable­Eq
  7. Decidable­LE
  8. Decidable­LT
  9. Decidable­Pred
  10. Decidable­Rel
  11. Dir­Entry
    1. IO.FS.Dir­Entry
  12. Div
  13. Div.mk
    1. Instance constructor of Div
  14. Dvd
  15. Dvd.mk
    1. Instance constructor of Dvd
  16. data
    1. IO.FS.Stream.Buffer.data (structure field)
  17. data
    1. String.data (structure field)
  18. dbg­Trace­If­Shared
  19. dbg_trace
  20. dcond
    1. Bool.dcond
  21. dec­Eq
    1. BitVec.dec­Eq
  22. dec­Eq
    1. Bool.dec­Eq
  23. dec­Eq
    1. ISize.dec­Eq
  24. dec­Eq
    1. Int.dec­Eq
  25. dec­Eq
    1. Int16.dec­Eq
  26. dec­Eq
    1. Int32.dec­Eq
  27. dec­Eq
    1. Int64.dec­Eq
  28. dec­Eq
    1. Int8.dec­Eq
  29. dec­Eq
    1. Nat.dec­Eq
  30. dec­Eq
    1. String.dec­Eq
  31. dec­Eq
    1. UInt16.dec­Eq
  32. dec­Eq
    1. UInt32.dec­Eq
  33. dec­Eq
    1. UInt64.dec­Eq
  34. dec­Eq
    1. UInt8.dec­Eq
  35. dec­Eq
    1. USize.dec­Eq
  36. dec­Le
    1. Float.dec­Le
  37. dec­Le
    1. Float32.dec­Le
  38. dec­Le
    1. ISize.dec­Le
  39. dec­Le
    1. Int16.dec­Le
  40. dec­Le
    1. Int32.dec­Le
  41. dec­Le
    1. Int64.dec­Le
  42. dec­Le
    1. Int8.dec­Le
  43. dec­Le
    1. Nat.dec­Le
  44. dec­Le
    1. UInt16.dec­Le
  45. dec­Le
    1. UInt32.dec­Le
  46. dec­Le
    1. UInt64.dec­Le
  47. dec­Le
    1. UInt8.dec­Le
  48. dec­Le
    1. USize.dec­Le
  49. dec­Lt
    1. Float.dec­Lt
  50. dec­Lt
    1. Float32.dec­Lt
  51. dec­Lt
    1. ISize.dec­Lt
  52. dec­Lt
    1. Int16.dec­Lt
  53. dec­Lt
    1. Int32.dec­Lt
  54. dec­Lt
    1. Int64.dec­Lt
  55. dec­Lt
    1. Int8.dec­Lt
  56. dec­Lt
    1. Nat.dec­Lt
  57. dec­Lt
    1. UInt16.dec­Lt
  58. dec­Lt
    1. UInt32.dec­Lt
  59. dec­Lt
    1. UInt64.dec­Lt
  60. dec­Lt
    1. UInt8.dec­Lt
  61. dec­Lt
    1. USize.dec­Lt
  62. decapitalize
    1. String.decapitalize
  63. decidable
  64. decidable_eq_none
    1. Option.decidable_eq_none
  65. decide
  66. decide
    1. Decidable.decide
  67. decide
    1. Lean.Meta.DSimp.Config.decide (structure field)
  68. decide
    1. Lean.Meta.Simp.Config.decide (structure field)
  69. decreasing_tactic
  70. decreasing_trivial
  71. decreasing_with
  72. dedicated
    1. Task.Priority.dedicated
  73. deep­Terms
    1. pp.deep­Terms
  74. default (Elan command)
  75. default
    1. Inhabited.default (class method)
  76. default
    1. Task.Priority.default
  77. default­Facets
    1. [anonymous] (structure field)
  78. delta (0) (1)
  79. diff
    1. guard_msgs.diff
  80. digit­Char
    1. Nat.digit­Char
  81. discard
    1. Functor.discard
  82. discharge
    1. trace.Meta.Tactic.simp.discharge
  83. div
    1. Div.div (class method)
  84. div
    1. Fin.div
  85. div
    1. Float.div
  86. div
    1. Float32.div
  87. div
    1. ISize.div
  88. div
    1. Int16.div
  89. div
    1. Int32.div
  90. div
    1. Int64.div
  91. div
    1. Int8.div
  92. div
    1. Nat.div
  93. div
    1. UInt16.div
  94. div
    1. UInt32.div
  95. div
    1. UInt64.div
  96. div
    1. UInt8.div
  97. div
    1. USize.div
  98. div2Induction
    1. Nat.div2Induction
  99. div­Rec
    1. BitVec.div­Rec
  100. div­Subtract­Shift
    1. BitVec.div­Subtract­Shift
  101. done (0) (1)
  102. down
    1. PLift.down (structure field)
  103. down
    1. ULift.down (structure field)
  104. drop
    1. Array.drop
  105. drop
    1. List.drop
  106. drop
    1. String.drop
  107. drop
    1. Subarray.drop
  108. drop
    1. Substring.drop
  109. drop­Last
    1. List.drop­Last
  110. drop­Last­TR
    1. List.drop­Last­TR
  111. drop­Prefix?
    1. String.drop­Prefix?
  112. drop­Prefix?
    1. Substring.drop­Prefix?
  113. drop­Right
    1. String.drop­Right
  114. drop­Right
    1. Substring.drop­Right
  115. drop­Right­While
    1. String.drop­Right­While
  116. drop­Right­While
    1. Substring.drop­Right­While
  117. drop­Suffix?
    1. String.drop­Suffix?
  118. drop­Suffix?
    1. Substring.drop­Suffix?
  119. drop­While
    1. List.drop­While
  120. drop­While
    1. String.drop­While
  121. drop­While
    1. Substring.drop­While
  122. dsimp (0) (1)
  123. dsimp!
  124. dsimp
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  125. dsimp?
  126. dsimp?!
  127. 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. Equivalence
  47. Equivalence.mk
    1. Constructor of Equivalence
  48. Error
    1. IO.Error
  49. Even
  50. Even.plus­Two
    1. Constructor of Even
  51. Even.zero
    1. Constructor of Even
  52. Except
  53. Except.bind
  54. Except.error
    1. Constructor of Except
  55. Except.is­Ok
  56. Except.map
  57. Except.map­Error
  58. Except.ok
    1. Constructor of Except
  59. Except.or­Else­Lazy
  60. Except.pure
  61. Except.to­Bool
  62. Except.to­Option
  63. Except.try­Catch
  64. Except­Cps­T
  65. Except­CpsT.lift
  66. Except­CpsT.run
  67. Except­CpsT.run­Catch
  68. Except­CpsT.run­K
  69. Except­T
  70. ExceptT.adapt
  71. ExceptT.bind
  72. ExceptT.bind­Cont
  73. ExceptT.lift
  74. ExceptT.map
  75. ExceptT.mk
  76. ExceptT.pure
  77. ExceptT.run
  78. ExceptT.try­Catch
  79. Exists
  80. Exists.choose
  81. Exists.intro
    1. Constructor of Exists
  82. ediv
    1. Int.ediv
  83. elem
    1. Array.elem
  84. elem
    1. List.elem
  85. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  86. elim
    1. And.elim
  87. elim
    1. Empty.elim
  88. elim
    1. False.elim
  89. elim
    1. HEq.elim
  90. elim
    1. Iff.elim
  91. elim
    1. Not.elim
  92. elim
    1. Option.elim
  93. elim
    1. PEmpty.elim
  94. elim
    1. Subsingleton.elim
  95. elim
    1. Sum.elim
  96. elim0
    1. Fin.elim0
  97. elim­M
    1. Option.elim­M
  98. emod
    1. Int.emod
  99. empty
    1. Array.empty
  100. empty
    1. Subarray.empty
  101. empty­With­Capacity
    1. Array.empty­With­Capacity
  102. end­Pos
    1. String.end­Pos
  103. ends­With
    1. String.ends­With
  104. enter
  105. env (Lake command)
  106. env
    1. IO.Process.SpawnArgs.cmd (structure field)
  107. environment variables
  108. eprint
    1. IO.eprint
  109. eprintln
    1. IO.eprintln
  110. eq­Rec_heq
  111. eq_of_beq
    1. LawfulBEq.eq_of_beq (class method)
  112. eq_of_heq
  113. eq_refl
  114. erase
    1. Array.erase
  115. erase
    1. List.erase
  116. erase­Dups
    1. List.erase­Dups
  117. erase­Idx!
    1. Array.erase­Idx!
  118. erase­Idx
    1. Array.erase­Idx
  119. erase­Idx
    1. List.erase­Idx
  120. erase­Idx­If­In­Bounds
    1. Array.erase­Idx­If­In­Bounds
  121. erase­Idx­TR
    1. List.erase­Idx­TR
  122. erase­P
    1. Array.erase­P
  123. erase­P
    1. List.erase­P
  124. erase­PTR
    1. List.erase­PTR
  125. erase­Reps
    1. Array.erase­Reps
  126. erase­Reps
    1. List.erase­Reps
  127. erase­TR
    1. List.erase­TR
  128. erw (0) (1)
  129. eta
    1. Lean.Meta.DSimp.Config.eta (structure field)
  130. eta
    1. Lean.Meta.Simp.Config.eta (structure field)
  131. eta­Struct
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
  132. eta­Struct
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  133. eval.derive.repr
  134. eval.pp
  135. eval.type
  136. exact
  137. exact
    1. Quotient.exact
  138. exact?
  139. exact_mod_cast
  140. exe (Lake command)
  141. exe­Extension
    1. System.FilePath.exe­Extension
  142. exe­Name
    1. [anonymous] (structure field)
  143. execution
    1. IO.AccessRight.execution (structure field)
  144. exfalso
  145. exists
  146. exit
    1. IO.Process.exit
  147. exit­Code
    1. IO.Process.Output.exit­Code (structure field)
  148. exp
    1. Float.exp
  149. exp
    1. Float32.exp
  150. exp2
    1. Float.exp2
  151. exp2
    1. Float32.exp2
  152. expand­Macro?
    1. Lean.Macro.expand­Macro?
  153. expose_names
  154. ext (0) (1)
  155. ext1
  156. ext­Separator
    1. System.FilePath.ext­Separator
  157. extension
    1. System.FilePath.extension
  158. extensionality
    1. of propositions
  159. extra­Dep­Targets
    1. [anonymous] (structure field) (0) (1)
  160. extract
    1. Array.extract
  161. extract
    1. List.extract
  162. extract
    1. String.Iterator.extract
  163. extract
    1. String.extract
  164. extract
    1. Substring.extract
  165. extract­Lsb'
    1. BitVec.extract­Lsb'
  166. extract­Lsb
    1. BitVec.extract­Lsb

F

  1. False
  2. False.elim
  3. File­Path
    1. System.File­Path
  4. File­Right
    1. IO.File­Right
  5. Fin
  6. Fin.add
  7. Fin.add­Cases
  8. Fin.add­Nat
  9. Fin.cases
  10. Fin.cast
  11. Fin.cast­Add
  12. Fin.cast­LE
  13. Fin.cast­LT
  14. Fin.cast­Succ
  15. Fin.div
  16. Fin.elim0
  17. Fin.foldl
  18. Fin.foldl­M
  19. Fin.foldr
  20. Fin.foldr­M
  21. Fin.h­Iterate
  22. Fin.h­Iterate­From
  23. Fin.induction
  24. Fin.induction­On
  25. Fin.land
  26. Fin.last
  27. Fin.last­Cases
  28. Fin.log2
  29. Fin.lor
  30. Fin.mk
    1. Constructor of Fin
  31. Fin.mod
  32. Fin.modn
  33. Fin.mul
  34. Fin.nat­Add
  35. Fin.of­Nat'
  36. Fin.pred
  37. Fin.rev
  38. Fin.reverse­Induction
  39. Fin.shift­Left
  40. Fin.shift­Right
  41. Fin.sub
  42. Fin.sub­Nat
  43. Fin.succ
  44. Fin.succ­Rec
  45. Fin.succ­Rec­On
  46. Fin.to­Nat
  47. Fin.xor
  48. Float
  49. Float.abs
  50. Float.acos
  51. Float.acosh
  52. Float.add
  53. Float.asin
  54. Float.asinh
  55. Float.atan
  56. Float.atan2
  57. Float.atanh
  58. Float.beq
  59. Float.cbrt
  60. Float.ceil
  61. Float.cos
  62. Float.cosh
  63. Float.dec­Le
  64. Float.dec­Lt
  65. Float.div
  66. Float.exp
  67. Float.exp2
  68. Float.floor
  69. Float.fr­Exp
  70. Float.is­Finite
  71. Float.is­Inf
  72. Float.is­Na­N
  73. Float.le
  74. Float.log
  75. Float.log10
  76. Float.log2
  77. Float.lt
  78. Float.mul
  79. Float.neg
  80. Float.of­Binary­Scientific
  81. Float.of­Bits
  82. Float.of­Int
  83. Float.of­Nat
  84. Float.of­Scientific
  85. Float.pow
  86. Float.round
  87. Float.scale­B
  88. Float.sin
  89. Float.sinh
  90. Float.sqrt
  91. Float.sub
  92. Float.tan
  93. Float.tanh
  94. Float.to­Bits
  95. Float.to­Float32
  96. Float.to­ISize
  97. Float.to­Int16
  98. Float.to­Int32
  99. Float.to­Int64
  100. Float.to­Int8
  101. Float.to­String
  102. Float.to­UInt16
  103. Float.to­UInt32
  104. Float.to­UInt64
  105. Float.to­UInt8
  106. Float.to­USize
  107. Float32
  108. Float32.abs
  109. Float32.acos
  110. Float32.acosh
  111. Float32.add
  112. Float32.asin
  113. Float32.asinh
  114. Float32.atan
  115. Float32.atan2
  116. Float32.atanh
  117. Float32.beq
  118. Float32.cbrt
  119. Float32.ceil
  120. Float32.cos
  121. Float32.cosh
  122. Float32.dec­Le
  123. Float32.dec­Lt
  124. Float32.div
  125. Float32.exp
  126. Float32.exp2
  127. Float32.floor
  128. Float32.fr­Exp
  129. Float32.is­Finite
  130. Float32.is­Inf
  131. Float32.is­Na­N
  132. Float32.le
  133. Float32.log
  134. Float32.log10
  135. Float32.log2
  136. Float32.lt
  137. Float32.mul
  138. Float32.neg
  139. Float32.of­Binary­Scientific
  140. Float32.of­Bits
  141. Float32.of­Int
  142. Float32.of­Nat
  143. Float32.of­Scientific
  144. Float32.pow
  145. Float32.round
  146. Float32.scale­B
  147. Float32.sin
  148. Float32.sinh
  149. Float32.sqrt
  150. Float32.sub
  151. Float32.tan
  152. Float32.tanh
  153. Float32.to­Bits
  154. Float32.to­Float
  155. Float32.to­ISize
  156. Float32.to­Int16
  157. Float32.to­Int32
  158. Float32.to­Int64
  159. Float32.to­Int8
  160. Float32.to­String
  161. Float32.to­UInt16
  162. Float32.to­UInt32
  163. Float32.to­UInt64
  164. Float32.to­UInt8
  165. Float32.to­USize
  166. For­In
  167. For­In'
  168. ForIn'.mk
    1. Instance constructor of For­In'
  169. ForIn.mk
    1. Instance constructor of For­In
  170. For­In­Step
  171. For­InStep.done
    1. Constructor of For­In­Step
  172. For­InStep.value
  173. For­InStep.yield
    1. Constructor of For­In­Step
  174. For­M
  175. ForM.for­In
  176. ForM.mk
    1. Instance constructor of For­M
  177. Function.comp
  178. Function.const
  179. Function.curry
  180. Function.uncurry
  181. Functor
  182. Functor.discard
  183. Functor.map­Rev
  184. Functor.mk
    1. Instance constructor of Functor
  185. fail
  186. fail
    1. OptionT.fail
  187. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
  188. fail­If­Unchanged
    1. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  189. fail_if_success (0) (1)
  190. failure
    1. ReaderT.failure
  191. failure
    1. StateT.failure
  192. failure
    1. [anonymous] (class method)
  193. false_or_by_contra
  194. fdiv
    1. Int.fdiv
  195. field­Idx­Kind
    1. Lean.field­Idx­Kind
  196. field­Notation
    1. pp.field­Notation
  197. file­Name
    1. IO.FS.DirEntry.file­Name (structure field)
  198. file­Name
    1. System.FilePath.file­Name
  199. file­Stem
    1. System.FilePath.file­Stem
  200. fill
    1. BitVec.fill
  201. filter
    1. Array.filter
  202. filter
    1. List.filter
  203. filter
    1. Option.filter
  204. filter­M
    1. Array.filter­M
  205. filter­M
    1. List.filter­M
  206. filter­Map
    1. Array.filter­Map
  207. filter­Map
    1. List.filter­Map
  208. filter­Map­M
    1. Array.filter­Map­M
  209. filter­Map­M
    1. List.filter­Map­M
  210. filter­Map­TR
    1. List.filter­Map­TR
  211. filter­Rev­M
    1. Array.filter­Rev­M
  212. filter­Rev­M
    1. List.filter­Rev­M
  213. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  214. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  215. filter­TR
    1. List.filter­TR
  216. fin­Idx­Of?
    1. Array.fin­Idx­Of?
  217. fin­Idx­Of?
    1. List.fin­Idx­Of?
  218. fin­Range
    1. Array.fin­Range
  219. fin­Range
    1. List.fin­Range
  220. find
    1. String.find
  221. find?
    1. Array.find?
  222. find?
    1. List.find?
  223. find­Extern­Lib?
    1. Lake.find­Extern­Lib?
  224. find­Fin­Idx?
    1. Array.find­Fin­Idx?
  225. find­Fin­Idx?
    1. List.find­Fin­Idx?
  226. find­Idx
    1. Array.find­Idx
  227. find­Idx
    1. List.find­Idx
  228. find­Idx?
    1. Array.find­Idx?
  229. find­Idx?
    1. List.find­Idx?
  230. find­Idx­M?
    1. Array.find­Idx­M?
  231. find­Lean­Exe?
    1. Lake.find­Lean­Exe?
  232. find­Lean­Lib?
    1. Lake.find­Lean­Lib?
  233. find­Line­Start
    1. String.find­Line­Start
  234. find­M?
    1. Array.find­M?
  235. find­M?
    1. List.find­M?
  236. find­Module?
    1. Lake.find­Module?
  237. find­Package?
    1. Lake.find­Package?
  238. find­Rev?
    1. Array.find­Rev?
  239. find­Rev?
    1. Subarray.find­Rev?
  240. find­Rev­M?
    1. Array.find­Rev­M?
  241. find­Rev­M?
    1. Subarray.find­Rev­M?
  242. find­Some!
    1. Array.find­Some!
  243. find­Some?
    1. Array.find­Some?
  244. find­Some?
    1. List.find­Some?
  245. find­Some­M?
    1. Array.find­Some­M?
  246. find­Some­M?
    1. List.find­Some­M?
  247. find­Some­Rev?
    1. Array.find­Some­Rev?
  248. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
  249. find­Some­Rev­M?
    1. Subarray.find­Some­Rev­M?
  250. first (0) (1)
  251. first­Diff­Pos
    1. String.first­Diff­Pos
  252. first­M
    1. Array.first­M
  253. first­M
    1. List.first­M
  254. fix
    1. Lean.Order.fix
  255. fix
    1. WellFounded.fix
  256. fix_eq
    1. Lean.Order.fix_eq
  257. flags
    1. IO.AccessRight.flags
  258. flags
    1. IO.FileRight.flags
  259. flat­Map
    1. Array.flat­Map
  260. flat­Map
    1. List.flat­Map
  261. flat­Map­M
    1. Array.flat­Map­M
  262. flat­Map­M
    1. List.flat­Map­M
  263. flat­Map­TR
    1. List.flat­Map­TR
  264. flatten
    1. Array.flatten
  265. flatten
    1. List.flatten
  266. flatten­TR
    1. List.flatten­TR
  267. floor
    1. Float.floor
  268. floor
    1. Float32.floor
  269. flush
    1. IO.FS.Handle.flush
  270. flush
    1. IO.FS.Stream.flush (structure field)
  271. fmod
    1. Int.fmod
  272. focus (0) (1)
  273. fold
    1. Nat.fold
  274. fold­I
    1. Prod.fold­I
  275. fold­M
    1. Nat.fold­M
  276. fold­Rev
    1. Nat.fold­Rev
  277. fold­Rev­M
    1. Nat.fold­Rev­M
  278. fold­TR
    1. Nat.fold­TR
  279. foldl
    1. Array.foldl
  280. foldl
    1. Fin.foldl
  281. foldl
    1. List.foldl
  282. foldl
    1. String.foldl
  283. foldl
    1. Subarray.foldl
  284. foldl
    1. Substring.foldl
  285. foldl­M
    1. Array.foldl­M
  286. foldl­M
    1. Fin.foldl­M
  287. foldl­M
    1. List.foldl­M
  288. foldl­M
    1. Subarray.foldl­M
  289. foldl­Rec­On
    1. List.foldl­Rec­On
  290. foldr
    1. Array.foldr
  291. foldr
    1. Fin.foldr
  292. foldr
    1. List.foldr
  293. foldr
    1. String.foldr
  294. foldr
    1. Subarray.foldr
  295. foldr
    1. Substring.foldr
  296. foldr­M
    1. Array.foldr­M
  297. foldr­M
    1. Fin.foldr­M
  298. foldr­M
    1. List.foldr­M
  299. foldr­M
    1. Subarray.foldr­M
  300. foldr­Rec­On
    1. List.foldr­Rec­On
  301. foldr­TR
    1. List.foldr­TR
  302. for­A
    1. List.for­A
  303. for­Async
    1. Std.Channel.for­Async
  304. for­In'
    1. ForIn'.for­In' (class method)
  305. for­In
    1. ForIn.for­In (class method)
  306. for­In
    1. ForM.for­In
  307. for­In
    1. Subarray.for­In
  308. for­M
    1. Array.for­M
  309. for­M
    1. ForM.for­M (class method)
  310. for­M
    1. List.for­M
  311. for­M
    1. Nat.for­M
  312. for­M
    1. Option.for­M
  313. for­M
    1. Subarray.for­M
  314. for­Rev­M
    1. Array.for­Rev­M
  315. for­Rev­M
    1. Nat.for­Rev­M
  316. for­Rev­M
    1. Subarray.for­Rev­M
  317. format
    1. Option.format
  318. forward
    1. String.Iterator.forward
  319. fr­Exp
    1. Float.fr­Exp
  320. fr­Exp
    1. Float32.fr­Exp
  321. from­State­M
    1. EStateM.from­State­M
  322. from­UTF8!
    1. String.from­UTF8!
  323. from­UTF8
    1. String.from­UTF8
  324. from­UTF8?
    1. String.from­UTF8?
  325. front
    1. String.front
  326. front
    1. Substring.front
  327. fst
    1. MProd.fst (structure field)
  328. fst
    1. PProd.fst (structure field)
  329. fst
    1. PSigma.fst (structure field)
  330. fst
    1. Prod.fst (structure field)
  331. fst
    1. Sigma.fst (structure field)
  332. fun
  333. fun_cases
  334. fun_induction
  335. 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. String.get!
  11. get!
    1. Subarray.get!
  12. get'
    1. String.get'
  13. get
    1. EStateM.get
  14. get
    1. List.get
  15. get
    1. MonadState.get
  16. get
    1. MonadState.get (class method)
  17. get
    1. Monad­StateOf.get (class method)
  18. get
    1. Option.get
  19. get
    1. ST.Ref.get
  20. get
    1. State­RefT'.get
  21. get
    1. StateT.get
  22. get
    1. String.get
  23. get
    1. Subarray.get
  24. get
    1. Substring.get
  25. get
    1. Task.get
  26. get
    1. Thunk.get
  27. get?
    1. String.get?
  28. get­Augmented­Env
    1. Lake.get­Augmented­Env
  29. get­Augmented­Lean­Path
    1. Lake.get­Augmented­Lean­Path
  30. get­Augmented­Lean­Src­Path
    1. Lake.get­Augmented­Lean­Src­Path
  31. get­Augmented­Shared­Lib­Path
    1. Lake.get­Augmented­Shared­Lib­Path
  32. get­Char
    1. Lean.TSyntax.get­Char
  33. get­Curr­Namespace
    1. Lean.Macro.get­Curr­Namespace
  34. get­Current­Dir
    1. IO.Process.get­Current­Dir
  35. get­D
    1. Array.get­D
  36. get­D
    1. List.get­D
  37. get­D
    1. Option.get­D
  38. get­D
    1. Subarray.get­D
  39. get­DM
    1. Option.get­DM
  40. get­Elan?
    1. Lake.get­Elan?
  41. get­Elan­Home?
    1. Lake.get­Elan­Home?
  42. get­Elan­Install?
    1. Lake.get­Elan­Install?
  43. get­Elan­Toolchain
    1. Lake.get­Elan­Toolchain
  44. get­Elem!
    1. GetElem?.get­Elem? (class method)
  45. get­Elem!_def
    1. Lawful­GetElem.get­Elem!_def (class method)
  46. get­Elem
    1. GetElem.get­Elem (class method)
  47. get­Elem?
    1. [anonymous] (class method)
  48. get­Elem?_def
    1. Lawful­GetElem.get­Elem?_def (class method)
  49. get­Env
    1. IO.get­Env
  50. get­Env­Lean­Path
    1. Lake.get­Env­Lean­Path
  51. get­Env­Lean­Src­Path
    1. Lake.get­Env­Lean­Src­Path
  52. get­Env­Shared­Lib­Path
    1. Lake.get­Env­Shared­Lib­Path
  53. get­Even­Elems
    1. Array.get­Even­Elems
  54. get­Hygiene­Info
    1. Lean.TSyntax.get­Hygiene­Info
  55. get­Id
    1. Lean.TSyntax.get­Id
  56. get­Kind
    1. Lean.Syntax.get­Kind
  57. get­Lake
    1. Lake.get­Lake
  58. get­Lake­Env
    1. Lake.get­Lake­Env
  59. get­Lake­Home
    1. Lake.get­Lake­Home
  60. get­Lake­Install
    1. Lake.get­Lake­Install
  61. get­Lake­Lib­Dir
    1. Lake.get­Lake­Lib­Dir
  62. get­Lake­Src­Dir
    1. Lake.get­Lake­Src­Dir
  63. get­Last!
    1. List.get­Last!
  64. get­Last
    1. List.get­Last
  65. get­Last?
    1. List.get­Last?
  66. get­Last­D
    1. List.get­Last­D
  67. get­Lean
    1. Lake.get­Lean
  68. get­Lean­Ar
    1. Lake.get­Lean­Ar
  69. get­Lean­Cc
    1. Lake.get­Lean­Cc
  70. get­Lean­Cc?
    1. Lake.get­Lean­Cc?
  71. get­Lean­Include­Dir
    1. Lake.get­Lean­Include­Dir
  72. get­Lean­Install
    1. Lake.get­Lean­Install
  73. get­Lean­Lib­Dir
    1. Lake.get­Lean­Lib­Dir
  74. get­Lean­Path
    1. Lake.get­Lean­Path
  75. get­Lean­Shared­Lib
    1. Lake.get­Lean­Shared­Lib
  76. get­Lean­Src­Dir
    1. Lake.get­Lean­Src­Dir
  77. get­Lean­Src­Path
    1. Lake.get­Lean­Src­Path
  78. get­Lean­Sysroot
    1. Lake.get­Lean­Sysroot
  79. get­Lean­System­Lib­Dir
    1. Lake.get­Lean­System­Lib­Dir
  80. get­Leanc
    1. Lake.get­Leanc
  81. get­Left
    1. Sum.get­Left
  82. get­Left?
    1. Sum.get­Left?
  83. get­Line
    1. IO.FS.Handle.get­Line
  84. get­Line
    1. IO.FS.Stream.get­Line (structure field)
  85. get­Lsb'
    1. BitVec.get­Lsb'
  86. get­Lsb?
    1. BitVec.get­Lsb?
  87. get­Lsb­D
    1. BitVec.get­Lsb­D
  88. get­M
    1. Option.get­M
  89. get­Max?
    1. Array.get­Max?
  90. get­Modify
  91. get­Msb'
    1. BitVec.get­Msb'
  92. get­Msb?
    1. BitVec.get­Msb?
  93. get­Msb­D
    1. BitVec.get­Msb­D
  94. get­Name
    1. Lean.TSyntax.get­Name
  95. get­Nat
    1. Lean.TSyntax.get­Nat
  96. get­No­Cache
    1. Lake.get­No­Cache
  97. get­Num­Heartbeats
    1. IO.get­Num­Heartbeats
  98. get­PID
    1. IO.Process.get­PID
  99. get­Pkg­Url­Map
    1. Lake.get­Pkg­Url­Map
  100. get­Random­Bytes
    1. IO.get­Random­Bytes
  101. get­Right
    1. Sum.get­Right
  102. get­Right?
    1. Sum.get­Right?
  103. get­Root­Package
    1. Lake.get­Root­Package
  104. get­Scientific
    1. Lean.TSyntax.get­Scientific
  105. get­Shared­Lib­Path
    1. Lake.get­Shared­Lib­Path
  106. get­Stderr
    1. IO.get­Stderr
  107. get­Stdin
    1. IO.get­Stdin
  108. get­Stdout
    1. IO.get­Stdout
  109. get­String
    1. Lean.TSyntax.get­String
  110. get­TID
    1. IO.get­TID
  111. get­Task­State
    1. IO.get­Task­State
  112. get­The
  113. get­Try­Cache
    1. Lake.get­Try­Cache
  114. get­Utf8Byte
    1. String.get­Utf8Byte
  115. get­Workspace
    1. Lake.MonadWorkspace.get­Workspace (class method)
  116. get_elem_tactic
  117. get_elem_tactic_trivial
  118. globs
    1. [anonymous] (structure field)
  119. goal
    1. main
  120. ground
    1. Lean.Meta.Simp.Config.ground (structure field)
  121. group
    1. IO.FileRight.group (structure field)
  122. group­By­Key
    1. Array.group­By­Key
  123. group­By­Key
    1. List.group­By­Key
  124. group­Kind
    1. Lean.group­Kind
  125. guard
  126. guard
    1. Option.guard
  127. guard_expr
  128. guard_hyp
  129. guard_msgs.diff
  130. 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. Hashable
  36. Hashable.mk
    1. Instance constructor of Hashable
  37. Homogeneous­Pow
  38. HomogeneousPow.mk
    1. Instance constructor of Homogeneous­Pow
  39. Hygiene­Info
    1. Lean.Syntax.Hygiene­Info
  40. h­Add
    1. HAdd.h­Add (class method)
  41. h­And
    1. HAnd.h­And (class method)
  42. h­Append
    1. HAppend.h­Append (class method)
  43. h­Div
    1. HDiv.h­Div (class method)
  44. h­Iterate
    1. Fin.h­Iterate
  45. h­Iterate­From
    1. Fin.h­Iterate­From
  46. h­Mod
    1. HMod.h­Mod (class method)
  47. h­Mul
    1. HMul.h­Mul (class method)
  48. h­Or
    1. HOr.h­Or (class method)
  49. h­Pow
    1. HPow.h­Pow (class method)
  50. h­Shift­Left
    1. HShiftLeft.h­Shift­Left (class method)
  51. h­Shift­Right
    1. HShiftRight.h­Shift­Right (class method)
  52. h­Sub
    1. HSub.h­Sub (class method)
  53. h­Xor
    1. HXor.h­Xor (class method)
  54. has­Decl
    1. Lean.Macro.has­Decl
  55. has­Finished
    1. IO.has­Finished
  56. has­Next
    1. String.Iterator.has­Next
  57. has­Prev
    1. String.Iterator.has­Prev
  58. hash
    1. BitVec.hash
  59. hash
    1. Hashable.hash (class method)
  60. hash
    1. String.hash
  61. hash_eq
  62. hash_eq
    1. LawfulHashable.hash_eq (class method)
  63. have
  64. have'
  65. have­I
  66. head!
    1. List.head!
  67. head
    1. List.head
  68. head?
    1. List.head?
  69. head­D
    1. List.head­D
  70. helim
    1. Subsingleton.helim
  71. heq_of_eq
  72. heq_of_eq­Rec_eq
  73. heq_of_heq_of_eq
  74. hrec­On
    1. Quot.hrec­On
  75. hrec­On
    1. Quotient.hrec­On
  76. hygiene
    1. in tactics
  77. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  78. 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.mk
    1. Constructor of IO.Process.Child
  85. IO.Process.Child.take­Stdin
  86. IO.Process.Child.try­Wait
  87. IO.Process.Child.wait
  88. IO.Process.Output
  89. IO.Process.Output.mk
    1. Constructor of IO.Process.Output
  90. IO.Process.Spawn­Args
  91. IO.Process.SpawnArgs.mk
    1. Constructor of IO.Process.Spawn­Args
  92. IO.Process.Stdio
  93. IO.Process.Stdio.inherit
    1. Constructor of IO.Process.Stdio
  94. IO.Process.Stdio.null
    1. Constructor of IO.Process.Stdio
  95. IO.Process.Stdio.piped
    1. Constructor of IO.Process.Stdio
  96. IO.Process.Stdio.to­Handle­Type
  97. IO.Process.Stdio­Config
  98. IO.Process.StdioConfig.mk
    1. Constructor of IO.Process.Stdio­Config
  99. IO.Process.exit
  100. IO.Process.get­Current­Dir
  101. IO.Process.get­PID
  102. IO.Process.output
  103. IO.Process.run
  104. IO.Process.set­Current­Dir
  105. IO.Process.spawn
  106. IO.Promise
  107. IO.Promise.is­Resolved
  108. IO.Promise.new
  109. IO.Promise.resolve
  110. IO.Promise.result!
  111. IO.Promise.result?
  112. IO.Promise.result­D
  113. IO.Ref
  114. IO.Task­State
  115. IO.TaskState.finished
    1. Constructor of IO.Task­State
  116. IO.TaskState.running
    1. Constructor of IO.Task­State
  117. IO.TaskState.waiting
    1. Constructor of IO.Task­State
  118. IO.add­Heartbeats
  119. IO.app­Dir
  120. IO.app­Path
  121. IO.as­Task
  122. IO.bind­Task
  123. IO.cancel
  124. IO.chain­Task
  125. IO.check­Canceled
  126. IO.current­Dir
  127. IO.eprint
  128. IO.eprintln
  129. IO.get­Env
  130. IO.get­Num­Heartbeats
  131. IO.get­Random­Bytes
  132. IO.get­Stderr
  133. IO.get­Stdin
  134. IO.get­Stdout
  135. IO.get­TID
  136. IO.get­Task­State
  137. IO.has­Finished
  138. IO.iterate
  139. IO.lazy­Pure
  140. IO.map­Task
  141. IO.map­Tasks
  142. IO.mk­Ref
  143. IO.mono­Ms­Now
  144. IO.mono­Nanos­Now
  145. IO.of­Except
  146. IO.print
  147. IO.println
  148. IO.rand
  149. IO.set­Access­Rights
  150. IO.set­Rand­Seed
  151. IO.set­Stderr
  152. IO.set­Stdin
  153. IO.set­Stdout
  154. IO.sleep
  155. IO.to­EIO
  156. IO.user­Error
  157. IO.wait
  158. IO.wait­Any
  159. IO.with­Stderr
  160. IO.with­Stdin
  161. IO.with­Stdout
  162. ISize
  163. ISize.abs
  164. ISize.add
  165. ISize.complement
  166. ISize.dec­Eq
  167. ISize.dec­Le
  168. ISize.dec­Lt
  169. ISize.div
  170. ISize.land
  171. ISize.le
  172. ISize.lor
  173. ISize.lt
  174. ISize.max­Value
  175. ISize.min­Value
  176. ISize.mod
  177. ISize.mul
  178. ISize.neg
  179. ISize.of­Bit­Vec
  180. ISize.of­Int
  181. ISize.of­Int­LE
  182. ISize.of­Int­Truncate
  183. ISize.of­Nat
  184. ISize.shift­Left
  185. ISize.shift­Right
  186. ISize.size
  187. ISize.sub
  188. ISize.to­Bit­Vec
  189. ISize.to­Float
  190. ISize.to­Float32
  191. ISize.to­Int
  192. ISize.to­Int16
  193. ISize.to­Int32
  194. ISize.to­Int64
  195. ISize.to­Int8
  196. ISize.to­Nat­Clamp­Neg
  197. ISize.xor
  198. Id
  199. Id.run
  200. Ident
    1. Lean.Syntax.Ident
  201. Iff
  202. Iff.elim
  203. Iff.intro
    1. Constructor of Iff
  204. Inhabited
  205. Inhabited.mk
    1. Instance constructor of Inhabited
  206. Int
  207. Int.add
  208. Int.bdiv
  209. Int.bmod
  210. Int.cast
  211. Int.dec­Eq
  212. Int.ediv
  213. Int.emod
  214. Int.fdiv
  215. Int.fmod
  216. Int.gcd
  217. Int.lcm
  218. Int.le
  219. Int.lt
  220. Int.mul
  221. Int.nat­Abs
  222. Int.neg
  223. Int.neg­Of­Nat
  224. Int.neg­Succ
    1. Constructor of Int
  225. Int.not
  226. Int.of­Nat
    1. Constructor of Int
  227. Int.pow
  228. Int.repr
  229. Int.shift­Right
  230. Int.sign
  231. Int.sub
  232. Int.sub­Nat­Nat
  233. Int.tdiv
  234. Int.tmod
  235. Int.to­ISize
  236. Int.to­Int16
  237. Int.to­Int32
  238. Int.to­Int64
  239. Int.to­Int8
  240. Int.to­Nat
  241. Int.to­Nat?
  242. Int16
  243. Int16.abs
  244. Int16.add
  245. Int16.complement
  246. Int16.dec­Eq
  247. Int16.dec­Le
  248. Int16.dec­Lt
  249. Int16.div
  250. Int16.land
  251. Int16.le
  252. Int16.lor
  253. Int16.lt
  254. Int16.max­Value
  255. Int16.min­Value
  256. Int16.mod
  257. Int16.mul
  258. Int16.neg
  259. Int16.of­Bit­Vec
  260. Int16.of­Int
  261. Int16.of­Int­LE
  262. Int16.of­Int­Truncate
  263. Int16.of­Nat
  264. Int16.shift­Left
  265. Int16.shift­Right
  266. Int16.size
  267. Int16.sub
  268. Int16.to­Bit­Vec
  269. Int16.to­Float
  270. Int16.to­Float32
  271. Int16.to­ISize
  272. Int16.to­Int
  273. Int16.to­Int32
  274. Int16.to­Int64
  275. Int16.to­Int8
  276. Int16.to­Nat­Clamp­Neg
  277. Int16.xor
  278. Int32
  279. Int32.abs
  280. Int32.add
  281. Int32.complement
  282. Int32.dec­Eq
  283. Int32.dec­Le
  284. Int32.dec­Lt
  285. Int32.div
  286. Int32.land
  287. Int32.le
  288. Int32.lor
  289. Int32.lt
  290. Int32.max­Value
  291. Int32.min­Value
  292. Int32.mod
  293. Int32.mul
  294. Int32.neg
  295. Int32.of­Bit­Vec
  296. Int32.of­Int
  297. Int32.of­Int­LE
  298. Int32.of­Int­Truncate
  299. Int32.of­Nat
  300. Int32.shift­Left
  301. Int32.shift­Right
  302. Int32.size
  303. Int32.sub
  304. Int32.to­Bit­Vec
  305. Int32.to­Float
  306. Int32.to­Float32
  307. Int32.to­ISize
  308. Int32.to­Int
  309. Int32.to­Int16
  310. Int32.to­Int64
  311. Int32.to­Int8
  312. Int32.to­Nat­Clamp­Neg
  313. Int32.xor
  314. Int64
  315. Int64.abs
  316. Int64.add
  317. Int64.complement
  318. Int64.dec­Eq
  319. Int64.dec­Le
  320. Int64.dec­Lt
  321. Int64.div
  322. Int64.land
  323. Int64.le
  324. Int64.lor
  325. Int64.lt
  326. Int64.max­Value
  327. Int64.min­Value
  328. Int64.mod
  329. Int64.mul
  330. Int64.neg
  331. Int64.of­Bit­Vec
  332. Int64.of­Int
  333. Int64.of­Int­LE
  334. Int64.of­Int­Truncate
  335. Int64.of­Nat
  336. Int64.shift­Left
  337. Int64.shift­Right
  338. Int64.size
  339. Int64.sub
  340. Int64.to­Bit­Vec
  341. Int64.to­Float
  342. Int64.to­Float32
  343. Int64.to­ISize
  344. Int64.to­Int
  345. Int64.to­Int16
  346. Int64.to­Int32
  347. Int64.to­Int8
  348. Int64.to­Nat­Clamp­Neg
  349. Int64.xor
  350. Int8
  351. Int8.abs
  352. Int8.add
  353. Int8.complement
  354. Int8.dec­Eq
  355. Int8.dec­Le
  356. Int8.dec­Lt
  357. Int8.div
  358. Int8.land
  359. Int8.le
  360. Int8.lor
  361. Int8.lt
  362. Int8.max­Value
  363. Int8.min­Value
  364. Int8.mod
  365. Int8.mul
  366. Int8.neg
  367. Int8.of­Bit­Vec
  368. Int8.of­Int
  369. Int8.of­Int­LE
  370. Int8.of­Int­Truncate
  371. Int8.of­Nat
  372. Int8.shift­Left
  373. Int8.shift­Right
  374. Int8.size
  375. Int8.sub
  376. Int8.to­Bit­Vec
  377. Int8.to­Float
  378. Int8.to­Float32
  379. Int8.to­ISize
  380. Int8.to­Int
  381. Int8.to­Int16
  382. Int8.to­Int32
  383. Int8.to­Int64
  384. Int8.to­Nat­Clamp­Neg
  385. Int8.xor
  386. Int­Cast
  387. IntCast.mk
    1. Instance constructor of Int­Cast
  388. Is­Infix
    1. List.Is­Infix
  389. Is­Prefix
    1. List.Is­Prefix
  390. Is­Suffix
    1. List.Is­Suffix
  391. Iterator
    1. String.Iterator
  392. i
    1. String.Iterator.i (structure field)
  393. id_map
    1. LawfulFunctor.id_map (class method)
  394. ident­Kind
    1. Lean.ident­Kind
  395. identifier
  396. identifier
    1. raw
  397. idx­Of
    1. Array.idx­Of
  398. idx­Of
    1. List.idx­Of
  399. idx­Of?
    1. Array.idx­Of?
  400. idx­Of?
    1. List.idx­Of?
  401. if ... then ... else ...
  402. if h : ... then ... else ...
  403. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  404. impredicative
  405. inaccessible
  406. ind
    1. Quot.ind
  407. ind
    1. Quotient.ind
  408. ind
    1. Squash.ind
  409. index
    1. Lean.Meta.DSimp.Config.index (structure field)
  410. index
    1. Lean.Meta.Simp.Config.index (structure field)
  411. index
    1. of inductive type
  412. indexed family
    1. of types
  413. induction
  414. induction
    1. Fin.induction
  415. induction­On
    1. Fin.induction­On
  416. induction­On
    1. Nat.div.induction­On
  417. induction­On
    1. Nat.mod.induction­On
  418. inductive.auto­Promote­Indices
  419. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  420. infer­Instance
  421. infer­Instance­As
  422. infer_instance
  423. inhabited­Left
    1. PSum.inhabited­Left
  424. inhabited­Left
    1. Sum.inhabited­Left
  425. inhabited­Right
    1. PSum.inhabited­Right
  426. inhabited­Right
    1. Sum.inhabited­Right
  427. init (Lake command)
  428. injection
  429. injections
  430. insert
    1. List.insert
  431. insert­Idx!
    1. Array.insert­Idx!
  432. insert­Idx
    1. Array.insert­Idx
  433. insert­Idx
    1. List.insert­Idx
  434. insert­Idx­If­In­Bounds
    1. Array.insert­Idx­If­In­Bounds
  435. insert­Idx­TR
    1. List.insert­Idx­TR
  436. insertion­Sort
    1. Array.insertion­Sort
  437. instance synthesis
  438. int­Cast
    1. IntCast.int­Cast (class method)
  439. int­Max
    1. BitVec.int­Max
  440. int­Min
    1. BitVec.int­Min
  441. intercalate
    1. List.intercalate
  442. intercalate
    1. String.intercalate
  443. intercalate­TR
    1. List.intercalate­TR
  444. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  445. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  446. intersperse
    1. List.intersperse
  447. intersperse­TR
    1. List.intersperse­TR
  448. intro (0) (1)
  449. intro | ... => ... | ... => ...
  450. intros
  451. inv­Image
  452. iota
    1. Lean.Meta.DSimp.Config.iota (structure field)
  453. iota
    1. Lean.Meta.Simp.Config.iota (structure field)
  454. is­Absolute
    1. System.FilePath.is­Absolute
  455. is­Alpha
    1. Char.is­Alpha
  456. is­Alphanum
    1. Char.is­Alphanum
  457. is­Digit
    1. Char.is­Digit
  458. is­Dir
    1. System.FilePath.is­Dir
  459. is­Empty
    1. Array.is­Empty
  460. is­Empty
    1. List.is­Empty
  461. is­Empty
    1. String.is­Empty
  462. is­Empty
    1. Substring.is­Empty
  463. is­Emscripten
    1. System.Platform.is­Emscripten
  464. is­Eq
    1. Ordering.is­Eq
  465. is­Eq­Some
    1. Option.is­Eq­Some
  466. is­Eqv
    1. Array.is­Eqv
  467. is­Eqv
    1. List.is­Eqv
  468. is­Exclusive­Unsafe
  469. is­Finite
    1. Float.is­Finite
  470. is­Finite
    1. Float32.is­Finite
  471. is­GE
    1. Ordering.is­GE
  472. is­GT
    1. Ordering.is­GT
  473. is­Inf
    1. Float.is­Inf
  474. is­Inf
    1. Float32.is­Inf
  475. is­Int
    1. String.is­Int
  476. is­LE
    1. Ordering.is­LE
  477. is­LT
    1. Ordering.is­LT
  478. is­Left
    1. Sum.is­Left
  479. is­Lower
    1. Char.is­Lower
  480. is­Lt
    1. Fin.is­Lt (structure field)
  481. is­Na­N
    1. Float.is­Na­N
  482. is­Na­N
    1. Float32.is­Na­N
  483. is­Nat
    1. String.is­Nat
  484. is­Nat
    1. Substring.is­Nat
  485. is­Ne
    1. Ordering.is­Ne
  486. is­None
    1. Option.is­None
  487. is­OSX
    1. System.Platform.is­OSX
  488. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  489. is­Ok
    1. Except.is­Ok
  490. is­Perm
    1. List.is­Perm
  491. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  492. is­Prefix­Of
    1. Array.is­Prefix­Of
  493. is­Prefix­Of
    1. List.is­Prefix­Of
  494. is­Prefix­Of
    1. String.is­Prefix­Of
  495. is­Prefix­Of?
    1. List.is­Prefix­Of?
  496. is­Relative
    1. System.FilePath.is­Relative
  497. is­Resolved
    1. IO.Promise.is­Resolved
  498. is­Right
    1. Sum.is­Right
  499. is­Some
    1. Option.is­Some
  500. is­Sublist
    1. List.is­Sublist
  501. is­Suffix­Of
    1. List.is­Suffix­Of
  502. is­Suffix­Of?
    1. List.is­Suffix­Of?
  503. is­Tty
    1. IO.FS.Handle.is­Tty
  504. is­Tty
    1. IO.FS.Stream.is­Tty (structure field)
  505. is­Upper
    1. Char.is­Upper
  506. is­Valid
    1. String.Pos.is­Valid
  507. is­Valid­Char
    1. Nat.is­Valid­Char
  508. is­Valid­Char
    1. UInt32.is­Valid­Char
  509. is­Valid­Char­Nat
    1. Char.is­Valid­Char­Nat
  510. is­Whitespace
    1. Char.is­Whitespace
  511. is­Windows
    1. System.Platform.is­Windows
  512. iseqv
    1. Setoid.iseqv (class method)
  513. iter
    1. String.iter
  514. iterate
  515. iterate
    1. IO.iterate
  516. iunfoldr
    1. BitVec.iunfoldr
  517. iunfoldr_replace
    1. BitVec.iunfoldr_replace

J

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

K

  1. kill
    1. IO.Process.Child.kill
  2. kleisli­Left
    1. Bind.kleisli­Left
  3. kleisli­Right
    1. Bind.kleisli­Right

L

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

M

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

N

  1. Name­Lit
    1. Lean.Syntax.Name­Lit
  2. Nat
  3. Nat.add
  4. Nat.all
  5. Nat.all­M
  6. Nat.all­TR
  7. Nat.any
  8. Nat.any­M
  9. Nat.any­TR
  10. Nat.beq
  11. Nat.bitwise
  12. Nat.ble
  13. Nat.blt
  14. Nat.case­Strong­Rec­On
  15. Nat.cases­Aux­On
  16. Nat.cast
  17. Nat.dec­Eq
  18. Nat.dec­Le
  19. Nat.dec­Lt
  20. Nat.digit­Char
  21. Nat.div
  22. Nat.div.induction­On
  23. Nat.div2Induction
  24. Nat.fold
  25. Nat.fold­M
  26. Nat.fold­Rev
  27. Nat.fold­Rev­M
  28. Nat.fold­TR
  29. Nat.for­M
  30. Nat.for­Rev­M
  31. Nat.gcd
  32. Nat.is­Power­Of­Two
  33. Nat.is­Valid­Char
  34. Nat.land
  35. Nat.lcm
  36. Nat.le
  37. Nat.le.refl
    1. Constructor of Nat.le
  38. Nat.le.step
    1. Constructor of Nat.le
  39. Nat.log2
  40. Nat.lor
  41. Nat.lt
  42. Nat.max
  43. Nat.min
  44. Nat.mod
  45. Nat.mod.induction­On
  46. Nat.mod­Core
  47. Nat.mul
  48. Nat.next­Power­Of­Two
  49. Nat.pow
  50. Nat.pred
  51. Nat.rec­Aux
  52. Nat.repeat
  53. Nat.repeat­TR
  54. Nat.repr
  55. Nat.shift­Left
  56. Nat.shift­Right
  57. Nat.strong­Rec­On
  58. Nat.sub
  59. Nat.sub­Digit­Char
  60. Nat.succ
    1. Constructor of Nat
  61. Nat.super­Digit­Char
  62. Nat.test­Bit
  63. Nat.to­Digits
  64. Nat.to­Float
  65. Nat.to­Float32
  66. Nat.to­ISize
  67. Nat.to­Int16
  68. Nat.to­Int32
  69. Nat.to­Int64
  70. Nat.to­Int8
  71. Nat.to­Sub­Digits
  72. Nat.to­Subscript­String
  73. Nat.to­Super­Digits
  74. Nat.to­Superscript­String
  75. Nat.to­UInt16
  76. Nat.to­UInt32
  77. Nat.to­UInt64
  78. Nat.to­UInt8
  79. Nat.to­USize
  80. Nat.xor
  81. Nat.zero
    1. Constructor of Nat
  82. Nat­Cast
  83. NatCast.mk
    1. Instance constructor of Nat­Cast
  84. Nat­Pow
  85. NatPow.mk
    1. Instance constructor of Nat­Pow
  86. Ne­Zero
  87. NeZero.mk
    1. Instance constructor of Ne­Zero
  88. Neg
  89. Neg.mk
    1. Instance constructor of Neg
  90. New­Goals
    1. Lean.Meta.Rewrite.New­Goals
  91. Nodup
    1. List.Nodup
  92. Nonempty
  93. Nonempty.intro
    1. Constructor of Nonempty
  94. Not
  95. Not.elim
  96. Num­Lit
    1. Lean.Syntax.Num­Lit
  97. name
    1. Lake.LeanOption.name (structure field)
  98. name­Lit­Kind
    1. Lean.name­Lit­Kind
  99. namespace
    1. of inductive type
  100. nat­Abs
    1. Int.nat­Abs
  101. nat­Add
    1. Fin.nat­Add
  102. nat­Cast
    1. NatCast.nat­Cast (class method)
  103. native­Facets
    1. [anonymous] (structure field) (0) (1)
  104. native_decide
  105. ndrec
    1. HEq.ndrec
  106. ndrec­On
    1. HEq.ndrec­On
  107. neg
    1. BitVec.neg
  108. neg
    1. Float.neg
  109. neg
    1. Float32.neg
  110. neg
    1. ISize.neg
  111. neg
    1. Int.neg
  112. neg
    1. Int16.neg
  113. neg
    1. Int32.neg
  114. neg
    1. Int64.neg
  115. neg
    1. Int8.neg
  116. neg
    1. Neg.neg (class method)
  117. neg
    1. UInt16.neg
  118. neg
    1. UInt32.neg
  119. neg
    1. UInt64.neg
  120. neg
    1. UInt8.neg
  121. neg
    1. USize.neg
  122. neg­Of­Nat
    1. Int.neg­Of­Nat
  123. neutral­Config
    1. Lean.Meta.Simp.neutral­Config
  124. new (Lake command)
  125. new
    1. IO.Promise.new
  126. new
    1. Std.Channel.new
  127. new
    1. Std.Condvar.new
  128. new
    1. Std.Mutex.new
  129. new­Goals
    1. Lean.Meta.Rewrite.Config.new­Goals (structure field)
  130. next
  131. next ... => ...
  132. next'
    1. String.next'
  133. next
    1. RandomGen.next (class method)
  134. next
    1. String.Iterator.next
  135. next
    1. String.next
  136. next
    1. Substring.next
  137. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  138. next­Until
    1. String.next­Until
  139. next­While
    1. String.next­While
  140. nextn
    1. String.Iterator.nextn
  141. nextn
    1. Substring.nextn
  142. nil
    1. BitVec.nil
  143. nofun
  144. nomatch
  145. non­Backtrackable
    1. EStateM.non­Backtrackable
  146. norm_cast (0) (1)
  147. normalize
    1. System.FilePath.normalize
  148. not
    1. BitVec.not
  149. not
    1. Bool.not
  150. not
    1. Int.not
  151. not­M
  152. notify­All
    1. Std.Condvar.notify­All
  153. notify­One
    1. Std.Condvar.notify­One
  154. null­Kind
    1. Lean.null­Kind
  155. num­Bits
    1. System.Platform.num­Bits
  156. 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.lift­Or­Get
  31. Option.lt
  32. Option.map
  33. Option.map­A
  34. Option.map­M
  35. Option.max
  36. Option.merge
  37. Option.min
  38. Option.none
    1. Constructor of Option
  39. Option.or
  40. Option.or­Else
  41. Option.pbind
  42. Option.pelim
  43. Option.pmap
  44. Option.repr
  45. Option.sequence
  46. Option.some
    1. Constructor of Option
  47. Option.to­Array
  48. Option.to­List
  49. Option.try­Catch
  50. Option.unattach
  51. Option­T
  52. OptionT.bind
  53. OptionT.fail
  54. OptionT.lift
  55. OptionT.mk
  56. OptionT.or­Else
  57. OptionT.pure
  58. OptionT.run
  59. OptionT.try­Catch
  60. Or
  61. Or.by_cases
  62. Or.by_cases'
  63. Or.inl
    1. Constructor of Or
  64. Or.inr
    1. Constructor of Or
  65. Ord
  66. Ord.lex
  67. Ord.lex'
  68. Ord.mk
    1. Instance constructor of Ord
  69. Ord.on
  70. Ord.opposite
  71. Ord.to­BEq
  72. Ord.to­LE
  73. Ord.to­LT
  74. Ordering
  75. Ordering.eq
    1. Constructor of Ordering
  76. Ordering.gt
    1. Constructor of Ordering
  77. Ordering.is­Eq
  78. Ordering.is­GE
  79. Ordering.is­GT
  80. Ordering.is­LE
  81. Ordering.is­LT
  82. Ordering.is­Ne
  83. Ordering.lt
    1. Constructor of Ordering
  84. Ordering.swap
  85. Ordering.then
  86. Output
    1. IO.Process.Output
  87. obtain
  88. occs
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  89. of­Binary­Scientific
    1. Float.of­Binary­Scientific
  90. of­Binary­Scientific
    1. Float32.of­Binary­Scientific
  91. of­Bit­Vec
    1. ISize.of­Bit­Vec
  92. of­Bit­Vec
    1. Int16.of­Bit­Vec
  93. of­Bit­Vec
    1. Int32.of­Bit­Vec
  94. of­Bit­Vec
    1. Int64.of­Bit­Vec
  95. of­Bit­Vec
    1. Int8.of­Bit­Vec
  96. of­Bits
    1. Float.of­Bits
  97. of­Bits
    1. Float32.of­Bits
  98. of­Bool
    1. BitVec.of­Bool
  99. of­Bool­List­BE
    1. BitVec.of­Bool­List­BE
  100. of­Bool­List­LE
    1. BitVec.of­Bool­List­LE
  101. of­Buffer
    1. IO.FS.Stream.of­Buffer
  102. of­Except
    1. IO.of­Except
  103. of­Except
    1. MonadExcept.of­Except
  104. of­Fin
    1. UInt16.of­Fin
  105. of­Fin
    1. UInt32.of­Fin
  106. of­Fin
    1. UInt64.of­Fin
  107. of­Fin
    1. UInt8.of­Fin
  108. of­Fin
    1. USize.of­Fin
  109. of­Fn
    1. Array.of­Fn
  110. of­Fn
    1. List.of­Fn
  111. of­Handle
    1. IO.FS.Stream.of­Handle
  112. of­Int
    1. BitVec.of­Int
  113. of­Int
    1. Float.of­Int
  114. of­Int
    1. Float32.of­Int
  115. of­Int
    1. ISize.of­Int
  116. of­Int
    1. Int16.of­Int
  117. of­Int
    1. Int32.of­Int
  118. of­Int
    1. Int64.of­Int
  119. of­Int
    1. Int8.of­Int
  120. of­Int­LE
    1. ISize.of­Int­LE
  121. of­Int­LE
    1. Int16.of­Int­LE
  122. of­Int­LE
    1. Int32.of­Int­LE
  123. of­Int­LE
    1. Int64.of­Int­LE
  124. of­Int­LE
    1. Int8.of­Int­LE
  125. of­Int­Truncate
    1. ISize.of­Int­Truncate
  126. of­Int­Truncate
    1. Int16.of­Int­Truncate
  127. of­Int­Truncate
    1. Int32.of­Int­Truncate
  128. of­Int­Truncate
    1. Int64.of­Int­Truncate
  129. of­Int­Truncate
    1. Int8.of­Int­Truncate
  130. of­Nat'
    1. Fin.of­Nat'
  131. of­Nat
    1. BitVec.of­Nat
  132. of­Nat
    1. Char.of­Nat
  133. of­Nat
    1. Float.of­Nat
  134. of­Nat
    1. Float32.of­Nat
  135. of­Nat
    1. ISize.of­Nat
  136. of­Nat
    1. Int16.of­Nat
  137. of­Nat
    1. Int32.of­Nat
  138. of­Nat
    1. Int64.of­Nat
  139. of­Nat
    1. Int8.of­Nat
  140. of­Nat
    1. OfNat.of­Nat (class method)
  141. of­Nat
    1. UInt16.of­Nat
  142. of­Nat
    1. UInt32.of­Nat
  143. of­Nat
    1. UInt64.of­Nat
  144. of­Nat
    1. UInt8.of­Nat
  145. of­Nat
    1. USize.of­Nat
  146. of­Nat32
    1. USize.of­Nat32
  147. of­Nat­LT
    1. BitVec.of­Nat­LT
  148. of­Nat­LT
    1. UInt16.of­Nat­LT
  149. of­Nat­LT
    1. UInt32.of­Nat­LT
  150. of­Nat­LT
    1. UInt64.of­Nat­LT
  151. of­Nat­LT
    1. UInt8.of­Nat­LT
  152. of­Nat­LT
    1. USize.of­Nat­LT
  153. of­Nat­Truncate
    1. UInt16.of­Nat­Truncate
  154. of­Nat­Truncate
    1. UInt32.of­Nat­Truncate
  155. of­Nat­Truncate
    1. UInt64.of­Nat­Truncate
  156. of­Nat­Truncate
    1. UInt8.of­Nat­Truncate
  157. of­Nat­Truncate
    1. USize.of­Nat­Truncate
  158. of­Scientific
    1. Float.of­Scientific
  159. of­Scientific
    1. Float32.of­Scientific
  160. of­Scientific
    1. OfScientific.of­Scientific (class method)
  161. of­Subarray
    1. Array.of­Subarray
  162. of­UInt8
    1. Char.of­UInt8
  163. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  164. offset­Of­Pos
    1. String.offset­Of­Pos
  165. omega
  166. on
    1. Ord.on
  167. open
  168. opposite
    1. Ord.opposite
  169. opt­Param
  170. optional
  171. or
    1. BitVec.or
  172. or
    1. Bool.or
  173. or
    1. List.or
  174. or
    1. Option.or
  175. or­Else'
    1. EStateM.or­Else'
  176. or­Else
    1. EStateM.or­Else
  177. or­Else
    1. MonadExcept.or­Else
  178. or­Else
    1. Option.or­Else
  179. or­Else
    1. OptionT.or­Else
  180. or­Else
    1. ReaderT.or­Else
  181. or­Else
    1. StateT.or­Else
  182. or­Else
    1. [anonymous] (class method)
  183. or­Else­Lazy
    1. Except.or­Else­Lazy
  184. or­M
  185. orelse'
    1. MonadExcept.orelse'
  186. other
    1. IO.FileRight.other (structure field)
  187. out
    1. NeZero.out (class method)
  188. out­Param
  189. output
    1. IO.Process.output
  190. override list (Elan command)
  191. override set (Elan command)
  192. override unset (Elan command)

P

  1. PEmpty
  2. PEmpty.elim
  3. PLift
  4. PLift.up
    1. Constructor of PLift
  5. PProd
  6. PProd.mk
    1. Constructor of PProd
  7. PSigma
  8. PSigma.mk
    1. Constructor of PSigma
  9. PSum
  10. PSum.inhabited­Left
  11. PSum.inhabited­Right
  12. PSum.inl
    1. Constructor of PSum
  13. PSum.inr
    1. Constructor of PSum
  14. PUnit
  15. PUnit.unit
    1. Constructor of PUnit
  16. Pairwise
    1. List.Pairwise
  17. Partial­Order
    1. Lean.Order.Partial­Order
  18. Perm
    1. List.Perm
  19. Pos
    1. String.Pos
  20. Pow
  21. Pow.mk
    1. Instance constructor of Pow
  22. Prec
    1. Lean.Syntax.Prec
  23. Preresolved
    1. Lean.Syntax.Preresolved
  24. Prio
    1. Lean.Syntax.Prio
  25. Priority
    1. Task.Priority
  26. Prod
  27. Prod.all­I
  28. Prod.any­I
  29. Prod.fold­I
  30. Prod.lex­Lt
  31. Prod.map
  32. Prod.mk
    1. Constructor of Prod
  33. Prod.swap
  34. Promise
    1. IO.Promise
  35. Prop
  36. Pure
  37. Pure.mk
    1. Instance constructor of Pure
  38. pack (Lake command)
  39. parameter
    1. of inductive type
  40. parent
    1. System.FilePath.parent
  41. parser
  42. partition
    1. Array.partition
  43. partition
    1. List.partition
  44. partition­M
    1. List.partition­M
  45. partition­Map
    1. List.partition­Map
  46. path
    1. IO.FS.DirEntry.path
  47. path­Exists
    1. System.FilePath.path­Exists
  48. path­Separator
    1. System.FilePath.path­Separator
  49. path­Separators
    1. System.FilePath.path­Separators
  50. pattern
  51. pbind
    1. Option.pbind
  52. pelim
    1. Option.pelim
  53. placeholder term
  54. pmap
    1. Array.pmap
  55. pmap
    1. List.pmap
  56. pmap
    1. Option.pmap
  57. polymorphism
    1. universe
  58. pop
    1. Array.pop
  59. pop­Front
    1. Subarray.pop­Front
  60. pop­While
    1. Array.pop­While
  61. pos
    1. IO.FS.Stream.Buffer.pos (structure field)
  62. pos
    1. String.Iterator.pos
  63. pos­Of
    1. String.pos­Of
  64. pos­Of
    1. Substring.pos­Of
  65. pow
    1. Float.pow
  66. pow
    1. Float32.pow
  67. pow
    1. HomogeneousPow.pow (class method)
  68. pow
    1. Int.pow
  69. pow
    1. Nat.pow
  70. pow
    1. NatPow.pow (class method)
  71. pow
    1. Pow.pow (class method)
  72. pp
    1. eval.pp
  73. pp.deep­Terms
  74. pp.deepTerms.threshold
  75. pp.field­Notation
  76. pp.match
  77. pp.max­Steps
  78. pp.mvars
  79. pp.proofs
  80. pp.proofs.threshold
  81. precompile­Modules
    1. [anonymous] (structure field)
  82. pred
    1. Fin.pred
  83. pred
    1. Nat.pred
  84. predicative
  85. prev
    1. String.Iterator.prev
  86. prev
    1. String.prev
  87. prev
    1. Substring.prev
  88. prevn
    1. String.Iterator.prevn
  89. prevn
    1. Substring.prevn
  90. print
    1. IO.print
  91. println
    1. IO.println
  92. proj
    1. Lean.Meta.DSimp.Config.proj (structure field)
  93. proj
    1. Lean.Meta.Simp.Config.proj (structure field)
  94. proof state
  95. proofs
    1. pp.proofs
  96. property
    1. Subtype.property (structure field)
  97. propext
  98. proposition
  99. proposition
    1. decidable
  100. ptr­Addr­Unsafe
  101. ptr­Eq
  102. ptr­Eq
    1. ST.Ref.ptr­Eq
  103. ptr­Eq­List
  104. pure
    1. EStateM.pure
  105. pure
    1. Except.pure
  106. pure
    1. ExceptT.pure
  107. pure
    1. OptionT.pure
  108. pure
    1. Pure.pure (class method)
  109. pure
    1. ReaderT.pure
  110. pure
    1. StateT.pure
  111. pure
    1. Task.pure
  112. pure
    1. Thunk.pure
  113. pure_bind
    1. [anonymous] (class method)
  114. pure_seq
    1. [anonymous] (class method)
  115. push
    1. Array.push
  116. push
    1. String.push
  117. push_cast
  118. pushn
    1. String.pushn
  119. put­Str
    1. IO.FS.Handle.put­Str
  120. put­Str
    1. IO.FS.Stream.put­Str (structure field)
  121. put­Str­Ln
    1. IO.FS.Handle.put­Str­Ln
  122. 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. Reader­M
  4. Reader­T
  5. ReaderT.adapt
  6. ReaderT.bind
  7. ReaderT.failure
  8. ReaderT.or­Else
  9. ReaderT.pure
  10. ReaderT.read
  11. ReaderT.run
  12. Ref
    1. IO.Ref
  13. Ref
    1. ST.Ref
  14. Result
    1. EStateM.Result
  15. r
    1. Setoid.r (class method)
  16. rand
    1. IO.rand
  17. rand­Bool
  18. rand­Nat
  19. range'
    1. Array.range'
  20. range'
    1. List.range'
  21. range'TR
    1. List.range'TR
  22. range
    1. Array.range
  23. range
    1. List.range
  24. range
    1. RandomGen.range (class method)
  25. raw
    1. Lean.TSyntax.raw (structure field)
  26. rcases
  27. read
    1. IO.AccessRight.read (structure field)
  28. read
    1. IO.FS.Handle.read
  29. read
    1. IO.FS.Stream.read (structure field)
  30. read
    1. MonadReader.read (class method)
  31. read
    1. Monad­ReaderOf.read (class method)
  32. read
    1. ReaderT.read
  33. read­Bin­File
    1. IO.FS.read­Bin­File
  34. read­Bin­To­End
    1. IO.FS.Handle.read­Bin­To­End
  35. read­Bin­To­End­Into
    1. IO.FS.Handle.read­Bin­To­End­Into
  36. read­Dir
    1. System.FilePath.read­Dir
  37. read­File
    1. IO.FS.read­File
  38. read­The
  39. read­To­End
    1. IO.FS.Handle.read­To­End
  40. real­Path
    1. IO.FS.real­Path
  41. rec
    1. Quot.rec
  42. rec
    1. Quotient.rec
  43. rec­Aux
    1. Nat.rec­Aux
  44. rec­On
    1. Quot.rec­On
  45. rec­On
    1. Quotient.rec­On
  46. rec­On­Subsingleton
    1. Quot.rec­On­Subsingleton
  47. rec­On­Subsingleton
    1. Quotient.rec­On­Subsingleton
  48. rec­On­Subsingleton₂
    1. Quotient.rec­On­Subsingleton₂
  49. recursor
  50. recv?
    1. Std.Channel.Sync.recv?
  51. recv?
    1. Std.Channel.recv?
  52. recv­All­Current
    1. Std.Channel.recv­All­Current
  53. reduce
  54. reduction
    1. ι (iota)
  55. refine
  56. refine'
  57. refl
    1. Equivalence.refl (structure field)
  58. refl
    1. Setoid.refl
  59. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  60. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  61. rel
    1. Lean.Order.PartialOrder.rel (class method)
  62. rel
    1. Well­FoundedRelation.rel (class method)
  63. rel_antisymm
    1. Lean.Order.PartialOrder.rel_antisymm (class method)
  64. rel_refl
    1. Lean.Order.PartialOrder.rel_refl (class method)
  65. rel_trans
    1. Lean.Order.PartialOrder.rel_trans (class method)
  66. relaxed­Auto­Implicit
  67. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  68. remaining­To­String
    1. String.Iterator.remaining­To­String
  69. remove­All
    1. List.remove­All
  70. remove­Dir
    1. IO.FS.remove­Dir
  71. remove­Dir­All
    1. IO.FS.remove­Dir­All
  72. remove­File
    1. IO.FS.remove­File
  73. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  74. rename
  75. rename
    1. IO.FS.rename
  76. rename_i
  77. repeat (0) (1)
  78. repeat'
  79. repeat
    1. Nat.repeat
  80. repeat1'
  81. repeat­TR
    1. Nat.repeat­TR
  82. replace
  83. replace
    1. Array.replace
  84. replace
    1. List.replace
  85. replace
    1. String.replace
  86. replace­TR
    1. List.replace­TR
  87. replicate
    1. Array.replicate
  88. replicate
    1. BitVec.replicate
  89. replicate
    1. List.replicate
  90. replicate­TR
    1. List.replicate­TR
  91. repr
    1. Int.repr
  92. repr
    1. Nat.repr
  93. repr
    1. Option.repr
  94. repr
    1. USize.repr
  95. repr
    1. eval.derive.repr
  96. resolve
    1. IO.Promise.resolve
  97. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  98. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  99. restore
    1. EStateM.Backtrackable.restore (class method)
  100. restore­M
    1. MonadControl.restore­M (class method)
  101. restore­M
    1. Monad­ControlT.restore­M (class method)
  102. result!
    1. IO.Promise.result!
  103. result
    1. trace.compiler.ir.result
  104. result?
    1. IO.Promise.result?
  105. result­D
    1. IO.Promise.result­D
  106. rev
    1. Fin.rev
  107. rev­Find
    1. String.rev­Find
  108. rev­Pos­Of
    1. String.rev­Pos­Of
  109. reverse
    1. Array.reverse
  110. reverse
    1. BitVec.reverse
  111. reverse
    1. List.reverse
  112. reverse­Induction
    1. Fin.reverse­Induction
  113. revert
  114. rewind
    1. IO.FS.Handle.rewind
  115. rewrite (0) (1)
  116. rewrite
    1. trace.Meta.Tactic.simp.rewrite
  117. rfl (0) (1) (2)
  118. rfl'
  119. rfl
    1. HEq.rfl
  120. rfl
    1. LawfulBEq.rfl (class method)
  121. rhs
  122. right (0) (1)
  123. right
    1. And.right (structure field)
  124. rightpad
    1. Array.rightpad
  125. rightpad
    1. List.rightpad
  126. rintro
  127. root
    1. IO.FS.DirEntry.root (structure field)
  128. root
    1. [anonymous] (structure field)
  129. roots
    1. [anonymous] (structure field)
  130. rotate­Left
    1. BitVec.rotate­Left
  131. rotate­Left
    1. List.rotate­Left
  132. rotate­Right
    1. BitVec.rotate­Right
  133. rotate­Right
    1. List.rotate­Right
  134. rotate_left
  135. rotate_right
  136. round
    1. Float.round
  137. round
    1. Float32.round
  138. run (Elan command)
  139. run'
    1. EStateM.run'
  140. run'
    1. State­CpsT.run'
  141. run'
    1. State­RefT'.run'
  142. run'
    1. StateT.run'
  143. run
    1. EStateM.run
  144. run
    1. Except­CpsT.run
  145. run
    1. ExceptT.run
  146. run
    1. IO.Process.run
  147. run
    1. Id.run
  148. run
    1. OptionT.run
  149. run
    1. ReaderT.run
  150. run
    1. State­CpsT.run
  151. run
    1. State­RefT'.run
  152. run
    1. StateT.run
  153. run­Catch
    1. Except­CpsT.run­Catch
  154. run­EST
  155. run­K
    1. Except­CpsT.run­K
  156. run­K
    1. State­CpsT.run­K
  157. run­ST
  158. run_tac
  159. rw (0) (1)
  160. rw?
  161. rw_mod_cast
  162. rwa

S

  1. ST
  2. ST.Ref
  3. ST.Ref.get
  4. ST.Ref.mk
    1. Constructor of ST.Ref
  5. ST.Ref.modify
  6. ST.Ref.modify­Get
  7. ST.Ref.ptr­Eq
  8. ST.Ref.set
  9. ST.Ref.swap
  10. ST.Ref.take
  11. ST.Ref.to­Monad­State­Of
  12. ST.mk­Ref
  13. STWorld
  14. STWorld.mk
    1. Instance constructor of STWorld
  15. Scientific­Lit
    1. Lean.Syntax.Scientific­Lit
  16. Script­M
    1. Lake.Script­M (0) (1)
  17. Seq
  18. Seq.mk
    1. Instance constructor of Seq
  19. Seq­Left
  20. SeqLeft.mk
    1. Instance constructor of Seq­Left
  21. Seq­Right
  22. SeqRight.mk
    1. Instance constructor of Seq­Right
  23. Setoid
  24. Setoid.mk
    1. Instance constructor of Setoid
  25. Setoid.refl
  26. Setoid.symm
  27. Setoid.trans
  28. Shift­Left
  29. ShiftLeft.mk
    1. Instance constructor of Shift­Left
  30. Shift­Right
  31. ShiftRight.mk
    1. Instance constructor of Shift­Right
  32. Sigma
  33. Sigma.mk
    1. Constructor of Sigma
  34. Simp­Extension
    1. Lean.Meta.Simp­Extension
  35. Size­Of
  36. SizeOf.mk
    1. Instance constructor of Size­Of
  37. Sort
  38. Source­Info
    1. Lean.Source­Info
  39. Spawn­Args
    1. IO.Process.Spawn­Args
  40. Squash
  41. Squash.ind
  42. Squash.lift
  43. Squash.mk
  44. State­Cps­T
  45. State­CpsT.lift
  46. State­CpsT.run
  47. State­CpsT.run'
  48. State­CpsT.run­K
  49. State­M
  50. State­Ref­T'
  51. State­RefT'.get
  52. State­RefT'.lift
  53. State­RefT'.modify­Get
  54. State­RefT'.run
  55. State­RefT'.run'
  56. State­RefT'.set
  57. State­T
  58. StateT.bind
  59. StateT.failure
  60. StateT.get
  61. StateT.lift
  62. StateT.map
  63. StateT.modify­Get
  64. StateT.or­Else
  65. StateT.pure
  66. StateT.run
  67. StateT.run'
  68. StateT.set
  69. Std.Atomic­T
  70. Std.Channel
  71. Std.Channel.Sync
  72. Std.Channel.Sync.recv?
  73. Std.Channel.close
  74. Std.Channel.for­Async
  75. Std.Channel.new
  76. Std.Channel.recv?
  77. Std.Channel.recv­All­Current
  78. Std.Channel.send
  79. Std.Channel.sync
  80. Std.Condvar
  81. Std.Condvar.new
  82. Std.Condvar.notify­All
  83. Std.Condvar.notify­One
  84. Std.Condvar.wait
  85. Std.Condvar.wait­Until
  86. Std.Mutex
  87. Std.Mutex.atomically
  88. Std.Mutex.atomically­Once
  89. Std.Mutex.new
  90. Std­Gen
  91. Stdio
    1. IO.Process.Stdio
  92. Stdio­Config
    1. IO.Process.Stdio­Config
  93. Str­Lit
    1. Lean.Syntax.Str­Lit
  94. Stream
    1. IO.FS.Stream
  95. String
  96. String.Iterator
  97. String.Iterator.at­End
  98. String.Iterator.curr
  99. String.Iterator.extract
  100. String.Iterator.forward
  101. String.Iterator.has­Next
  102. String.Iterator.has­Prev
  103. String.Iterator.mk
    1. Constructor of String.Iterator
  104. String.Iterator.next
  105. String.Iterator.nextn
  106. String.Iterator.pos
  107. String.Iterator.prev
  108. String.Iterator.prevn
  109. String.Iterator.remaining­Bytes
  110. String.Iterator.remaining­To­String
  111. String.Iterator.set­Curr
  112. String.Iterator.to­End
  113. String.Pos
  114. String.Pos.is­Valid
  115. String.Pos.min
  116. String.Pos.mk
    1. Constructor of String.Pos
  117. String.all
  118. String.any
  119. String.append
  120. String.at­End
  121. String.back
  122. String.capitalize
  123. String.contains
  124. String.crlf­To­Lf
  125. String.dec­Eq
  126. String.decapitalize
  127. String.drop
  128. String.drop­Prefix?
  129. String.drop­Right
  130. String.drop­Right­While
  131. String.drop­Suffix?
  132. String.drop­While
  133. String.end­Pos
  134. String.ends­With
  135. String.extract
  136. String.find
  137. String.find­Line­Start
  138. String.first­Diff­Pos
  139. String.foldl
  140. String.foldr
  141. String.from­UTF8
  142. String.from­UTF8!
  143. String.from­UTF8?
  144. String.front
  145. String.get
  146. String.get!
  147. String.get'
  148. String.get?
  149. String.get­Utf8Byte
  150. String.hash
  151. String.intercalate
  152. String.is­Empty
  153. String.is­Int
  154. String.is­Nat
  155. String.is­Prefix­Of
  156. String.iter
  157. String.join
  158. String.le
  159. String.length
  160. String.map
  161. String.mk
    1. Constructor of String
  162. String.mk­Iterator
  163. String.modify
  164. String.next
  165. String.next'
  166. String.next­Until
  167. String.next­While
  168. String.offset­Of­Pos
  169. String.pos­Of
  170. String.prev
  171. String.push
  172. String.pushn
  173. String.quote
  174. String.remove­Leading­Spaces
  175. String.replace
  176. String.rev­Find
  177. String.rev­Pos­Of
  178. String.set
  179. String.singleton
  180. String.split
  181. String.split­On
  182. String.starts­With
  183. String.strip­Prefix
  184. String.strip­Suffix
  185. String.substr­Eq
  186. String.take
  187. String.take­Right
  188. String.take­Right­While
  189. String.take­While
  190. String.to­Format
  191. String.to­Int!
  192. String.to­Int?
  193. String.to­List
  194. String.to­Lower
  195. String.to­Name
  196. String.to­Nat!
  197. String.to­Nat?
  198. String.to­Substring
  199. String.to­Substring'
  200. String.to­UTF8
  201. String.to­Upper
  202. String.trim
  203. String.trim­Left
  204. String.trim­Right
  205. String.utf8Byte­Size
  206. String.utf8Decode­Char?
  207. String.utf8Encode­Char
  208. String.validate­UTF8
  209. Sub
  210. Sub.mk
    1. Instance constructor of Sub
  211. Subarray
  212. Subarray.all
  213. Subarray.all­M
  214. Subarray.any
  215. Subarray.any­M
  216. Subarray.drop
  217. Subarray.empty
  218. Subarray.find­Rev?
  219. Subarray.find­Rev­M?
  220. Subarray.find­Some­Rev­M?
  221. Subarray.foldl
  222. Subarray.foldl­M
  223. Subarray.foldr
  224. Subarray.foldr­M
  225. Subarray.for­In
  226. Subarray.for­M
  227. Subarray.for­Rev­M
  228. Subarray.get
  229. Subarray.get!
  230. Subarray.get­D
  231. Subarray.mk
    1. Constructor of Subarray
  232. Subarray.pop­Front
  233. Subarray.size
  234. Subarray.split
  235. Subarray.take
  236. Subarray.to­Array
  237. Sublist
    1. List.Sublist
  238. Subsingleton
  239. Subsingleton.elim
  240. Subsingleton.helim
  241. Subsingleton.intro
    1. Instance constructor of Subsingleton
  242. Substring
  243. Substring.all
  244. Substring.any
  245. Substring.at­End
  246. Substring.beq
  247. Substring.bsize
  248. Substring.common­Prefix
  249. Substring.common­Suffix
  250. Substring.contains
  251. Substring.drop
  252. Substring.drop­Prefix?
  253. Substring.drop­Right
  254. Substring.drop­Right­While
  255. Substring.drop­Suffix?
  256. Substring.drop­While
  257. Substring.extract
  258. Substring.foldl
  259. Substring.foldr
  260. Substring.front
  261. Substring.get
  262. Substring.is­Empty
  263. Substring.is­Nat
  264. Substring.mk
    1. Constructor of Substring
  265. Substring.next
  266. Substring.nextn
  267. Substring.pos­Of
  268. Substring.prev
  269. Substring.prevn
  270. Substring.same­As
  271. Substring.split­On
  272. Substring.take
  273. Substring.take­Right
  274. Substring.take­Right­While
  275. Substring.take­While
  276. Substring.to­Iterator
  277. Substring.to­Name
  278. Substring.to­Nat?
  279. Substring.to­String
  280. Substring.trim
  281. Substring.trim­Left
  282. Substring.trim­Right
  283. Subtype
  284. Subtype.mk
    1. Constructor of Subtype
  285. Sum
  286. Sum.elim
  287. Sum.get­Left
  288. Sum.get­Left?
  289. Sum.get­Right
  290. Sum.get­Right?
  291. Sum.inhabited­Left
  292. Sum.inhabited­Right
  293. Sum.inl
    1. Constructor of Sum
  294. Sum.inr
    1. Constructor of Sum
  295. Sum.is­Left
  296. Sum.is­Right
  297. Sum.map
  298. Sum.swap
  299. Sync
    1. Std.Channel.Sync
  300. Syntax
    1. Lean.Syntax
  301. Syntax­Node­Kind
    1. Lean.Syntax­Node­Kind
  302. Syntax­Node­Kinds
    1. Lean.Syntax­Node­Kinds
  303. System.File­Path
  304. System.FilePath.add­Extension
  305. System.FilePath.components
  306. System.FilePath.exe­Extension
  307. System.FilePath.ext­Separator
  308. System.FilePath.extension
  309. System.FilePath.file­Name
  310. System.FilePath.file­Stem
  311. System.FilePath.is­Absolute
  312. System.FilePath.is­Dir
  313. System.FilePath.is­Relative
  314. System.FilePath.join
  315. System.FilePath.metadata
  316. System.FilePath.mk
    1. Constructor of System.File­Path
  317. System.FilePath.normalize
  318. System.FilePath.parent
  319. System.FilePath.path­Exists
  320. System.FilePath.path­Separator
  321. System.FilePath.path­Separators
  322. System.FilePath.read­Dir
  323. System.FilePath.walk­Dir
  324. System.FilePath.with­Extension
  325. System.FilePath.with­File­Name
  326. System.Platform.is­Emscripten
  327. System.Platform.is­OSX
  328. System.Platform.is­Windows
  329. System.Platform.num­Bits
  330. System.Platform.target
  331. System.mk­File­Path
  332. s
    1. String.Iterator.s (structure field)
  333. sadd­Overflow
    1. BitVec.sadd­Overflow
  334. same­As
    1. Substring.same­As
  335. save
    1. EStateM.Backtrackable.save (class method)
  336. scale­B
    1. Float.scale­B
  337. scale­B
    1. Float32.scale­B
  338. scientific­Lit­Kind
    1. Lean.scientific­Lit­Kind
  339. script doc (Lake command)
  340. script list (Lake command)
  341. script run (Lake command)
  342. sdiv
    1. BitVec.sdiv
  343. self uninstall (Elan command)
  344. self update (Elan command)
  345. semi­Out­Param
  346. send
    1. Std.Channel.send
  347. seq
    1. Seq.seq (class method)
  348. seq­Left
    1. SeqLeft.seq­Left (class method)
  349. seq­Left_eq
    1. [anonymous] (class method)
  350. seq­Right
    1. EStateM.seq­Right
  351. seq­Right
    1. SeqRight.seq­Right (class method)
  352. seq­Right_eq
    1. [anonymous] (class method)
  353. seq_assoc
    1. LawfulApplicative.pure_seq (class method)
  354. seq_pure
    1. LawfulApplicative.seq­Right_eq (class method)
  355. sequence
    1. Option.sequence
  356. serve (Lake command)
  357. set!
    1. Array.set!
  358. set
    1. Array.set
  359. set
    1. EStateM.set
  360. set
    1. List.set
  361. set
    1. MonadState.set (class method)
  362. set
    1. Monad­StateOf.set (class method)
  363. set
    1. ST.Ref.set
  364. set
    1. State­RefT'.set
  365. set
    1. StateT.set
  366. set
    1. String.set
  367. set­Access­Rights
    1. IO.set­Access­Rights
  368. set­Curr
    1. String.Iterator.set­Curr
  369. set­Current­Dir
    1. IO.Process.set­Current­Dir
  370. set­If­In­Bounds
    1. Array.set­If­In­Bounds
  371. set­Kind
    1. Lean.Syntax.set­Kind
  372. set­Rand­Seed
    1. IO.set­Rand­Seed
  373. set­Stderr
    1. IO.set­Stderr
  374. set­Stdin
    1. IO.set­Stdin
  375. set­Stdout
    1. IO.set­Stdout
  376. set­TR
    1. List.set­TR
  377. set­Width'
    1. BitVec.set­Width'
  378. set­Width
    1. BitVec.set­Width
  379. set_option
  380. setsid
    1. IO.Process.SpawnArgs.args (structure field)
  381. shift­Concat
    1. BitVec.shift­Concat
  382. shift­Left
    1. BitVec.shift­Left
  383. shift­Left
    1. Fin.shift­Left
  384. shift­Left
    1. ISize.shift­Left
  385. shift­Left
    1. Int16.shift­Left
  386. shift­Left
    1. Int32.shift­Left
  387. shift­Left
    1. Int64.shift­Left
  388. shift­Left
    1. Int8.shift­Left
  389. shift­Left
    1. Nat.shift­Left
  390. shift­Left
    1. ShiftLeft.shift­Left (class method)
  391. shift­Left
    1. UInt16.shift­Left
  392. shift­Left
    1. UInt32.shift­Left
  393. shift­Left
    1. UInt64.shift­Left
  394. shift­Left
    1. UInt8.shift­Left
  395. shift­Left
    1. USize.shift­Left
  396. shift­Left­Rec
    1. BitVec.shift­Left­Rec
  397. shift­Left­Zero­Extend
    1. BitVec.shift­Left­Zero­Extend
  398. shift­Right
    1. Fin.shift­Right
  399. shift­Right
    1. ISize.shift­Right
  400. shift­Right
    1. Int.shift­Right
  401. shift­Right
    1. Int16.shift­Right
  402. shift­Right
    1. Int32.shift­Right
  403. shift­Right
    1. Int64.shift­Right
  404. shift­Right
    1. Int8.shift­Right
  405. shift­Right
    1. Nat.shift­Right
  406. shift­Right
    1. ShiftRight.shift­Right (class method)
  407. shift­Right
    1. UInt16.shift­Right
  408. shift­Right
    1. UInt32.shift­Right
  409. shift­Right
    1. UInt64.shift­Right
  410. shift­Right
    1. UInt8.shift­Right
  411. shift­Right
    1. USize.shift­Right
  412. show
  413. show (Elan command)
  414. show_term
  415. shrink
    1. Array.shrink
  416. sign
    1. Int.sign
  417. sign­Extend
    1. BitVec.sign­Extend
  418. simp (0) (1)
  419. simp!
  420. simp?
  421. simp?!
  422. simp_all
  423. simp_all!
  424. simp_all?
  425. simp_all?!
  426. simp_all_arith
  427. simp_all_arith!
  428. simp_arith
  429. simp_arith!
  430. simp_match
  431. simp_wf
  432. simpa
  433. simpa!
  434. simpa?
  435. simpa?!
  436. simprocs
  437. sin
    1. Float.sin
  438. sin
    1. Float32.sin
  439. single­Pass
    1. Lean.Meta.Simp.Config.single­Pass (structure field)
  440. singleton
    1. Array.singleton
  441. singleton
    1. List.singleton
  442. singleton
    1. String.singleton
  443. sinh
    1. Float.sinh
  444. sinh
    1. Float32.sinh
  445. size
    1. Array.size
  446. size
    1. ISize.size
  447. size
    1. Int16.size
  448. size
    1. Int32.size
  449. size
    1. Int64.size
  450. size
    1. Int8.size
  451. size
    1. Subarray.size
  452. size
    1. UInt16.size
  453. size
    1. UInt32.size
  454. size
    1. UInt64.size
  455. size
    1. UInt8.size
  456. size
    1. USize.size
  457. size­Of
    1. SizeOf.size­Of (class method)
  458. skip (0) (1)
  459. skip­Assigned­Instances
    1. tactic.skip­Assigned­Instances
  460. sle
    1. BitVec.sle
  461. sleep
  462. sleep
    1. IO.sleep
  463. slt
    1. BitVec.slt
  464. smod
    1. BitVec.smod
  465. smt­SDiv
    1. BitVec.smt­SDiv
  466. smt­UDiv
    1. BitVec.smt­UDiv
  467. snd
    1. MProd.snd (structure field)
  468. snd
    1. PProd.snd (structure field)
  469. snd
    1. PSigma.snd (structure field)
  470. snd
    1. Prod.snd (structure field)
  471. snd
    1. Sigma.snd (structure field)
  472. solve
  473. solve_by_elim
  474. sorry
  475. sound
    1. Quot.sound
  476. sound
    1. Quotient.sound
  477. span
    1. List.span
  478. spawn
    1. IO.Process.spawn
  479. spawn
    1. Task.spawn
  480. specialize
  481. split
  482. split
    1. RandomGen.split (class method)
  483. split
    1. String.split
  484. split
    1. Subarray.split
  485. split­At
    1. List.split­At
  486. split­By
    1. List.split­By
  487. split­On
    1. String.split­On
  488. split­On
    1. Substring.split­On
  489. sqrt
    1. Float.sqrt
  490. sqrt
    1. Float32.sqrt
  491. src­Dir
    1. [anonymous] (structure field) (0) (1)
  492. srem
    1. BitVec.srem
  493. sshift­Right'
    1. BitVec.sshift­Right'
  494. sshift­Right
    1. BitVec.sshift­Right
  495. sshift­Right­Rec
    1. BitVec.sshift­Right­Rec
  496. ssub­Overflow
    1. BitVec.ssub­Overflow
  497. st­M
    1. MonadControl.st­M (class method)
  498. st­M
    1. Monad­ControlT.st­M (class method)
  499. start
    1. Subarray.start (structure field)
  500. start­Pos
    1. Substring.start­Pos (structure field)
  501. start_le_stop
    1. Subarray.start_le_stop (structure field)
  502. starts­With
    1. String.starts­With
  503. std­Next
  504. std­Range
  505. std­Split
  506. stderr
    1. IO.Process.Child.stderr (structure field)
  507. stderr
    1. IO.Process.Output.stderr (structure field)
  508. stderr
    1. IO.Process.StdioConfig.stderr (structure field)
  509. stdin
    1. IO.Process.Child.stdin (structure field)
  510. stdin
    1. IO.Process.StdioConfig.stdin (structure field)
  511. stdout
    1. IO.Process.Child.stdout (structure field)
  512. stdout
    1. IO.Process.Output.stdout (structure field)
  513. stdout
    1. IO.Process.StdioConfig.stdout (structure field)
  514. stop
  515. stop
    1. Subarray.stop (structure field)
  516. stop­Pos
    1. Substring.stop­Pos (structure field)
  517. stop_le_array_size
    1. Subarray.stop_le_array_size (structure field)
  518. str
    1. Substring.str (structure field)
  519. str­Lit­Kind
    1. Lean.str­Lit­Kind
  520. strip­Prefix
    1. String.strip­Prefix
  521. strip­Suffix
    1. String.strip­Suffix
  522. strong­Rec­On
    1. Nat.strong­Rec­On
  523. sub
    1. BitVec.sub
  524. sub
    1. Fin.sub
  525. sub
    1. Float.sub
  526. sub
    1. Float32.sub
  527. sub
    1. ISize.sub
  528. sub
    1. Int.sub
  529. sub
    1. Int16.sub
  530. sub
    1. Int32.sub
  531. sub
    1. Int64.sub
  532. sub
    1. Int8.sub
  533. sub
    1. Nat.sub
  534. sub
    1. Sub.sub (class method)
  535. sub
    1. UInt16.sub
  536. sub
    1. UInt32.sub
  537. sub
    1. UInt64.sub
  538. sub
    1. UInt8.sub
  539. sub
    1. USize.sub
  540. sub­Digit­Char
    1. Nat.sub­Digit­Char
  541. sub­Nat
    1. Fin.sub­Nat
  542. sub­Nat­Nat
    1. Int.sub­Nat­Nat
  543. subst
  544. subst
    1. Eq.subst
  545. subst
    1. HEq.subst
  546. subst_eqs
  547. subst_vars
  548. substr­Eq
    1. String.substr­Eq
  549. succ
    1. Fin.succ
  550. succ­Rec
    1. Fin.succ­Rec
  551. succ­Rec­On
    1. Fin.succ­Rec­On
  552. suffices
  553. sum
    1. Array.sum
  554. sum
    1. List.sum
  555. super­Digit­Char
    1. Nat.super­Digit­Char
  556. support­Interpreter
    1. [anonymous] (structure field)
  557. swap
    1. Array.swap
  558. swap
    1. Ordering.swap
  559. swap
    1. Prod.swap
  560. swap
    1. ST.Ref.swap
  561. swap
    1. Sum.swap
  562. swap­At!
    1. Array.swap­At!
  563. swap­At
    1. Array.swap­At
  564. swap­If­In­Bounds
    1. Array.swap­If­In­Bounds
  565. symm
  566. symm
    1. Eq.symm
  567. symm
    1. Equivalence.symm (structure field)
  568. symm
    1. Setoid.symm
  569. symm_saturate
  570. sync
    1. Std.Channel.sync
  571. synthInstance.max­Heartbeats
  572. synthInstance.max­Size
  573. synthesis
    1. of type class instances

T

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

V

  1. val
    1. Char.val (structure field)
  2. val
    1. Fin.val (structure field)
  3. val
    1. Subtype.val (structure field)
  4. valid
    1. Char.valid (structure field)
  5. validate­UTF8
    1. String.validate­UTF8
  6. value
    1. For­InStep.value
  7. value
    1. Lake.LeanOption.value (structure field)

W

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

X

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

Z

  1. Zero
  2. Zero.mk
    1. Instance constructor of Zero
  3. zero
    1. BitVec.zero
  4. zero
    1. Zero.zero (class method)
  5. zero­Extend
    1. BitVec.zero­Extend
  6. zeta
  7. zeta
    1. Lean.Meta.DSimp.Config.zeta (structure field)
  8. zeta
    1. Lean.Meta.Simp.Config.zeta (structure field)
  9. zeta­Delta
    1. Lean.Meta.DSimp.Config.zeta­Delta (structure field)
  10. zeta­Delta
    1. Lean.Meta.Simp.Config.zeta­Delta (structure field)
  11. zeta­Unused
    1. Lean.Meta.DSimp.Config.zeta­Unused (structure field)
  12. zeta­Unused
    1. Lean.Meta.Simp.Config.zeta­Unused (structure field)
  13. zip
    1. Array.zip
  14. zip
    1. List.zip
  15. zip­Idx
    1. Array.zip­Idx
  16. zip­Idx
    1. List.zip­Idx
  17. zip­Idx­TR
    1. List.zip­Idx­TR
  18. zip­With
    1. Array.zip­With
  19. zip­With
    1. List.zip­With
  20. zip­With­All
    1. Array.zip­With­All
  21. zip­With­All
    1. List.zip­With­All
  22. zip­With­TR
    1. List.zip­With­TR