feat: add trivial extensible (macro) tactic

src/Init/Core.lean

@@ -983,7 +983,7 @@ instance : Subsingleton (Squash α) where
     induction a using Squash.ind
     induction b using Squash.ind
     apply Quot.sound
-    exact trivial
+    trivial
 
 namespace Lean
 /- Kernel reduction hints -/

src/Init/Notation.lean

@@ -302,6 +302,14 @@ syntax "repeat " tacticSeq : tactic
 macro_rules
   | `(tactic| repeat $seq) => `(tactic| first ($seq); repeat $seq | skip)
 
+syntax "trivial" : tactic
+
+macro_rules | `(tactic| trivial) => `(tactic| assumption)
+macro_rules | `(tactic| trivial) => `(tactic| rfl)
+macro_rules | `(tactic| trivial) => `(tactic| contradiction)
+macro_rules | `(tactic| trivial) => `(tactic| apply True.intro)
+macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)
+
 end Tactic
 
 namespace Attr

tests/lean/run/extmacro.lean

@@ -1,19 +1,19 @@
 macro "ext_tactic" t:tactic "=>" newT:tactic : command => `(macro_rules | `($t) => `($newT))
 
-syntax "trivial" : tactic
+syntax "trivial'" : tactic
 
-ext_tactic trivial => apply Eq.refl
+ext_tactic trivial' => apply Eq.refl
 
 theorem tst1 (x : Nat) : x = x :=
-by trivial
+by trivial'
 
 -- theorem tst2 (x y : Nat) (h : x = y) : x = y :=
--- by trivial -- fail as expected
+-- by trivial' -- fail as expected
 
-ext_tactic trivial => assumption
+ext_tactic trivial' => assumption
 
 theorem tst1b (x : Nat) : x = x :=
-by trivial -- still works
+by trivial' -- still works
 
 theorem tst2 (x y : Nat) (h : x = y) : x = y :=
-by trivial -- works too
+by trivial' -- works too