include "basics/lists/list.ma".

(*************************)

axiom ltb: nat → nat → bool.

(*************************)

record label: Type[0] ≝ {label_name: nat}.

record ident: Type[0] ≝ {ident_name: nat}.

record fname: Type[0] ≝ {function_name: nat}.

definition label_of_fname: fname → label ≝
 λf. mk_label (function_name f).
 
coercion label_of_fname.

record storeT: Type[1] ≝
 { store:> Type[0]
 ; get: store → option ident → nat
 ; set: store → option ident → nat → store
 ; get_set_hit: ∀s,x,v. get (set s x v) x = v
 ; get_set_miss: ∀s,x,y,v. get (set s x v) y = get s y
 }.