extracted/i8051bis.ml

   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 (** val internal_ram_size : Z.z **)
  24 let 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 **)
  30 let 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