diff options
| author | Son Ho | 2022-05-09 11:13:11 +0200 |
|---|---|---|
| committer | Son Ho | 2022-05-09 11:13:11 +0200 |
| commit | c42b8de26e46d98d2dc0732888dc82f89102fb3e (patch) | |
| tree | ddd47e4e2174c8f125ade91d8dcb1ff7e19a787b | |
| parent | 0191a1196d48e819c834687dc8a6710651ebe76a (diff) | |
Make minor modifications
Diffstat (limited to '')
| -rw-r--r-- | tests/betree/BetreeMain.Clauses.fst | 10 |
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) : |