1use flux_attrs::*;
2
3#[extern_spec]
4#[refined_by(is_some: bool)]
5enum Option<T> {
6 #[variant(Option<T>[false])]
7 None,
8 #[variant((T) -> Option<T>[true])]
9 Some(T),
10}
11
12#[extern_spec]
13impl<T> Option<T> {
14 #[sig(fn(&Self[@b]) -> bool[b])]
15 fn is_some(&self) -> bool;
16
17 #[sig(fn(&Self[@b]) -> bool[!b])]
18 fn is_none(&self) -> bool;
19
20 #[sig(fn(&Self[@b]) -> Option<&T>[b])]
21 fn as_ref(&self) -> Option<&T>;
22
23 #[sig(fn(&mut Self[@b]) -> Option<&mut T>[b])]
24 fn as_mut(&mut self) -> Option<&mut T>;
25
26 #[sig(fn(&Self[@b]) -> &[T][if b { 1 } else { 0 }])]
27 fn as_slice(&self) -> &[T];
28
29 #[sig(fn(&mut Self[@b]) -> &mut [T][if b { 1 } else { 0 }])]
30 fn as_mut_slice(&mut self) -> &mut [T];
31}