Commit e174d748 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Use of_list for constructing sets/maps in examples

parent 5e814944
Pipeline #11257 failed with stage
in 2 minutes and 47 seconds
...@@ -255,9 +255,9 @@ Definition test_int : OakValue := build_oak_value oak_int 5%Z. ...@@ -255,9 +255,9 @@ Definition test_int : OakValue := build_oak_value oak_int 5%Z.
Definition test_set : OakValue := Definition test_set : OakValue :=
build_oak_value build_oak_value
(oak_set oak_int) (oak_set oak_int)
(FSet.add 5 (FSet.add 6 FSet.empty))%Z. (FSet.of_list [5; 6]%Z).
Definition test_fmap : FMap Z Z := Definition test_fmap : FMap Z Z :=
(FMap.add 5 10 (FMap.add 6 10 (FMap.add 5 15 FMap.empty)))%Z. (FMap.of_list [(5, 10); (6, 10); (5, 15)])%Z.
Definition test_map : OakValue := Definition test_map : OakValue :=
build_oak_value build_oak_value
...@@ -267,7 +267,7 @@ Definition test_map : OakValue := ...@@ -267,7 +267,7 @@ Definition test_map : OakValue :=
Definition test_map2 : OakValue := Definition test_map2 : OakValue :=
build_oak_value build_oak_value
(oak_map (oak_map oak_int oak_int) oak_int) (oak_map (oak_map oak_int oak_int) oak_int)
(FMap.add test_fmap 15%Z FMap.empty). (FMap.of_list [(test_fmap, 15)])%Z.
Compute (extract_oak_value oak_bool test_bool) : option bool. Compute (extract_oak_value oak_bool test_bool) : option bool.
Compute (extract_oak_value oak_int test_bool) : option Z. Compute (extract_oak_value oak_int test_bool) : option Z.
...@@ -283,4 +283,3 @@ Compute ...@@ -283,4 +283,3 @@ Compute
: option (FMap (FMap Z Z) Z). : option (FMap (FMap Z Z) Z).
Compute (option_map FSet.elements (extract_oak_value (oak_set oak_int) test_set)). Compute (option_map FSet.elements (extract_oak_value (oak_set oak_int) test_set)).
Compute (option_map FMap.elements (extract_oak_value (oak_map oak_int oak_int) test_map)). Compute (option_map FMap.elements (extract_oak_value (oak_map oak_int oak_int) test_map)).
*)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment