source: LTS/Common.ma @ 3379

Last change on this file since 3379 was 3378, checked in by sacerdot, 6 years ago
  • Stuff common to both languages is now in Common.ma
  • object (intermediate) code Vm (in progress)
File size: 618 bytes
Line 
1include "basics/lists/list.ma".
2
3(*************************)
4
5axiom ltb: nat → nat → bool.
6
7(*************************)
8
9record label: Type[0] ≝ {label_name: nat}.
10
11record ident: Type[0] ≝ {ident_name: nat}.
12
13record fname: Type[0] ≝ {function_name: nat}.
14
15definition label_of_fname: fname → label ≝
16 λf. mk_label (function_name f).
17 
18coercion label_of_fname.
19
20record storeT: Type[1] ≝
21 { store:> Type[0]
22 ; get: store → option ident → nat
23 ; set: store → option ident → nat → store
24 ; get_set_hit: ∀s,x,v. get (set s x v) x = v
25 ; get_set_miss: ∀s,x,y,v. get (set s x v) y = get s y
26 }.
Note: See TracBrowser for help on using the repository browser.