litex-lang 0.9.88-beta

The Formal Way to Write Math as It Looks
Documentation 
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
42
43
44
45
46
47
48

// Integers strictly above 0 are at least 1 (uses Z and order on R).

pub const FUNDAMENTAL_NUMBER_PROPERTIES: &str = r#"
know:
    forall x Z, y Z:
        y < x
        =>:
            y + 1 <= x

    forall x Z, y Z:
        x < y
        =>:
            x <= y - 1

    forall x Z, y Z:
        y <= x < y + 1
        =>:
            x = y

    forall x Q:
        exist p, q Z st {q > 0, x = p / q}

    forall x, y R:
        x < y
        =>:
            exist z Q st {x < z < y}

    forall a, b Z:
        closed_range(a, b) = {x Z: a <= x <= b}

    forall a, b Z:
        range(a, b) = {x Z: a <= x < b}

    forall a, b Z:
        b != 0
        a % b = 0
        =>:
            exist k Z st {a = k * b}

    forall a, b N_pos:
        exist k N_pos st {a = k * b}

    # Litex evaluates `1 % 1 = 0`. For modulus `k` in `N_pos` with `k >= 2`, the remainder of 1 is 1.
    forall k N_pos:
        k >= 2 or k != 1
        =>:
            1 % k = 1
"#;