Add requires to rust doc

cryspen · Dec 10, 2024 · 9a2f48f · 9a2f48f
1 parent 18ac15e
commit 9a2f48f
Showing 1 changed file with 11 additions and 1 deletion.
diff --git 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,