source: driver/extracted/option.ml @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 1.0 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Jmeq
14
15open Russell
16
17open Bool
18
19open Nat
20
21open List
22
23open Setoids
24
25open Relations
26
27open Monad
28
29(** val option : Monad.monadProps **)
30let option =
31  Monad.makeMonadProps (fun _ x -> Types.Some x) (fun _ _ m f ->
32    match m with
33    | Types.None -> Types.None
34    | Types.Some x -> f x)
35
36(** val opt_safe : 'a1 Types.option -> 'a1 **)
37let opt_safe m =
38  (match m with
39   | Types.None -> (fun _ -> Logic.false_rect_Type0 __)
40   | Types.Some t -> (fun _ -> t)) __
41
42(** val opt_try_catch : 'a1 Types.option -> (Types.unit0 -> 'a1) -> 'a1 **)
43let opt_try_catch m f =
44  match m with
45  | Types.None -> f Types.It
46  | Types.Some x -> x
47
48(** val optPred : Monad.injMonadPred **)
49let optPred =
50  { Monad.im_pred = Monad.Mk_MonadPred; Monad.mp_inject = (fun _ _ m_sig ->
51    let m = m_sig in
52    (match Obj.magic m with
53     | Types.None -> (fun _ -> Obj.magic Types.None)
54     | Types.Some x -> (fun _ -> Obj.magic (Types.Some x))) __) }
55
Note: See TracBrowser for help on using the repository browser.