From f4c72025ee93ef2a1c20c7981209c7cbe061c749 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Aug 2021 09:33:32 -0700
Subject: [PATCH] feat: add `calc` tactic macro

---
 src/Init/NotationExtra.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index a62107e949..996695cb9d 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -101,6 +101,8 @@ macro_rules
   | `(calc $p:term := $h:term) => `(show $p from $h)
   | `(calc $p:term := $h:term $rest:calcStep*) => ``(trans (show $p from $h) (calc $rest:calcStep*))
 
+macro "calc " steps:withPosition(calcStep+) : tactic => `(exact calc $(steps.getArgs)*)
+
 @[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
   | _       => throw ()