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. admit
  9. all
    1. Nat.all
    2. String.all
  10. allM
    1. Nat.allM
  11. allTR
    1. Nat.allTR
  12. all_goals (0) (1)
  13. and_intros
  14. any
    1. Nat.any
    2. String.any
  15. anyM
    1. Nat.anyM
  16. anyTR
    1. Nat.anyTR
  17. any_goals (0) (1)
  18. append
    1. Append.append (class method)
    2. String.append
  19. appendGoals
    1. Lean.Elab.Tactic.appendGoals
  20. apply (0) (1)
  21. apply?
  22. applyEqLemma
    1. Nat.applyEqLemma
  23. applySimprocConst
    1. Nat.applySimprocConst
  24. apply_assumption
  25. apply_ext_theorem
  26. apply_mod_cast
  27. apply_rfl
  28. apply_rules
  29. arg [@]i
  30. args
  31. arith
    1. Lean.Meta.Simp.Config.ground (structure field)
  32. array_get_dec
  33. assumption
    1. inaccessible
  34. assumption_mod_cast
  35. atEnd
    1. String.Iterator.atEnd
    2. String.atEnd
  36. autoPromoteIndices
    1. inductive.autoPromoteIndices
  37. 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. 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. 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. checkpoint
  26. clear
  27. closeMainGoal
    1. Lean.Elab.Tactic.closeMainGoal
  28. closeMainGoalUsing
    1. Lean.Elab.Tactic.closeMainGoalUsing
  29. codepointPosToUtf16Pos
    1. String.codepointPosToUtf16Pos
  30. codepointPosToUtf16PosFrom
    1. String.codepointPosToUtf16PosFrom
  31. codepointPosToUtf8PosFrom
    1. String.codepointPosToUtf8PosFrom
  32. comment
    1. block
    2. line
  33. compare
    1. Ord.compare (class method)
  34. congr (0) (1)
  35. constructor (0) (1)
  36. contains
    1. String.contains
  37. contextual
    1. Lean.Meta.Simp.Config.contextual (structure field)
  38. contradiction
  39. conv
  40. conv => ...
  41. conv' (0) (1)
  42. crlfToLf
    1. String.crlfToLf
  43. csize
    1. String.csize
  44. cumulativity
  45. curr
    1. String.Iterator.curr
  46. 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. 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_of_beq
    1. LawfulBEq.eq_of_beq (class method)
  18. eq_refl
  19. erw (0) (1)
  20. eta
    1. Lean.Meta.DSimp.Config.index (structure field)
    2. Lean.Meta.Simp.Config.maxSteps (structure field)
  21. etaStruct
    1. Lean.Meta.DSimp.Config.eta (structure field)
    2. Lean.Meta.Simp.Config.failIfUnchanged (structure field)
  22. exact
  23. exact?
  24. exact_mod_cast
  25. exfalso
  26. exists
  27. ext (0) (1)
  28. ext1
  29. extensionality
    1. of propositions
  30. 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. 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. getCurrMacroScope
    1. Lean.Elab.Tactic.getCurrMacroScope
  14. getElem
    1. GetElem.getElem (class method)
  15. getElem!
    1. GetElem?.getElem! (class method)
  16. getElem!_def
    1. LawfulGetElem.getElem?_def (class method)
  17. getElem?
    1. GetElem?.getElem? (class method)
  18. getElem?_def
    1. LawfulGetElem.getElem!_def (class method)
  19. getFVarId
    1. Lean.Elab.Tactic.getFVarId
  20. getFVarIds
    1. Lean.Elab.Tactic.getFVarIds
  21. getGoals
    1. Lean.Elab.Tactic.getGoals
  22. getMainGoal
    1. Lean.Elab.Tactic.getMainGoal
  23. getMainModule
    1. Lean.Elab.Tactic.getMainModule
  24. getMainTag
    1. Lean.Elab.Tactic.getMainTag
  25. getUnsolvedGoals
    1. Lean.Elab.Tactic.getUnsolvedGoals
  26. getUtf8Byte
    1. String.getUtf8Byte
  27. get_elem_tactic
  28. get_elem_tactic_trivial
  29. goal
    1. main
  30. ground
    1. Lean.Meta.Simp.Config.autoUnfold (structure field)
  31. guard_expr
  32. guard_hyp
  33. 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. hAdd
    1. HAdd.hAdd (class method)
  30. hAnd
    1. HAnd.hAnd (class method)
  31. hAppend
    1. HAppend.hAppend (class method)
  32. hDiv
    1. HDiv.hDiv (class method)
  33. hMod
    1. HMod.hMod (class method)
  34. hMul
    1. HMul.hMul (class method)
  35. hOr
    1. HOr.hOr (class method)
  36. hPow
    1. HPow.hPow (class method)
  37. hShiftLeft
    1. HShiftLeft.hShiftLeft (class method)
  38. hShiftRight
    1. HShiftRight.hShiftRight (class method)
  39. hSub
    1. HSub.hSub (class method)
  40. hXor
    1. HXor.hXor (class method)
  41. hasNext
    1. String.Iterator.hasNext
  42. hasPrev
    1. String.Iterator.hasPrev
  43. hash
    1. Hashable.hash (class method)
    2. String.hash
  44. have
  45. have'
  46. haveI
  47. hygiene
    1. in tactics
  48. hygienic
    1. tactic.hygienic

