blob: 02c5536a8061c2cc5802b4d857e8e536c5c5bf90 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
// set of maps from anything to a specific type a
const mapSet : <a>[<b>[b]a]bool;
const emptySet : <a>[a]bool;
axiom mapSet[5]; // type error
axiom mapSet[emptySet] == true;
axiom mapSet[emptySet := false] != mapSet;
axiom mapSet[emptySet := 5] == mapSet; // type error
axiom emptySet[13 := true][13] == true;
axiom (forall f : <c>[c]int, x : ref :: mapSet[f] ==> f[x] >= 0);
axiom (forall f : <c>[c]c :: mapSet[f]); // type error
axiom mapSet[mapSet] == true; // type error
type ref;
|
