-
Notifications
You must be signed in to change notification settings - Fork 1
Open
Description
Right now, it looks like I need to explicitly provide type parameters in ravencheck specs. For example, for a generic option (definition given below), I need to explicitly annotate the generic type everywhere it might be needed in ravencheck specifications (see the test_is_some spec below). It would be nice to instead infer this parameter when possible.
#[define]
pub enum Opt<T> {
Some(T),
None,
}
#[define]
pub fn is_some<T>(opt: &Opt<T>) -> bool {
match opt {
Opt::<T>::Some(v) => true,
Opt::<T>::None => false,
}
}
#[verify]
fn test_is_some<T>(v: T) -> bool {
is_some::<T>(Opt::<T>::Some(v))
}Metadata
Metadata
Assignees
Labels
No labels