From 1aeb18868a5de15f731750ea418063c44d2b3b2b Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Fri, 22 May 2026 16:47:15 +0200
Subject: [PATCH] fix: make A an outParam of Wp and TotalWp

This reduces the need for type annotations and there should be at most
one Wp instance per Expr.
---
 Iris/Iris/BI/WeakestPre.lean | 8 ++++----
 Iris/Iris/Tests/WP.lean      | 8 +++-----
 2 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/Iris/Iris/BI/WeakestPre.lean b/Iris/Iris/BI/WeakestPre.lean
index 1b7a1fd6..327771e7 100644
--- a/Iris/Iris/BI/WeakestPre.lean
+++ b/Iris/Iris/BI/WeakestPre.lean
@@ -45,10 +45,10 @@ instance : Std.IsPreorder Stuckness where
 
 end Stuckness
 
-class Wp (PROP Expr : Type _) (Val : outParam (Type _)) (A : Type _) where
+class Wp (PROP Expr : Type _) (Val : outParam (Type _)) (A : outParam (Type _)) where
   wp : A → CoPset → Expr → (Val → PROP) → PROP
 
-class TotalWP (PROP Expr) (Val : outParam (Type _)) (A : Type _) where
+class TotalWp (PROP Expr) (Val : outParam (Type _)) (A : outParam (Type _)) where
   totalWp : A → CoPset → Expr → (Val → PROP) → PROP
 
 syntax wpExpr :=
@@ -109,7 +109,7 @@ meta def wpMacro : Lean.Macro := fun stx => do
     let (e, s, E) ← parseWpExpr expr
     let (Φ, useTotal?) ← parseWpPostcond postcond
     if useTotal? then
-      `(TotalWP.totalWp $s $E $e $Φ)
+      `(TotalWp.totalWp $s $E $e $Φ)
     else
       `(Wp.wp $s $E $e $Φ)
   | _ => Lean.Macro.throwUnsupported
@@ -137,7 +137,7 @@ meta def unexpanderWp : PrettyPrinter.Unexpander
     `(WP $wpExpr {{ $wpPostcondInner }})
   | _ => throw ()
 
-@[app_unexpander TotalWP.totalWp]
+@[app_unexpander TotalWp.totalWp]
 meta def unexpanderTotalWp : PrettyPrinter.Unexpander
   | `($_wp $s $E $e $Φ) => do
     let wpExpr ← makeWpExpr s E e
diff --git a/Iris/Iris/Tests/WP.lean b/Iris/Iris/Tests/WP.lean
index 5b09f796..ab2c68b7 100644
--- a/Iris/Iris/Tests/WP.lean
+++ b/Iris/Iris/Tests/WP.lean
@@ -16,13 +16,11 @@ open Iris
 section TestWP
 set_option linter.unusedVariables false
 
-variable (PROP Expr : Type _) (Val : outParam (Type _)) (A : Type _)
-variable [Wp PROP Expr Val A]
+variable (PROP Expr : Type _) (Val : Type _)
 variable [Wp PROP Expr Val Stuckness]
-variable [TotalWP PROP Expr Val A]
-variable [TotalWP PROP Expr Val Stuckness]
+variable [TotalWp PROP Expr Val Stuckness]
 
-variable (e : Expr) (s : A) (E : CoPset)
+variable (e : Expr) (s : Stuckness) (E : CoPset)
 
 -- Base no-binder cases
 variable (Φ : Val → PROP)