From 8a486dbff30eb322f5ef245841d4fa0ecfe53516 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 14 Nov 2022 22:25:58 +0100
Subject: [PATCH] Style: `:=` belongs to line end

These are all the occurrences of `^ *:=`. `:=$` occurs ~2000 times between Iris
and stdpp.

Noticed while confirming this is the preferred stdpp/iris style.
---
 iris/algebra/view.v                   | 12 ++++++------
 iris/base_logic/bi.v                  |  4 ++--
 iris/program_logic/total_weakestpre.v |  4 ++--
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index c260a1b21..85ec57056 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -210,15 +210,15 @@ Section cmra.
       | None => ∃ a, rel n a (view_frag_proj x)
       end := eq_refl _.
   Local Definition view_pcore_eq :
-      pcore = λ x, Some (View (core (view_auth_proj x)) (core (view_frag_proj x)))
-    := eq_refl _.
+      pcore = λ x, Some (View (core (view_auth_proj x)) (core (view_frag_proj x))) :=
+    eq_refl _.
   Local Definition view_core_eq :
-      core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x))
-    := eq_refl _.
+      core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x)) :=
+    eq_refl _.
   Local Definition view_op_eq :
       op = λ x y, View (view_auth_proj x ⋅ view_auth_proj y)
-                       (view_frag_proj x â‹… view_frag_proj y)
-    := eq_refl _.
+                       (view_frag_proj x â‹… view_frag_proj y) :=
+    eq_refl _.
 
   Lemma view_cmra_mixin : CmraMixin (view rel).
   Proof.
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index f803dbd10..d8574dee5 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -194,8 +194,8 @@ Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
 Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
-Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid M A)
-  := uPred_primitive.cmra_valid_ne.
+Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid M A) :=
+  uPred_primitive.cmra_valid_ne.
 
 (** Re-exporting primitive lemmas that are not in any interface *)
 Lemma ownM_op (a1 a2 : M) :
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index b9ea90171..992fb12cb 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -57,8 +57,8 @@ Proof.
     rewrite /curry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
 Qed.
 
-Local Definition twp_def `{!irisGS_gen hlc Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness
-  := λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
+Local Definition twp_def `{!irisGS_gen hlc Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness :=
+  λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
 Local Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
 Definition twp' := twp_aux.(unseal).
 Global Arguments twp' {hlc Λ Σ _}.
-- 
GitLab