Skip to content

Commit

Permalink
Temporarily fixed the universe of state in ISTATE to avoid the 'being…
Browse files Browse the repository at this point in the history
… polymorphic in 2 universes' problem with the lax typechecker.
  • Loading branch information
Danel Ahman committed Aug 16, 2016
1 parent 0731016 commit a8db6c4
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion examples/preorders/IST.fst
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit a8db6c4

Please sign in to comment.