Index

Symbols

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

A

  1. ac_rfl
  2. adaptExpander
    1. Lean.Elab.Tactic.adaptExpander
  3. add
    1. Nat.add
  4. admit
  5. all
    1. Nat.all
    2. String.all
  6. allM
    1. Nat.allM
  7. allTR
    1. Nat.allTR
  8. all_goals (0) (1)
  9. and_intros
  10. any
    1. Nat.any
    2. String.any
  11. anyM
    1. Nat.anyM
  12. anyTR
    1. Nat.anyTR
  13. any_goals (0) (1)
  14. append
    1. String.append
  15. appendGoals
    1. Lean.Elab.Tactic.appendGoals
  16. apply (0) (1)
  17. apply?
  18. applyEqLemma
    1. Nat.applyEqLemma
  19. applySimprocConst
    1. Nat.applySimprocConst
  20. apply_assumption
  21. apply_ext_theorem
  22. apply_mod_cast
  23. apply_rfl
  24. apply_rules
  25. arg [@]i
  26. args
  27. arith
    1. Lean.Meta.Simp.Config.ground (structure field)
  28. array_get_dec
  29. assumption
    1. inaccessible
  30. assumption_mod_cast
  31. atEnd
    1. String.Iterator.atEnd
    2. String.atEnd
  32. autoPromoteIndices
    1. inductive.autoPromoteIndices
  33. autoUnfold
    1. Lean.Meta.DSimp.Config.decide (structure field)
    2. Lean.Meta.Simp.Config.decide (structure field)

B

  1. back
    1. String.back
  2. below
    1. Nat.below
  3. beq
    1. Nat.beq
  4. beta
    1. Lean.Meta.DSimp.Config.etaStruct (structure field)
    2. Lean.Meta.Simp.Config.arith (structure field)
  5. bitwise
    1. Nat.bitwise
  6. ble
    1. Nat.ble
  7. blt
    1. Nat.blt
  8. bootstrap.inductiveCheckResultingUniverse
  9. bv_check
  10. bv_decide
  11. bv_decide?
  12. bv_normalize
  13. bv_omega
  14. by_cases
  15. 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. Char.val
  10. Char.valid
  11. Config
    1. Lean.Meta.DSimp.Config
    2. Lean.Meta.Rewrite.Config
    3. Lean.Meta.Simp.Config
  12. calc
  13. capitalize
    1. String.capitalize
  14. case
  15. case ... => ...
  16. case'
  17. case' ... => ...
  18. caseStrongInductionOn
    1. Nat.caseStrongInductionOn
  19. cases
  20. casesOn
    1. Nat.casesOn
  21. cast
    1. Nat.cast
  22. change (0) (1)
  23. change ... with ...
  24. checkpoint
  25. clear
  26. closeMainGoal
    1. Lean.Elab.Tactic.closeMainGoal
  27. closeMainGoalUsing
    1. Lean.Elab.Tactic.closeMainGoalUsing
  28. codepointPosToUtf16Pos
    1. String.codepointPosToUtf16Pos
  29. codepointPosToUtf16PosFrom
    1. String.codepointPosToUtf16PosFrom
  30. codepointPosToUtf8PosFrom
    1. String.codepointPosToUtf8PosFrom
  31. comment
    1. block
    2. line
  32. congr (0) (1)
  33. constructor (0) (1)
  34. contains
    1. String.contains
  35. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  36. contradiction
  37. conv
  38. conv => ...
  39. conv' (0) (1)
  40. crlfToLf
    1. String.crlfToLf
  41. csize
    1. String.csize
  42. cumulativity
  43. curr
    1. String.Iterator.curr
  44. customEliminators
    1. tactic.customEliminators

