Index

Symbols

  1. ( ... )
  2. . ...
  3. <;> (0) (1)
  4. _private.Init.Dynamic.0.TypeName.data
  5. { ... }
  6. ·
  7. · ...
  8. ι-reduction

A

  1. Add
  2. Add.add
  3. Append
  4. Append.append
  5. Array
  6. Array.all
  7. Array.all­Diff
  8. Array.all­M
  9. Array.any
  10. Array.any­M
  11. Array.append
  12. Array.append­List
  13. Array.attach
  14. Array.attach­With
  15. Array.back
  16. Array.back!
  17. Array.back?
  18. Array.bin­Insert
  19. Array.bin­Insert­M
  20. Array.bin­Search
  21. Array.bin­Search­Contains
  22. Array.concat­Map
  23. Array.concat­Map­M
  24. Array.contains
  25. Array.elem
  26. Array.empty
  27. Array.erase
  28. Array.erase­Idx
  29. Array.erase­Reps
  30. Array.extract
  31. Array.ferase­Idx
  32. Array.filter
  33. Array.filter­M
  34. Array.filter­Map
  35. Array.filter­Map­M
  36. Array.filter­Pairs­M
  37. Array.filter­Sep­Elems
  38. Array.filter­Sep­Elems­M
  39. Array.find?
  40. Array.find­Idx?
  41. Array.find­Idx­M?
  42. Array.find­M?
  43. Array.find­Rev?
  44. Array.find­Rev­M?
  45. Array.find­Some!
  46. Array.find­Some?
  47. Array.find­Some­M?
  48. Array.find­Some­Rev?
  49. Array.find­Some­Rev­M?
  50. Array.flat­Map
  51. Array.flat­Map­M
  52. Array.flatten
  53. Array.foldl
  54. Array.foldl­M
  55. Array.foldr
  56. Array.foldr­M
  57. Array.for­In'
  58. Array.for­M
  59. Array.for­Rev­M
  60. Array.get
  61. Array.get!
  62. Array.get?
  63. Array.get­D
  64. Array.get­Even­Elems
  65. Array.get­Idx?
  66. Array.get­Max?
  67. Array.group­By­Key
  68. Array.index­Of?
  69. Array.insert­At
  70. Array.insert­At!
  71. Array.insertion­Sort
  72. Array.is­Empty
  73. Array.is­Eqv
  74. Array.is­Prefix­Of
  75. Array.map
  76. Array.map­Fin­Idx
  77. Array.map­Fin­Idx­M
  78. Array.map­Idx
  79. Array.map­Idx­M
  80. Array.map­Indexed
  81. Array.map­Indexed­M
  82. Array.map­M
  83. Array.map­M'
  84. Array.map­Mono
  85. Array.map­Mono­M
  86. Array.mk
    1. Constructor of Array
  87. Array.mk­Array
  88. Array.modify
  89. Array.modify­M
  90. Array.modify­Op
  91. Array.of­Fn
  92. Array.of­Subarray
  93. Array.partition
  94. Array.pop
  95. Array.pop­While
  96. Array.push
  97. Array.qsort
  98. Array.qsort­Ord
  99. Array.range
  100. Array.reduce­Get­Elem
  101. Array.reduce­Get­Elem!
  102. Array.reduce­Get­Elem?
  103. Array.reduce­Option
  104. Array.reverse
  105. Array.sequence­Map
  106. Array.set
  107. Array.set!
  108. Array.set­D
  109. Array.singleton
  110. Array.size
  111. Array.split
  112. Array.swap
  113. Array.swap!
  114. Array.swap­At
  115. Array.swap­At!
  116. Array.take
  117. Array.take­While
  118. Array.to­List
  119. Array.to­List­Append
  120. Array.to­List­Rev
  121. Array.to­PArray'
  122. Array.to­Subarray
  123. Array.uget
  124. Array.unattach
  125. Array.unzip
  126. Array.uset
  127. Array.usize
  128. Array.zip
  129. Array.zip­With
  130. Array.zip­With­Index
  131. ac_rfl
  132. adapt­Expander
    1. Lean.Elab.Tactic.adapt­Expander
  133. add
    1. Add.add (class method)
    2. Nat.add
  134. add­Macro­Scope
    1. Lean.Macro.add­Macro­Scope
  135. admit
  136. all
    1. Array.all
    2. Nat.all
    3. String.all
    4. Subarray.all
  137. all­Diff
    1. Array.all­Diff
  138. all­M
    1. Array.all­M
    2. Nat.all­M
    3. Subarray.all­M
  139. all­TR
    1. Nat.all­TR
  140. all_goals (0) (1)
  141. and_intros
  142. any
    1. Array.any
    2. Nat.any
    3. String.any
    4. Subarray.any
  143. any­M
    1. Array.any­M
    2. Nat.any­M
    3. Subarray.any­M
  144. any­TR
    1. Nat.any­TR
  145. any_goals (0) (1)
  146. append
    1. Append.append (class method)
    2. Array.append
    3. String.append
  147. append­Goals
    1. Lean.Elab.Tactic.append­Goals
  148. append­List
    1. Array.append­List
  149. apply (0) (1)
  150. apply?
  151. apply­Eq­Lemma
    1. Nat.apply­Eq­Lemma
  152. apply­Simproc­Const
    1. Nat.apply­Simproc­Const
  153. apply_assumption
  154. apply_ext_theorem
  155. apply_mod_cast
  156. apply_rfl
  157. apply_rules
  158. arg [@]i
  159. args
  160. arith
    1. Lean.Meta.Simp.Config.ground (structure field)
  161. array
    1. Subarray.start_le_stop (structure field)
  162. array_get_dec
  163. assumption
    1. inaccessible
  164. assumption_mod_cast
  165. at­End
    1. String.Iterator.at­End
    2. String.at­End
  166. attach
    1. Array.attach
  167. attach­With
    1. Array.attach­With
  168. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  169. auto­Unfold
    1. Lean.Meta.DSimp.Config.decide (structure field)
    2. Lean.Meta.Simp.Config.decide (structure field)

B

  1. BEq
  2. BEq.beq
  3. back
    1. Array.back
    2. String.back
  4. back!
    1. Array.back!
  5. back?
    1. Array.back?
  6. backward.synthInstance.canon­Instances
  7. below
    1. Nat.below
  8. beq
    1. BEq.beq (class method)
    2. Nat.beq
  9. beta
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
    2. Lean.Meta.Simp.Config.arith (structure field)
  10. bin­Insert
    1. Array.bin­Insert
  11. bin­Insert­M
    1. Array.bin­Insert­M
  12. bin­Search
    1. Array.bin­Search
  13. bin­Search­Contains
    1. Array.bin­Search­Contains
  14. bitwise
    1. Nat.bitwise
  15. ble
    1. Nat.ble
  16. blt
    1. Nat.blt
  17. bootstrap.inductive­Check­Resulting­Universe
  18. bv_check
  19. bv_decide
  20. bv_decide?
  21. bv_normalize
  22. bv_omega
  23. by_cases
  24. byte­Idx
    1. String.Pos.byte­Idx (structure field)

