From 7386cc3b126cf77dbdb270cdd6988f7abbf7b4ae Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Tue, 8 Jul 2025 15:57:22 +0200
Subject: [PATCH] chore: Turn `Std.Do.Triple` elaborator into a macro (#9251)

This PR demotes the builtin elaborators for `Std.Do.PostCond.total` and
`Std.Do.Triple` into macros, following the DefEq improvements of #9015.

Co-authored-by: Sebastian Graf <sg@lean-fro.org>
---
 src/Lean/Elab/Tactic/Do/Syntax.lean | 6 ++++--
 src/Std/Do/PostCond.lean            | 7 ++++++-
 src/Std/Do/Triple/Basic.lean        | 3 ++-
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Do/Syntax.lean b/src/Lean/Elab/Tactic/Do/Syntax.lean
index 0c234300c6..08a4e394d2 100644
--- a/src/Lean/Elab/Tactic/Do/Syntax.lean
+++ b/src/Lean/Elab/Tactic/Do/Syntax.lean
@@ -14,7 +14,8 @@ namespace Std.Do
 open Lean Parser Meta Elab Term PrettyPrinter Delaborator
 
 open Std.Do in
-@[builtin_delab app.Std.Do.PostCond.total]
+-- TODO: Remove after stage0 update
+-- @[builtin_delab app.Std.Do.PostCond.total]
 private meta def unexpandPostCondTotal : Delab := do
   match ← SubExpr.withAppArg <| delab with
   | `(fun $xs:term* => $e) =>
@@ -22,7 +23,8 @@ private meta def unexpandPostCondTotal : Delab := do
     return ⟨t.raw⟩
   | t => `($(mkIdent ``PostCond.total):term $t)
 
-@[inherit_doc Triple, builtin_doc, builtin_term_elab triple]
+-- TODO: Remove after stage0 update
+-- @[inherit_doc Triple, builtin_doc, builtin_term_elab triple]
 private meta def elabTriple : TermElab
   | `(⦃$P⦄ $x ⦃$Q⦄), _ => do
     -- In a simple world, this would just be a macro expanding to
diff --git a/src/Std/Do/PostCond.lean b/src/Std/Do/PostCond.lean
index cd46e2731e..01de8575be 100644
--- a/src/Std/Do/PostCond.lean
+++ b/src/Std/Do/PostCond.lean
@@ -190,7 +190,6 @@ abbrev PostCond (α : Type u) (ps : PostShape.{u}) : Type u :=
 scoped macro:max "post⟨" handlers:term,+,? "⟩" : term =>
   `(by exact ⟨$handlers,*, ()⟩)
   -- NB: Postponement through by exact is the entire point of this macro
-  -- until https://github.com/leanprover/lean4/pull/8074 lands
 
 /-- A postcondition expressing total correctness. -/
 abbrev PostCond.total (p : α → Assertion ps) : PostCond α ps :=
@@ -200,6 +199,12 @@ abbrev PostCond.total (p : α → Assertion ps) : PostCond α ps :=
 scoped macro:max ppAllowUngrouped "⇓" xs:term:max+ " => " e:term : term =>
   `(PostCond.total (by exact fun $xs* => spred($e)))
 
+@[app_unexpander PostCond.total]
+private meta def unexpandPostCondTotal : Lean.PrettyPrinter.Unexpander
+  | `($_ fun $xs:term* => $e) => do
+    `(⇓ $xs* => $(← SPred.Notation.unpack e))
+  | _ => throw ()
+
 /-- A postcondition expressing partial correctness. -/
 abbrev PostCond.partial (p : α → Assertion ps) : PostCond α ps :=
   (p, FailConds.true)
diff --git a/src/Std/Do/Triple/Basic.lean b/src/Std/Do/Triple/Basic.lean
index dbede852d5..2c0cd3d382 100644
--- a/src/Std/Do/Triple/Basic.lean
+++ b/src/Std/Do/Triple/Basic.lean
@@ -33,7 +33,8 @@ def Triple [WP m ps] {α : Type u} (x : m α) (P : Assertion ps) (Q : PostCond 
   P ⊢ₛ wp⟦x⟧ Q
 
 @[inherit_doc Std.Do.Triple]
-scoped syntax:lead (name := triple) "⦃" term "⦄ " term:lead " ⦃" term "⦄" : term
+scoped macro:lead (name := triple) "⦃" P:term "⦄ " x:term:lead " ⦃" Q:term "⦄" : term =>
+  `(Triple $x spred($P) $Q)
 
 @[app_unexpander Triple]
 private meta def unexpandTriple : Lean.PrettyPrinter.Unexpander