From 47c0533d8640af625d6f403a0784edaa6cc26fac Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Feb 2019 15:21:56 -0500 Subject: 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. --- src/Language.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'src/Language.v') 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) -- cgit v1.2.3