Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (8 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/bindLists.ml

    r2717 r2743  
    3333type ('b, 'e) bind_list = ('b, 'e List.list) Bind_new.bind_new
    3434
     35(** val dpi1__o__blist_from_list__o__inject :
     36    ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list)
     37    Bind_new.bind_new Types.sig0 **)
     38let dpi1__o__blist_from_list__o__inject x4 =
     39  Bind_new.Bret x4.Types.dpi1
     40
     41(** val eject__o__blist_from_list__o__inject :
     42    'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new
     43    Types.sig0 **)
     44let eject__o__blist_from_list__o__inject x4 =
     45  Bind_new.Bret (Types.pi1 x4)
     46
     47(** val blist_from_list__o__inject :
     48    'a2 List.list -> ('a1, 'a2 List.list) Bind_new.bind_new Types.sig0 **)
     49let blist_from_list__o__inject x3 =
     50  Bind_new.Bret x3
     51
     52(** val dpi1__o__blist_from_list :
     53    ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list)
     54    Bind_new.bind_new **)
     55let dpi1__o__blist_from_list x3 =
     56  let l = x3.Types.dpi1 in Bind_new.Bret l
     57
     58(** val eject__o__blist_from_list :
     59    'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new **)
     60let eject__o__blist_from_list x3 =
     61  let l = Types.pi1 x3 in Bind_new.Bret l
     62
    3563(** val bappend :
    3664    ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)
Note: See TracChangeset for help on using the changeset viewer.