Skip to content

Commit

Permalink
Merge pull request #380 from hacspec/change-hax-lib-def
Browse files Browse the repository at this point in the history
Change definition of hax_lib::implies in Fstar to get lax typechecking working for libcrux Kyber.
  • Loading branch information
franziskuskiefer authored Dec 1, 2023
2 parents 1b2ffe4 + 544cb87 commit 156f523
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion hax-lib/proofs/fstar/extraction/Hax_lib.fst
Original file line number Diff line number Diff line change
@@ -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: bool): bool = (not lhs) || rhs

0 comments on commit 156f523

Please sign in to comment.