diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-02-21 14:10:06 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-02-21 14:10:06 -0500 |
| commit | 9f20d9299eab7caab6421860b6a54f831af73921 (patch) | |
| tree | 9e2dcb53a357f93751c3f1e1237a3d0900d02b2d /src/coq/Syntax.v | |
| parent | fe5ac0fba7f973b2557c7ae7a6bb9248024ffacd (diff) | |
Finish semantics for Featherweight Ur
Diffstat (limited to 'src/coq/Syntax.v')
| -rw-r--r-- | src/coq/Syntax.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/coq/Syntax.v b/src/coq/Syntax.v index b19a790e..2378037e 100644 --- a/src/coq/Syntax.v +++ b/src/coq/Syntax.v @@ -25,15 +25,12 @@ * POSSIBILITY OF SUCH DAMAGE. *) -Require Import String. +Require Import Name. +Export Name. Set Implicit Arguments. -Definition name : Type := string. -Definition name_eq_dec : forall (x y : name), {x = y} + {x <> y} := string_dec. - - (** Syntax of Featherweight Ur *) Inductive kind : Type := @@ -160,9 +157,12 @@ Section vars. -> deq (CApp (CApp (CMap k1 k2) f) (CConcat (CSingle c1 c2) c3)) (CConcat (CSingle c1 (CApp f c2)) (CApp (CApp (CMap k1 k2) f) c3)) - | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), - (*disj c1 c2 - ->*) deq (CGuarded c1 c2 c) c + | Eq_Guarded_Remove : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), + disj c1 c2 + -> deq (CGuarded c1 c2 c) c + | Eq_Guarded_Cong : forall k1 k2 (c1 c2 : con (KRecord k1)) (c c' : con k2), + (dvar c1 c2 -> deq c c') + -> deq (CGuarded c1 c2 c) (CGuarded c1 c2 c') | Eq_Map_Ident : forall k c, deq (CApp (CApp (CMap k k) (CAbs (fun x => CVar x))) c) c |