Commit 5bb47351 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tests.

parent d3736048
......@@ -70,3 +70,9 @@ Failed to progress.
============================
bool_decide (∅ ⊆ {[1; 2; 3]}) = true
The command has indeed failed with message:
Nothing to inject.
The command has indeed failed with message:
Nothing to inject.
The command has indeed failed with message:
Failed to progress.
......@@ -68,3 +68,17 @@ Proof.
Show.
reflexivity.
Qed.
Lemma should_not_unfold (m1 m2 : gmap nat nat) k x :
dom (gset nat) m1 = dom (gset nat) m2
<[k:=x]> m1 = <[k:=x]> m2
True.
Proof.
(** Make sure that [injection]/[simplify_eq] does not unfold constructs on
[gmap] and [gset]. *)
intros Hdom Hinsert.
Fail injection Hdom.
Fail injection Hinsert.
Fail progress simplify_eq.
done.
Qed.
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