Last change
on this file since 2968 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:
635 bytes

Line  

1  open Preamble 

2  

3  open Hints_declaration 

4  

5  open Core_notation 

6  

7  open Pts 

8  

9  open Logic 

10  

11  open Types 

12  

13  open Bool 

14  

15  open Relations 

16  

17  open Nat 

18  

19  open List 

20  

21  open Div_and_mod 

22  

23  open Jmeq 

24  

25  open Russell 

26  

27  open Util 

28  

29  val eq_rect_Type0_r : 'a1 > 'a2 > 'a1 > 'a2 

30  

31  val eq_rect_r2 : 'a1 > 'a1 > 'a2 > 'a2 

32  

33  val eq_rect_Type2_r : 'a1 > 'a2 > 'a1 > 'a2 

34  

35  val dec_bounded_forall : 

36  (Nat.nat > (__, __) Types.sum) > Nat.nat > (__, __) Types.sum 

37  

38  val dec_bounded_exists : 

39  (Nat.nat > (__, __) Types.sum) > Nat.nat > (__, __) Types.sum 

40  

41  val dec_true : (__, __) Types.sum > (__ > 'a1) > 'a1 

42  

43  val dec_false : (__, __) Types.sum > (__ > 'a1) > 'a1 

44  

Note: See
TracBrowser
for help on using the repository browser.