blob: 594130a8d3b832d46a29b2770af1205fb7a3f7ff (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
default Order dec
$include <prelude.sail>
$include <smt.sail>
overload operator / = {ediv_int}
union T = {C1 : int, C2 : int}
function test (x : int, y : T) -> int = match y {
C1(z) if z == 0 => 0,
C1(z) if z != 0 => x / z,
C2(z) => z
}
|