I

  1. Inhabited
  2. Inhabited.default
  3. Iterator
    1. String.Iterator
  4. i
    1. String.Iterator.s (structure field)
  5. ibelow
    1. Nat.ibelow
  6. identifier
    1. raw
  7. if ... then ... else ...
  8. if h : ... then ... else ...
  9. imax
    1. Nat.imax
  10. implicitDefEqProofs
    1. Lean.Meta.Simp.Config.dsimp (structure field)
  11. impredicative
  12. inaccessible
  13. index
    1. Lean.Meta.DSimp.Config.unfoldPartialApp (structure field)
    2. Lean.Meta.Simp.Config.unfoldPartialApp (structure field)
    3. of inductive type
  14. indexed family
    1. of types
  15. induction
  16. inductionOn
    1. Nat.div.inductionOn
    2. Nat.mod.inductionOn
  17. inductive.autoPromoteIndices
  18. inductiveCheckResultingUniverse
    1. bootstrap.inductiveCheckResultingUniverse
  19. inferInstance
  20. inferInstanceAs
  21. infer_instance
  22. injection
  23. injections
  24. instance synthesis
  25. intercalate
    1. String.intercalate
  26. intro (0) (1)
  27. intro | ... => ... | ... => ...
  28. intros
  29. iota
    1. Lean.Meta.DSimp.Config.failIfUnchanged (structure field)
    2. Lean.Meta.Simp.Config.iota (structure field)
  30. isAlpha
    1. Char.isAlpha
  31. isAlphanum
    1. Char.isAlphanum
  32. isDigit
    1. Char.isDigit
  33. isEmpty
    1. String.isEmpty
  34. isInt
    1. String.isInt
  35. isLower
    1. Char.isLower
  36. isNat
    1. String.isNat
  37. isPowerOfTwo
    1. Nat.isPowerOfTwo
  38. isPrefixOf
    1. String.isPrefixOf
  39. isUpper
    1. Char.isUpper
  40. isValid
    1. String.Pos.isValid
  41. isValidChar
    1. Nat.isValidChar
  42. isValue
    1. Nat.isValue
  43. isWhitespace
    1. Char.isWhitespace
  44. iter
    1. String.iter
  45. 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. Lean.Elab.Tactic.Tactic
  12. Lean.Elab.Tactic.TacticM
  13. Lean.Elab.Tactic.adaptExpander
  14. Lean.Elab.Tactic.appendGoals
  15. Lean.Elab.Tactic.closeMainGoal
  16. Lean.Elab.Tactic.closeMainGoalUsing
  17. Lean.Elab.Tactic.dsimpLocation'
  18. Lean.Elab.Tactic.elabCasesTargets
  19. Lean.Elab.Tactic.elabDSimpConfigCore
  20. Lean.Elab.Tactic.elabSimpArgs
  21. Lean.Elab.Tactic.elabSimpConfig
  22. Lean.Elab.Tactic.elabSimpConfigCtxCore
  23. Lean.Elab.Tactic.elabTerm
  24. Lean.Elab.Tactic.elabTermEnsuringType
  25. Lean.Elab.Tactic.elabTermWithHoles
  26. Lean.Elab.Tactic.ensureHasNoMVars
  27. Lean.Elab.Tactic.focus
  28. Lean.Elab.Tactic.getCurrMacroScope
  29. Lean.Elab.Tactic.getFVarId
  30. Lean.Elab.Tactic.getFVarIds
  31. Lean.Elab.Tactic.getGoals
  32. Lean.Elab.Tactic.getMainGoal
  33. Lean.Elab.Tactic.getMainModule
  34. Lean.Elab.Tactic.getMainTag
  35. Lean.Elab.Tactic.getUnsolvedGoals
  36. Lean.Elab.Tactic.liftMetaMAtMain
  37. Lean.Elab.Tactic.mkTacticAttribute
  38. Lean.Elab.Tactic.orElse
  39. Lean.Elab.Tactic.pruneSolvedGoals
  40. Lean.Elab.Tactic.run
  41. Lean.Elab.Tactic.runTermElab
  42. Lean.Elab.Tactic.setGoals
  43. Lean.Elab.Tactic.sortMVarIdArrayByIndex
  44. Lean.Elab.Tactic.sortMVarIdsByIndex
  45. Lean.Elab.Tactic.tacticElabAttribute
  46. Lean.Elab.Tactic.tagUntaggedGoals
  47. Lean.Elab.Tactic.tryCatch
  48. Lean.Elab.Tactic.tryTactic
  49. Lean.Elab.Tactic.tryTactic?
  50. Lean.Elab.Tactic.withLocation
  51. Lean.Elab.registerDerivingHandler
  52. Lean.Meta.DSimp.Config
  53. Lean.Meta.DSimp.Config.autoUnfold
  54. Lean.Meta.DSimp.Config.beta
  55. Lean.Meta.DSimp.Config.decide
  56. Lean.Meta.DSimp.Config.eta
  57. Lean.Meta.DSimp.Config.etaStruct
  58. Lean.Meta.DSimp.Config.failIfUnchanged
  59. Lean.Meta.DSimp.Config.index
  60. Lean.Meta.DSimp.Config.iota
  61. Lean.Meta.DSimp.Config.mk
    1. Constructor of Lean.Meta.DSimp.Config
  62. Lean.Meta.DSimp.Config.proj
  63. Lean.Meta.DSimp.Config.unfoldPartialApp
  64. Lean.Meta.DSimp.Config.zeta
  65. Lean.Meta.DSimp.Config.zetaDelta
  66. Lean.Meta.Occurrences
  67. Lean.Meta.Occurrences.all
    1. Constructor of Lean.Meta.Occurrences
  68. Lean.Meta.Occurrences.neg
    1. Constructor of Lean.Meta.Occurrences
  69. Lean.Meta.Occurrences.pos
    1. Constructor of Lean.Meta.Occurrences
  70. Lean.Meta.Rewrite.Config
  71. Lean.Meta.Rewrite.Config.mk
    1. Constructor of Lean.Meta.Rewrite.Config
  72. Lean.Meta.Rewrite.Config.newGoals
  73. Lean.Meta.Rewrite.Config.occs
  74. Lean.Meta.Rewrite.Config.offsetCnstrs
  75. Lean.Meta.Rewrite.Config.transparency
  76. Lean.Meta.Rewrite.NewGoals
  77. Lean.Meta.Simp.Config
  78. Lean.Meta.Simp.Config.arith
  79. Lean.Meta.Simp.Config.autoUnfold
  80. Lean.Meta.Simp.Config.beta
  81. Lean.Meta.Simp.Config.contextual
  82. Lean.Meta.Simp.Config.decide
  83. Lean.Meta.Simp.Config.dsimp
  84. Lean.Meta.Simp.Config.eta
  85. Lean.Meta.Simp.Config.etaStruct
  86. Lean.Meta.Simp.Config.failIfUnchanged
  87. Lean.Meta.Simp.Config.ground
  88. Lean.Meta.Simp.Config.implicitDefEqProofs
  89. Lean.Meta.Simp.Config.index
  90. Lean.Meta.Simp.Config.iota
  91. Lean.Meta.Simp.Config.maxDischargeDepth
  92. Lean.Meta.Simp.Config.maxSteps
  93. Lean.Meta.Simp.Config.memoize
  94. Lean.Meta.Simp.Config.mk
    1. Constructor of Lean.Meta.Simp.Config
  95. Lean.Meta.Simp.Config.proj
  96. Lean.Meta.Simp.Config.singlePass
  97. Lean.Meta.Simp.Config.unfoldPartialApp
  98. Lean.Meta.Simp.Config.zeta
  99. Lean.Meta.Simp.Config.zetaDelta
  100. Lean.Meta.Simp.neutralConfig
  101. Lean.Meta.SimpExtension
  102. Lean.Meta.TransparencyMode
  103. Lean.Meta.TransparencyMode.all
    1. Constructor of Lean.Meta.TransparencyMode
  104. Lean.Meta.TransparencyMode.default
    1. Constructor of Lean.Meta.TransparencyMode
  105. Lean.Meta.TransparencyMode.instances
    1. Constructor of Lean.Meta.TransparencyMode
  106. Lean.Meta.TransparencyMode.reducible
    1. Constructor of Lean.Meta.TransparencyMode
  107. Lean.Meta.registerSimpAttr
  108. land
    1. Nat.land
  109. lcm
    1. Nat.lcm
  110. le
    1. LE.le (class method)
    2. Nat.le
    3. String.le
  111. lean_is_string
  112. lean_string_object
  113. lean_to_string
  114. left (0) (1)
  115. length
    1. String.length
  116. let
  117. let rec
  118. let'
  119. letI
  120. level
    1. of universe
  121. lhs
  122. liftMetaMAtMain
    1. Lean.Elab.Tactic.liftMetaMAtMain
  123. linter.unnecessarySimpa
  124. literal
    1. raw string
    2. string
  125. log2
    1. Nat.log2
  126. lor
    1. Nat.lor
  127. lt
    1. LT.lt (class method)
    2. Nat.lt
  128. lt_wfRel
    1. Nat.lt_wfRel

