blob: 826361be2b261fe09f6b47681545d1d81db5b3b0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Require Import Arith List.
Require Import OrderedTypeEx.
Module Adr.
Include Nat_as_OT.
Definition nat2t (i: nat) : t := i.
End Adr.
Inductive expr := Const: Adr.t -> expr.
Inductive control := Go: expr -> control.
Definition program := (Adr.t * (control))%type.
Fail Definition myprog : program := (Adr.nat2t 0, Go (Adr.nat2t 0) ).
|
