From 4017a79c53ab068a48dce516a7105cf5ff47c781 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Thu, 13 Feb 2025 09:28:20 +0100 Subject: [PATCH] implies to prop --- hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst | 2 ++ 1 file changed, 2 insertions(+) diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst index 41500f3b7..a60a10d64 100644 --- a/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst +++ b/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst @@ -1,3 +1,5 @@ module Hax_lib.Prop type t_Prop = Type0 + +unfold let implies (lhs: t_Prop) (rhs: (x:unit{lhs} -> t_Prop)): t_Prop = (~ lhs) \/ rhs ()