From 0b840f7aaece0c209850adb2a81904b54f410091 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 23 Oct 2008 16:22:18 +0000
Subject: Open notation for declaring record instances. It solves feature
 request 1852, makes me and Arnaud happy and will permit to factor some more
 code in typeclasses. - Records are introduced using the syntax "{| x := t; y
 := foo |}" and "with" clauses are currently parsed but not yet supported in
 the elaboration. You are invited to suggest other syntaxes :) - Missing
 fields are turned into holes, extra fields cause an error message. The
 current implementation finds the type of the record at pretyping time, from
 the typing constraint alone (and just expects an inductive with one
 constructor). It is then impossible to use scope information to parse the
 bodies: that may be wrong. The other solution I see is using the fields to
 detect the type earlier, before internalisation of the bodies, but then we
 get in name clash hell. - In funind/contrib/interface I mostly put [assert
 false] everywhere to avoid warnings.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11496 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/option.ml  | 6 +++++-
 lib/option.mli | 2 ++
 2 files changed, 7 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/option.ml b/lib/option.ml
index 543c108ab9..3d98034256 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 (** Module implementing basic combinators for OCaml option type.
    It tries follow closely the style of OCaml standard library.
@@ -97,6 +97,10 @@ let fold_right f x a =
   | Some y -> f y a
   | _ -> a
 
+(** [cata f a x] is [a] if [x] is [None] and [f y] if [x] is [Some y]. *)
+let cata f a = function
+  | Some c -> f c
+  | None -> a
 
 (** {6 More Specific operations} ***)
 
diff --git a/lib/option.mli b/lib/option.mli
index c1260d9acf..04f3ca37d0 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -66,6 +66,8 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a
 (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
 val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
 
+(** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
+val cata : ('a -> 'b) -> 'b -> 'a option -> 'b
 
 (** {6 More Specific Operations} ***)
 
-- 
cgit v1.2.3