verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.25k stars 72 forks source link

spurious 'let variables in trigger' error #1347

Open tjhance opened 1 week ago

tjhance commented 1 week ago
struct Node {
    child: Option<Box<Node>>,
}

impl Node {
    pub spec fn map(self) -> Map<int, int>;
}

impl Clone for Node {
    fn clone(&self) -> (res: Self)
        ensures forall |key: int| #[trigger] self.map().dom().contains(key) ==> key == 3
    {   
        Node { child: None }
    }   
}

This gives:

error: let variables in triggers not supported, use #![trigger ...] instead