|
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 | |
|---|
| 1 | include "basics/lists/list.ma". |
|---|
| 2 | |
|---|
| 3 | (*************************) |
|---|
| 4 | |
|---|
| 5 | axiom ltb: nat → nat → bool. |
|---|
| 6 | |
|---|
| 7 | (*************************) |
|---|
| 8 | |
|---|
| 9 | record label: Type[0] ≝ {label_name: nat}. |
|---|
| 10 | |
|---|
| 11 | record ident: Type[0] ≝ {ident_name: nat}. |
|---|
| 12 | |
|---|
| 13 | record fname: Type[0] ≝ {function_name: nat}. |
|---|
| 14 | |
|---|
| 15 | definition label_of_fname: fname → label ≝ |
|---|
| 16 | λf. mk_label (function_name f). |
|---|
| 17 | |
|---|
| 18 | coercion label_of_fname. |
|---|
| 19 | |
|---|
| 20 | record 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.
