1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
type Result⟨T⟩ = std::result::Result⟨T, Error⟩;
type List⟨+T, -A⟩ {
}
alias type int = Integer;
class Integer(base Number) {
refine {
requires() {
Self > 0;
}
ensures() {
}
}
}
function five(): i32 {
5
}
#[ensures(result.0 / 2 == result.1 && result.2 == 'a')]
function tuple(): (i32, i32, char) {
(10, 5, 'a')
}
predicate function all_zeroes(a: &MyArray) -> bool {
forall(lambda(i: usize) {
0 <= i && i < a.len() && a.lookup(i) == 0
})
}