D

  1. data
    1. String.data (structure field)
  2. dbg_cache
    1. tactic.dbg_cache
  3. dbg_trace
  4. decEq
    1. Nat.decEq
    2. String.decEq
  5. decLe
    1. Nat.decLe
  6. decLt
    1. Nat.decLt
  7. decapitalize
    1. String.decapitalize
  8. decide
    1. Lean.Meta.DSimp.Config.zeta (structure field)
    2. Lean.Meta.Simp.Config.zeta (structure field)
  9. decreasing_tactic
  10. decreasing_trivial
  11. decreasing_with
  12. deepTerms
    1. pp.deepTerms
  13. delta (0) (1)
  14. digitChar
    1. Nat.digitChar
  15. discharge
    1. trace.Meta.Tactic.simp.discharge
  16. div
    1. Nat.div
  17. div2Induction
    1. Nat.div2Induction
  18. done (0) (1)
  19. drop
    1. String.drop
  20. dropRight
    1. String.dropRight
  21. dropRightWhile
    1. String.dropRightWhile
  22. dropWhile
    1. String.dropWhile
  23. dsimp (0) (1)
    1. Lean.Meta.Simp.Config.maxDischargeDepth (structure field)
  24. dsimp!
  25. dsimp?
  26. dsimp?!
  27. dsimpLocation'
    1. Lean.Elab.Tactic.dsimpLocation'

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. elimOffset
    1. Nat.elimOffset
  13. endPos
    1. String.endPos
  14. endsWith
    1. String.endsWith
  15. ensureHasNoMVars
    1. Lean.Elab.Tactic.ensureHasNoMVars
  16. enter
  17. eq_refl
  18. erw (0) (1)
  19. eta
    1. Lean.Meta.DSimp.Config.index (structure field)
    2. Lean.Meta.Simp.Config.maxSteps (structure field)
  20. etaStruct
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.failIfUnchanged (structure field)
  21. exact
  22. exact?
  23. exact_mod_cast
  24. exfalso
  25. exists
  26. ext (0) (1)
  27. ext1
  28. extensionality
    1. of propositions
  29. 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. find
    1. String.find
  6. findLineStart
    1. String.findLineStart
  7. first (0) (1)
  8. firstDiffPos
    1. String.firstDiffPos
  9. focus (0) (1)
    1. Lean.Elab.Tactic.focus
  10. fold
    1. Nat.fold
  11. foldM
    1. Nat.foldM
  12. foldRev
    1. Nat.foldRev
  13. foldRevM
    1. Nat.foldRevM
  14. foldTR
    1. Nat.foldTR
  15. foldl
    1. String.foldl
  16. foldr
    1. String.foldr
  17. forM
    1. Nat.forM
  18. forRevM
    1. Nat.forRevM
  19. forward
    1. String.Iterator.forward
  20. fromExpr?
    1. Nat.fromExpr?
    2. String.fromExpr?
  21. fromUTF8
    1. String.fromUTF8
  22. fromUTF8!
    1. String.fromUTF8!
  23. fromUTF8?
    1. String.fromUTF8?
  24. front
    1. String.front
  25. fun
  26. funext (0) (1)

G

  1. gcd
    1. Nat.gcd
  2. generalize
  3. get
    1. String.get
  4. get!
    1. String.get!
  5. get'
    1. String.get'
  6. get?
    1. String.get?
  7. getCurrMacroScope
    1. Lean.Elab.Tactic.getCurrMacroScope
  8. getFVarId
    1. Lean.Elab.Tactic.getFVarId
  9. getFVarIds
    1. Lean.Elab.Tactic.getFVarIds
  10. getGoals
    1. Lean.Elab.Tactic.getGoals
  11. getMainGoal
    1. Lean.Elab.Tactic.getMainGoal
  12. getMainModule
    1. Lean.Elab.Tactic.getMainModule
  13. getMainTag
    1. Lean.Elab.Tactic.getMainTag
  14. getUnsolvedGoals
    1. Lean.Elab.Tactic.getUnsolvedGoals
  15. getUtf8Byte
    1. String.getUtf8Byte
  16. get_elem_tactic
  17. get_elem_tactic_trivial
  18. goal
    1. main
  19. ground
    1. Lean.Meta.Simp.Config.autoUnfold (structure field)
  20. guard_expr
  21. guard_hyp
  22. guard_target

