From ed0ad804bd09b2b76ec2535367ab9dd57b2600b0 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 4 Feb 2020 14:06:47 +0100
Subject: gcombine_null

---
 lib/Maps.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'lib/Maps.v')

diff --git a/lib/Maps.v b/lib/Maps.v
index e938f205..0beb11b4 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -116,6 +116,19 @@ Module Type TREE.
     forall (m1: t A) (m2: t B) (i: elt),
     get i (combine f m1 m2) = f (get i m1) (get i m2).
 
+  Parameter combine_null :
+    forall (A B C: Type) (f: A -> B -> option C),
+    t A -> t B -> t C.
+
+  Axiom gcombine_null:
+    forall (A B C: Type) (f: A -> B -> option C),
+    forall (m1: t A) (m2: t B) (i: elt),
+      get i (combine_null f m1 m2) =
+      match (get i m1), (get i m2) with
+      | (Some x1), (Some x2) => f x1 x2
+      | _, _ => None
+      end.
+
   (** Enumerating the bindings of a tree. *)
   Parameter elements:
     forall (A: Type), t A -> list (elt * A).
-- 
cgit