From 77100af764d9bf9b34787074299af0ef724c1020 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 1 Dec 2021 08:52:44 +0100
Subject: [PATCH] Fix formatting of bool_to_Z_spec

---
 theories/numbers.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/numbers.v b/theories/numbers.v
index f8f237cf..4acc4adf 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -553,8 +553,7 @@ Lemma bool_to_Z_eq_0 b : bool_to_Z b = 0 ↔ b = false.
 Proof. destruct b; naive_solver. Qed.
 Lemma bool_to_Z_neq_0 b : bool_to_Z b ≠ 0 ↔ b = true.
 Proof. destruct b; naive_solver. Qed.
-Lemma bool_to_Z_spec b n:
-  Z.testbit (bool_to_Z b) n = bool_decide (n = 0) && b.
+Lemma bool_to_Z_spec b n : Z.testbit (bool_to_Z b) n = bool_decide (n = 0) && b.
 Proof. by destruct b, n. Qed.
 
 
-- 
GitLab