H

  1. hasNext
    1. String.Iterator.hasNext
  2. hasPrev
    1. String.Iterator.hasPrev
  3. hash
    1. String.hash
  4. have
  5. have'
  6. haveI
  7. hygiene
    1. in tactics
  8. hygienic
    1. tactic.hygienic

I

  1. Iterator
    1. String.Iterator
  2. i
    1. String.Iterator.s (structure field)
  3. ibelow
    1. Nat.ibelow
  4. identifier
    1. raw
  5. if ... then ... else ...
  6. if h : ... then ... else ...
  7. imax
    1. Nat.imax
  8. implicitDefEqProofs
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  9. impredicative
  10. inaccessible
  11. index
    1. Lean.Meta.DSimp.Config.unfoldPartialApp (structure field)
    2. Lean.Meta.Simp.Config.unfoldPartialApp (structure field)
    3. of inductive type
  12. indexed family
    1. of types
  13. induction
  14. inductionOn
    1. Nat.div.inductionOn
    2. Nat.mod.inductionOn
  15. inductive.autoPromoteIndices
  16. inductiveCheckResultingUniverse
    1. bootstrap.inductiveCheckResultingUniverse
  17. infer_instance
  18. injection
  19. injections
  20. intercalate
    1. String.intercalate
  21. intro (0) (1)
  22. intro | ... => ... | ... => ...
  23. intros
  24. iota
    1. Lean.Meta.DSimp.Config.failIfUnchanged (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  25. isAlpha
    1. Char.isAlpha
  26. isAlphanum
    1. Char.isAlphanum
  27. isDigit
    1. Char.isDigit
  28. isEmpty
    1. String.isEmpty
  29. isInt
    1. String.isInt
  30. isLower
    1. Char.isLower
  31. isNat
    1. String.isNat
  32. isPowerOfTwo
    1. Nat.isPowerOfTwo
  33. isPrefixOf
    1. String.isPrefixOf
  34. isUpper
    1. Char.isUpper
  35. isValid
    1. String.Pos.isValid
  36. isValidChar
    1. Nat.isValidChar
  37. isValue
    1. Nat.isValue
  38. isWhitespace
    1. Char.isWhitespace
  39. iter
    1. String.iter
  40. iterate

J

  1. join
    1. String.join

L

  1. Lean.Elab.Tactic.Tactic
  2. Lean.Elab.Tactic.TacticM
  3. Lean.Elab.Tactic.adaptExpander
  4. Lean.Elab.Tactic.appendGoals
  5. Lean.Elab.Tactic.closeMainGoal
  6. Lean.Elab.Tactic.closeMainGoalUsing
  7. Lean.Elab.Tactic.dsimpLocation'
  8. Lean.Elab.Tactic.elabCasesTargets
  9. Lean.Elab.Tactic.elabDSimpConfigCore
  10. Lean.Elab.Tactic.elabSimpArgs
  11. Lean.Elab.Tactic.elabSimpConfig
  12. Lean.Elab.Tactic.elabSimpConfigCtxCore
  13. Lean.Elab.Tactic.elabTerm
  14. Lean.Elab.Tactic.elabTermEnsuringType
  15. Lean.Elab.Tactic.elabTermWithHoles
  16. Lean.Elab.Tactic.ensureHasNoMVars
  17. Lean.Elab.Tactic.focus
  18. Lean.Elab.Tactic.getCurrMacroScope
  19. Lean.Elab.Tactic.getFVarId
  20. Lean.Elab.Tactic.getFVarIds
  21. Lean.Elab.Tactic.getGoals
  22. Lean.Elab.Tactic.getMainGoal
  23. Lean.Elab.Tactic.getMainModule
  24. Lean.Elab.Tactic.getMainTag
  25. Lean.Elab.Tactic.getUnsolvedGoals
  26. Lean.Elab.Tactic.liftMetaMAtMain
  27. Lean.Elab.Tactic.mkTacticAttribute
  28. Lean.Elab.Tactic.orElse
  29. Lean.Elab.Tactic.pruneSolvedGoals
  30. Lean.Elab.Tactic.run
  31. Lean.Elab.Tactic.runTermElab
  32. Lean.Elab.Tactic.setGoals
  33. Lean.Elab.Tactic.sortMVarIdArrayByIndex
  34. Lean.Elab.Tactic.sortMVarIdsByIndex
  35. Lean.Elab.Tactic.tacticElabAttribute
  36. Lean.Elab.Tactic.tagUntaggedGoals
  37. Lean.Elab.Tactic.tryCatch
  38. Lean.Elab.Tactic.tryTactic
  39. Lean.Elab.Tactic.tryTactic?
  40. Lean.Elab.Tactic.withLocation
  41. Lean.Meta.DSimp.Config
  42. Lean.Meta.DSimp.Config.autoUnfold
  43. Lean.Meta.DSimp.Config.beta
  44. Lean.Meta.DSimp.Config.decide
  45. Lean.Meta.DSimp.Config.eta
  46. Lean.Meta.DSimp.Config.etaStruct
  47. Lean.Meta.DSimp.Config.failIfUnchanged
  48. Lean.Meta.DSimp.Config.index
  49. Lean.Meta.DSimp.Config.iota
  50. Lean.Meta.DSimp.Config.mk
    1. Constructor of Lean.Meta.DSimp.Config
  51. Lean.Meta.DSimp.Config.proj
  52. Lean.Meta.DSimp.Config.unfoldPartialApp
  53. Lean.Meta.DSimp.Config.zeta
  54. Lean.Meta.DSimp.Config.zetaDelta
  55. Lean.Meta.Occurrences
  56. Lean.Meta.Occurrences.all
    1. Constructor of Lean.Meta.Occurrences
  57. Lean.Meta.Occurrences.neg
    1. Constructor of Lean.Meta.Occurrences
  58. Lean.Meta.Occurrences.pos
    1. Constructor of Lean.Meta.Occurrences
  59. Lean.Meta.Rewrite.Config
  60. Lean.Meta.Rewrite.Config.mk
    1. Constructor of Lean.Meta.Rewrite.Config
  61. Lean.Meta.Rewrite.Config.newGoals
  62. Lean.Meta.Rewrite.Config.occs
  63. Lean.Meta.Rewrite.Config.offsetCnstrs
  64. Lean.Meta.Rewrite.Config.transparency
  65. Lean.Meta.Rewrite.NewGoals
  66. Lean.Meta.Simp.Config
  67. Lean.Meta.Simp.Config.arith
  68. Lean.Meta.Simp.Config.autoUnfold
  69. Lean.Meta.Simp.Config.beta
  70. Lean.Meta.Simp.Config.contextual
  71. Lean.Meta.Simp.Config.decide
  72. Lean.Meta.Simp.Config.dsimp
  73. Lean.Meta.Simp.Config.eta
  74. Lean.Meta.Simp.Config.etaStruct
  75. Lean.Meta.Simp.Config.failIfUnchanged
  76. Lean.Meta.Simp.Config.ground
  77. Lean.Meta.Simp.Config.implicitDefEqProofs
  78. Lean.Meta.Simp.Config.index
  79. Lean.Meta.Simp.Config.iota
  80. Lean.Meta.Simp.Config.maxDischargeDepth
  81. Lean.Meta.Simp.Config.maxSteps
  82. Lean.Meta.Simp.Config.memoize
  83. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  84. Lean.Meta.Simp.Config.proj
  85. Lean.Meta.Simp.Config.singlePass
  86. Lean.Meta.Simp.Config.unfoldPartialApp
  87. Lean.Meta.Simp.Config.zeta
  88. Lean.Meta.Simp.Config.zetaDelta
  89. Lean.Meta.Simp.neutralConfig
  90. Lean.Meta.SimpExtension
  91. Lean.Meta.TransparencyMode
  92. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.TransparencyMode
  93. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.TransparencyMode
  94. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.TransparencyMode
  95. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.TransparencyMode
  96. Lean.Meta.registerSimpAttr
  97. land
    1. Nat.land
  98. lcm
    1. Nat.lcm
  99. le
    1. Nat.le
    2. String.le
  100. lean_is_string
  101. lean_string_object
  102. lean_to_string
  103. left (0) (1)
  104. length
    1. String.length
  105. let
  106. let rec
  107. let'
  108. letI
  109. level
    1. of universe
  110. lhs
  111. liftMetaMAtMain
    1. Lean.Elab.Tactic.liftMetaMAtMain
  112. linter.unnecessarySimpa
  113. literal
    1. raw string
    2. string
  114. log2
    1. Nat.log2
  115. lor
    1. Nat.lor
  116. lt
    1. Nat.lt
  117. lt_wfRel
    1. Nat.lt_wfRel

M

  1. main goal
  2. map
    1. String.map
  3. match
    1. pp.match
  4. max
    1. Nat.max
  5. maxDischargeDepth
    1. Lean.Meta.Simp.Config.etaStruct (structure field)
  6. maxSteps
    1. Lean.Meta.Simp.Config.zetaDelta (structure field)
    2. pp.maxSteps
  7. memoize
    1. Lean.Meta.Simp.Config.index (structure field)
  8. min
    1. Nat.min
    2. String.Pos.min
  9. mkIterator
    1. String.mkIterator
  10. mkTacticAttribute
    1. Lean.Elab.Tactic.mkTacticAttribute
  11. mod
    1. Nat.mod
  12. modCore
    1. Nat.modCore
  13. modify
    1. String.modify
  14. mul
    1. Nat.mul
  15. mvars
    1. pp.mvars

N

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

O

  1. Occurrences
    1. Lean.Meta.Occurrences
  2. obtain
  3. occs
    1. Lean.Meta.Rewrite.Config.newGoals (structure field)
  4. offsetCnstrs
    1. Lean.Meta.Rewrite.Config.transparency (structure field)
  5. offsetOfPos
    1. String.offsetOfPos
  6. omega
  7. open
  8. orElse
    1. Lean.Elab.Tactic.orElse

P

  1. Pos
    1. String.Pos
  2. Prop
  3. parameter
    1. of inductive type
  4. pattern
  5. polymorphism
    1. universe
  6. pos
    1. String.Iterator.pos
  7. posOf
    1. String.posOf
  8. pow
    1. Nat.pow
  9. pp.deepTerms
  10. pp.deepTerms.threshold
  11. pp.match
  12. pp.maxSteps
  13. pp.mvars
  14. pp.proofs
  15. pp.proofs.threshold
  16. pred
    1. Nat.pred
  17. predicative
  18. prev
    1. String.Iterator.prev
    2. String.prev
  19. prevn
    1. String.Iterator.prevn
  20. proj
    1. Lean.Meta.DSimp.Config.iota (structure field)
    2. Lean.Meta.Simp.Config.memoize (structure field)
  21. proof state
  22. proofs
    1. pp.proofs
  23. propext
  24. proposition
  25. pruneSolvedGoals
    1. Lean.Elab.Tactic.pruneSolvedGoals
  26. push
    1. String.push
  27. push_cast
  28. pushn
    1. String.pushn

Q

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

R

  1. rcases
  2. rec
    1. Nat.rec
  3. recOn
    1. Nat.recOn
  4. recursor
  5. reduce
  6. reduceAdd
    1. Nat.reduceAdd
  7. reduceAppend
    1. String.reduceAppend
  8. reduceBEq
    1. Nat.reduceBEq
    2. String.reduceBEq
  9. reduceBNe
    1. Nat.reduceBNe
    2. String.reduceBNe
  10. reduceBeqDiff
    1. Nat.reduceBeqDiff
  11. reduceBin
    1. Nat.reduceBin
  12. reduceBinPred
    1. Nat.reduceBinPred
    2. String.reduceBinPred
  13. reduceBneDiff
    1. Nat.reduceBneDiff
  14. reduceBoolPred
    1. Nat.reduceBoolPred
    2. String.reduceBoolPred
  15. reduceDiv
    1. Nat.reduceDiv
  16. reduceEq
    1. String.reduceEq
  17. reduceEqDiff
    1. Nat.reduceEqDiff
  18. reduceGE
    1. String.reduceGE
  19. reduceGT
    1. Nat.reduceGT
    2. String.reduceGT
  20. reduceGcd
    1. Nat.reduceGcd
  21. reduceLE
    1. String.reduceLE
  22. reduceLT
    1. Nat.reduceLT
    2. String.reduceLT
  23. reduceLTLE
    1. Nat.reduceLTLE
  24. reduceLeDiff
    1. Nat.reduceLeDiff
  25. reduceMk
    1. String.reduceMk
  26. reduceMod
    1. Nat.reduceMod
  27. reduceMul
    1. Nat.reduceMul
  28. reduceNatEqExpr
    1. Nat.reduceNatEqExpr
  29. reduceNe
    1. String.reduceNe
  30. reducePow
    1. Nat.reducePow
  31. reduceSub
    1. Nat.reduceSub
  32. reduceSubDiff
    1. Nat.reduceSubDiff
  33. reduceSucc
    1. Nat.reduceSucc
  34. reduceUnary
    1. Nat.reduceUnary
  35. reduction
    1. ι (iota)
  36. refine
  37. refine'
  38. registerSimpAttr
    1. Lean.Meta.registerSimpAttr
  39. remainingBytes
    1. String.Iterator.remainingBytes
  40. remainingToString
    1. String.Iterator.remainingToString
  41. removeLeadingSpaces
    1. String.removeLeadingSpaces
  42. rename
  43. rename_i
  44. repeat (0) (1)
    1. Nat.repeat
  45. repeat'
  46. repeat1'
  47. repeatTR
    1. Nat.repeatTR
  48. replace
    1. String.replace
  49. repr
    1. Nat.repr
  50. revFind
    1. String.revFind
  51. revPosOf
    1. String.revPosOf
  52. revert
  53. rewrite (0) (1)
    1. trace.Meta.Tactic.simp.rewrite
  54. rfl (0) (1)
  55. rfl'
  56. rhs
  57. right (0) (1)
  58. rintro
  59. rotate_left
  60. rotate_right
  61. run
    1. Lean.Elab.Tactic.run
  62. runTermElab
    1. Lean.Elab.Tactic.runTermElab
  63. run_tac
  64. rw (0) (1)
  65. rw?
  66. rw_mod_cast
  67. rwa

S

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

T

  1. Tactic
    1. Lean.Elab.Tactic.Tactic
  2. TacticM
    1. Lean.Elab.Tactic.TacticM
  3. TransparencyMode
    1. Lean.Meta.TransparencyMode
  4. Type
  5. tactic
  6. tactic'
  7. tactic.customEliminators
  8. tactic.dbg_cache
  9. tactic.hygienic
  10. tactic.simp.trace (0) (1)
  11. tactic.skipAssignedInstances
  12. tacticElabAttribute
    1. Lean.Elab.Tactic.tacticElabAttribute
  13. tagUntaggedGoals
    1. Lean.Elab.Tactic.tagUntaggedGoals
  14. take
    1. String.take
  15. takeRight
    1. String.takeRight
  16. takeRightWhile
    1. String.takeRightWhile
  17. takeWhile
    1. String.takeWhile
  18. testBit
    1. Nat.testBit
  19. threshold
    1. pp.deepTerms.threshold
    2. pp.proofs.threshold
  20. toDigits
    1. Nat.toDigits
  21. toDigitsCore
    1. Nat.toDigitsCore
  22. toEnd
    1. String.Iterator.toEnd
  23. toFileMap
    1. String.toFileMap
  24. toFloat
    1. Nat.toFloat
  25. toFormat
    1. String.toFormat
  26. toInt!
    1. String.toInt!
  27. toInt?
    1. String.toInt?
  28. toLevel
    1. Nat.toLevel
  29. toList
    1. String.toList
  30. toLower
    1. String.toLower
  31. toName
    1. String.toName
  32. toNat!
    1. String.toNat!
  33. toNat?
    1. String.toNat?
  34. toSubDigits
    1. Nat.toSubDigits
  35. toSubscriptString
    1. Nat.toSubscriptString
  36. toSubstring
    1. String.toSubstring
  37. toSubstring'
    1. String.toSubstring'
  38. toSuperDigits
    1. Nat.toSuperDigits
  39. toSuperscriptString
    1. Nat.toSuperscriptString
  40. toUInt16
    1. Nat.toUInt16
  41. toUInt32
    1. Nat.toUInt32
  42. toUInt64
    1. Nat.toUInt64
  43. toUInt8
    1. Nat.toUInt8
  44. toUSize
    1. Nat.toUSize
  45. toUTF8
    1. String.toUTF8
  46. toUpper
    1. String.toUpper
  47. trace
    1. tactic.simp.trace (0) (1)
  48. trace.Meta.Tactic.simp.discharge
  49. trace.Meta.Tactic.simp.rewrite
  50. trace_state (0) (1)
  51. transparency
    1. Lean.Meta.Rewrite.Config.occs (structure field)
  52. trim
    1. String.trim
  53. trimLeft
    1. String.trimLeft
  54. trimRight
    1. String.trimRight
  55. trivial
  56. try (0) (1)
  57. tryCatch
    1. Lean.Elab.Tactic.tryCatch
  58. tryTactic
    1. Lean.Elab.Tactic.tryTactic
  59. tryTactic?
    1. Lean.Elab.Tactic.tryTactic?
  60. 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. utf16Length
    1. String.utf16Length
  8. utf16PosToCodepointPos
    1. String.utf16PosToCodepointPos
  9. utf16PosToCodepointPosFrom
    1. String.utf16PosToCodepointPosFrom
  10. utf8ByteSize
    1. String.utf8ByteSize
  11. utf8DecodeChar?
    1. String.utf8DecodeChar?
  12. 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. withLocation
    1. Lean.Elab.Tactic.withLocation
  3. with_reducible
  4. with_reducible_and_instances
  5. with_unfolding_all

X

  1. xor
    1. Nat.xor

Z

  1. zeta
    1. Lean.Meta.DSimp.Config.zetaDelta (structure field)
    2. Lean.Meta.Simp.Config.eta (structure field)
  2. zetaDelta
    1. Lean.Meta.DSimp.Config.proj (structure field)
    2. Lean.Meta.Simp.Config.proj (structure field)
String
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.reduceAnd, Nat.strongRecOn, Nat.reduceShiftLeft
Lean.Elab.Tactic
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.withCaseRef, Lean.Elab.Tactic.isHoleRHS, Lean.Elab.Tactic.deltaTarget, Lean.Elab.Tactic.renameInaccessibles, Lean.Elab.Tactic.getNameOfIdent', Lean.Elab.Tactic.elabAsFVar, Lean.Elab.Tactic.tactic.customEliminators, 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.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.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_