Mercurial > urweb

comparison src/coq/Syntax.v @ 619:f38e009009bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Time to start thinking about guards
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 13:22:30 -0500
parents be88d2d169f6
children d828b143e147
comparison
equal deleted inserted replaced
618:be88d2d169f6 619:f38e009009bb
185 | Cast : forall t1 t2, deq t1 t2 -> exp t1 -> exp t2 185 | Cast : forall t1 t2, deq t1 t2 -> exp t1 -> exp t2
186 | Empty : exp (TRecord (CEmpty _)) 186 | Empty : exp (TRecord (CEmpty _))
187 | Single : forall c t, exp t -> exp (TRecord (CConcat (CSingle c t) (CEmpty _))) 187 | Single : forall c t, exp t -> exp (TRecord (CConcat (CSingle c t) (CEmpty _)))
188 | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t 188 | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t
189 | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c') 189 | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c')
190 | Concat : forall c1 c2, disj c1 c2 -> exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2)) 190 | Concat : forall c1 c2, exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2))
191 | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (CGuarded c1 c2 c). 191 | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (CGuarded c1 c2 c).
192 End vars. 192 End vars.