%
% types for a 2^k x N RAM
%

ram_types[k:nat, N:posnat]: THEORY 
BEGIN
  IMPORTING 
    bitvectors@top

% types for address and dataword vectors
  ram_addresst : TYPE+ = bvec[k];
  ram_wordt    : TYPE+ = bvec[N];

% ramt implements the ram
  ramt : TYPE+ = [bvec[k] -> bvec[N]];

END ram_types