fix: quantify over α before ps in PostCond definitions (#12708)

This PR changes the order of implicit parameters `α` and `ps` such that
`α` consistently comes before `ps` in `PostCond.noThrow`,
`PostCond.mayThrow`, `PostCond.entails`, `PostCond.and`, `PostCond.imp`
and theorems.

src/Std/Do/PostCond.lean

@@ -339,7 +339,7 @@ A postcondition expressing total correctness.
 That is, it expresses that the asserted computation finishes without throwing an exception
 *and* the result satisfies the given predicate `p`.
 -/
-abbrev PostCond.noThrow (p : α → Assertion ps) : PostCond α ps :=
+abbrev PostCond.noThrow {α ps} (p : α → Assertion ps) : PostCond α ps :=
   (p, ExceptConds.false)
 
 @[inherit_doc PostCond.noThrow]
@@ -352,7 +352,7 @@ That is, it expresses that *if* the asserted computation finishes without throwi
 *then* the result satisfies the given predicate `p`.
 Nothing is asserted when the computation throws an exception.
 -/
-abbrev PostCond.mayThrow (p : α → Assertion ps) : PostCond α ps :=
+abbrev PostCond.mayThrow {α ps} (p : α → Assertion ps) : PostCond α ps :=
   (p, ExceptConds.true)
 
 @[inherit_doc PostCond.mayThrow]
@@ -373,28 +373,28 @@ While implication of postconditions (`PostCond.imp`) results in a new postcondit
 an ordinary proposition.
 -/
 @[simp]
-def PostCond.entails (p q : PostCond α ps) : Prop :=
+def PostCond.entails {α ps} (p q : PostCond α ps) : Prop :=
   (∀ a, SPred.entails (p.1 a) (q.1 a)) ∧ ExceptConds.entails p.2 q.2
 
 @[inherit_doc PostCond.entails]
 scoped infixr:25 " ⊢ₚ " => PostCond.entails
 
-theorem PostCond.entails.mk {P Q : PostCond α ps} (h₁ : ∀ a, P.1 a ⊢ₛ Q.1 a) (h₂ : P.2 ⊢ₑ Q.2) : P ⊢ₚ Q :=
+theorem PostCond.entails.mk {α ps} {P Q : PostCond α ps} (h₁ : ∀ a, P.1 a ⊢ₛ Q.1 a) (h₂ : P.2 ⊢ₑ Q.2) : P ⊢ₚ Q :=
   ⟨h₁, h₂⟩
 
 @[refl, simp]
-theorem PostCond.entails.refl (Q : PostCond α ps) : Q ⊢ₚ Q := ⟨fun a => SPred.entails.refl (Q.1 a), ExceptConds.entails.refl Q.2⟩
-theorem PostCond.entails.rfl {Q : PostCond α ps} : Q ⊢ₚ Q := refl Q
+theorem PostCond.entails.refl {α ps} (Q : PostCond α ps) : Q ⊢ₚ Q := ⟨fun a => SPred.entails.refl (Q.1 a), ExceptConds.entails.refl Q.2⟩
+theorem PostCond.entails.rfl {α ps} {Q : PostCond α ps} : Q ⊢ₚ Q := refl Q
 
-theorem PostCond.entails.trans {P Q R : PostCond α ps} (h₁ : P ⊢ₚ Q) (h₂ : Q ⊢ₚ R) : P ⊢ₚ R :=
+theorem PostCond.entails.trans {α ps} {P Q R : PostCond α ps} (h₁ : P ⊢ₚ Q) (h₂ : Q ⊢ₚ R) : P ⊢ₚ R :=
   ⟨fun a => (h₁.1 a).trans (h₂.1 a), h₁.2.trans h₂.2⟩
 
 @[simp]
-theorem PostCond.entails_noThrow (p : α → Assertion ps) (q : PostCond α ps) : PostCond.noThrow p ⊢ₚ q ↔ ∀ a, p a ⊢ₛ q.1 a := by
+theorem PostCond.entails_noThrow {α ps} (p : α → Assertion ps) (q : PostCond α ps) : PostCond.noThrow p ⊢ₚ q ↔ ∀ a, p a ⊢ₛ q.1 a := by
   simp only [entails, ExceptConds.entails_false, and_true]
 
 @[simp]
-theorem PostCond.entails_mayThrow (p : PostCond α ps) (q : α → Assertion ps) : p ⊢ₚ PostCond.mayThrow q ↔ ∀ a, p.1 a ⊢ₛ q a := by
+theorem PostCond.entails_mayThrow {α ps} (p : PostCond α ps) (q : α → Assertion ps) : p ⊢ₚ PostCond.mayThrow q ↔ ∀ a, p.1 a ⊢ₛ q a := by
   simp only [entails, ExceptConds.entails_true, and_true]
 
 /--
@@ -403,7 +403,7 @@ Conjunction of postconditions.
 This is defined pointwise, as the conjunction of the assertions about the return value and the
 conjunctions of the assertions about each potential exception.
 -/
-abbrev PostCond.and (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
+abbrev PostCond.and {α ps} (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
   (fun a => SPred.and (p.1 a) (q.1 a), ExceptConds.and p.2 q.2)
 
 @[inherit_doc PostCond.and]
@@ -418,7 +418,7 @@ implications of each of the assertions about each potential exception.
 While entailment of postconditions (`PostCond.entails`) is an ordinary proposition, implication of
 postconditions is itself a postcondition.
 -/
-abbrev PostCond.imp (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
+abbrev PostCond.imp {α ps} (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
   (fun a => SPred.imp (p.1 a) (q.1 a), ExceptConds.imp p.2 q.2)
 
 @[inherit_doc PostCond.imp]
@@ -427,7 +427,7 @@ scoped infixr:25 " →ₚ " => PostCond.imp
 theorem PostCond.and_imp : P' ∧ₚ (P' →ₚ Q') ⊢ₚ P' ∧ₚ Q' := by
   simp [SPred.and_imp, ExceptConds.and_imp]
 
-theorem PostCond.and_left_of_entails {p q : PostCond α ps} (h : p ⊢ₚ q) :
+theorem PostCond.and_left_of_entails {α ps} {p q : PostCond α ps} (h : p ⊢ₚ q) :
     p = (p ∧ₚ q) := by
   ext
   · exact (SPred.and_eq_left.mp (h.1 _)).to_eq

tests/elab/doForInvariant.lean

@@ -69,7 +69,7 @@ elab_rules : doElem <= dec
     let mutVarBinders ← Term.Quotation.mkTuple reassignments
     let cursorσ := mkApp2 (mkConst ``Prod [v, mi.u]) cursor σ
     let success ← Term.elabFun (← `(fun ($cursorBinder, $(⟨mutVarBinders⟩)) $stateBinders* => $body)) (← mkArrow cursorσ assertion)
-    let inv := mkApp3 (mkConst ``Std.Do.PostCond.noThrow [mkLevelMax v mi.u]) ps cursorσ success
+    let inv := mkApp3 (mkConst ``Std.Do.PostCond.noThrow [mkLevelMax v mi.u]) cursorσ ps success
     let forIn := mkApp5 app instMonad instForIn ps instWP inv
     return mkApp6 bind m instBind σ γ forIn k