M

  1. Mod
  2. Mod.mod
  3. Mul
  4. Mul.mul
  5. main goal
  6. map
    1. String.map
  7. match
    1. pp.match
  8. max
    1. Nat.max
  9. maxDischargeDepth
    1. Lean.Meta.Simp.Config.etaStruct (structure field)
  10. maxHeartbeats
    1. synthInstance.maxHeartbeats
  11. maxSize
    1. synthInstance.maxSize
  12. maxSteps
    1. Lean.Meta.Simp.Config.zetaDelta (structure field)
    2. pp.maxSteps
  13. memoize
    1. Lean.Meta.Simp.Config.index (structure field)
  14. min
    1. Nat.min
    2. String.Pos.min
  15. mk
    1. Dynamic.mk
  16. mkIterator
    1. String.mkIterator
  17. mkTacticAttribute
    1. Lean.Elab.Tactic.mkTacticAttribute
  18. mod
    1. Mod.mod (class method)
    2. Nat.mod
  19. modCore
    1. Nat.modCore
  20. modify
    1. String.modify
  21. mul
    1. Mul.mul (class method)
    2. Nat.mul
  22. 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. NatPow
  115. NatPow.pow
  116. NeZero
  117. NeZero.out
  118. Neg
  119. Neg.neg
  120. NewGoals
    1. Lean.Meta.Rewrite.NewGoals
  121. Nonempty
  122. Nonempty.intro
    1. Constructor of Nonempty
  123. namespace
    1. of inductive type
  124. natCast
    1. NatCast.natCast (class method)
  125. native_decide
  126. neg
    1. Neg.neg (class method)
  127. neutralConfig
    1. Lean.Meta.Simp.neutralConfig
  128. newGoals
    1. Lean.Meta.Rewrite.Config.offsetCnstrs (structure field)
  129. next
    1. String.Iterator.next
    2. String.next
  130. next ... => ...
  131. next'
    1. String.next'
  132. nextPowerOfTwo
    1. Nat.nextPowerOfTwo
  133. nextUntil
    1. String.nextUntil
  134. nextWhile
    1. String.nextWhile
  135. nextn
    1. String.Iterator.nextn
  136. noConfusion
    1. Nat.noConfusion
  137. noConfusionType
    1. Nat.noConfusionType
  138. nofun
  139. nomatch
  140. norm_cast (0) (1)

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

Q

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

R

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

S

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

T

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