Last change
on this file since 2993 was
2773,
checked in by sacerdot, 7 years ago

 everything extracted again after all bugs in Matita's extraction have
been fixed. No more need for manual patching
 new extraction after file reorganization (by James)

File size:
1.0 KB

Rev  Line  

[2601]  1  open Preamble 

 2  

[2773]  3  open Hints_declaration 

 4  

 5  open Core_notation 

 6  

 7  open Pts 

 8  

 9  open Logic 

 10  

 11  open Types 

 12  

[2601]  13  open Jmeq 

 14  

 15  open Russell 

 16  

 17  open Bool 

 18  

 19  open Nat 

 20  

 21  open List 

 22  

 23  open Setoids 

 24  

 25  open Relations 

 26  

 27  open Monad 

 28  

[2773]  29  (** val option : Monad.monadProps **) 

 30  let option = 

[2601]  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 **) 

 37  let 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 **) 

 43  let 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 **) 

 49  let 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.