Add type.related_hetero

1 files changed, 8 insertions, 0 deletions

diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index 5fa3a25bd..6c18a75fc 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -113,6 +113,14 @@ Module Compilers.
 
     Notation eqv := (@related _ _ (fun _ => eq)).
 
+    Fixpoint related_hetero {base_type} {base_interp1 base_interp2 : base_type -> Type}
+             (R : forall t, base_interp1 t -> base_interp2 t -> Prop) {t : type base_type}
+      : interp base_interp1 t -> interp base_interp2 t -> Prop
+      := match t with
+         | base t => R t
+         | arrow s d => respectful_hetero _ _ _ _ (@related_hetero _ _ _ R s) (fun _ _ => @related_hetero _ _ _ R d)
+         end%signature.
+
     Fixpoint app_curried {base_type} {f : base_type -> Type} {t : type base_type}
       : interp f t -> for_each_lhs_of_arrow (interp f) t -> f (final_codomain t)
       := match t with