diff options
Diffstat (limited to 'src/coq/Syntax.v')
| -rw-r--r-- | src/coq/Syntax.v | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/src/coq/Syntax.v b/src/coq/Syntax.v index 2378037e..03f8d82e 100644 --- a/src/coq/Syntax.v +++ b/src/coq/Syntax.v @@ -54,7 +54,7 @@ Section vars. | CSingle : forall k, con KName -> con k -> con (KRecord k) | CConcat : forall k, con (KRecord k) -> con (KRecord k) -> con (KRecord k) | CMap : forall k1 k2, con (KArrow (KArrow k1 k2) (KArrow (KRecord k1) (KRecord k2))) - | CGuarded : forall k1 k2, con (KRecord k1) -> con (KRecord k1) -> con k2 -> con k2. + | TGuarded : forall k, con (KRecord k) -> con (KRecord k) -> con KType -> con KType. Variable dvar : forall k, con (KRecord k) -> con (KRecord k) -> Type. @@ -91,11 +91,11 @@ Section vars. subs c2 c2' -> subs c3 c3' -> subs (fun x => CConcat (c2 x) (c3 x)) (CConcat c2' c3') - | S_CGuarded : forall k2 k3 (c2 c3 : _ -> con (KRecord k2)) (c4 : _ -> con k3) c2' c3' c4', + | S_TGuarded : forall k2 (c2 c3 : _ -> con (KRecord k2)) c4 c2' c3' c4', subs c2 c2' -> subs c3 c3' -> subs c4 c4' - -> subs (fun x => CGuarded (c2 x) (c3 x) (c4 x)) (CGuarded c2' c3' c4'). + -> subs (fun x => TGuarded (c2 x) (c3 x) (c4 x)) (TGuarded c2' c3' c4'). End subs. Inductive disj : forall k, con (KRecord k) -> con (KRecord k) -> Prop := @@ -157,13 +157,6 @@ 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_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 | Eq_Map_Dist : forall k1 k2 f c1 c2, @@ -188,5 +181,6 @@ Section vars. | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c') | Concat : forall c1 c2, exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2)) - | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (CGuarded c1 c2 c). + | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (TGuarded c1 c2 c) + | GuardedApp : forall k (c1 c2 : con (KRecord k)) t, exp (TGuarded c1 c2 t) -> disj c1 c2 -> exp t. End vars. |