C

  1. Char
  2. Char.is­Alpha
  3. Char.is­Alphanum
  4. Char.is­Digit
  5. Char.is­Lower
  6. Char.is­Upper
  7. Char.is­Whitespace
  8. Char.mk
    1. Constructor of Char
  9. Char­Lit
    1. Lean.Syntax.Char­Lit
  10. Command
    1. Lean.Syntax.Command
  11. Config
    1. Lean.Meta.DSimp.Config
    2. Lean.Meta.Rewrite.Config
    3. Lean.Meta.Simp.Config
  12. calc
  13. canon­Instances
    1. backward.synthInstance.canon­Instances
  14. capitalize
    1. String.capitalize
  15. case
  16. case ... => ...
  17. case'
  18. case' ... => ...
  19. case­Strong­Induction­On
    1. Nat.case­Strong­Induction­On
  20. cases
  21. cases­On
    1. Nat.cases­On
  22. cast
    1. Nat.cast
  23. change (0) (1)
  24. change ... with ...
  25. char­Lit­Kind
    1. Lean.char­Lit­Kind
  26. checkpoint
  27. choice­Kind
    1. Lean.choice­Kind
  28. clear
  29. close­Main­Goal
    1. Lean.Elab.Tactic.close­Main­Goal
  30. close­Main­Goal­Using
    1. Lean.Elab.Tactic.close­Main­Goal­Using
  31. codepoint­Pos­To­Utf16Pos
    1. String.codepoint­Pos­To­Utf16Pos
  32. codepoint­Pos­To­Utf16Pos­From
    1. String.codepoint­Pos­To­Utf16Pos­From
  33. codepoint­Pos­To­Utf8Pos­From
    1. String.codepoint­Pos­To­Utf8Pos­From
  34. col­Eq
  35. col­Ge
  36. col­Gt
  37. comment
    1. block
    2. line
  38. compare
    1. Ord.compare (class method)
  39. concat­Map
    1. Array.concat­Map
  40. concat­Map­M
    1. Array.concat­Map­M
  41. configuration
    1. of tactics
  42. congr (0) (1)
  43. constructor (0) (1)
  44. contains
    1. Array.contains
    2. String.contains
  45. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  46. contradiction
  47. conv
  48. conv => ...
  49. conv' (0) (1)
  50. crlf­To­Lf
    1. String.crlf­To­Lf
  51. csize
    1. String.csize
  52. cumulativity
  53. curr
    1. String.Iterator.curr
  54. custom­Eliminators
    1. tactic.custom­Eliminators

D

  1. Decidable
  2. Decidable.is­False
    1. Constructor of Decidable
  3. Decidable.is­True
    1. Constructor of Decidable
  4. Decidable­Eq
  5. Decidable­Rel
  6. Div
  7. Div.div
  8. Dvd
  9. Dvd.dvd
  10. Dynamic
  11. Dynamic.get?
  12. Dynamic.mk
  13. data
    1. String.data (structure field)
    2. _private.Init.Dynamic.0.TypeName.data (class method)
  14. dbg_cache
    1. tactic.dbg_cache
  15. dbg_trace
  16. dec­Eq
    1. Nat.dec­Eq
    2. String.dec­Eq
  17. dec­Le
    1. Nat.dec­Le
  18. dec­Lt
    1. Nat.dec­Lt
  19. decapitalize
    1. String.decapitalize
  20. decide
    1. Lean.Meta.DSimp.Config.zeta (structure field)
    2. Lean.Meta.Simp.Config.zeta (structure field)
  21. decreasing_tactic
  22. decreasing_trivial
  23. decreasing_with
  24. deep­Terms
    1. pp.deep­Terms
  25. default
    1. Inhabited.default (class method)
  26. delta (0) (1)
  27. digit­Char
    1. Nat.digit­Char
  28. discharge
    1. trace.Meta.Tactic.simp.discharge
  29. div
    1. Div.div (class method)
    2. Nat.div
  30. div2Induction
    1. Nat.div2Induction
  31. done (0) (1)
  32. drop
    1. String.drop
    2. Subarray.drop
  33. drop­Right
    1. String.drop­Right
  34. drop­Right­While
    1. String.drop­Right­While
  35. drop­While
    1. String.drop­While
  36. dsimp (0) (1)
    1. Lean.Meta.Simp.Config.max­Discharge­Depth (structure field)
  37. dsimp!
  38. dsimp?
  39. dsimp?!
  40. dsimp­Location'
    1. Lean.Elab.Tactic.dsimp­Location'
  41. dvd
    1. Dvd.dvd (class method)

E

  1. Even
  2. Even.plus­Two
    1. Constructor of Even
  3. Even.zero
    1. Constructor of Even
  4. elab­Cases­Targets
    1. Lean.Elab.Tactic.elab­Cases­Targets
  5. elab­DSimp­Config­Core
    1. Lean.Elab.Tactic.elab­DSimp­Config­Core
  6. elab­Simp­Args
    1. Lean.Elab.Tactic.elab­Simp­Args
  7. elab­Simp­Config
    1. Lean.Elab.Tactic.elab­Simp­Config
  8. elab­Simp­Config­Ctx­Core
    1. Lean.Elab.Tactic.elab­Simp­Config­Ctx­Core
  9. elab­Term
    1. Lean.Elab.Tactic.elab­Term
  10. elab­Term­Ensuring­Type
    1. Lean.Elab.Tactic.elab­Term­Ensuring­Type
  11. elab­Term­With­Holes
    1. Lean.Elab.Tactic.elab­Term­With­Holes
  12. elem
    1. Array.elem
  13. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  14. elim­Offset
    1. Nat.elim­Offset
  15. empty
    1. Array.empty
    2. Subarray.empty
  16. end­Pos
    1. String.end­Pos
  17. ends­With
    1. String.ends­With
  18. ensure­Has­No­MVars
    1. Lean.Elab.Tactic.ensure­Has­No­MVars
  19. enter
  20. eq_of_beq
    1. LawfulBEq.eq_of_beq (class method)
  21. eq_refl
  22. erase
    1. Array.erase
  23. erase­Idx
    1. Array.erase­Idx
  24. erase­Reps
    1. Array.erase­Reps
  25. erw (0) (1)
  26. eta
    1. Lean.Meta.DSimp.Config.index (structure field)
    2. Lean.Meta.Simp.Config.max­Steps (structure field)
  27. eta­Struct
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  28. exact
  29. exact?
  30. exact_mod_cast
  31. exfalso
  32. exists
  33. expand­Macro?
    1. Lean.Macro.expand­Macro?
  34. ext (0) (1)
  35. ext1
  36. extensionality
    1. of propositions
  37. extract
    1. Array.extract
    2. String.Iterator.extract
    3. String.extract

F

  1. fail
  2. fail­If­Unchanged
    1. Lean.Meta.DSimp.Config.auto­Unfold (structure field)
    2. Lean.Meta.Simp.Config.implicit­Def­Eq­Proofs (structure field)
  3. fail_if_success (0) (1)
  4. false_or_by_contra
  5. ferase­Idx
    1. Array.ferase­Idx
  6. field­Idx­Kind
    1. Lean.field­Idx­Kind
  7. filter
    1. Array.filter
  8. filter­M
    1. Array.filter­M
  9. filter­Map
    1. Array.filter­Map
  10. filter­Map­M
    1. Array.filter­Map­M
  11. filter­Pairs­M
    1. Array.filter­Pairs­M
  12. filter­Sep­Elems
    1. Array.filter­Sep­Elems
  13. filter­Sep­Elems­M
    1. Array.filter­Sep­Elems­M
  14. find
    1. String.find
  15. find?
    1. Array.find?
  16. find­Idx?
    1. Array.find­Idx?
  17. find­Idx­M?
    1. Array.find­Idx­M?
  18. find­Line­Start
    1. String.find­Line­Start
  19. find­M?
    1. Array.find­M?
  20. find­Rev?
    1. Array.find­Rev?
    2. Subarray.find­Rev?
  21. find­Rev­M?
    1. Array.find­Rev­M?
    2. Subarray.find­Rev­M?
  22. find­Some!
    1. Array.find­Some!
  23. find­Some?
    1. Array.find­Some?
  24. find­Some­M?
    1. Array.find­Some­M?
  25. find­Some­Rev?
    1. Array.find­Some­Rev?
  26. find­Some­Rev­M?
    1. Array.find­Some­Rev­M?
    2. Subarray.find­Some­Rev­M?
  27. first (0) (1)
  28. first­Diff­Pos
    1. String.first­Diff­Pos
  29. flat­Map
    1. Array.flat­Map
  30. flat­Map­M
    1. Array.flat­Map­M
  31. flatten
    1. Array.flatten
  32. focus (0) (1)
    1. Lean.Elab.Tactic.focus
  33. fold
    1. Nat.fold
  34. fold­M
    1. Nat.fold­M
  35. fold­Rev
    1. Nat.fold­Rev
  36. fold­Rev­M
    1. Nat.fold­Rev­M
  37. fold­TR
    1. Nat.fold­TR
  38. foldl
    1. Array.foldl
    2. String.foldl
    3. Subarray.foldl
  39. foldl­M
    1. Array.foldl­M
    2. Subarray.foldl­M
  40. foldr
    1. Array.foldr
    2. String.foldr
    3. Subarray.foldr
  41. foldr­M
    1. Array.foldr­M
    2. Subarray.foldr­M
  42. for­In
    1. Subarray.for­In
  43. for­In'
    1. Array.for­In'
  44. for­M
    1. Array.for­M
    2. Nat.for­M
    3. Subarray.for­M
  45. for­Rev­M
    1. Array.for­Rev­M
    2. Nat.for­Rev­M
    3. Subarray.for­Rev­M
  46. forward
    1. String.Iterator.forward
  47. from­Expr?
    1. Nat.from­Expr?
    2. String.from­Expr?
  48. from­UTF8
    1. String.from­UTF8
  49. from­UTF8!
    1. String.from­UTF8!
  50. from­UTF8?
    1. String.from­UTF8?
  51. front
    1. String.front
  52. fun
  53. funext (0) (1)

