fix(hax-lib): expose missing items in dummy

cryspen · Feb 20, 2025 · 1977822 · 1977822
1 parent ffe0fdf
commit 1977822
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs
@@ -36,6 +36,9 @@ identity_proc_macro_attribute!(
     fstar_replace,
     coq_replace,
     proverif_replace,
+    fstar_replace_body,
+    coq_replace_body,
+    proverif_replace_body,
     fstar_before,
     coq_before,
     proverif_before,
@@ -82,6 +85,19 @@ pub fn proverif_unsafe_expr(_payload: TokenStream) -> TokenStream {
     unsafe_expr()
 }
 
+#[proc_macro]
+pub fn fstar_prop_expr(_payload: TokenStream) -> TokenStream {
+    quote! {::hax_lib::Prop::from_bool(true)}.into()
+}
+#[proc_macro]
+pub fn coq_prop_expr(_payload: TokenStream) -> TokenStream {
+    quote! {::hax_lib::Prop::from_bool(true)}.into()
+}
+#[proc_macro]
+pub fn proverif_prop_expr(_payload: TokenStream) -> TokenStream {
+    quote! {::hax_lib::Prop::from_bool(true)}.into()
+}
+
 fn not_hax_attribute(attr: &syn::Attribute) -> bool {
     if let Meta::List(ml) = &attr.meta {
         !matches!(expects_path_decoration(&ml.path), Ok(Some(_)))