source: driver/extracted/extranat.mli @ 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: 2.6 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open 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
32
33type nat_compared =
34| Nat_lt of Nat.nat * Nat.nat
35| Nat_eq of Nat.nat
36| Nat_gt of Nat.nat * Nat.nat
37
38val nat_compared_rect_Type4 :
39  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
40  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
41
42val nat_compared_rect_Type5 :
43  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
44  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
45
46val nat_compared_rect_Type3 :
47  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
48  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
49
50val nat_compared_rect_Type2 :
51  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
52  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
53
54val nat_compared_rect_Type1 :
55  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
56  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
57
58val nat_compared_rect_Type0 :
59  (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
60  'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
61
62val nat_compared_inv_rect_Type4 :
63  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
64  -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
65  -> __ -> __ -> 'a1) -> 'a1
66
67val nat_compared_inv_rect_Type3 :
68  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
69  -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
70  -> __ -> __ -> 'a1) -> 'a1
71
72val nat_compared_inv_rect_Type2 :
73  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
74  -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
75  -> __ -> __ -> 'a1) -> 'a1
76
77val nat_compared_inv_rect_Type1 :
78  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
79  -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
80  -> __ -> __ -> 'a1) -> 'a1
81
82val nat_compared_inv_rect_Type0 :
83  Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
84  -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
85  -> __ -> __ -> 'a1) -> 'a1
86
87val nat_compared_discr :
88  Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __
89
90val nat_compared_jmdiscr :
91  Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __
92
93val nat_compare : Nat.nat -> Nat.nat -> nat_compared
94
95val eq_nat_dec : Nat.nat -> Nat.nat -> (__, __) Types.sum
96
Note: See TracBrowser for help on using the repository browser.