diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-24 15:43:01 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-24 15:43:01 -0500 |
commit | 525032e2662840e3c11dec5179467e09109a0cac (patch) | |
tree | fceb7705d7f5338f1163217ccbdbb794a2da6aa5 | |
parent | 40c7ffa60a077040ad741bc1a68bb4679efe4475 (diff) |
Add smart_interp_flat_map2
-rw-r--r-- | src/Reflection/Syntax.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 58000fdca..46a91e30b 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -111,6 +111,19 @@ Section language. (@smart_interp_flat_map f g h tt pair A (fst v)) (@smart_interp_flat_map f g h tt pair B (snd v)) end. + Fixpoint smart_interp_flat_map2 {f1 f2 g} + (h : forall x, f1 x -> f2 x -> g (Tbase x)) + (tt : g Unit) + (pair : forall A B, g A -> g B -> g (Prod A B)) + {t} + : interp_flat_type_gen f1 t -> interp_flat_type_gen f2 t -> g t + := match t return interp_flat_type_gen f1 t -> interp_flat_type_gen f2 t -> g t with + | Tbase _ => h _ + | Unit => fun _ _ => tt + | Prod A B => fun v1 v2 => pair _ _ + (@smart_interp_flat_map2 f1 f2 g h tt pair A (fst v1) (fst v2)) + (@smart_interp_flat_map2 f1 f2 g h tt pair B (snd v1) (snd v2)) + end. Fixpoint smart_interp_map_hetero {f g g'} (h : forall x, f x -> g (Tflat (Tbase x))) (tt : g Unit) |