From 4058f67dfb48669288026fd837c5a44eca907e9c Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl> Date: Mon, 8 Aug 2022 14:32:51 +0000 Subject: [PATCH] Avoid really long line --- iris/algebra/view.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/iris/algebra/view.v b/iris/algebra/view.v index aa39cebce..cca42710d 100644 --- a/iris/algebra/view.v +++ b/iris/algebra/view.v @@ -216,7 +216,8 @@ Section cmra. 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) + op = λ x y, View (view_auth_proj x ⋅ view_auth_proj y) + (view_frag_proj x ⋅ view_frag_proj y) := eq_refl _. Lemma view_cmra_mixin : CmraMixin (view rel). -- GitLab