source: driver/extracted/extralib.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: 635 bytes
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 List
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2
30
31val eq_rect_r2 : 'a1 -> 'a1 -> 'a2 -> 'a2
32
33val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2
34
35val dec_bounded_forall :
36  (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum
37
38val dec_bounded_exists :
39  (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum
40
41val dec_true : (__, __) Types.sum -> (__ -> 'a1) -> 'a1
42
43val dec_false : (__, __) Types.sum -> (__ -> 'a1) -> 'a1
44
Note: See TracBrowser for help on using the repository browser.