** Module lib_locations Imports lib_nat_bool_rels lib_list
$location : Type(location)
$make_location : nat->location
$location_elim :
{C_location:location->TYPE}
({address:nat}C_location (make_location address))->{z:location}
C_location z
[[C_location:location->TYPE]
[f_make_location:{address:nat}C_location (make_location address)]
[address:nat]
location_elim C_location f_make_location (make_location address)
==> f_make_location address]
address = ... : location->nat
location_eq = ... : location->location->bool
* location_eq_character = ... :
{m,n:location}iff (is_true (location_eq m n)) (Eq m n)
* location_eq_refl = ... : {x:location}is_true (location_eq x x)
Env = ... : (location->Type)->Type