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. ac_rfl
  6. adapt­Expander
    1. Lean.Elab.Tactic.adapt­Expander
  7. add
    1. Add.add (class method)
    2. Nat.add
  8. add­Macro­Scope
    1. Lean.Macro.add­Macro­Scope
  9. admit
  10. all
    1. Nat.all
    2. String.all
  11. all­M
    1. Nat.all­M
  12. all­TR
    1. Nat.all­TR
  13. all_goals (0) (1)
  14. and_intros
  15. any
    1. Nat.any
    2. String.any
  16. any­M
    1. Nat.any­M
  17. any­TR
    1. Nat.any­TR
  18. any_goals (0) (1)
  19. append
    1. Append.append (class method)
    2. String.append
  20. append­Goals
    1. Lean.Elab.Tactic.append­Goals
  21. apply (0) (1)
  22. apply?
  23. apply­Eq­Lemma
    1. Nat.apply­Eq­Lemma
  24. apply­Simproc­Const
    1. Nat.apply­Simproc­Const
  25. apply_assumption
  26. apply_ext_theorem
  27. apply_mod_cast
  28. apply_rfl
  29. apply_rules
  30. arg [@]i
  31. args
  32. arith
    1. Lean.Meta.Simp.Config.ground (structure field)
  33. array_get_dec
  34. assumption
    1. inaccessible
  35. assumption_mod_cast
  36. at­End
    1. String.Iterator.at­End
    2. String.at­End
  37. auto­Promote­Indices
    1. inductive.auto­Promote­Indices
  38. 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. String.back
  4. backward.synthInstance.canon­Instances
  5. below
    1. Nat.below
  6. beq
    1. BEq.beq (class method)
    2. Nat.beq
  7. beta
    1. Lean.Meta.DSimp.Config.eta­Struct (structure field)
    2. Lean.Meta.Simp.Config.arith (structure field)
  8. bitwise
    1. Nat.bitwise
  9. ble
    1. Nat.ble
  10. blt
    1. Nat.blt
  11. bootstrap.inductive­Check­Resulting­Universe
  12. bv_check
  13. bv_decide
  14. bv_decide?
  15. bv_normalize
  16. bv_omega
  17. by_cases
  18. 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. configuration
    1. of tactics
  40. congr (0) (1)
  41. constructor (0) (1)
  42. contains
    1. String.contains
  43. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  44. contradiction
  45. conv
  46. conv => ...
  47. conv' (0) (1)
  48. crlf­To­Lf
    1. String.crlf­To­Lf
  49. csize
    1. String.csize
  50. cumulativity
  51. curr
    1. String.Iterator.curr
  52. 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
  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. elems­And­Seps
    1. Lean.Syntax.TSepArray.elems­And­Seps (structure field)
  13. elim­Offset
    1. Nat.elim­Offset
  14. end­Pos
    1. String.end­Pos
  15. ends­With
    1. String.ends­With
  16. ensure­Has­No­MVars
    1. Lean.Elab.Tactic.ensure­Has­No­MVars
  17. enter
  18. eq_of_beq
    1. LawfulBEq.eq_of_beq (class method)
  19. eq_refl
  20. erw (0) (1)
  21. eta
    1. Lean.Meta.DSimp.Config.index (structure field)
    2. Lean.Meta.Simp.Config.max­Steps (structure field)
  22. eta­Struct
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.fail­If­Unchanged (structure field)
  23. exact
  24. exact?
  25. exact_mod_cast
  26. exfalso
  27. exists
  28. expand­Macro?
    1. Lean.Macro.expand­Macro?
  29. ext (0) (1)
  30. ext1
  31. extensionality
    1. of propositions
  32. extract
    1. String.Iterator.extract
    2. 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. field­Idx­Kind
    1. Lean.field­Idx­Kind
  6. find
    1. String.find
  7. find­Line­Start
    1. String.find­Line­Start
  8. first (0) (1)
  9. first­Diff­Pos
    1. String.first­Diff­Pos
  10. focus (0) (1)
    1. Lean.Elab.Tactic.focus
  11. fold
    1. Nat.fold
  12. fold­M
    1. Nat.fold­M
  13. fold­Rev
    1. Nat.fold­Rev
  14. fold­Rev­M
    1. Nat.fold­Rev­M
  15. fold­TR
    1. Nat.fold­TR
  16. foldl
    1. String.foldl
  17. foldr
    1. String.foldr
  18. for­M
    1. Nat.for­M
  19. for­Rev­M
    1. Nat.for­Rev­M
  20. forward
    1. String.Iterator.forward
  21. from­Expr?
    1. Nat.from­Expr?
    2. String.from­Expr?
  22. from­UTF8
    1. String.from­UTF8
  23. from­UTF8!
    1. String.from­UTF8!
  24. from­UTF8?
    1. String.from­UTF8?
  25. front
    1. String.front
  26. fun
  27. 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. String.get
  10. get!
    1. String.get!
  11. get'
    1. String.get'
  12. get?
    1. Dynamic.get?
    2. 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­Elem
    1. GetElem.get­Elem (class method)
  17. get­Elem!
    1. GetElem?.get­Elem! (class method)
  18. get­Elem!_def
    1. Lawful­GetElem.get­Elem?_def (class method)
  19. get­Elem?
    1. GetElem?.get­Elem? (class method)
  20. get­Elem?_def
    1. Lawful­GetElem.get­Elem!_def (class method)
  21. get­FVar­Id
    1. Lean.Elab.Tactic.get­FVar­Id
  22. get­FVar­Ids
    1. Lean.Elab.Tactic.get­FVar­Ids
  23. get­Goals
    1. Lean.Elab.Tactic.get­Goals
  24. get­Hygiene­Info
    1. Lean.TSyntax.get­Hygiene­Info
  25. get­Id
    1. Lean.TSyntax.get­Id
  26. get­Kind
    1. Lean.Syntax.get­Kind
  27. get­Main­Goal
    1. Lean.Elab.Tactic.get­Main­Goal
  28. get­Main­Module
    1. Lean.Elab.Tactic.get­Main­Module
  29. get­Main­Tag
    1. Lean.Elab.Tactic.get­Main­Tag
  30. get­Name
    1. Lean.TSyntax.get­Name
  31. get­Nat
    1. Lean.TSyntax.get­Nat
  32. get­Scientific
    1. Lean.TSyntax.get­Scientific
  33. get­String
    1. Lean.TSyntax.get­String
  34. get­Unsolved­Goals
    1. Lean.Elab.Tactic.get­Unsolved­Goals
  35. get­Utf8Byte
    1. String.get­Utf8Byte
  36. get_elem_tactic
  37. get_elem_tactic_trivial
  38. goal
    1. main
  39. ground
    1. Lean.Meta.Simp.Config.auto­Unfold (structure field)
  40. group­Kind
    1. Lean.group­Kind
  41. guard_expr
  42. guard_hyp
  43. 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. indexed family
    1. of types
  17. induction
  18. induction­On
    1. Nat.div.induction­On
    2. Nat.mod.induction­On
  19. inductive.auto­Promote­Indices
  20. inductive­Check­Resulting­Universe
    1. bootstrap.inductive­Check­Resulting­Universe
  21. infer­Instance
  22. infer­Instance­As
  23. infer_instance
  24. injection
  25. injections
  26. instance synthesis
  27. intercalate
    1. String.intercalate
  28. interpolated­Str­Kind
    1. Lean.interpolated­Str­Kind
  29. interpolated­Str­Lit­Kind
    1. Lean.interpolated­Str­Lit­Kind
  30. intro (0) (1)
  31. intro | ... => ... | ... => ...
  32. intros
  33. iota
    1. Lean.Meta.DSimp.Config.fail­If­Unchanged (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  34. is­Alpha
    1. Char.is­Alpha
  35. is­Alphanum
    1. Char.is­Alphanum
  36. is­Digit
    1. Char.is­Digit
  37. is­Empty
    1. String.is­Empty
  38. is­Int
    1. String.is­Int
  39. is­Lower
    1. Char.is­Lower
  40. is­Nat
    1. String.is­Nat
  41. is­Of­Kind
    1. Lean.Syntax.is­Of­Kind
  42. is­Power­Of­Two
    1. Nat.is­Power­Of­Two
  43. is­Prefix­Of
    1. String.is­Prefix­Of
  44. is­Upper
    1. Char.is­Upper
  45. is­Valid
    1. String.Pos.is­Valid
  46. is­Valid­Char
    1. Nat.is­Valid­Char
  47. is­Value
    1. Nat.is­Value
  48. is­Whitespace
    1. Char.is­Whitespace
  49. iter
    1. String.iter
  50. 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_string
  148. lean_string_object
  149. lean_to_string
  150. left (0) (1)
  151. length
    1. String.length
  152. let
  153. let rec
  154. let'
  155. let­I
  156. level
    1. of universe
  157. lhs
  158. lift­Meta­MAt­Main
    1. Lean.Elab.Tactic.lift­Meta­MAt­Main
  159. line­Eq
  160. linter.unnecessary­Simpa
  161. literal
    1. raw string
    2. string
  162. log2
    1. Nat.log2
  163. lor
    1. Nat.lor
  164. lt
    1. LT.lt (class method)
    2. Nat.lt
  165. 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. String.map
  8. match
    1. pp.match
  9. max
    1. Nat.max
  10. max­Discharge­Depth
    1. Lean.Meta.Simp.Config.eta­Struct (structure field)
  11. max­Heartbeats
    1. synthInstance.max­Heartbeats
  12. max­Size
    1. synthInstance.max­Size
  13. max­Steps
    1. Lean.Meta.Simp.Config.zeta­Delta (structure field)
    2. pp.max­Steps
  14. memoize
    1. Lean.Meta.Simp.Config.index (structure field)
  15. min
    1. Nat.min
    2. String.Pos.min
  16. mk
    1. Dynamic.mk
  17. mk­Iterator
    1. String.mk­Iterator
  18. mk­Tactic­Attribute
    1. Lean.Elab.Tactic.mk­Tactic­Attribute
  19. mod
    1. Mod.mod (class method)
    2. Nat.mod
  20. mod­Core
    1. Nat.mod­Core
  21. modify
    1. String.modify
  22. mul
    1. Mul.mul (class method)
    2. Nat.mul
  23. 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. offset­Cnstrs
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  7. offset­Of­Pos
    1. String.offset­Of­Pos
  8. omega
  9. open
  10. or­Else
    1. Lean.Elab.Tactic.or­Else
  11. out
    1. NeZero.out (class method)
  12. 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. pattern
  11. polymorphism
    1. universe
  12. pos
    1. String.Iterator.pos
  13. pos­Of
    1. String.pos­Of
  14. pow
    1. HomogeneousPow.pow (class method)
    2. Nat.pow
    3. NatPow.pow (class method)
    4. Pow.pow (class method)
  15. pp.deep­Terms
  16. pp.deepTerms.threshold
  17. pp.match
  18. pp.max­Steps
  19. pp.mvars
  20. pp.proofs
  21. pp.proofs.threshold
  22. pred
    1. Nat.pred
  23. predicative
  24. prev
    1. String.Iterator.prev
    2. String.prev
  25. prevn
    1. String.Iterator.prevn
  26. proj
    1. Lean.Meta.DSimp.Config.iota (structure field)
    2. Lean.Meta.Simp.Config.memoize (structure field)
  27. proof state
  28. proofs
    1. pp.proofs
  29. propext
  30. proposition
  31. prune­Solved­Goals
    1. Lean.Elab.Tactic.prune­Solved­Goals
  32. push
    1. String.push
  33. push_cast
  34. pushn
    1. String.pushn

Q

  1. quantification
    1. impredicative
    2. predicative
  2. quote
    1. String.quote

R

  1. Repr
  2. Repr.repr­Prec
  3. raw
    1. Lean.TSyntax.raw (structure field)
  4. rcases
  5. rec
    1. Nat.rec
  6. rec­On
    1. Nat.rec­On
  7. recursor
  8. reduce
  9. reduce­Add
    1. Nat.reduce­Add
  10. reduce­Append
    1. String.reduce­Append
  11. reduce­BEq
    1. Nat.reduce­BEq
    2. String.reduce­BEq
  12. reduce­BNe
    1. Nat.reduce­BNe
    2. String.reduce­BNe
  13. reduce­Beq­Diff
    1. Nat.reduce­Beq­Diff
  14. reduce­Bin
    1. Nat.reduce­Bin
  15. reduce­Bin­Pred
    1. Nat.reduce­Bin­Pred
    2. String.reduce­Bin­Pred
  16. reduce­Bne­Diff
    1. Nat.reduce­Bne­Diff
  17. reduce­Bool­Pred
    1. Nat.reduce­Bool­Pred
    2. String.reduce­Bool­Pred
  18. reduce­Div
    1. Nat.reduce­Div
  19. reduce­Eq
    1. String.reduce­Eq
  20. reduce­Eq­Diff
    1. Nat.reduce­Eq­Diff
  21. reduce­GE
    1. String.reduce­GE
  22. reduce­GT
    1. Nat.reduce­GT
    2. String.reduce­GT
  23. reduce­Gcd
    1. Nat.reduce­Gcd
  24. reduce­LE
    1. String.reduce­LE
  25. reduce­LT
    1. Nat.reduce­LT
    2. String.reduce­LT
  26. reduce­LTLE
    1. Nat.reduce­LTLE
  27. reduce­Le­Diff
    1. Nat.reduce­Le­Diff
  28. reduce­Mk
    1. String.reduce­Mk
  29. reduce­Mod
    1. Nat.reduce­Mod
  30. reduce­Mul
    1. Nat.reduce­Mul
  31. reduce­Nat­Eq­Expr
    1. Nat.reduce­Nat­Eq­Expr
  32. reduce­Ne
    1. String.reduce­Ne
  33. reduce­Pow
    1. Nat.reduce­Pow
  34. reduce­Sub
    1. Nat.reduce­Sub
  35. reduce­Sub­Diff
    1. Nat.reduce­Sub­Diff
  36. reduce­Succ
    1. Nat.reduce­Succ
  37. reduce­Unary
    1. Nat.reduce­Unary
  38. reduction
    1. ι (iota)
  39. refine
  40. refine'
  41. register­Deriving­Handler
    1. Lean.Elab.register­Deriving­Handler
  42. register­Simp­Attr
    1. Lean.Meta.register­Simp­Attr
  43. remaining­Bytes
    1. String.Iterator.remaining­Bytes
  44. remaining­To­String
    1. String.Iterator.remaining­To­String
  45. remove­Leading­Spaces
    1. String.remove­Leading­Spaces
  46. rename
  47. rename_i
  48. repeat (0) (1)
    1. Nat.repeat
  49. repeat'
  50. repeat1'
  51. repeat­TR
    1. Nat.repeat­TR
  52. replace
    1. String.replace
  53. repr
    1. Nat.repr
  54. repr­Prec
    1. Repr.repr­Prec (class method)
  55. resolve­Global­Name
    1. Lean.Macro.resolve­Global­Name
  56. resolve­Namespace
    1. Lean.Macro.resolve­Namespace
  57. rev­Find
    1. String.rev­Find
  58. rev­Pos­Of
    1. String.rev­Pos­Of
  59. revert
  60. rewrite (0) (1)
    1. trace.Meta.Tactic.simp.rewrite
  61. rfl (0) (1)
    1. LawfulBEq.rfl (class method)
  62. rfl'
  63. rhs
  64. right (0) (1)
  65. rintro
  66. rotate_left
  67. rotate_right
  68. run
    1. Lean.Elab.Tactic.run
  69. run­Term­Elab
    1. Lean.Elab.Tactic.run­Term­Elab
  70. run_tac
  71. rw (0) (1)
  72. rw?
  73. rw_mod_cast
  74. 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. Syntax
    1. Lean.Syntax
  147. Syntax­Node­Kind
    1. Lean.Syntax­Node­Kind
  148. s
    1. String.Iterator.i (structure field)
  149. save
  150. scientific­Lit­Kind
    1. Lean.scientific­Lit­Kind
  151. semi­Out­Param
  152. set
    1. String.set
  153. set­Curr
    1. String.Iterator.set­Curr
  154. set­Goals
    1. Lean.Elab.Tactic.set­Goals
  155. set­Kind
    1. Lean.Syntax.set­Kind
  156. set_option
  157. shift­Left
    1. Nat.shift­Left
    2. ShiftLeft.shift­Left (class method)
  158. shift­Right
    1. Nat.shift­Right
    2. ShiftRight.shift­Right (class method)
  159. show
  160. show_term
  161. simp (0) (1)
  162. simp!
  163. simp?
  164. simp?!
  165. simp_all
  166. simp_all!
  167. simp_all?
  168. simp_all?!
  169. simp_all_arith
  170. simp_all_arith!
  171. simp_arith
  172. simp_arith!
  173. simp_match
  174. simp_wf
  175. simpa
  176. simpa!
  177. simpa?
  178. simpa?!
  179. simprocs
  180. single­Pass
    1. Lean.Meta.Simp.Config.single­Pass (structure field)
  181. singleton
    1. String.singleton
  182. size­Of
    1. SizeOf.size­Of (class method)
  183. skip (0) (1)
  184. skip­Assigned­Instances
    1. tactic.skip­Assigned­Instances
  185. sleep
  186. solve
  187. solve_by_elim
  188. sorry
  189. sort­MVar­Id­Array­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Id­Array­By­Index
  190. sort­MVar­Ids­By­Index
    1. Lean.Elab.Tactic.sort­MVar­Ids­By­Index
  191. specialize
  192. split
    1. String.split
  193. split­On
    1. String.split­On
  194. starts­With
    1. String.starts­With
  195. stop
  196. str
    1. String.str
  197. str­Lit­Kind
    1. Lean.str­Lit­Kind
  198. strong­Induction­On
    1. Nat.strong­Induction­On
  199. sub
    1. Nat.sub
    2. Sub.sub (class method)
  200. sub­Digit­Char
    1. Nat.sub­Digit­Char
  201. subst
  202. subst_eqs
  203. subst_vars
  204. substr­Eq
    1. String.substr­Eq
  205. suffices
  206. super­Digit­Char
    1. Nat.super­Digit­Char
  207. symm
  208. symm_saturate
  209. synthInstance.max­Heartbeats
  210. synthInstance.max­Size
  211. 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. String.take
  22. take­Right
    1. String.take­Right
  23. take­Right­While
    1. String.take­Right­While
  24. take­While
    1. 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­Digits
    1. Nat.to­Digits
  31. to­Digits­Core
    1. Nat.to­Digits­Core
  32. to­End
    1. String.Iterator.to­End
  33. to­File­Map
    1. String.to­File­Map
  34. to­Float
    1. Nat.to­Float
  35. to­Format
    1. String.to­Format
  36. to­Get­Elem
    1. GetElem?.to­Get­Elem (class method)
  37. to­Int!
    1. String.to­Int!
  38. to­Int?
    1. String.to­Int?
  39. to­Level
    1. Nat.to­Level
  40. to­List
    1. String.to­List
  41. to­Lower
    1. String.to­Lower
  42. to­Name
    1. String.to­Name
  43. to­Nat!
    1. String.to­Nat!
  44. to­Nat?
    1. String.to­Nat?
  45. to­String
    1. ToString.to­String (class method)
  46. to­Sub­Digits
    1. Nat.to­Sub­Digits
  47. to­Subscript­String
    1. Nat.to­Subscript­String
  48. to­Substring
    1. String.to­Substring
  49. to­Substring'
    1. String.to­Substring'
  50. to­Super­Digits
    1. Nat.to­Super­Digits
  51. to­Superscript­String
    1. Nat.to­Superscript­String
  52. to­UInt16
    1. Nat.to­UInt16
  53. to­UInt32
    1. Nat.to­UInt32
  54. to­UInt64
    1. Nat.to­UInt64
  55. to­UInt8
    1. Nat.to­UInt8
  56. to­USize
    1. Nat.to­USize
  57. to­UTF8
    1. String.to­UTF8
  58. to­Upper
    1. String.to­Upper
  59. trace
    1. Lean.Macro.trace
    2. tactic.simp.trace (0) (1)
  60. trace.Meta.Tactic.simp.discharge
  61. trace.Meta.Tactic.simp.rewrite
  62. trace_state (0) (1)
  63. transparency
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  64. trim
    1. String.trim
  65. trim­Left
    1. String.trim­Left
  66. trim­Right
    1. String.trim­Right
  67. trivial
  68. try (0) (1)
  69. try­Catch
    1. Lean.Elab.Tactic.try­Catch
  70. try­Tactic
    1. Lean.Elab.Tactic.try­Tactic
  71. try­Tactic?
    1. Lean.Elab.Tactic.try­Tactic?
  72. type constructor

U

  1. unfold (0) (1)
  2. unfold­Partial­App
    1. Lean.Meta.DSimp.Config.beta (structure field)
    2. Lean.Meta.Simp.Config.beta (structure field)
  3. unhygienic
  4. universe
  5. universe polymorphism
  6. unnecessary­Simpa
    1. linter.unnecessary­Simpa
  7. unsupported­Syntax
    1. Lean.Macro.Exception.unsupported­Syntax
  8. utf16Length
    1. String.utf16Length
  9. utf16Pos­To­Codepoint­Pos
    1. String.utf16Pos­To­Codepoint­Pos
  10. utf16Pos­To­Codepoint­Pos­From
    1. String.utf16Pos­To­Codepoint­Pos­From
  11. utf8Byte­Size
    1. String.utf8Byte­Size
  12. utf8Decode­Char?
    1. String.utf8Decode­Char?
  13. 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)
