Commit 176ba07b authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Make the precondition for FCo preservation stricter

parent 1fb1a5e7
......@@ -18,7 +18,7 @@ args = Args{replay=Nothing, maxSuccess=1000, maxDiscardRatio=1000000, maxSize=10
-- The type of a term does not change when a reduction step is performed
coPreservation :: Term -> Property
coPreservation te = (isRight ty) && (not $ CoI.isVal te)
coPreservation te = (isRight ty) && (not $ CoI.isVal te) && (isJust $ CoI.stepEval te)
==> ty == tyStep
where ty = CoI.typeOf te CoI.Nil
tyStep = (flip CoI.typeOf) CoI.Nil $ fromMaybe undefined $ CoI.stepEval te
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment