Skip to content
Snippets Groups Projects
Commit 4a40da5e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tweak tests.

parent 493c8ca1
No related branches found
No related tags found
No related merge requests found
Pipeline #51310 canceled
This commit is part of merge request !309. Comments created here will be created in the context of that merge request.
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 1 deletion
tests/gmap.v
+ 3
− 1
View file @ 4a40da5e
From stdpp Require Import pmap gmap. From stdpp Require Import strings pmap gmap.
Definition pmap_insert_positives (n : positive) : Pmap unit := Definition pmap_insert_positives (n : positive) : Pmap unit :=
Pos.iter (λ rec p m, Pos.iter (λ rec p m,
...@@ -51,10 +51,12 @@ Time Eval vm_compute in gmap_insert_positives_test 512000. ...@@ -51,10 +51,12 @@ Time Eval vm_compute in gmap_insert_positives_test 512000.
Time Eval vm_compute in gmap_insert_positives_test 1000000. Time Eval vm_compute in gmap_insert_positives_test 1000000.
*) *)
Check "gmap_insert_comm".
Theorem gmap_insert_comm : Theorem gmap_insert_comm :
{[ 3:=false; 2:=true]} =@{gmap nat bool} {[ 2:=true; 3:=false ]}. {[ 3:=false; 2:=true]} =@{gmap nat bool} {[ 2:=true; 3:=false ]}.
Proof. simpl. Show. reflexivity. Qed. Proof. simpl. Show. reflexivity. Qed.
Check "gmap_lookup_concrete".
Theorem gmap_lookup_concrete : Theorem gmap_lookup_concrete :
lookup (M:=gmap nat bool) 2 {[ 3:=false; 2:=true ]} = Some true. lookup (M:=gmap nat bool) 2 {[ 3:=false; 2:=true ]} = Some true.
Proof. simpl. Show. reflexivity. Qed. Proof. simpl. Show. reflexivity. Qed.
......
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