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. adaptExpander
    1. Lean.Elab.Tactic.adaptExpander
  7. add
    1. Add.add (class method)
    2. Nat.add
  8. addMacroScope
    1. Lean.Macro.addMacroScope
  9. admit
  10. all
    1. Nat.all
    2. String.all
  11. allM
    1. Nat.allM
  12. allTR
    1. Nat.allTR
  13. all_goals (0) (1)
  14. and_intros
  15. any
    1. Nat.any
    2. String.any
  16. anyM
    1. Nat.anyM
  17. anyTR
    1. Nat.anyTR
  18. any_goals (0) (1)
  19. append
    1. Append.append (class method)
    2. String.append
  20. appendGoals
    1. Lean.Elab.Tactic.appendGoals
  21. apply (0) (1)
  22. apply?
  23. applyEqLemma
    1. Nat.applyEqLemma
  24. applySimprocConst
    1. Nat.applySimprocConst
  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. atEnd
    1. String.Iterator.atEnd
    2. String.atEnd
  37. autoPromoteIndices
    1. inductive.autoPromoteIndices
  38. autoUnfold
    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.canonInstances
  5. below
    1. Nat.below
  6. beq
    1. BEq.beq (class method)
    2. Nat.beq
  7. beta
    1. Lean.Meta.DSimp.Config.etaStruct (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.inductiveCheckResultingUniverse
  12. bv_check
  13. bv_decide
  14. bv_decide?
  15. bv_normalize
  16. bv_omega
  17. by_cases
  18. byteIdx
    1. String.Pos.byteIdx (structure field)

C

  1. Char
  2. Char.isAlpha
  3. Char.isAlphanum
  4. Char.isDigit
  5. Char.isLower
  6. Char.isUpper
  7. Char.isWhitespace
  8. Char.mk
    1. Constructor of Char
  9. CharLit
    1. Lean.Syntax.CharLit
  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. canonInstances
    1. backward.synthInstance.canonInstances
  14. capitalize
    1. String.capitalize
  15. case
  16. case ... => ...
  17. case'
  18. case' ... => ...
  19. caseStrongInductionOn
    1. Nat.caseStrongInductionOn
  20. cases
  21. casesOn
    1. Nat.casesOn
  22. cast
    1. Nat.cast
  23. change (0) (1)
  24. change ... with ...
  25. charLitKind
    1. Lean.charLitKind
  26. checkpoint
  27. choiceKind
    1. Lean.choiceKind
  28. clear
  29. closeMainGoal
    1. Lean.Elab.Tactic.closeMainGoal
  30. closeMainGoalUsing
    1. Lean.Elab.Tactic.closeMainGoalUsing
  31. codepointPosToUtf16Pos
    1. String.codepointPosToUtf16Pos
  32. codepointPosToUtf16PosFrom
    1. String.codepointPosToUtf16PosFrom
  33. codepointPosToUtf8PosFrom
    1. String.codepointPosToUtf8PosFrom
  34. colEq
  35. colGe
  36. colGt
  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. crlfToLf
    1. String.crlfToLf
  49. csize
    1. String.csize
  50. cumulativity
  51. curr
    1. String.Iterator.curr
  52. customEliminators
    1. tactic.customEliminators

D

  1. Decidable
  2. Decidable.isFalse
    1. Constructor of Decidable
  3. Decidable.isTrue
    1. Constructor of Decidable
  4. DecidableEq
  5. DecidableRel
  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. decEq
    1. Nat.decEq
    2. String.decEq
  17. decLe
    1. Nat.decLe
  18. decLt
    1. Nat.decLt
  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. deepTerms
    1. pp.deepTerms
  25. default
    1. Inhabited.default (class method)
  26. delta (0) (1)
  27. digitChar
    1. Nat.digitChar
  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. dropRight
    1. String.dropRight
  34. dropRightWhile
    1. String.dropRightWhile
  35. dropWhile
    1. String.dropWhile
  36. dsimp (0) (1)
    1. Lean.Meta.Simp.Config.maxDischargeDepth (structure field)
  37. dsimp!
  38. dsimp?
  39. dsimp?!
  40. dsimpLocation'
    1. Lean.Elab.Tactic.dsimpLocation'
  41. dvd
    1. Dvd.dvd (class method)

E

  1. Even
  2. Even.plusTwo
    1. Constructor of Even
  3. Even.zero
    1. Constructor of Even
  4. elabCasesTargets
    1. Lean.Elab.Tactic.elabCasesTargets
  5. elabDSimpConfigCore
    1. Lean.Elab.Tactic.elabDSimpConfigCore
  6. elabSimpArgs
    1. Lean.Elab.Tactic.elabSimpArgs
  7. elabSimpConfig
    1. Lean.Elab.Tactic.elabSimpConfig
  8. elabSimpConfigCtxCore
    1. Lean.Elab.Tactic.elabSimpConfigCtxCore
  9. elabTerm
    1. Lean.Elab.Tactic.elabTerm
  10. elabTermEnsuringType
    1. Lean.Elab.Tactic.elabTermEnsuringType
  11. elabTermWithHoles
    1. Lean.Elab.Tactic.elabTermWithHoles
  12. elemsAndSeps
    1. Lean.Syntax.TSepArray.elemsAndSeps (structure field)
  13. elimOffset
    1. Nat.elimOffset
  14. endPos
    1. String.endPos
  15. endsWith
    1. String.endsWith
  16. ensureHasNoMVars
    1. Lean.Elab.Tactic.ensureHasNoMVars
  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.maxSteps (structure field)
  22. etaStruct
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.failIfUnchanged (structure field)
  23. exact
  24. exact?
  25. exact_mod_cast
  26. exfalso
  27. exists
  28. expandMacro?
    1. Lean.Macro.expandMacro?
  29. ext (0) (1)
  30. ext1
  31. extensionality
    1. of propositions
  32. extract
    1. String.Iterator.extract
    2. String.extract

F

  1. fail
  2. failIfUnchanged
    1. Lean.Meta.DSimp.Config.autoUnfold (structure field)
    2. Lean.Meta.Simp.Config.implicitDefEqProofs (structure field)
  3. fail_if_success (0) (1)
  4. false_or_by_contra
  5. fieldIdxKind
    1. Lean.fieldIdxKind
  6. find
    1. String.find
  7. findLineStart
    1. String.findLineStart
  8. first (0) (1)
  9. firstDiffPos
    1. String.firstDiffPos
  10. focus (0) (1)
    1. Lean.Elab.Tactic.focus
  11. fold
    1. Nat.fold
  12. foldM
    1. Nat.foldM
  13. foldRev
    1. Nat.foldRev
  14. foldRevM
    1. Nat.foldRevM
  15. foldTR
    1. Nat.foldTR
  16. foldl
    1. String.foldl
  17. foldr
    1. String.foldr
  18. forM
    1. Nat.forM
  19. forRevM
    1. Nat.forRevM
  20. forward
    1. String.Iterator.forward
  21. fromExpr?
    1. Nat.fromExpr?
    2. String.fromExpr?
  22. fromUTF8
    1. String.fromUTF8
  23. fromUTF8!
    1. String.fromUTF8!
  24. fromUTF8?
    1. String.fromUTF8?
  25. front
    1. String.front
  26. fun
  27. funext (0) (1)

G

  1. GetElem
  2. GetElem.getElem
  3. GetElem?
  4. GetElem?.getElem!
  5. GetElem?.getElem?
  6. GetElem?.toGetElem
  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. getChar
    1. Lean.TSyntax.getChar
  14. getCurrMacroScope
    1. Lean.Elab.Tactic.getCurrMacroScope
  15. getCurrNamespace
    1. Lean.Macro.getCurrNamespace
  16. getElem
    1. GetElem.getElem (class method)
  17. getElem!
    1. GetElem?.getElem! (class method)
  18. getElem!_def
    1. LawfulGetElem.getElem?_def (class method)
  19. getElem?
    1. GetElem?.getElem? (class method)
  20. getElem?_def
    1. LawfulGetElem.getElem!_def (class method)
  21. getFVarId
    1. Lean.Elab.Tactic.getFVarId
  22. getFVarIds
    1. Lean.Elab.Tactic.getFVarIds
  23. getGoals
    1. Lean.Elab.Tactic.getGoals
  24. getHygieneInfo
    1. Lean.TSyntax.getHygieneInfo
  25. getId
    1. Lean.TSyntax.getId
  26. getKind
    1. Lean.Syntax.getKind
  27. getMainGoal
    1. Lean.Elab.Tactic.getMainGoal
  28. getMainModule
    1. Lean.Elab.Tactic.getMainModule
  29. getMainTag
    1. Lean.Elab.Tactic.getMainTag
  30. getName
    1. Lean.TSyntax.getName
  31. getNat
    1. Lean.TSyntax.getNat
  32. getScientific
    1. Lean.TSyntax.getScientific
  33. getString
    1. Lean.TSyntax.getString
  34. getUnsolvedGoals
    1. Lean.Elab.Tactic.getUnsolvedGoals
  35. getUtf8Byte
    1. String.getUtf8Byte
  36. get_elem_tactic
  37. get_elem_tactic_trivial
  38. goal
    1. main
  39. ground
    1. Lean.Meta.Simp.Config.autoUnfold (structure field)
  40. groupKind
    1. Lean.groupKind
  41. guard_expr
  42. guard_hyp
  43. guard_target

H

  1. HAdd
  2. HAdd.hAdd
  3. HAnd
  4. HAnd.hAnd
  5. HAppend
  6. HAppend.hAppend
  7. HDiv
  8. HDiv.hDiv
  9. HMod
  10. HMod.hMod
  11. HMul
  12. HMul.hMul
  13. HOr
  14. HOr.hOr
  15. HPow
  16. HPow.hPow
  17. HShiftLeft
  18. HShiftLeft.hShiftLeft
  19. HShiftRight
  20. HShiftRight.hShiftRight
  21. HSub
  22. HSub.hSub
  23. HXor
  24. HXor.hXor
  25. Hashable
  26. Hashable.hash
  27. HomogeneousPow
  28. HomogeneousPow.pow
  29. HygieneInfo
    1. Lean.Syntax.HygieneInfo
  30. hAdd
    1. HAdd.hAdd (class method)
  31. hAnd
    1. HAnd.hAnd (class method)
  32. hAppend
    1. HAppend.hAppend (class method)
  33. hDiv
    1. HDiv.hDiv (class method)
  34. hMod
    1. HMod.hMod (class method)
  35. hMul
    1. HMul.hMul (class method)
  36. hOr
    1. HOr.hOr (class method)
  37. hPow
    1. HPow.hPow (class method)
  38. hShiftLeft
    1. HShiftLeft.hShiftLeft (class method)
  39. hShiftRight
    1. HShiftRight.hShiftRight (class method)
  40. hSub
    1. HSub.hSub (class method)
  41. hXor
    1. HXor.hXor (class method)
  42. hasDecl
    1. Lean.Macro.hasDecl
  43. hasNext
    1. String.Iterator.hasNext
  44. hasPrev
    1. String.Iterator.hasPrev
  45. hash
    1. Hashable.hash (class method)
    2. String.hash
  46. have
  47. have'
  48. haveI
  49. hygiene
    1. in tactics
  50. hygieneInfoKind
    1. Lean.hygieneInfoKind
  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. identKind
    1. Lean.identKind
  8. identifier
    1. raw
  9. if ... then ... else ...
  10. if h : ... then ... else ...
  11. imax
    1. Nat.imax
  12. implicitDefEqProofs
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  13. impredicative
  14. inaccessible
  15. index
    1. Lean.Meta.DSimp.Config.unfoldPartialApp (structure field)
    2. Lean.Meta.Simp.Config.unfoldPartialApp (structure field)
    3. of inductive type
  16. indexed family
    1. of types
  17. induction
  18. inductionOn
    1. Nat.div.inductionOn
    2. Nat.mod.inductionOn
  19. inductive.autoPromoteIndices
  20. inductiveCheckResultingUniverse
    1. bootstrap.inductiveCheckResultingUniverse
  21. inferInstance
  22. inferInstanceAs
  23. infer_instance
  24. injection
  25. injections
  26. instance synthesis
  27. intercalate
    1. String.intercalate
  28. interpolatedStrKind
    1. Lean.interpolatedStrKind
  29. interpolatedStrLitKind
    1. Lean.interpolatedStrLitKind
  30. intro (0) (1)
  31. intro | ... => ... | ... => ...
  32. intros
  33. iota
    1. Lean.Meta.DSimp.Config.failIfUnchanged (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  34. isAlpha
    1. Char.isAlpha
  35. isAlphanum
    1. Char.isAlphanum
  36. isDigit
    1. Char.isDigit
  37. isEmpty
    1. String.isEmpty
  38. isInt
    1. String.isInt
  39. isLower
    1. Char.isLower
  40. isNat
    1. String.isNat
  41. isOfKind
    1. Lean.Syntax.isOfKind
  42. isPowerOfTwo
    1. Nat.isPowerOfTwo
  43. isPrefixOf
    1. String.isPrefixOf
  44. isUpper
    1. Char.isUpper
  45. isValid
    1. String.Pos.isValid
  46. isValidChar
    1. Nat.isValidChar
  47. isValue
    1. Nat.isValue
  48. isWhitespace
    1. Char.isWhitespace
  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. LawfulBEq
  6. LawfulBEq.eq_of_beq
  7. LawfulBEq.rfl
  8. LawfulGetElem
  9. LawfulGetElem.getElem!_def
  10. LawfulGetElem.getElem?_def
  11. LeadingIdentBehavior
    1. Lean.Parser.LeadingIdentBehavior
  12. Lean.Elab.Tactic.Tactic
  13. Lean.Elab.Tactic.TacticM
  14. Lean.Elab.Tactic.adaptExpander
  15. Lean.Elab.Tactic.appendGoals
  16. Lean.Elab.Tactic.closeMainGoal
  17. Lean.Elab.Tactic.closeMainGoalUsing
  18. Lean.Elab.Tactic.dsimpLocation'
  19. Lean.Elab.Tactic.elabCasesTargets
  20. Lean.Elab.Tactic.elabDSimpConfigCore
  21. Lean.Elab.Tactic.elabSimpArgs
  22. Lean.Elab.Tactic.elabSimpConfig
  23. Lean.Elab.Tactic.elabSimpConfigCtxCore
  24. Lean.Elab.Tactic.elabTerm
  25. Lean.Elab.Tactic.elabTermEnsuringType
  26. Lean.Elab.Tactic.elabTermWithHoles
  27. Lean.Elab.Tactic.ensureHasNoMVars
  28. Lean.Elab.Tactic.focus
  29. Lean.Elab.Tactic.getCurrMacroScope
  30. Lean.Elab.Tactic.getFVarId
  31. Lean.Elab.Tactic.getFVarIds
  32. Lean.Elab.Tactic.getGoals
  33. Lean.Elab.Tactic.getMainGoal
  34. Lean.Elab.Tactic.getMainModule
  35. Lean.Elab.Tactic.getMainTag
  36. Lean.Elab.Tactic.getUnsolvedGoals
  37. Lean.Elab.Tactic.liftMetaMAtMain
  38. Lean.Elab.Tactic.mkTacticAttribute
  39. Lean.Elab.Tactic.orElse
  40. Lean.Elab.Tactic.pruneSolvedGoals
  41. Lean.Elab.Tactic.run
  42. Lean.Elab.Tactic.runTermElab
  43. Lean.Elab.Tactic.setGoals
  44. Lean.Elab.Tactic.sortMVarIdArrayByIndex
  45. Lean.Elab.Tactic.sortMVarIdsByIndex
  46. Lean.Elab.Tactic.tacticElabAttribute
  47. Lean.Elab.Tactic.tagUntaggedGoals
  48. Lean.Elab.Tactic.tryCatch
  49. Lean.Elab.Tactic.tryTactic
  50. Lean.Elab.Tactic.tryTactic?
  51. Lean.Elab.Tactic.withLocation
  52. Lean.Elab.registerDerivingHandler
  53. Lean.Macro.Exception.unsupportedSyntax
  54. Lean.Macro.addMacroScope
  55. Lean.Macro.expandMacro?
  56. Lean.Macro.getCurrNamespace
  57. Lean.Macro.hasDecl
  58. Lean.Macro.resolveGlobalName
  59. Lean.Macro.resolveNamespace
  60. Lean.Macro.throwError
  61. Lean.Macro.throwErrorAt
  62. Lean.Macro.throwUnsupported
  63. Lean.Macro.trace
  64. Lean.Macro.withFreshMacroScope
  65. Lean.MacroM
  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.NewGoals
  75. Lean.Meta.Simp.Config
  76. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  77. Lean.Meta.Simp.neutralConfig
  78. Lean.Meta.SimpExtension
  79. Lean.Meta.TransparencyMode
  80. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.TransparencyMode
  81. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.TransparencyMode
  82. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.TransparencyMode
  83. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.TransparencyMode
  84. Lean.Meta.registerSimpAttr
  85. Lean.Parser.LeadingIdentBehavior
  86. Lean.Parser.LeadingIdentBehavior.both
    1. Constructor of Lean.Parser.LeadingIdentBehavior
  87. Lean.Parser.LeadingIdentBehavior.default
    1. Constructor of Lean.Parser.LeadingIdentBehavior
  88. Lean.Parser.LeadingIdentBehavior.symbol
    1. Constructor of Lean.Parser.LeadingIdentBehavior
  89. Lean.SourceInfo
  90. Lean.SourceInfo.none
    1. Constructor of Lean.SourceInfo
  91. Lean.SourceInfo.original
    1. Constructor of Lean.SourceInfo
  92. Lean.SourceInfo.synthetic
    1. Constructor of Lean.SourceInfo
  93. Lean.Syntax
  94. Lean.Syntax.CharLit
  95. Lean.Syntax.Command
  96. Lean.Syntax.HygieneInfo
  97. Lean.Syntax.Ident
  98. Lean.Syntax.Level
  99. Lean.Syntax.NameLit
  100. Lean.Syntax.NumLit
  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.ScientificLit
  107. Lean.Syntax.StrLit
  108. Lean.Syntax.TSepArray
  109. Lean.Syntax.TSepArray.mk
    1. Constructor of Lean.Syntax.TSepArray
  110. Lean.Syntax.Tactic
  111. Lean.Syntax.Term
  112. Lean.Syntax.atom
    1. Constructor of Lean.Syntax
  113. Lean.Syntax.getKind
  114. Lean.Syntax.ident
    1. Constructor of Lean.Syntax
  115. Lean.Syntax.isOfKind
  116. Lean.Syntax.missing
    1. Constructor of Lean.Syntax
  117. Lean.Syntax.node
    1. Constructor of Lean.Syntax
  118. Lean.Syntax.setKind
  119. Lean.SyntaxNodeKind
  120. Lean.TSyntax
  121. Lean.TSyntax.getChar
  122. Lean.TSyntax.getHygieneInfo
  123. Lean.TSyntax.getId
  124. Lean.TSyntax.getName
  125. Lean.TSyntax.getNat
  126. Lean.TSyntax.getScientific
  127. Lean.TSyntax.getString
  128. Lean.TSyntax.mk
    1. Constructor of Lean.TSyntax
  129. Lean.TSyntaxArray
  130. Lean.charLitKind
  131. Lean.choiceKind
  132. Lean.fieldIdxKind
  133. Lean.groupKind
  134. Lean.hygieneInfoKind
  135. Lean.identKind
  136. Lean.interpolatedStrKind
  137. Lean.interpolatedStrLitKind
  138. Lean.nameLitKind
  139. Lean.nullKind
  140. Lean.numLitKind
  141. Lean.scientificLitKind
  142. Lean.strLitKind
  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. letI
  156. level
    1. of universe
  157. lhs
  158. liftMetaMAtMain
    1. Lean.Elab.Tactic.liftMetaMAtMain
  159. lineEq
  160. linter.unnecessarySimpa
  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_wfRel
    1. Nat.lt_wfRel

M

  1. MacroM
    1. Lean.MacroM
  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. maxDischargeDepth
    1. Lean.Meta.Simp.Config.etaStruct (structure field)
  11. maxHeartbeats
    1. synthInstance.maxHeartbeats
  12. maxSize
    1. synthInstance.maxSize
  13. maxSteps
    1. Lean.Meta.Simp.Config.zetaDelta (structure field)
    2. pp.maxSteps
  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. mkIterator
    1. String.mkIterator
  18. mkTacticAttribute
    1. Lean.Elab.Tactic.mkTacticAttribute
  19. mod
    1. Mod.mod (class method)
    2. Nat.mod
  20. modCore
    1. Nat.modCore
  21. modify
    1. String.modify
  22. mul
    1. Mul.mul (class method)
    2. Nat.mul
  23. mvars
    1. pp.mvars

N

  1. NameLit
    1. Lean.Syntax.NameLit
  2. Nat
  3. Nat.add
  4. Nat.all
  5. Nat.allM
  6. Nat.allTR
  7. Nat.any
  8. Nat.anyM
  9. Nat.anyTR
  10. Nat.applyEqLemma
  11. Nat.applySimprocConst
  12. Nat.below
  13. Nat.beq
  14. Nat.bitwise
  15. Nat.ble
  16. Nat.blt
  17. Nat.caseStrongInductionOn
  18. Nat.casesOn
  19. Nat.cast
  20. Nat.decEq
  21. Nat.decLe
  22. Nat.decLt
  23. Nat.digitChar
  24. Nat.div
  25. Nat.div.inductionOn
  26. Nat.div2Induction
  27. Nat.elimOffset
  28. Nat.fold
  29. Nat.foldM
  30. Nat.foldRev
  31. Nat.foldRevM
  32. Nat.foldTR
  33. Nat.forM
  34. Nat.forRevM
  35. Nat.fromExpr?
  36. Nat.gcd
  37. Nat.ibelow
  38. Nat.imax
  39. Nat.isPowerOfTwo
  40. Nat.isValidChar
  41. Nat.isValue
  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_wfRel
  51. Nat.max
  52. Nat.min
  53. Nat.mod
  54. Nat.mod.inductionOn
  55. Nat.modCore
  56. Nat.mul
  57. Nat.nextPowerOfTwo
  58. Nat.noConfusion
  59. Nat.noConfusionType
  60. Nat.pow
  61. Nat.pred
  62. Nat.rec
  63. Nat.recOn
  64. Nat.reduceAdd
  65. Nat.reduceBEq
  66. Nat.reduceBNe
  67. Nat.reduceBeqDiff
  68. Nat.reduceBin
  69. Nat.reduceBinPred
  70. Nat.reduceBneDiff
  71. Nat.reduceBoolPred
  72. Nat.reduceDiv
  73. Nat.reduceEqDiff
  74. Nat.reduceGT
  75. Nat.reduceGcd
  76. Nat.reduceLT
  77. Nat.reduceLTLE
  78. Nat.reduceLeDiff
  79. Nat.reduceMod
  80. Nat.reduceMul
  81. Nat.reduceNatEqExpr
  82. Nat.reducePow
  83. Nat.reduceSub
  84. Nat.reduceSubDiff
  85. Nat.reduceSucc
  86. Nat.reduceUnary
  87. Nat.repeat
  88. Nat.repeatTR
  89. Nat.repr
  90. Nat.shiftLeft
  91. Nat.shiftRight
  92. Nat.strongInductionOn
  93. Nat.sub
  94. Nat.subDigitChar
  95. Nat.succ
    1. Constructor of Nat
  96. Nat.superDigitChar
  97. Nat.testBit
  98. Nat.toDigits
  99. Nat.toDigitsCore
  100. Nat.toFloat
  101. Nat.toLevel
  102. Nat.toSubDigits
  103. Nat.toSubscriptString
  104. Nat.toSuperDigits
  105. Nat.toSuperscriptString
  106. Nat.toUInt16
  107. Nat.toUInt32
  108. Nat.toUInt64
  109. Nat.toUInt8
  110. Nat.toUSize
  111. Nat.xor
  112. Nat.zero
    1. Constructor of Nat
  113. NatCast
  114. NatCast.natCast
  115. NatPow
  116. NatPow.pow
  117. NeZero
  118. NeZero.out
  119. Neg
  120. Neg.neg
  121. NewGoals
    1. Lean.Meta.Rewrite.NewGoals
  122. Nonempty
  123. Nonempty.intro
    1. Constructor of Nonempty
  124. NumLit
    1. Lean.Syntax.NumLit
  125. nameLitKind
    1. Lean.nameLitKind
  126. namespace
    1. of inductive type
  127. natCast
    1. NatCast.natCast (class method)
  128. native_decide
  129. neg
    1. Neg.neg (class method)
  130. neutralConfig
    1. Lean.Meta.Simp.neutralConfig
  131. newGoals
    1. Lean.Meta.Rewrite.Config.offsetCnstrs (structure field)
  132. next
    1. String.Iterator.next
    2. String.next
  133. next ... => ...
  134. next'
    1. String.next'
  135. nextPowerOfTwo
    1. Nat.nextPowerOfTwo
  136. nextUntil
    1. String.nextUntil
  137. nextWhile
    1. String.nextWhile
  138. nextn
    1. String.Iterator.nextn
  139. noConfusion
    1. Nat.noConfusion
  140. noConfusionType
    1. Nat.noConfusionType
  141. nofun
  142. nomatch
  143. norm_cast (0) (1)
  144. nullKind
    1. Lean.nullKind
  145. numLitKind
    1. Lean.numLitKind

O

  1. Occurrences
    1. Lean.Meta.Occurrences
  2. Ord
  3. Ord.compare
  4. obtain
  5. occs
    1. Lean.Meta.Rewrite.Config.newGoals (structure field)
  6. offsetCnstrs
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  7. offsetOfPos
    1. String.offsetOfPos
  8. omega
  9. open
  10. orElse
    1. Lean.Elab.Tactic.orElse
  11. out
    1. NeZero.out (class method)
  12. outParam

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. posOf
    1. String.posOf
  14. pow
    1. HomogeneousPow.pow (class method)
    2. Nat.pow
    3. NatPow.pow (class method)
    4. Pow.pow (class method)
  15. pp.deepTerms
  16. pp.deepTerms.threshold
  17. pp.match
  18. pp.maxSteps
  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. pruneSolvedGoals
    1. Lean.Elab.Tactic.pruneSolvedGoals
  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.reprPrec
  3. raw
    1. Lean.TSyntax.raw (structure field)
  4. rcases
  5. rec
    1. Nat.rec
  6. recOn
    1. Nat.recOn
  7. recursor
  8. reduce
  9. reduceAdd
    1. Nat.reduceAdd
  10. reduceAppend
    1. String.reduceAppend
  11. reduceBEq
    1. Nat.reduceBEq
    2. String.reduceBEq
  12. reduceBNe
    1. Nat.reduceBNe
    2. String.reduceBNe
  13. reduceBeqDiff
    1. Nat.reduceBeqDiff
  14. reduceBin
    1. Nat.reduceBin
  15. reduceBinPred
    1. Nat.reduceBinPred
    2. String.reduceBinPred
  16. reduceBneDiff
    1. Nat.reduceBneDiff
  17. reduceBoolPred
    1. Nat.reduceBoolPred
    2. String.reduceBoolPred
  18. reduceDiv
    1. Nat.reduceDiv
  19. reduceEq
    1. String.reduceEq
  20. reduceEqDiff
    1. Nat.reduceEqDiff
  21. reduceGE
    1. String.reduceGE
  22. reduceGT
    1. Nat.reduceGT
    2. String.reduceGT
  23. reduceGcd
    1. Nat.reduceGcd
  24. reduceLE
    1. String.reduceLE
  25. reduceLT
    1. Nat.reduceLT
    2. String.reduceLT
  26. reduceLTLE
    1. Nat.reduceLTLE
  27. reduceLeDiff
    1. Nat.reduceLeDiff
  28. reduceMk
    1. String.reduceMk
  29. reduceMod
    1. Nat.reduceMod
  30. reduceMul
    1. Nat.reduceMul
  31. reduceNatEqExpr
    1. Nat.reduceNatEqExpr
  32. reduceNe
    1. String.reduceNe
  33. reducePow
    1. Nat.reducePow
  34. reduceSub
    1. Nat.reduceSub
  35. reduceSubDiff
    1. Nat.reduceSubDiff
  36. reduceSucc
    1. Nat.reduceSucc
  37. reduceUnary
    1. Nat.reduceUnary
  38. reduction
    1. ι (iota)
  39. refine
  40. refine'
  41. registerDerivingHandler
    1. Lean.Elab.registerDerivingHandler
  42. registerSimpAttr
    1. Lean.Meta.registerSimpAttr
  43. remainingBytes
    1. String.Iterator.remainingBytes
  44. remainingToString
    1. String.Iterator.remainingToString
  45. removeLeadingSpaces
    1. String.removeLeadingSpaces
  46. rename
  47. rename_i
  48. repeat (0) (1)
    1. Nat.repeat
  49. repeat'
  50. repeat1'
  51. repeatTR
    1. Nat.repeatTR
  52. replace
    1. String.replace
  53. repr
    1. Nat.repr
  54. reprPrec
    1. Repr.reprPrec (class method)
  55. resolveGlobalName
    1. Lean.Macro.resolveGlobalName
  56. resolveNamespace
    1. Lean.Macro.resolveNamespace
  57. revFind
    1. String.revFind
  58. revPosOf
    1. String.revPosOf
  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. runTermElab
    1. Lean.Elab.Tactic.runTermElab
  70. run_tac
  71. rw (0) (1)
  72. rw?
  73. rw_mod_cast
  74. rwa

S

  1. ScientificLit
    1. Lean.Syntax.ScientificLit
  2. ShiftLeft
  3. ShiftLeft.shiftLeft
  4. ShiftRight
  5. ShiftRight.shiftRight
  6. SimpExtension
    1. Lean.Meta.SimpExtension
  7. SizeOf
  8. SizeOf.sizeOf
  9. Sort
  10. SourceInfo
    1. Lean.SourceInfo
  11. StrLit
    1. Lean.Syntax.StrLit
  12. String
  13. String.Iterator
  14. String.Iterator.atEnd
  15. String.Iterator.curr
  16. String.Iterator.extract
  17. String.Iterator.forward
  18. String.Iterator.hasNext
  19. String.Iterator.hasPrev
  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.remainingBytes
  27. String.Iterator.remainingToString
  28. String.Iterator.setCurr
  29. String.Iterator.toEnd
  30. String.Pos
  31. String.Pos.isValid
  32. String.Pos.min
  33. String.Pos.mk
    1. Constructor of String.Pos
  34. String.all
  35. String.any
  36. String.append
  37. String.atEnd
  38. String.back
  39. String.capitalize
  40. String.codepointPosToUtf16Pos
  41. String.codepointPosToUtf16PosFrom
  42. String.codepointPosToUtf8PosFrom
  43. String.contains
  44. String.crlfToLf
  45. String.csize
  46. String.decEq
  47. String.decapitalize
  48. String.drop
  49. String.dropRight
  50. String.dropRightWhile
  51. String.dropWhile
  52. String.endPos
  53. String.endsWith
  54. String.extract
  55. String.find
  56. String.findLineStart
  57. String.firstDiffPos
  58. String.foldl
  59. String.foldr
  60. String.fromExpr?
  61. String.fromUTF8
  62. String.fromUTF8!
  63. String.fromUTF8?
  64. String.front
  65. String.get
  66. String.get!
  67. String.get'
  68. String.get?
  69. String.getUtf8Byte
  70. String.hash
  71. String.intercalate
  72. String.isEmpty
  73. String.isInt
  74. String.isNat
  75. String.isPrefixOf
  76. String.iter
  77. String.join
  78. String.le
  79. String.length
  80. String.map
  81. String.mk
    1. Constructor of String
  82. String.mkIterator
  83. String.modify
  84. String.next
  85. String.next'
  86. String.nextUntil
  87. String.nextWhile
  88. String.offsetOfPos
  89. String.posOf
  90. String.prev
  91. String.push
  92. String.pushn
  93. String.quote
  94. String.reduceAppend
  95. String.reduceBEq
  96. String.reduceBNe
  97. String.reduceBinPred
  98. String.reduceBoolPred
  99. String.reduceEq
  100. String.reduceGE
  101. String.reduceGT
  102. String.reduceLE
  103. String.reduceLT
  104. String.reduceMk
  105. String.reduceNe
  106. String.removeLeadingSpaces
  107. String.replace
  108. String.revFind
  109. String.revPosOf
  110. String.set
  111. String.singleton
  112. String.split
  113. String.splitOn
  114. String.startsWith
  115. String.str
  116. String.substrEq
  117. String.take
  118. String.takeRight
  119. String.takeRightWhile
  120. String.takeWhile
  121. String.toFileMap
  122. String.toFormat
  123. String.toInt!
  124. String.toInt?
  125. String.toList
  126. String.toLower
  127. String.toName
  128. String.toNat!
  129. String.toNat?
  130. String.toSubstring
  131. String.toSubstring'
  132. String.toUTF8
  133. String.toUpper
  134. String.trim
  135. String.trimLeft
  136. String.trimRight
  137. String.utf16Length
  138. String.utf16PosToCodepointPos
  139. String.utf16PosToCodepointPosFrom
  140. String.utf8ByteSize
  141. String.utf8DecodeChar?
  142. String.utf8EncodeChar
  143. String.validateUTF8
  144. Sub
  145. Sub.sub
  146. Syntax
    1. Lean.Syntax
  147. SyntaxNodeKind
    1. Lean.SyntaxNodeKind
  148. s
    1. String.Iterator.i (structure field)
  149. save
  150. scientificLitKind
    1. Lean.scientificLitKind
  151. semiOutParam
  152. set
    1. String.set
  153. setCurr
    1. String.Iterator.setCurr
  154. setGoals
    1. Lean.Elab.Tactic.setGoals
  155. setKind
    1. Lean.Syntax.setKind
  156. set_option
  157. shiftLeft
    1. Nat.shiftLeft
    2. ShiftLeft.shiftLeft (class method)
  158. shiftRight
    1. Nat.shiftRight
    2. ShiftRight.shiftRight (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. singlePass
    1. Lean.Meta.Simp.Config.singlePass (structure field)
  181. singleton
    1. String.singleton
  182. sizeOf
    1. SizeOf.sizeOf (class method)
  183. skip (0) (1)
  184. skipAssignedInstances
    1. tactic.skipAssignedInstances
  185. sleep
  186. solve
  187. solve_by_elim
  188. sorry
  189. sortMVarIdArrayByIndex
    1. Lean.Elab.Tactic.sortMVarIdArrayByIndex
  190. sortMVarIdsByIndex
    1. Lean.Elab.Tactic.sortMVarIdsByIndex
  191. specialize
  192. split
    1. String.split
  193. splitOn
    1. String.splitOn
  194. startsWith
    1. String.startsWith
  195. stop
  196. str
    1. String.str
  197. strLitKind
    1. Lean.strLitKind
  198. strongInductionOn
    1. Nat.strongInductionOn
  199. sub
    1. Nat.sub
    2. Sub.sub (class method)
  200. subDigitChar
    1. Nat.subDigitChar
  201. subst
  202. subst_eqs
  203. subst_vars
  204. substrEq
    1. String.substrEq
  205. suffices
  206. superDigitChar
    1. Nat.superDigitChar
  207. symm
  208. symm_saturate
  209. synthInstance.maxHeartbeats
  210. synthInstance.maxSize
  211. synthesis
    1. of type class instances

T

  1. TSepArray
    1. Lean.Syntax.TSepArray
  2. TSyntax
    1. Lean.TSyntax
  3. TSyntaxArray
    1. Lean.TSyntaxArray
  4. Tactic
    1. Lean.Elab.Tactic.Tactic
    2. Lean.Syntax.Tactic
  5. TacticM
    1. Lean.Elab.Tactic.TacticM
  6. Term
    1. Lean.Syntax.Term
  7. ToString
  8. ToString.toString
  9. TransparencyMode
    1. Lean.Meta.TransparencyMode
  10. Type
  11. TypeName
  12. tactic
  13. tactic'
  14. tactic.customEliminators
  15. tactic.dbg_cache
  16. tactic.hygienic
  17. tactic.simp.trace (0) (1)
  18. tactic.skipAssignedInstances
  19. tacticElabAttribute
    1. Lean.Elab.Tactic.tacticElabAttribute
  20. tagUntaggedGoals
    1. Lean.Elab.Tactic.tagUntaggedGoals
  21. take
    1. String.take
  22. takeRight
    1. String.takeRight
  23. takeRightWhile
    1. String.takeRightWhile
  24. takeWhile
    1. String.takeWhile
  25. testBit
    1. Nat.testBit
  26. threshold
    1. pp.deepTerms.threshold
    2. pp.proofs.threshold
  27. throwError
    1. Lean.Macro.throwError
  28. throwErrorAt
    1. Lean.Macro.throwErrorAt
  29. throwUnsupported
    1. Lean.Macro.throwUnsupported
  30. toDigits
    1. Nat.toDigits
  31. toDigitsCore
    1. Nat.toDigitsCore
  32. toEnd
    1. String.Iterator.toEnd
  33. toFileMap
    1. String.toFileMap
  34. toFloat
    1. Nat.toFloat
  35. toFormat
    1. String.toFormat
  36. toGetElem
    1. GetElem?.toGetElem (class method)
  37. toInt!
    1. String.toInt!
  38. toInt?
    1. String.toInt?
  39. toLevel
    1. Nat.toLevel
  40. toList
    1. String.toList
  41. toLower
    1. String.toLower
  42. toName
    1. String.toName
  43. toNat!
    1. String.toNat!
  44. toNat?
    1. String.toNat?
  45. toString
    1. ToString.toString (class method)
  46. toSubDigits
    1. Nat.toSubDigits
  47. toSubscriptString
    1. Nat.toSubscriptString
  48. toSubstring
    1. String.toSubstring
  49. toSubstring'
    1. String.toSubstring'
  50. toSuperDigits
    1. Nat.toSuperDigits
  51. toSuperscriptString
    1. Nat.toSuperscriptString
  52. toUInt16
    1. Nat.toUInt16
  53. toUInt32
    1. Nat.toUInt32
  54. toUInt64
    1. Nat.toUInt64
  55. toUInt8
    1. Nat.toUInt8
  56. toUSize
    1. Nat.toUSize
  57. toUTF8
    1. String.toUTF8
  58. toUpper
    1. String.toUpper
  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. trimLeft
    1. String.trimLeft
  66. trimRight
    1. String.trimRight
  67. trivial
  68. try (0) (1)
  69. tryCatch
    1. Lean.Elab.Tactic.tryCatch
  70. tryTactic
    1. Lean.Elab.Tactic.tryTactic
  71. tryTactic?
    1. Lean.Elab.Tactic.tryTactic?
  72. type constructor

U

  1. unfold (0) (1)
  2. unfoldPartialApp
    1. Lean.Meta.DSimp.Config.beta (structure field)
    2. Lean.Meta.Simp.Config.beta (structure field)
  3. unhygienic
  4. universe
  5. universe polymorphism
  6. unnecessarySimpa
    1. linter.unnecessarySimpa
  7. unsupportedSyntax
    1. Lean.Macro.Exception.unsupportedSyntax
  8. utf16Length
    1. String.utf16Length
  9. utf16PosToCodepointPos
    1. String.utf16PosToCodepointPos
  10. utf16PosToCodepointPosFrom
    1. String.utf16PosToCodepointPosFrom
  11. utf8ByteSize
    1. String.utf8ByteSize
  12. utf8DecodeChar?
    1. String.utf8DecodeChar?
  13. utf8EncodeChar
    1. String.utf8EncodeChar

V

  1. val
    1. Char.val (structure field)
  2. valid
    1. Char.valid (structure field)
  3. validateUTF8
    1. String.validateUTF8

W

  1. whnf
  2. withFreshMacroScope
    1. Lean.Macro.withFreshMacroScope
  3. withLocation
    1. Lean.Elab.Tactic.withLocation
  4. withPosition
  5. withPositionAfterLinebreak
  6. with_reducible
  7. with_reducible_and_instances
  8. with_unfolding_all
  9. withoutPosition

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.zetaDelta (structure field)
    2. Lean.Meta.Simp.Config.eta (structure field)
  5. zetaDelta
    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