source: extracted/i8051bis.ml @ 2829

Last change on this file since 2829 was 2829, checked in by sacerdot, 7 years ago

Semantics files committed.

File size: 551 bytes
Line 
1open Preamble
2
3open Types
4
5open Bool
6
7open Relations
8
9open Nat
10
11open Hints_declaration
12
13open Core_notation
14
15open Pts
16
17open Logic
18
19open Positive
20
21open Z
22
23(** val internal_ram_size : Z.z **)
24let internal_ram_size =
25  Z.two_p
26    (Z.z_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
27      Nat.O)))))))))
28
29(** val external_ram_size : Z.z **)
30let external_ram_size =
31  Z.two_p
32    (Z.z_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
33      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
34      Nat.O)))))))))))))))))
35
Note: See TracBrowser for help on using the repository browser.