From c9f4cf296671baf01f3f08d2e027b415ef014059 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 23 Oct 2018 21:59:09 -0400 Subject: Add some equality lemmas about Positive{Map,Set} --- src/Util/MSetPositive/Equality.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 src/Util/MSetPositive/Equality.v (limited to 'src/Util/MSetPositive') diff --git a/src/Util/MSetPositive/Equality.v b/src/Util/MSetPositive/Equality.v new file mode 100644 index 000000000..4a5872a5e --- /dev/null +++ b/src/Util/MSetPositive/Equality.v @@ -0,0 +1,15 @@ +Require Import Coq.MSets.MSetPositive. +Require Import Crypto.Util.Bool.Equality. +Require Import Crypto.Util.Decidable. + +Module PositiveSet. + Scheme Equality for PositiveSet.tree. + + Notation t_beq := tree_beq. + Notation t_eq_dec := tree_eq_dec. + Notation internal_t_dec_bl := internal_tree_dec_bl. + Notation internal_t_dec_lb := internal_tree_dec_lb. + + Global Instance tree_dec_eq : DecidableRel (@eq PositiveSet.tree) := tree_eq_dec. + Global Instance t_dec_eq : DecidableRel (@eq PositiveSet.t) := t_eq_dec. +End PositiveSet. -- cgit v1.2.3