creusot_contracts/
well_founded.rs

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
39
40
41
use crate::*;

// Instances of this trait are types which are allowed as variants of recursive definitions.
#[trusted]
pub trait WellFounded {}

// FIXME: Int is NOT well-founded. But this is required for induction over integers
#[trusted]
impl WellFounded for Int {}

#[trusted]
impl WellFounded for u8 {}
#[trusted]
impl WellFounded for u16 {}
#[trusted]
impl WellFounded for u32 {}
#[trusted]
impl WellFounded for u64 {}
#[trusted]
impl WellFounded for u128 {}
#[trusted]
impl WellFounded for usize {}

#[trusted]
impl WellFounded for i8 {}
#[trusted]
impl WellFounded for i16 {}
#[trusted]
impl WellFounded for i32 {}
#[trusted]
impl WellFounded for i64 {}
#[trusted]
impl WellFounded for i128 {}
#[trusted]
impl WellFounded for isize {}

#[trusted]
impl<T: WellFounded> WellFounded for &T {}

#[trusted]
impl<T: WellFounded> WellFounded for &mut T {}