flux-rs / flux

Refinement Types for Rust
MIT License
660 stars 21 forks source link

Allow fully qualified names for struct-generated sorts #784

Closed ranjitjhala closed 2 months ago

ranjitjhala commented 2 months ago

In particular, make this work

// Currently need the below
// use Blob::Bob;

mod Blob {

    #![flux::defs(
    fn use_bob(z: Blob::Bob) -> int {
        z.idx + Blob::A
    }
    )]

    pub const A: usize = 12;

    #[flux::opaque]
    #[flux::refined_by(idx:int)]
    pub struct Bob {
        idx: i32,
    }
}