Skip to content

Commit

Permalink
fix(hax-lib): use super::* in refinement expansion
Browse files Browse the repository at this point in the history
This commit fixes #761.

Considering:
```rust
use some::path::to::T;

pub struct MyRefinedType(T);
```

The generated code wraps the struct declaration in a module.
That module used not to have `T` in scope.

This commit adds a `use super::*` before declaring the type of the
refinement type.
  • Loading branch information
W95Psp committed Jul 10, 2024
1 parent b462111 commit 2dd6c10
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions hax-lib-macros/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -820,6 +820,9 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm::
quote! {
#[allow(non_snake_case)]
mod #module_ident {
#[allow(unused_imports)]
use super::*;

#refinement_item

#newtype_as_ref_attr
Expand All @@ -828,7 +831,9 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm::

#[::hax_lib::exclude]
impl #generics ::hax_lib::Refinement for #ident <#generics_args> {

type InnerType = #inner_ty;

fn new(x: Self::InnerType) -> Self {
#debug_assert
Self(x)
Expand Down

0 comments on commit 2dd6c10

Please sign in to comment.