test/mono/assert.sail


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

val f : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}

function f(n,m) = {
    assert(constraint('n in {8,16} & 'm < 'n));
    let 'p = 2 * n in
    let x : bits('p) = replicate_bits(0b0,'p) in
    ()
}

val g : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}

function g(n,m) = {
    assert(constraint('n in {8,16}) & 'm < 'n);
    let 'p = 2 * n in
    let x : bits('p) = replicate_bits(0b0,'p) in
    ()
}
val h : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}

function h(n,m) = {
    assert(('n == 8 | 'n == 16) & 'm < 'n);
    let 'p = 2 * n in
    let x : bits('p) = replicate_bits(0b0,'p) in
    ()
}