fix(macros): forall and exists return props

cryspen · Feb 12, 2025 · ffb6b22 · ffb6b22
1 parent e49ac46
commit ffb6b22
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs
@@ -10,12 +10,12 @@ impl ToTokens for HaxQuantifiers {
             #AttrHaxLang
             #status_attr
             fn forall<T, U:Into<hax_lib::Prop>, F: Fn(T) -> U>(f: F) -> hax_lib::Prop {
-                true
+                true.into()
             }
             #AttrHaxLang
             #status_attr
             fn exists<T, U:Into<hax_lib::Prop>, F: Fn(T) -> U>(f: F) -> hax_lib::Prop {
-                true
+                true.into()
             }
 
             use ::hax_lib::fstar_unsafe_expr as fstar;