G

  1. Get­Elem
  2. GetElem.get­Elem
  3. Get­Elem?
  4. GetElem?.get­Elem!
  5. GetElem?.get­Elem?
  6. GetElem?.to­Get­Elem
  7. gcd
    1. Nat.gcd
  8. generalize
  9. get
    1. Array.get
    2. String.get
    3. Subarray.get
  10. get!
    1. Array.get!
    2. String.get!
    3. Subarray.get!
  11. get'
    1. String.get'
  12. get?
    1. Array.get?
    2. Dynamic.get?
    3. String.get?
  13. get­Char
    1. Lean.TSyntax.get­Char
  14. get­Curr­Macro­Scope
    1. Lean.Elab.Tactic.get­Curr­Macro­Scope
  15. get­Curr­Namespace
    1. Lean.Macro.get­Curr­Namespace
  16. get­D
    1. Array.get­D
    2. Subarray.get­D
  17. get­Elem
    1. GetElem.get­Elem (class method)
  18. get­Elem!
    1. GetElem?.get­Elem! (class method)
  19. get­Elem!_def
    1. Lawful­GetElem.get­Elem?_def (class method)
  20. get­Elem?
    1. GetElem?.get­Elem? (class method)
  21. get­Elem?_def
    1. Lawful­GetElem.get­Elem!_def (class method)
  22. get­Even­Elems
    1. Array.get­Even­Elems
  23. get­FVar­Id
    1. Lean.Elab.Tactic.get­FVar­Id
  24. get­FVar­Ids
    1. Lean.Elab.Tactic.get­FVar­Ids
  25. get­Goals
    1. Lean.Elab.Tactic.get­Goals
  26. get­Hygiene­Info
    1. Lean.TSyntax.get­Hygiene­Info
  27. get­Id
    1. Lean.TSyntax.get­Id
  28. get­Idx?
    1. Array.get­Idx?
  29. get­Kind
    1. Lean.Syntax.get­Kind
  30. get­Main­Goal
    1. Lean.Elab.Tactic.get­Main­Goal
  31. get­Main­Module
    1. Lean.Elab.Tactic.get­Main­Module
  32. get­Main­Tag
    1. Lean.Elab.Tactic.get­Main­Tag
  33. get­Max?
    1. Array.get­Max?
  34. get­Name
    1. Lean.TSyntax.get­Name
  35. get­Nat
    1. Lean.TSyntax.get­Nat
  36. get­Scientific
    1. Lean.TSyntax.get­Scientific
  37. get­String
    1. Lean.TSyntax.get­String
  38. get­Unsolved­Goals
    1. Lean.Elab.Tactic.get­Unsolved­Goals
  39. get­Utf8Byte
    1. String.get­Utf8Byte
  40. get_elem_tactic
  41. get_elem_tactic_trivial
  42. goal
    1. main
  43. ground
    1. Lean.Meta.Simp.Config.auto­Unfold (structure field)
  44. group­By­Key
    1. Array.group­By­Key
  45. group­Kind
    1. Lean.group­Kind
  46. guard_expr
  47. guard_hyp
  48. guard_target

H

  1. HAdd
  2. HAdd.h­Add
  3. HAnd
  4. HAnd.h­And
  5. HAppend
  6. HAppend.h­Append
  7. HDiv
  8. HDiv.h­Div
  9. HMod
  10. HMod.h­Mod
  11. HMul
  12. HMul.h­Mul
  13. HOr
  14. HOr.h­Or
  15. HPow
  16. HPow.h­Pow
  17. HShift­Left
  18. HShiftLeft.h­Shift­Left
  19. HShift­Right
  20. HShiftRight.h­Shift­Right
  21. HSub
  22. HSub.h­Sub
  23. HXor
  24. HXor.h­Xor
  25. Hashable
  26. Hashable.hash
  27. Homogeneous­Pow
  28. HomogeneousPow.pow
  29. Hygiene­Info
    1. Lean.Syntax.Hygiene­Info
  30. h­Add
    1. HAdd.h­Add (class method)
  31. h­And
    1. HAnd.h­And (class method)
  32. h­Append
    1. HAppend.h­Append (class method)
  33. h­Div
    1. HDiv.h­Div (class method)
  34. h­Mod
    1. HMod.h­Mod (class method)
  35. h­Mul
    1. HMul.h­Mul (class method)
  36. h­Or
    1. HOr.h­Or (class method)
  37. h­Pow
    1. HPow.h­Pow (class method)
  38. h­Shift­Left
    1. HShiftLeft.h­Shift­Left (class method)
  39. h­Shift­Right
    1. HShiftRight.h­Shift­Right (class method)
  40. h­Sub
    1. HSub.h­Sub (class method)
  41. h­Xor
    1. HXor.h­Xor (class method)
  42. has­Decl
    1. Lean.Macro.has­Decl
  43. has­Next
    1. String.Iterator.has­Next
  44. has­Prev
    1. String.Iterator.has­Prev
  45. hash
    1. Hashable.hash (class method)
    2. String.hash
  46. have
  47. have'
  48. have­I
  49. hygiene
    1. in tactics
  50. hygiene­Info­Kind
    1. Lean.hygiene­Info­Kind
  51. hygienic
    1. tactic.hygienic

