feat: add a by? macro (#143)

leanprover-community · May 24, 2023 · 60f19be · 60f19be
1 parent 2f23536
commit 60f19be
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 4 deletions.
diff --git a/Std/Data/List/Basic.lean b/Std/Data/List/Basic.lean
@@ -1194,7 +1194,7 @@ rotate [0, 1, 2, 3, 4, 5] 2 = [2, 3, 4, 5, 0, 1]
   let (l₁, l₂) := List.splitAt (n % l.length) l
   l₂ ++ l₁
 
-/-- rotate' is the same as `rotate`, but slower. Used for proofs about `rotate` -/
+/-- `rotate'` is the same as `rotate`, but slower. Used for proofs about `rotate` -/
 @[simp] def rotate' : List α → Nat → List α
   | [], _ => []
   | l, 0 => l

diff --git a/Std/Tactic/Lint/Frontend.lean b/Std/Tactic/Lint/Frontend.lean
@@ -34,7 +34,7 @@ default ones. e.g. `#lint doc_blame_thm` will run all default tests and `doc_bla
 You can append `only name1 name2 ...` to any command to run a subset of linters, e.g.
 `#lint only unused_arguments in Std`
 
-You can add custom linters by defining a term of type `Linter` with the `@[std_linter]` namespace.
+You can add custom linters by defining a term of type `Linter` with the `@[std_linter]` attribute.
 A linter defined with the name `Std.Tactic.Lint.myNewCheck` can be run with `#lint myNewCheck`
 or `#lint only myNewCheck`.
 If you add the attribute `@[std_linter disabled]` to `linter.myNewCheck` it will be registered,
@@ -64,7 +64,7 @@ inductive LintVerbosity
 /-- `getChecks slow extra use_only` produces a list of linters.
 `extras` is a list of names that should resolve to declarations with type `linter`.
 If `useOnly` is true, it only uses the linters in `extra`.
-Otherwise, it uses all linters in the environment tagged with `@[linter]`.
+Otherwise, it uses all linters in the environment tagged with `@[std_linter]`.
 If `slow` is false, it only uses the fast default tests. -/
 def getChecks (slow : Bool) (useOnly : Bool) : CoreM (Array NamedLinter) := do
   let mut result := #[]

diff --git a/Std/Tactic/Lint/Misc.lean b/Std/Tactic/Lint/Misc.lean
@@ -106,7 +106,7 @@ has been used. -/
     | false, true => pure "is a def, should be lemma/theorem"
     | _, _ => return none
 
-/-- A linter for missing checking whether statements of declarations are well-typed. -/
+/-- A linter for checking whether statements of declarations are well-typed. -/
 @[std_linter] def checkType : Linter where
   noErrorsFound :=
     "The statements of all declarations type-check with default reducibility settings."

diff --git a/Std/Tactic/ShowTerm.lean b/Std/Tactic/ShowTerm.lean
@@ -30,3 +30,12 @@ elab (name := showTerm) tk:"show_term " t:term : term <= ty => do
   Term.synthesizeSyntheticMVarsNoPostponing
   addTermSuggestion tk (← instantiateMVars e).headBeta (origSpan? := ← getRef)
   pure e
+
+/--
+The command `by?` will print a suggestion for replacing the proof block with a proof term
+using `show_term`.
+-/
+syntax (name := by?) "by?" tacticSeq : term
+macro_rules
+  | `(term| by?%$tk $t) => `(show_term%$tk by%$tk $t)
+