Merge pull request #391 from hacspec/revert-380-change-hax-lib-def

Revert "Change definition of hax_lib::implies in Fstar to get lax typechecking working for libcrux Kyber."
cryspen · Dec 13, 2023 · 3cd2e34 · 3cd2e34
2 parents 1f17240 + af479ab
commit 3cd2e34
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.fst
@@ -11,4 +11,4 @@ let v_assume (v__formula: bool) = assume v__formula
 
 unfold let v_exists (v__f: 'a -> Type0): Type0 = exists (x: 'a). v__f x
 unfold let v_forall (v__f: 'a -> Type0): Type0 = forall (x: 'a). v__f x
-unfold let implies (lhs: bool) (rhs: bool): bool = (not lhs) || rhs
+unfold let implies (lhs: bool) (rhs: unit -> bool): bool = (not lhs) || rhs ()