I

  1. Ident
    1. Lean.Syntax.Ident
  2. Inhabited
  3. Inhabited.default
  4. Iterator
    1. String.Iterator
  5. i
    1. String.Iterator.s (structure field)
  6. ibelow
    1. Nat.ibelow
  7. ident­Kind
    1. Lean.ident­Kind
  8. identifier
    1. raw
  9. if ... then ... else ...
  10. if h : ... then ... else ...
  11. imax
    1. Nat.imax
  12. implicit­Def­Eq­Proofs
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  13. impredicative
  14. inaccessible
  15. index
    1. Lean.Meta.DSimp.Config.unfold­Partial­App (structure field)
    2. Lean.Meta.Simp.Config.unfold­Partial­App (structure field)
    3. of inductive type
  16. index­Of?
    1. Array.index­Of?
  17. indexed family
    1. of types
  18. induction
  19. induction­On
    1. Nat.div.induction­On
    2. Nat.mod.induction­On
  20. inductive.auto­Promote­Indices
  21. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  22. infer­Instance
  23. infer­Instance­As
  24. infer_instance
  25. injection
  26. injections
  27. insert­At
    1. Array.insert­At
  28. insert­At!
    1. Array.insert­At!
  29. insertion­Sort
    1. Array.insertion­Sort
  30. instance synthesis
  31. intercalate
    1. String.intercalate
  32. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  33. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  34. intro (0) (1)
  35. intro | ... => ... | ... => ...
  36. intros
  37. iota
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  38. is­Alpha
    1. Char.is­Alpha
  39. is­Alphanum
    1. Char.is­Alphanum
  40. is­Digit
    1. Char.is­Digit
  41. is­Empty
    1. Array.is­Empty
    2. String.is­Empty
  42. is­Eqv
    1. Array.is­Eqv
  43. is­Int
    1. String.is­Int
  44. is­Lower
    1. Char.is­Lower
  45. is­Nat
    1. String.is­Nat
  46. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  47. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  48. is­Prefix­Of
    1. Array.is­Prefix­Of
    2. String.is­Prefix­Of
  49. is­Upper
    1. Char.is­Upper
  50. is­Valid
    1. String.Pos.is­Valid
  51. is­Valid­Char
    1. Nat.is­Valid­Char
  52. is­Value
    1. Nat.is­Value
  53. is­Whitespace
    1. Char.is­Whitespace
  54. iter
    1. String.iter
  55. iterate

J

  1. join
    1. String.join

L

  1. LE
  2. LE.le
  3. LT
  4. LT.lt
  5. Lawful­BEq
  6. LawfulBEq.eq_of_beq
  7. LawfulBEq.rfl
  8. Lawful­Get­Elem
  9. Lawful­GetElem.get­Elem!_def
  10. Lawful­GetElem.get­Elem?_def
  11. Leading­Ident­Behavior
    1. Lean.Parser.Leading­Ident­Behavior
  12. Lean.Elab.Tactic.Tactic
  13. Lean.Elab.Tactic.Tactic­M
  14. Lean.Elab.Tactic.adapt­Expander
  15. Lean.Elab.Tactic.append­Goals
  16. Lean.Elab.Tactic.close­Main­Goal
  17. Lean.Elab.Tactic.close­Main­Goal­Using
  18. Lean.Elab.Tactic.dsimp­Location'
  19. Lean.Elab.Tactic.elab­Cases­Targets
  20. Lean.Elab.Tactic.elab­DSimp­Config­Core
  21. Lean.Elab.Tactic.elab­Simp­Args
  22. Lean.Elab.Tactic.elab­Simp­Config
  23. Lean.Elab.Tactic.elab­Simp­Config­Ctx­Core
  24. Lean.Elab.Tactic.elab­Term
  25. Lean.Elab.Tactic.elab­Term­Ensuring­Type
  26. Lean.Elab.Tactic.elab­Term­With­Holes
  27. Lean.Elab.Tactic.ensure­Has­No­MVars
  28. Lean.Elab.Tactic.focus
  29. Lean.Elab.Tactic.get­Curr­Macro­Scope
  30. Lean.Elab.Tactic.get­FVar­Id
  31. Lean.Elab.Tactic.get­FVar­Ids
  32. Lean.Elab.Tactic.get­Goals
  33. Lean.Elab.Tactic.get­Main­Goal
  34. Lean.Elab.Tactic.get­Main­Module
  35. Lean.Elab.Tactic.get­Main­Tag
  36. Lean.Elab.Tactic.get­Unsolved­Goals
  37. Lean.Elab.Tactic.lift­Meta­MAt­Main
  38. Lean.Elab.Tactic.mk­Tactic­Attribute
  39. Lean.Elab.Tactic.or­Else
  40. Lean.Elab.Tactic.prune­Solved­Goals
  41. Lean.Elab.Tactic.run
  42. Lean.Elab.Tactic.run­Term­Elab
  43. Lean.Elab.Tactic.set­Goals
  44. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  45. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  46. Lean.Elab.Tactic.tactic­Elab­Attribute
  47. Lean.Elab.Tactic.tag­Untagged­Goals
  48. Lean.Elab.Tactic.try­Catch
  49. Lean.Elab.Tactic.try­Tactic
  50. Lean.Elab.Tactic.try­Tactic?
  51. Lean.Elab.Tactic.with­Location
  52. Lean.Elab.register­Deriving­Handler
  53. Lean.Macro.Exception.unsupported­Syntax
  54. Lean.Macro.add­Macro­Scope
  55. Lean.Macro.expand­Macro?
  56. Lean.Macro.get­Curr­Namespace
  57. Lean.Macro.has­Decl
  58. Lean.Macro.resolve­Global­Name
  59. Lean.Macro.resolve­Namespace
  60. Lean.Macro.throw­Error
  61. Lean.Macro.throw­Error­At
  62. Lean.Macro.throw­Unsupported
  63. Lean.Macro.trace
  64. Lean.Macro.with­Fresh­Macro­Scope
  65. Lean.Macro­M
  66. Lean.Meta.DSimp.Config
  67. Lean.Meta.DSimp.Config.mk
    1. Constructor of Lean.Meta.DSimp.Config
  68. Lean.Meta.Occurrences
  69. Lean.Meta.Occurrences.all
    1. Constructor of Lean.Meta.Occurrences
  70. Lean.Meta.Occurrences.neg
    1. Constructor of Lean.Meta.Occurrences
  71. Lean.Meta.Occurrences.pos
    1. Constructor of Lean.Meta.Occurrences
  72. Lean.Meta.Rewrite.Config
  73. Lean.Meta.Rewrite.Config.mk
    1. Constructor of Lean.Meta.Rewrite.Config
  74. Lean.Meta.Rewrite.New­Goals
  75. Lean.Meta.Simp.Config
  76. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  77. Lean.Meta.Simp.neutral­Config
  78. Lean.Meta.Simp­Extension
  79. Lean.Meta.Transparency­Mode
  80. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.Transparency­Mode
  81. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.Transparency­Mode
  82. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.Transparency­Mode
  83. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.Transparency­Mode
  84. Lean.Meta.register­Simp­Attr
  85. Lean.Parser.Leading­Ident­Behavior
  86. Lean.Parser.Leading­IdentBehavior.both
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  87. Lean.Parser.Leading­IdentBehavior.default
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  88. Lean.Parser.Leading­IdentBehavior.symbol
    1. Constructor of Lean.Parser.Leading­Ident­Behavior
  89. Lean.Source­Info
  90. Lean.SourceInfo.none
    1. Constructor of Lean.Source­Info
  91. Lean.SourceInfo.original
    1. Constructor of Lean.Source­Info
  92. Lean.SourceInfo.synthetic
    1. Constructor of Lean.Source­Info
  93. Lean.Syntax
  94. Lean.Syntax.Char­Lit
  95. Lean.Syntax.Command
  96. Lean.Syntax.Hygiene­Info
  97. Lean.Syntax.Ident
  98. Lean.Syntax.Level
  99. Lean.Syntax.Name­Lit
  100. Lean.Syntax.Num­Lit
  101. Lean.Syntax.Prec
  102. Lean.Syntax.Preresolved
  103. Lean.Syntax.Preresolved.decl
    1. Constructor of Lean.Syntax.Preresolved
  104. Lean.Syntax.Preresolved.namespace
    1. Constructor of Lean.Syntax.Preresolved
  105. Lean.Syntax.Prio
  106. Lean.Syntax.Scientific­Lit
  107. Lean.Syntax.Str­Lit
  108. Lean.Syntax.TSep­Array
  109. Lean.Syntax.TSepArray.mk
    1. Constructor of Lean.Syntax.TSep­Array
  110. Lean.Syntax.Tactic
  111. Lean.Syntax.Term
  112. Lean.Syntax.atom
    1. Constructor of Lean.Syntax
  113. Lean.Syntax.get­Kind
  114. Lean.Syntax.ident
    1. Constructor of Lean.Syntax
  115. Lean.Syntax.is­Of­Kind
  116. Lean.Syntax.missing
    1. Constructor of Lean.Syntax
  117. Lean.Syntax.node
    1. Constructor of Lean.Syntax
  118. Lean.Syntax.set­Kind
  119. Lean.Syntax­Node­Kind
  120. Lean.TSyntax
  121. Lean.TSyntax.get­Char
  122. Lean.TSyntax.get­Hygiene­Info
  123. Lean.TSyntax.get­Id
  124. Lean.TSyntax.get­Name
  125. Lean.TSyntax.get­Nat
  126. Lean.TSyntax.get­Scientific
  127. Lean.TSyntax.get­String
  128. Lean.TSyntax.mk
    1. Constructor of Lean.TSyntax
  129. Lean.TSyntax­Array
  130. Lean.char­Lit­Kind
  131. Lean.choice­Kind
  132. Lean.field­Idx­Kind
  133. Lean.group­Kind
  134. Lean.hygiene­Info­Kind
  135. Lean.ident­Kind
  136. Lean.interpolated­Str­Kind
  137. Lean.interpolated­Str­Lit­Kind
  138. Lean.name­Lit­Kind
  139. Lean.null­Kind
  140. Lean.num­Lit­Kind
  141. Lean.scientific­Lit­Kind
  142. Lean.str­Lit­Kind
  143. Level
    1. Lean.Syntax.Level
  144. land
    1. Nat.land
  145. lcm
    1. Nat.lcm
  146. le
    1. LE.le (class method)
    2. Nat.le
    3. String.le
  147. lean_is_array
  148. lean_is_string
  149. lean_string_object (0) (1)
  150. lean_to_array
  151. lean_to_string
  152. left (0) (1)
  153. length
    1. String.length
  154. let
  155. let rec
  156. let'
  157. let­I
  158. lhs
  159. lift­Meta­MAt­Main
    1. Lean.Elab.Tactic.lift­Meta­MAt­Main
  160. line­Eq
  161. linter.unnecessary­Simpa
  162. literal
    1. raw string
    2. string
  163. log2
    1. Nat.log2
  164. lor
    1. Nat.lor
  165. lt
    1. LT.lt (class method)
    2. Nat.lt
  166. lt_wf­Rel
    1. Nat.lt_wf­Rel

