summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tests/betree/BetreeMain.Clauses.fst10
1 files changed, 6 insertions, 4 deletions
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) :