From a8db6c47e8b699b98be4c7c6f8c2e0edbce85933 Mon Sep 17 00:00:00 2001 From: Danel Ahman Date: Mon, 15 Aug 2016 23:26:43 -0700 Subject: [PATCH] Temporarily fixed the universe of state in ISTATE to avoid the 'being polymorphic in 2 universes' problem with the lax typechecker. --- examples/preorders/IST.fst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/examples/preorders/IST.fst b/examples/preorders/IST.fst index 97484f7efcd..c3d8d1e692c 100644 --- a/examples/preorders/IST.fst +++ b/examples/preorders/IST.fst @@ -28,7 +28,8 @@ let ist_wp (state:Type) (a:Type) = ist_post state a -> Tot (ist_pre state) (* A WP-style preorder-indexed state monad. *) -new_effect ISTATE (state:Type) (rel:relation state{preorder rel}) = STATE_h state +new_effect ISTATE (state:Type0) (rel:relation state{preorder rel}) = STATE_h state //typechecks with --lax flag on +//new_effect ISTATE (state:Type) (rel:relation state{preorder rel}) = STATE_h state //does not typecheck with --lax flag on (* Currently not possible, but at this point one would like to show that