Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131#[allow(unused_imports)]use verus_builtin::*;#[allow(unused_imports)]use verus_builtin_macros::*;
verus! {
// ANCHOR: pointstruct Point { x: int, y: int,}// ANCHOR_END: point
// ANCHOR: point-implimpl Point { spec fn len2(&self) -> int { self.x * self.x + self.y * self.y }}
fn rotate_90(p: Point) -> (o: Point) ensures o.len2() == p.len2(){ let o = Point { x: -p.y, y: p.x }; assert((-p.y) * (-p.y) == p.y * p.y) by(nonlinear_arith); o}// ANCHOR_END: point-impl
// ANCHOR: beverageenum Beverage { Coffee { creamers: nat, sugar: bool }, Soda { flavor: Syrup }, Water { ice: bool },}// ANCHOR_END: beverage
// ANCHOR: syrupenum Syrup { Cola, RootBeer, Orange, LemonLime,}// ANCHOR_END: syrup
struct Dessert {}impl Dessert { fn new() -> Dessert { Dessert {} }}
// ANCHOR: make_floatfn make_float(bev: Beverage) -> Dessert requires bev is Soda{ assert(bev !is Coffee); Dessert::new(/*...*/)}// ANCHOR_END: make_float
// ANCHOR: count_creamersproof fn sufficiently_creamy(bev: Beverage) -> bool requires bev is Coffee{ bev->creamers >= 2}// ANCHOR_END: count_creamers
// ANCHOR: lifeenum Life { Mammal { legs: int, has_pocket: bool }, Arthropod { legs: int, wings: int }, Plant { leaves: int },}
spec fn is_insect(l: Life) -> bool{ l is Arthropod && l->Arthropod_legs == 6}// ANCHOR_END: life
// ANCHOR: shapeenum Shape { Circle(int), Rect(int, int),}
spec fn area_2(s: Shape) -> int { match s { Shape::Circle(radius) => { radius * radius * 3 }, Shape::Rect(width, height) => { width * height } }}// ANCHOR_END: shape
// ANCHOR: rect_heightspec fn rect_height(s: Shape) -> int recommends s is Rect{ s->1}// ANCHOR_END: rect_height
// ANCHOR: cuddlyuse Life::*;spec fn cuddly(l: Life) -> bool { ||| l matches Mammal { legs, .. } && legs == 4 ||| l matches Arthropod { legs, wings } && legs == 8 && wings == 0}// ANCHOR_END: cuddly
// ANCHOR: kangaroospec fn is_kangaroo(l: Life) -> bool { &&& l matches Life::Mammal { legs, has_pocket } &&& legs == 2 &&& has_pocket}
spec fn walks_upright(l: Life) -> bool { l matches Life::Mammal { legs, .. } ==> legs == 2}// ANCHOR_END: kangaroo
fn main() {}
} // verus!