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

Line  

1  open Preamble 

2  

3  open Types 

4  

5  open Bool 

6  

7  open Relations 

8  

9  open Nat 

10  

11  open Hints_declaration 

12  

13  open Core_notation 

14  

15  open Pts 

16  

17  open Logic 

18  

19  open Positive 

20  

21  open Z 

22  

23  open Setoids 

24  

25  open Monad 

26  

27  open Option 

28  

29  open Extranat 

30  

31  open Vector 

32  

33  open Div_and_mod 

34  

35  open Jmeq 

36  

37  open Russell 

38  

39  open List 

40  

41  open Util 

42  

43  open FoldStuff 

44  

45  open BitVector 

46  

47  open Exp 

48  

49  open Arithmetic 

50  

51  open Division 

52  

53  val z_of_unsigned_bitvector : Nat.nat > BitVector.bitVector > Z.z 

54  

55  val z_of_signed_bitvector : Nat.nat > BitVector.bitVector > Z.z 

56  

57  val bits_of_pos : Positive.pos > Bool.bool List.list 

58  

59  val zeroext_reversed : 

60  Nat.nat > Nat.nat > BitVector.bitVector > BitVector.bitVector 

61  

62  val bitvector_of_Z : Nat.nat > Z.z > BitVector.bitVector 

63  

64  val pos_length : Positive.pos > Nat.nat 

65  

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