Skip to main content

litex/builtin_code/
common_functions.rs

1pub const BUILTIN_ENV_CODE_FOR_COMMON_FUNCTIONS: &str = r#"
2# Existence of such function is valid by definition of comparison
3
4let max_of_finite_set fn(s power_set(R): $is_finite_set(s)) R
5let min_of_finite_set fn(s power_set(R): $is_finite_set(s)) R
6
7know:
8    forall s power_set(R), item s:
9        $is_finite_set(s)
10        =>:
11            item <= max_of_finite_set(s)
12            min_of_finite_set(s) <= item
13
14    forall s power_set(R):
15        $is_finite_set(s)
16        =>:
17            max_of_finite_set(s) $in s
18            min_of_finite_set(s) $in s
19
20let min_of_N_set fn(s power_set(N)) N
21
22know:
23    forall s power_set(N), item s:
24        min_of_N_set(s) <= item
25
26    forall s power_set(N):
27        min_of_N_set(s) $in s
28"#;