String
String.dropSuffix?, String.stripSuffix, String.stripPrefix, String.dropPrefix?, String.data, String.mk
Nat
Nat.caseStrongRecOn, Nat.reduceXor, Nat.reduceShiftRight, Nat.reduceOr, Nat.and_forall_succ, Nat.and_two_pow_identity, Nat.le.step, Nat.sum, Nat.zero, Nat.le.refl, Nat.succ, Nat.or_exists_succ, Nat.and_pow_two_is_mod, Nat.toInt8, Nat.reduceAnd, Nat.strongRecOn, Nat.reduceShiftLeft
Lean.Elab.Tactic
Lean.Elab.Tactic.tryCatchRestore, Lean.Elab.Tactic.withRWRulesSeq, Lean.Elab.Tactic.unfoldLocalDecl, Lean.Elab.Tactic.expandOptLocation, Lean.Elab.Tactic.expandLocation, Lean.Elab.Tactic.deltaLocalDecl, Lean.Elab.Tactic.addCheckpoints, Lean.Elab.Tactic.mkTacticInfo, Lean.Elab.Tactic.evalClassical, Lean.Elab.Tactic.withCaseRef, Lean.Elab.Tactic.isHoleRHS, Lean.Elab.Tactic.deltaTarget, Lean.Elab.Tactic.pushGoals, Lean.Elab.Tactic.renameInaccessibles, Lean.Elab.Tactic.commandConfigElab, Lean.Elab.Tactic.getNameOfIdent', Lean.Elab.Tactic.pushGoal, Lean.Elab.Tactic.elabAsFVar, Lean.Elab.Tactic.tactic.customEliminators, Lean.Elab.Tactic.popMainGoal, Lean.Elab.Tactic.getInductiveValFromMajor, Lean.Elab.Tactic.tacticToDischarge, Lean.Elab.Tactic.rewriteLocalDecl, Lean.Elab.Tactic.elabSimpConfigCore, Lean.Elab.Tactic.saveTacticInfoForToken, Lean.Elab.Tactic.focusAndDone, Lean.Elab.Tactic.unfoldTarget, Lean.Elab.Tactic.getMainTarget, Lean.Elab.Tactic.withSimpDiagnostics, Lean.Elab.Tactic.checkCommandConfigElab, Lean.Elab.Tactic.dsimpLocation, Lean.Elab.Tactic.getMainDecl, Lean.Elab.Tactic.zetaDeltaLocalDecl, Lean.Elab.Tactic.elabTermForApply, Lean.Elab.Tactic.rewriteTarget, Lean.Elab.Tactic.configElab, Lean.Elab.Tactic.simpLocation, Lean.Elab.Tactic.refineCore, Lean.Elab.Tactic.evalDecideCore.diagnose, Lean.Elab.Tactic.throwNoGoalsToBeSolved, Lean.Elab.Tactic.closeUsingOrAdmit, Lean.Elab.Tactic.forEachVar, Lean.Elab.Tactic.checkConfigElab, Lean.Elab.Tactic.withTacticInfoContext, Lean.Elab.Tactic.withRestoreOrSaveFull, Lean.Elab.Tactic.logUnassignedAndAbort, Lean.Elab.Tactic.evalDecideBang, Lean.Elab.Tactic.traceSimpCall, Lean.Elab.Tactic.zetaDeltaTarget, Lean.Elab.Tactic.mkSimpContext, Lean.Elab.Tactic.withMacroExpansion, Lean.Elab.Tactic.evalDecideCore, Lean.Elab.Tactic.withCollectingNewGoalsFrom, Lean.Elab.Tactic.withMainContext, Lean.Elab.Tactic.elabRewriteConfig, Lean.Elab.Tactic.mkInitialTacticInfo, Lean.Elab.Tactic.liftMetaFinishingTactic, Lean.Elab.Tactic.mkSimpOnly, Lean.Elab.Tactic.classical, Lean.Elab.Tactic.liftMetaTactic1, Lean.Elab.Tactic.isCheckpointableTactic, Lean.Elab.Tactic.saveState, Lean.Elab.Tactic.mkSimpCallStx, Lean.Elab.Tactic.filterOldMVars, Lean.Elab.Tactic.replaceMainGoal, Lean.Elab.Tactic.liftMetaTactic, Lean.Elab.Tactic.done, Lean.Elab.Tactic.simpOnlyBuiltins, Lean.Elab.Tactic.withoutRecover
Char
Char.reduceVal, Char.ofUInt8, Char.reduceOfNatAux, Char.reduceIsDigit, Char.reduceUnary, Char.reduceBEq, Char.reduceEq, Char.fromExpr?, Char.rec, Char.reduceIsWhitespace, Char.recOn, Char.toNat, Char.toLower, Char.toUpper, Char.toUInt8, Char.reduceNe, Char.reduceIsUpper, Char.noConfusion, Char.quoteCore.smallCharToHex, Char.quote, Char.le, Char.reduceIsAlpha, Char.val, Char.reduceToNat, Char.reduceIsLower, Char.lt, Char.casesOn, Char.utf16Size, Char.mk, Char.reduceBNe, Char.isValidCharNat, Char.toString, Char.repr, Char.reduceToString, Char.reduceDefault, Char.reduceGT, Char.reduceLE, Char.ofNatAux, Char.reduceBinPred, Char.reduceToLower, Char.reduceLT, Char.isValue, Char.reduceGE, Char.utf8Size, Char.reduceIsAlphaNum, Char.reduceBoolPred, Char.quoteCore, Char.noConfusionType, Char.reduceToUpper, Char.ofNat
Tactics
Lean.Parser.Tactic.decideBang, Lean.Parser.Tactic.acNf0, Lean.Parser.Tactic.tacticAc_nf_, Lean.Parser.Tactic.classical