Add base.{base_,}interp_beq

These are the canonical boolean equality functions for the interpretations of the various base types.  This will probably come in handy for side conditions in proofs about reifications of rewrite rules.

1 files changed, 17 insertions, 0 deletions

diff --git a/src/Language.v b/src/Language.v
index 044d19a3e..b3f3ddf1e 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -315,6 +315,23 @@ Module Compilers.
          | type.option A => Datatypes.option (interp A)
          end%type.
 
+    Fixpoint base_interp_beq {t} : base_interp t -> base_interp t -> bool
+      := match t with
+         | type.unit => fun _ _ => true
+         | type.Z => Z.eqb
+         | type.bool => Bool.eqb
+         | type.nat => Nat.eqb
+         | type.zrange => zrange_beq
+         end.
+
+    Fixpoint interp_beq {t} : interp t -> interp t -> bool
+      := match t with
+         | type.type_base t => @base_interp_beq t
+         | type.prod A B => prod_beq _ _ (@interp_beq A) (@interp_beq B)
+         | type.list A => list_beq _ (@interp_beq A)
+         | type.option A => option_beq (@interp_beq A)
+         end.
+
     Definition try_make_base_transport_cps
                (P : type.base -> Type) (t1 t2 : type.base)
       : ~> option (P t1 -> P t2)