From c42b8de26e46d98d2dc0732888dc82f89102fb3e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 9 May 2022 11:13:11 +0200
Subject: Make minor modifications

---
 tests/betree/BetreeMain.Clauses.fst | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'tests/betree')

diff --git a/tests/betree/BetreeMain.Clauses.fst b/tests/betree/BetreeMain.Clauses.fst
index 0006e3ac..07484711 100644
--- a/tests/betree/BetreeMain.Clauses.fst
+++ b/tests/betree/BetreeMain.Clauses.fst
@@ -25,6 +25,9 @@ open BetreeMain.Types
  *
  * What follows is adapted from:
  * https://www.fstar-lang.org/tutorial/book/part2/part2_well_founded.html
+ *
+ * Also, the following PR might make things easier:
+ * https://github.com/FStarLang/FStar/pull/2561
  *)
 
 module P = FStar.Preorder
@@ -76,10 +79,9 @@ let coerce_wf #a #r (p: (x:a -> W.acc r x)) : x:a -> W.acc r x =
  * An issue here is that the `{well-founded ... }` notation
  *)
 assume
-val axiom_well_founded (a:Type) (rel:a -> a -> Type0)
-  (rwf:W.well_founded #a rel) (x y:a): Lemma
-  (requires (rel x y))
-  (ensures (x << y))
+val axiom_well_founded (a : Type) (rel : a -> a -> Type0)
+  (rwf : W.well_founded #a rel) (x y : a) :
+  Lemma (requires (rel x y)) (ensures (x << y))
 
 (* This lemma has a pattern (which makes it work) *)
 let wf_nat_pair_lem (p0 p1 : nat_pair) :
-- 
cgit v1.2.3