implies to prop

cryspen · Feb 13, 2025 · 9ed6044 · 9ed6044
1 parent 4017a79
commit 9ed6044
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst b/hax-lib/proofs/fstar/extraction/Hax_lib.Prop.fst
@@ -2,4 +2,4 @@ module Hax_lib.Prop
 
 type t_Prop = Type0
 
-unfold let implies (lhs: t_Prop) (rhs: (x:unit{lhs} -> t_Prop)): t_Prop = (~ lhs) \/ rhs ()
+unfold let implies #a #b (lhs: t_Prop) (rhs: (x:unit{lhs} -> t_Prop)): t_Prop = (~ lhs) \/ rhs ()