Commit 58d65dd9 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Remove examples in OakTypes.v

parent 4c7bf5e4
Pipeline #10818 failed with stage
in 2 minutes and 3 seconds
......@@ -69,7 +69,6 @@ Defined.
(*
Examples:
*)
Definition test_bool : OakValue := build_oak_value oak_bool true.
Definition test_int : OakValue := build_oak_value oak_int 5%Z.
Definition test_set : OakValue := build_oak_value (oak_set oak_int) {5%Z; {6%Z; {}}}.
......@@ -82,7 +81,4 @@ Compute (oak_value_extract oak_int test_int) : option Z.
Compute (oak_value_extract (oak_set oak_int) test_set) : option (set Z).
Compute (option_map SetInterface.elements (oak_value_extract (oak_set oak_int) test_set)).
Compute (option_map elements (oak_value_extract (oak_map oak_int oak_int) test_map)).
Check @MapAVL.Raw.Proofs.L.map_OrderedType.
Set Typeclasses Debug.
Check (option_map SetInterface.elements oak_value_extract (oak_set oak_int) test_set).
\ No newline at end of file
*)
\ No newline at end of file
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