Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  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:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/extranat.mli

    r2601 r2773  
    1616
    1717open Nat
     18
     19open Jmeq
     20
     21open Russell
     22
     23open List
     24
     25open Setoids
     26
     27open Monad
     28
     29open Option
     30
     31val nat_bound_opt : Nat.nat -> Nat.nat -> __ Types.option
    1832
    1933type nat_compared =
     
    4761
    4862val nat_compared_inv_rect_Type4 :
    49   Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    50   'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __ ->
    51   'a1) -> 'a1
     63  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
     64  -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
     65  -> __ -> __ -> 'a1) -> 'a1
    5266
    5367val nat_compared_inv_rect_Type3 :
    54   Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    55   'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __ ->
    56   'a1) -> 'a1
     68  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
     69  -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
     70  -> __ -> __ -> 'a1) -> 'a1
    5771
    5872val nat_compared_inv_rect_Type2 :
    59   Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    60   'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __ ->
    61   'a1) -> 'a1
     73  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
     74  -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
     75  -> __ -> __ -> 'a1) -> 'a1
    6276
    6377val nat_compared_inv_rect_Type1 :
    64   Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    65   'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __ ->
    66   'a1) -> 'a1
     78  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
     79  -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
     80  -> __ -> __ -> 'a1) -> 'a1
    6781
    6882val nat_compared_inv_rect_Type0 :
    69   Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
    70   'a1) -> (Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __ -> __ ->
    71   'a1) -> 'a1
     83  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
     84  -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
     85  -> __ -> __ -> 'a1) -> 'a1
    7286
    7387val nat_compared_discr :
     88  Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __
     89
     90val nat_compared_jmdiscr :
    7491  Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __
    7592
Note: See TracChangeset for help on using the changeset viewer.