Last change
on this file since 2960 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

Rev  Line  

[2601]  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  

[2773]  29  val eq_rect_Type0_r : 'a1 > 'a2 > 'a1 > 'a2 

[2601]  30  

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

 32  

[2773]  33  val eq_rect_Type2_r : 'a1 > 'a2 > 'a1 > 'a2 

[2601]  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.