Commit 8f80353d authored by Robbert Krebbers's avatar Robbert Krebbers

Add tests for `multiset_solver`.

parent d3d95ed9
From stdpp Require Import gmultiset.
Section test.
Context `{Countable A}.
Implicit Types x y : A.
Implicit Types X Y : gmultiset A.
Lemma test1 x y X : {[x]} ({[y]} X) .
Proof. multiset_solver. Qed.
Lemma test2 x y X : {[x]} ({[y]} X) = {[y]} ({[x]} X).
Proof. multiset_solver. Qed.
Lemma test3 x : {[x]} @{gmultiset A} .
Proof. multiset_solver. Qed.
Lemma test4 x y z X Y :
{[z]} X = {[y]} Y
{[x]} ({[z]} X) = {[y]} ({[x]} Y).
Proof. multiset_solver. Qed.
End test.
Markdown is supported
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