From 98ed62adc83e22d5ffbca310eaebfb16c1af42e4 Mon Sep 17 00:00:00 2001
From: karthikbhargavan <karthik.bhargavan@gmail.com>
Date: Sun, 9 Feb 2025 11:24:35 +0100
Subject: [PATCH] macro requires ensures

---
 hax-lib/macros/src/utils.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/hax-lib/macros/src/utils.rs b/hax-lib/macros/src/utils.rs
index f4c2ff72b..1a6ce7678 100644
--- a/hax-lib/macros/src/utils.rs
+++ b/hax-lib/macros/src/utils.rs
@@ -9,12 +9,12 @@ impl ToTokens for HaxQuantifiers {
         quote! {
             #AttrHaxLang
             #status_attr
-            fn forall<T, F: Fn(T) -> bool>(f: F) -> bool {
+            fn forall<T, U:Into<hax_lib::Prop>, F: Fn(T) -> U>(f: F) -> hax_lib::Prop {
                 true
             }
             #AttrHaxLang
             #status_attr
-            fn exists<T, F: Fn(T) -> bool>(f: F) -> bool {
+            fn exists<T, U:Into<hax_lib::Prop>, F: Fn(T) -> U>(f: F) -> hax_lib::Prop {
                 true
             }
 
@@ -279,7 +279,7 @@ pub fn make_fn_decoration(
             sig.output = if let FnDecorationKind::Decreases = &kind {
                 syn::parse_quote! { -> Box<dyn Any> }
             } else {
-                syn::parse_quote! { -> bool }
+                syn::parse_quote! { -> hax_lib::Prop }
             };
             sig
         };