M

  1. Macro­M
    1. Lean.Macro­M
  2. Mod
  3. Mod.mod
  4. Mul
  5. Mul.mul
  6. main goal
  7. map
    1. Array.map
    2. String.map
  8. map­Fin­Idx
    1. Array.map­Fin­Idx
  9. map­Fin­Idx­M
    1. Array.map­Fin­Idx­M
  10. map­Idx
    1. Array.map­Idx
  11. map­Idx­M
    1. Array.map­Idx­M
  12. map­Indexed
    1. Array.map­Indexed
  13. map­Indexed­M
    1. Array.map­Indexed­M
  14. map­M
    1. Array.map­M
  15. map­M'
    1. Array.map­M'
  16. map­Mono
    1. Array.map­Mono
  17. map­Mono­M
    1. Array.map­Mono­M
  18. match
    1. pp.match
  19. max
    1. Nat.max
  20. max­Discharge­Depth
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  21. max­Heartbeats
    1. synthInstance.max­Heartbeats
  22. max­Size
    1. synthInstance.max­Size
  23. max­Steps
    1. Lean.Meta.Simp.Config.zeta­Delta (structure field)
    2. pp.max­Steps
  24. memoize
    1. Lean.Meta.Simp.Config.index (structure field)
  25. min
    1. Nat.min
    2. String.Pos.min
  26. mk
    1. Dynamic.mk
  27. mk­Array
    1. Array.mk­Array
  28. mk­Iterator
    1. String.mk­Iterator
  29. mk­Tactic­Attribute
    1. Lean.Elab.Tactic.mk­Tactic­Attribute
  30. mod
    1. Mod.mod (class method)
    2. Nat.mod
  31. mod­Core
    1. Nat.mod­Core
  32. modify
    1. Array.modify
    2. String.modify
  33. modify­M
    1. Array.modify­M
  34. modify­Op
    1. Array.modify­Op
  35. mul
    1. Mul.mul (class method)
    2. Nat.mul
  36. 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.apply­Eq­Lemma
  11. Nat.apply­Simproc­Const
  12. Nat.below
  13. Nat.beq
  14. Nat.bitwise
  15. Nat.ble
  16. Nat.blt
  17. Nat.case­Strong­Induction­On
  18. Nat.cases­On
  19. Nat.cast
  20. Nat.dec­Eq
  21. Nat.dec­Le
  22. Nat.dec­Lt
  23. Nat.digit­Char
  24. Nat.div
  25. Nat.div.induction­On
  26. Nat.div2Induction
  27. Nat.elim­Offset
  28. Nat.fold
  29. Nat.fold­M
  30. Nat.fold­Rev
  31. Nat.fold­Rev­M
  32. Nat.fold­TR
  33. Nat.for­M
  34. Nat.for­Rev­M
  35. Nat.from­Expr?
  36. Nat.gcd
  37. Nat.ibelow
  38. Nat.imax
  39. Nat.is­Power­Of­Two
  40. Nat.is­Valid­Char
  41. Nat.is­Value
  42. Nat.land
  43. Nat.lcm
  44. Nat.le
  45. Nat.le.refl
    1. Constructor of Nat.le
  46. Nat.le.step
    1. Constructor of Nat.le
  47. Nat.log2
  48. Nat.lor
  49. Nat.lt
  50. Nat.lt_wf­Rel
  51. Nat.max
  52. Nat.min
  53. Nat.mod
  54. Nat.mod.induction­On
  55. Nat.mod­Core
  56. Nat.mul
  57. Nat.next­Power­Of­Two
  58. Nat.no­Confusion
  59. Nat.no­Confusion­Type
  60. Nat.pow
  61. Nat.pred
  62. Nat.rec
  63. Nat.rec­On
  64. Nat.reduce­Add
  65. Nat.reduce­BEq
  66. Nat.reduce­BNe
  67. Nat.reduce­Beq­Diff
  68. Nat.reduce­Bin
  69. Nat.reduce­Bin­Pred
  70. Nat.reduce­Bne­Diff
  71. Nat.reduce­Bool­Pred
  72. Nat.reduce­Div
  73. Nat.reduce­Eq­Diff
  74. Nat.reduce­GT
  75. Nat.reduce­Gcd
  76. Nat.reduce­LT
  77. Nat.reduce­LTLE
  78. Nat.reduce­Le­Diff
  79. Nat.reduce­Mod
  80. Nat.reduce­Mul
  81. Nat.reduce­Nat­Eq­Expr
  82. Nat.reduce­Pow
  83. Nat.reduce­Sub
  84. Nat.reduce­Sub­Diff
  85. Nat.reduce­Succ
  86. Nat.reduce­Unary
  87. Nat.repeat
  88. Nat.repeat­TR
  89. Nat.repr
  90. Nat.shift­Left
  91. Nat.shift­Right
  92. Nat.strong­Induction­On
  93. Nat.sub
  94. Nat.sub­Digit­Char
  95. Nat.succ
    1. Constructor of Nat
  96. Nat.super­Digit­Char
  97. Nat.test­Bit
  98. Nat.to­Digits
  99. Nat.to­Digits­Core
  100. Nat.to­Float
  101. Nat.to­Level
  102. Nat.to­Sub­Digits
  103. Nat.to­Subscript­String
  104. Nat.to­Super­Digits
  105. Nat.to­Superscript­String
  106. Nat.to­UInt16
  107. Nat.to­UInt32
  108. Nat.to­UInt64
  109. Nat.to­UInt8
  110. Nat.to­USize
  111. Nat.xor
  112. Nat.zero
    1. Constructor of Nat
  113. Nat­Cast
  114. NatCast.nat­Cast
  115. Nat­Pow
  116. NatPow.pow
  117. Ne­Zero
  118. NeZero.out
  119. Neg
  120. Neg.neg
  121. New­Goals
    1. Lean.Meta.Rewrite.New­Goals
  122. Nonempty
  123. Nonempty.intro
    1. Constructor of Nonempty
  124. Num­Lit
    1. Lean.Syntax.Num­Lit
  125. name­Lit­Kind
    1. Lean.name­Lit­Kind
  126. namespace
    1. of inductive type
  127. nat­Cast
    1. NatCast.nat­Cast (class method)
  128. native_decide
  129. neg
    1. Neg.neg (class method)
  130. neutral­Config
    1. Lean.Meta.Simp.neutral­Config
  131. new­Goals
    1. Lean.Meta.Rewrite.Config.offset­Cnstrs (structure field)
  132. next
    1. String.Iterator.next
    2. String.next
  133. next ... => ...
  134. next'
    1. String.next'
  135. next­Power­Of­Two
    1. Nat.next­Power­Of­Two
  136. next­Until
    1. String.next­Until
  137. next­While
    1. String.next­While
  138. nextn
    1. String.Iterator.nextn
  139. no­Confusion
    1. Nat.no­Confusion
  140. no­Confusion­Type
    1. Nat.no­Confusion­Type
  141. nofun
  142. nomatch
  143. norm_cast (0) (1)
  144. null­Kind
    1. Lean.null­Kind
  145. num­Lit­Kind
    1. Lean.num­Lit­Kind

