fix(hax-lib): make implies take a bool closure

cryspen · Dec 13, 2023 · af479ab · af479ab
1 parent a57bea1
commit af479ab
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: Type0) (rhs: unit -> Type0): Type0 = lhs ==> rhs ()
+unfold let implies (lhs: bool) (rhs: unit -> bool): bool = (not lhs) || rhs ()