Equality operators for an enum type are not supported well

[zpzigi754]

I tried the below code where an equality operator is used for an enum type.

use vstd::prelude::*;

verus! {

#[derive(PartialEq)]
pub enum Fruits {
    APPLE,
    BANANA,
}

pub struct Meal {
    pub fruit: Fruits,
}

impl Meal {
    fn does_not_work(&self) {
        if self.fruit == Fruits::BANANA {
        }
    }
}

fn main() {
}

}

It failed with the following error.

error: The verifier does not yet support the following Rust feature: ==/!= for non smt equality types
  --> rust_verify/example/guide/enum.rs:17:12
   |
17 |         if self.fruit == Fruits::BANANA {
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: aborting due to 1 previous error

I've confirmed that using match or if let (the same semantic) works well.

use vstd::prelude::*;

verus! {

pub enum Fruits {
    APPLE,
    BANANA,
}

pub struct Meal {
    pub fruit: Fruits,
}

impl Meal {
    fn work(&self) {
        match self.fruit {
            Fruits::BANANA => {},
            _ => {},
        }
    }

    fn work2(&self) {
        if let Fruits::BANANA = self.fruit {
        }
    }
}

fn main() {
}

}

[Chris-Hawblitzel]

There is a feature called Structural that can be used to make this work:

#[derive(Structural, PartialEq, Clone, Copy)]
pub enum Fruits {
    APPLE,
    BANANA,
}

pub struct Meal {
    pub fruit: Fruits,
}

impl Meal {
    fn test(&self) {
        if self.fruit == Fruits::BANANA {
        }
    }
}

I guess we need to add documentation on this, and perhaps also update the error message to hint at using Structural.

[zpzigi754]

Thank you for the suggestion of using Structural! I've also confirmed that the test code works with Structural.