O

  1. Occurrences
    1. Lean.Meta.Occurrences
  2. Ord
  3. Ord.compare
  4. obtain
  5. occs
    1. Lean.Meta.Rewrite.Config.new­Goals (structure field)
  6. of­Fn
    1. Array.of­Fn
  7. of­Subarray
    1. Array.of­Subarray
  8. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  9. offset­Of­Pos
    1. String.offset­Of­Pos
  10. omega
  11. open
  12. or­Else
    1. Lean.Elab.Tactic.or­Else
  13. out
    1. NeZero.out (class method)
  14. out­Param

P

  1. Pos
    1. String.Pos
  2. Pow
  3. Pow.pow
  4. Prec
    1. Lean.Syntax.Prec
  5. Preresolved
    1. Lean.Syntax.Preresolved
  6. Prio
    1. Lean.Syntax.Prio
  7. Prop
  8. parameter
    1. of inductive type
  9. parser
  10. partition
    1. Array.partition
  11. pattern
  12. polymorphism
    1. universe
  13. pop
    1. Array.pop
  14. pop­Front
    1. Subarray.pop­Front
  15. pop­While
    1. Array.pop­While
  16. pos
    1. String.Iterator.pos
  17. pos­Of
    1. String.pos­Of
  18. pow
    1. HomogeneousPow.pow (class method)
    2. Nat.pow
    3. NatPow.pow (class method)
    4. Pow.pow (class method)
  19. pp.deep­Terms
  20. pp.deepTerms.threshold
  21. pp.match
  22. pp.max­Steps
  23. pp.mvars
  24. pp.proofs
  25. pp.proofs.threshold
  26. pred
    1. Nat.pred
  27. predicative
  28. prev
    1. String.Iterator.prev
    2. String.prev
  29. prevn
    1. String.Iterator.prevn
  30. proj
    1. Lean.Meta.DSimp.Config.iota (structure field)
    2. Lean.Meta.Simp.Config.memoize (structure field)
  31. proofs
    1. pp.proofs
  32. propext
  33. proposition
  34. prune­Solved­Goals
    1. Lean.Elab.Tactic.prune­Solved­Goals
  35. push
    1. Array.push
    2. String.push
  36. push_cast
  37. pushn
    1. String.pushn

Q

  1. qsort
    1. Array.qsort
  2. qsort­Ord
    1. Array.qsort­Ord
  3. quantification
    1. impredicative
    2. predicative
  4. quote
    1. String.quote

R

  1. Repr
  2. Repr.repr­Prec
  3. range
    1. Array.range
  4. raw
    1. Lean.TSyntax.raw (structure field)
  5. rcases
  6. rec
    1. Nat.rec
  7. rec­On
    1. Nat.rec­On
  8. recursor
  9. reduce
  10. reduce­Add
    1. Nat.reduce­Add
  11. reduce­Append
    1. String.reduce­Append
  12. reduce­BEq
    1. Nat.reduce­BEq
    2. String.reduce­BEq
  13. reduce­BNe
    1. Nat.reduce­BNe
    2. String.reduce­BNe
  14. reduce­Beq­Diff
    1. Nat.reduce­Beq­Diff
  15. reduce­Bin
    1. Nat.reduce­Bin
  16. reduce­Bin­Pred
    1. Nat.reduce­Bin­Pred
    2. String.reduce­Bin­Pred
  17. reduce­Bne­Diff
    1. Nat.reduce­Bne­Diff
  18. reduce­Bool­Pred
    1. Nat.reduce­Bool­Pred
    2. String.reduce­Bool­Pred
  19. reduce­Div
    1. Nat.reduce­Div
  20. reduce­Eq
    1. String.reduce­Eq
  21. reduce­Eq­Diff
    1. Nat.reduce­Eq­Diff
  22. reduce­GE
    1. String.reduce­GE
  23. reduce­GT
    1. Nat.reduce­GT
    2. String.reduce­GT
  24. reduce­Gcd
    1. Nat.reduce­Gcd
  25. reduce­Get­Elem
    1. Array.reduce­Get­Elem
  26. reduce­Get­Elem!
    1. Array.reduce­Get­Elem!
  27. reduce­Get­Elem?
    1. Array.reduce­Get­Elem?
  28. reduce­LE
    1. String.reduce­LE
  29. reduce­LT
    1. Nat.reduce­LT
    2. String.reduce­LT
  30. reduce­LTLE
    1. Nat.reduce­LTLE
  31. reduce­Le­Diff
    1. Nat.reduce­Le­Diff
  32. reduce­Mk
    1. String.reduce­Mk
  33. reduce­Mod
    1. Nat.reduce­Mod
  34. reduce­Mul
    1. Nat.reduce­Mul
  35. reduce­Nat­Eq­Expr
    1. Nat.reduce­Nat­Eq­Expr
  36. reduce­Ne
    1. String.reduce­Ne
  37. reduce­Option
    1. Array.reduce­Option
  38. reduce­Pow
    1. Nat.reduce­Pow
  39. reduce­Sub
    1. Nat.reduce­Sub
  40. reduce­Sub­Diff
    1. Nat.reduce­Sub­Diff
  41. reduce­Succ
    1. Nat.reduce­Succ
  42. reduce­Unary
    1. Nat.reduce­Unary
  43. reduction
    1. ι (iota)
  44. refine
  45. refine'
  46. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  47. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  48. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  49. remaining­To­String
    1. String.Iterator.remaining­To­String
  50. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  51. rename
  52. rename_i
  53. repeat (0) (1)
    1. Nat.repeat
  54. repeat'
  55. repeat1'
  56. repeat­TR
    1. Nat.repeat­TR
  57. replace
    1. String.replace
  58. repr
    1. Nat.repr
  59. repr­Prec
    1. Repr.repr­Prec (class method)
  60. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  61. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  62. rev­Find
    1. String.rev­Find
  63. rev­Pos­Of
    1. String.rev­Pos­Of
  64. reverse
    1. Array.reverse
  65. revert
  66. rewrite (0) (1)
    1. trace.Meta.Tactic.simp.rewrite
  67. rfl (0) (1)
    1. LawfulBEq.rfl (class method)
  68. rfl'
  69. rhs
  70. right (0) (1)
  71. rintro
  72. rotate_left
  73. rotate_right
  74. run
    1. Lean.Elab.Tactic.run
  75. run­Term­Elab
    1. Lean.Elab.Tactic.run­Term­Elab
  76. run_tac
  77. rw (0) (1)
  78. rw?
  79. rw_mod_cast
  80. rwa

