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 Extranat |
---|

24 | |
---|

25 | open Vector |
---|

26 | |
---|

27 | open Div_and_mod |
---|

28 | |
---|

29 | open Jmeq |
---|

30 | |
---|

31 | open Russell |
---|

32 | |
---|

33 | open List |
---|

34 | |
---|

35 | open Util |
---|

36 | |
---|

37 | open FoldStuff |
---|

38 | |
---|

39 | open BitVector |
---|

40 | |
---|

41 | open Arithmetic |
---|

42 | |
---|

43 | open Division |
---|

44 | |
---|

45 | val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z |
---|

46 | |
---|

47 | val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z |
---|

48 | |
---|

49 | val bits_of_pos : Positive.pos -> Bool.bool List.list |
---|

50 | |
---|

51 | val zeroext_reversed : |
---|

52 | Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector |
---|

53 | |
---|

54 | val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector |
---|

55 | |
---|

56 | val pos_length : Positive.pos -> Nat.nat |
---|

57 | |
---|

**Note:** See

TracBrowser
for help on using the repository browser.