From 9a2f48f03c45b276cd2ab018ff394d95b01c42cc Mon Sep 17 00:00:00 2001
From: Lasse Letager Hansen <letager@cs.au.dk>
Date: Tue, 10 Dec 2024 17:44:27 +0100
Subject: [PATCH] Add requires to rust doc

---
 hax-lib/macros/src/dummy.rs | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs
index 5134763c6..05c43c433 100644
--- a/hax-lib/macros/src/dummy.rs
+++ b/hax-lib/macros/src/dummy.rs
@@ -16,12 +16,22 @@ macro_rules! identity_proc_macro_attribute {
     }
 }
 
+#[proc_macro_attribute]
+pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let item: ItemFn = parse_macro_input!(item);
+    let phi: syn::Expr = parse_macro_input!(attr);
+
+    quote! {
+        #[doc=concat!("Requires: ",stringify!(#phi))]
+        #item
+    }.into()
+}
+
 identity_proc_macro_attribute!(
     fstar_options,
     fstar_verification_status,
     include,
     exclude,
-    requires,
     ensures,
     pv_handwritten,
     pv_constructor,