S

  1. Scientific­Lit
    1. Lean.Syntax.Scientific­Lit
  2. Shift­Left
  3. ShiftLeft.shift­Left
  4. Shift­Right
  5. ShiftRight.shift­Right
  6. Simp­Extension
    1. Lean.Meta.Simp­Extension
  7. Size­Of
  8. SizeOf.size­Of
  9. Sort
  10. Source­Info
    1. Lean.Source­Info
  11. Str­Lit
    1. Lean.Syntax.Str­Lit
  12. String
  13. String.Iterator
  14. String.Iterator.at­End
  15. String.Iterator.curr
  16. String.Iterator.extract
  17. String.Iterator.forward
  18. String.Iterator.has­Next
  19. String.Iterator.has­Prev
  20. String.Iterator.mk
    1. Constructor of String.Iterator
  21. String.Iterator.next
  22. String.Iterator.nextn
  23. String.Iterator.pos
  24. String.Iterator.prev
  25. String.Iterator.prevn
  26. String.Iterator.remaining­Bytes
  27. String.Iterator.remaining­To­String
  28. String.Iterator.set­Curr
  29. String.Iterator.to­End
  30. String.Pos
  31. String.Pos.is­Valid
  32. String.Pos.min
  33. String.Pos.mk
    1. Constructor of String.Pos
  34. String.all
  35. String.any
  36. String.append
  37. String.at­End
  38. String.back
  39. String.capitalize
  40. String.codepoint­Pos­To­Utf16Pos
  41. String.codepoint­Pos­To­Utf16Pos­From
  42. String.codepoint­Pos­To­Utf8Pos­From
  43. String.contains
  44. String.crlf­To­Lf
  45. String.csize
  46. String.dec­Eq
  47. String.decapitalize
  48. String.drop
  49. String.drop­Right
  50. String.drop­Right­While
  51. String.drop­While
  52. String.end­Pos
  53. String.ends­With
  54. String.extract
  55. String.find
  56. String.find­Line­Start
  57. String.first­Diff­Pos
  58. String.foldl
  59. String.foldr
  60. String.from­Expr?
  61. String.from­UTF8
  62. String.from­UTF8!
  63. String.from­UTF8?
  64. String.front
  65. String.get
  66. String.get!
  67. String.get'
  68. String.get?
  69. String.get­Utf8Byte
  70. String.hash
  71. String.intercalate
  72. String.is­Empty
  73. String.is­Int
  74. String.is­Nat
  75. String.is­Prefix­Of
  76. String.iter
  77. String.join
  78. String.le
  79. String.length
  80. String.map
  81. String.mk
    1. Constructor of String
  82. String.mk­Iterator
  83. String.modify
  84. String.next
  85. String.next'
  86. String.next­Until
  87. String.next­While
  88. String.offset­Of­Pos
  89. String.pos­Of
  90. String.prev
  91. String.push
  92. String.pushn
  93. String.quote
  94. String.reduce­Append
  95. String.reduce­BEq
  96. String.reduce­BNe
  97. String.reduce­Bin­Pred
  98. String.reduce­Bool­Pred
  99. String.reduce­Eq
  100. String.reduce­GE
  101. String.reduce­GT
  102. String.reduce­LE
  103. String.reduce­LT
  104. String.reduce­Mk
  105. String.reduce­Ne
  106. String.remove­Leading­Spaces
  107. String.replace
  108. String.rev­Find
  109. String.rev­Pos­Of
  110. String.set
  111. String.singleton
  112. String.split
  113. String.split­On
  114. String.starts­With
  115. String.str
  116. String.substr­Eq
  117. String.take
  118. String.take­Right
  119. String.take­Right­While
  120. String.take­While
  121. String.to­File­Map
  122. String.to­Format
  123. String.to­Int!
  124. String.to­Int?
  125. String.to­List
  126. String.to­Lower
  127. String.to­Name
  128. String.to­Nat!
  129. String.to­Nat?
  130. String.to­Substring
  131. String.to­Substring'
  132. String.to­UTF8
  133. String.to­Upper
  134. String.trim
  135. String.trim­Left
  136. String.trim­Right
  137. String.utf16Length
  138. String.utf16Pos­To­Codepoint­Pos
  139. String.utf16Pos­To­Codepoint­Pos­From
  140. String.utf8Byte­Size
  141. String.utf8Decode­Char?
  142. String.utf8Encode­Char
  143. String.validate­UTF8
  144. Sub
  145. Sub.sub
  146. Subarray
  147. Subarray.all
  148. Subarray.all­M
  149. Subarray.any
  150. Subarray.any­M
  151. Subarray.drop
  152. Subarray.empty
  153. Subarray.find­Rev?
  154. Subarray.find­Rev­M?
  155. Subarray.find­Some­Rev­M?
  156. Subarray.foldl
  157. Subarray.foldl­M
  158. Subarray.foldr
  159. Subarray.foldr­M
  160. Subarray.for­In
  161. Subarray.for­M
  162. Subarray.for­Rev­M
  163. Subarray.get
  164. Subarray.get!
  165. Subarray.get­D
  166. Subarray.mk
    1. Constructor of Subarray
  167. Subarray.pop­Front
  168. Subarray.size
  169. Subarray.split
  170. Subarray.take
  171. Subarray.to­Array
  172. Syntax
    1. Lean.Syntax
  173. Syntax­Node­Kind
    1. Lean.Syntax­Node­Kind
  174. s
    1. String.Iterator.i (structure field)
  175. save
  176. scientific­Lit­Kind
    1. Lean.scientific­Lit­Kind
  177. semi­Out­Param
  178. sequence­Map
    1. Array.sequence­Map
  179. set
    1. Array.set
    2. String.set
  180. set!
    1. Array.set!
  181. set­Curr
    1. String.Iterator.set­Curr
  182. set­D
    1. Array.set­D
  183. set­Goals
    1. Lean.Elab.Tactic.set­Goals
  184. set­Kind
    1. Lean.Syntax.set­Kind
  185. set_option
  186. shift­Left
    1. Nat.shift­Left
    2. ShiftLeft.shift­Left (class method)
  187. shift­Right
    1. Nat.shift­Right
    2. ShiftRight.shift­Right (class method)
  188. show
  189. show_term
  190. simp (0) (1)
  191. simp!
  192. simp?
  193. simp?!
  194. simp_all
  195. simp_all!
  196. simp_all?
  197. simp_all?!
  198. simp_all_arith
  199. simp_all_arith!
  200. simp_arith
  201. simp_arith!
  202. simp_match
  203. simp_wf
  204. simpa
  205. simpa!
  206. simpa?
  207. simpa?!
  208. simprocs
  209. single­Pass
    1. Lean.Meta.Simp.Config.single­Pass (structure field)
  210. singleton
    1. Array.singleton
    2. String.singleton
  211. size
    1. Array.size
    2. Subarray.size
  212. size­Of
    1. SizeOf.size­Of (class method)
  213. skip (0) (1)
  214. skip­Assigned­Instances
    1. tactic.skip­Assigned­Instances
  215. sleep
  216. solve
  217. solve_by_elim
  218. sorry
  219. sort­MVar­Id­Array­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  220. sort­MVar­Ids­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  221. specialize
  222. split
    1. Array.split
    2. String.split
    3. Subarray.split
  223. split­On
    1. String.split­On
  224. start
    1. Subarray.stop (structure field)
  225. start_le_stop
    1. Subarray.stop_le_array_size (structure field)
  226. starts­With
    1. String.starts­With
  227. stop
    1. Subarray.start (structure field)
  228. stop_le_array_size
    1. Subarray.array (structure field)
  229. str
    1. String.str
  230. str­Lit­Kind
    1. Lean.str­Lit­Kind
  231. strong­Induction­On
    1. Nat.strong­Induction­On
  232. sub
    1. Nat.sub
    2. Sub.sub (class method)
  233. sub­Digit­Char
    1. Nat.sub­Digit­Char
  234. subst
  235. subst_eqs
  236. subst_vars
  237. substr­Eq
    1. String.substr­Eq
  238. suffices
  239. super­Digit­Char
    1. Nat.super­Digit­Char
  240. swap
    1. Array.swap
  241. swap!
    1. Array.swap!
  242. swap­At
    1. Array.swap­At
  243. swap­At!
    1. Array.swap­At!
  244. symm
  245. symm_saturate
  246. synthInstance.max­Heartbeats
  247. synthInstance.max­Size
  248. 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.Elab.Tactic.Tactic
    2. Lean.Syntax.Tactic
  5. Tactic­M
    1. Lean.Elab.Tactic.Tactic­M
  6. Term
    1. Lean.Syntax.Term
  7. To­String
  8. ToString.to­String
  9. Transparency­Mode
    1. Lean.Meta.Transparency­Mode
  10. Type
  11. Type­Name
  12. tactic
  13. tactic'
  14. tactic.custom­Eliminators
  15. tactic.dbg_cache
  16. tactic.hygienic
  17. tactic.simp.trace (0) (1)
  18. tactic.skip­Assigned­Instances
  19. tactic­Elab­Attribute
    1. Lean.Elab.Tactic.tactic­Elab­Attribute
  20. tag­Untagged­Goals
    1. Lean.Elab.Tactic.tag­Untagged­Goals
  21. take
    1. Array.take
    2. String.take
    3. Subarray.take
  22. take­Right
    1. String.take­Right
  23. take­Right­While
    1. String.take­Right­While
  24. take­While
    1. Array.take­While
    2. String.take­While
  25. test­Bit
    1. Nat.test­Bit
  26. threshold
    1. pp.deepTerms.threshold
    2. pp.proofs.threshold
  27. throw­Error
    1. Lean.Macro.throw­Error
  28. throw­Error­At
    1. Lean.Macro.throw­Error­At
  29. throw­Unsupported
    1. Lean.Macro.throw­Unsupported
  30. to­Array
    1. Subarray.to­Array
  31. to­Digits
    1. Nat.to­Digits
  32. to­Digits­Core
    1. Nat.to­Digits­Core
  33. to­End
    1. String.Iterator.to­End
  34. to­File­Map
    1. String.to­File­Map
  35. to­Float
    1. Nat.to­Float
  36. to­Format
    1. String.to­Format
  37. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  38. to­Int!
    1. String.to­Int!
  39. to­Int?
    1. String.to­Int?
  40. to­Level
    1. Nat.to­Level
  41. to­List
    1. Array.to­List
    2. Array.to­List (structure field)
    3. String.to­List
  42. to­List­Append
    1. Array.to­List­Append
  43. to­List­Rev
    1. Array.to­List­Rev
  44. to­Lower
    1. String.to­Lower
  45. to­Name
    1. String.to­Name
  46. to­Nat!
    1. String.to­Nat!
  47. to­Nat?
    1. String.to­Nat?
  48. to­PArray'
    1. Array.to­PArray'
  49. to­String
    1. ToString.to­String (class method)
  50. to­Sub­Digits
    1. Nat.to­Sub­Digits
  51. to­Subarray
    1. Array.to­Subarray
  52. to­Subscript­String
    1. Nat.to­Subscript­String
  53. to­Substring
    1. String.to­Substring
  54. to­Substring'
    1. String.to­Substring'
  55. to­Super­Digits
    1. Nat.to­Super­Digits
  56. to­Superscript­String
    1. Nat.to­Superscript­String
  57. to­UInt16
    1. Nat.to­UInt16
  58. to­UInt32
    1. Nat.to­UInt32
  59. to­UInt64
    1. Nat.to­UInt64
  60. to­UInt8
    1. Nat.to­UInt8
  61. to­USize
    1. Nat.to­USize
  62. to­UTF8
    1. String.to­UTF8
  63. to­Upper
    1. String.to­Upper
  64. trace
    1. Lean.Macro.trace
    2. tactic.simp.trace (0) (1)
  65. trace.Meta.Tactic.simp.discharge
  66. trace.Meta.Tactic.simp.rewrite
  67. trace_state (0) (1)
  68. transparency
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  69. trim
    1. String.trim
  70. trim­Left
    1. String.trim­Left
  71. trim­Right
    1. String.trim­Right
  72. trivial
  73. try (0) (1)
  74. try­Catch
    1. Lean.Elab.Tactic.try­Catch
  75. try­Tactic
    1. Lean.Elab.Tactic.try­Tactic
  76. try­Tactic?
    1. Lean.Elab.Tactic.try­Tactic?
  77. type constructor

U

  1. uget
    1. Array.uget
  2. unattach
    1. Array.unattach
  3. unfold (0) (1)
  4. unfold­Partial­App
    1. Lean.Meta.DSimp.Config.beta (structure field)
    2. Lean.Meta.Simp.Config.beta (structure field)
  5. unhygienic
  6. universe
  7. universe polymorphism
  8. unnecessary­Simpa
    1. linter.unnecessary­Simpa
  9. unsupported­Syntax
    1. Lean.Macro.Exception.unsupported­Syntax
  10. unzip
    1. Array.unzip
  11. uset
    1. Array.uset
  12. usize
    1. Array.usize
  13. utf16Length
    1. String.utf16Length
  14. utf16Pos­To­Codepoint­Pos
    1. String.utf16Pos­To­Codepoint­Pos
  15. utf16Pos­To­Codepoint­Pos­From
    1. String.utf16Pos­To­Codepoint­Pos­From
  16. utf8Byte­Size
    1. String.utf8Byte­Size
  17. utf8Decode­Char?
    1. String.utf8Decode­Char?
  18. utf8Encode­Char
    1. String.utf8Encode­Char

V

  1. val
    1. Char.val (structure field)
  2. valid
    1. Char.valid (structure field)
  3. validate­UTF8
    1. String.validate­UTF8

W

  1. whnf
  2. with­Fresh­Macro­Scope
    1. Lean.Macro.with­Fresh­Macro­Scope
  3. with­Location
    1. Lean.Elab.Tactic.with­Location
  4. with­Position
  5. with­Position­After­Linebreak
  6. with_reducible
  7. with_reducible_and_instances
  8. with_unfolding_all
  9. without­Position

X

  1. xor
    1. Nat.xor

Z

  1. Zero
  2. Zero.zero
  3. zero
    1. Zero.zero (class method)
  4. zeta
    1. Lean.Meta.DSimp.Config.zeta­Delta (structure field)
    2. Lean.Meta.Simp.Config.eta (structure field)
  5. zeta­Delta
    1. Lean.Meta.DSimp.Config.proj (structure field)
    2. Lean.Meta.Simp.Config.proj (structure field)
  6. zip
    1. Array.zip
  7. zip­With
    1. Array.zip­With
  8. zip­With­Index
    1. Array.zip­With­Index