Mercurial > urweb
changeset 662:039ad51cf9c3
Add guard elim rule
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 12 Mar 2009 12:25:05 -0400 |
| parents | d5552715db53 |
| children | bddf0da18db6 |
| files | doc/manual.tex |
| diffstat | 1 files changed, 4 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/doc/manual.tex Thu Mar 12 12:23:23 2009 -0400 +++ b/doc/manual.tex Thu Mar 12 12:25:05 2009 -0400 @@ -665,6 +665,10 @@ \Gamma \vdash c_1 :: \{\kappa\} & \Gamma \vdash c_2 :: \{\kappa'\} & \Gamma, c_1 \sim c_2 \vdash e : \tau +} +\quad \infer{\Gamma \vdash e \; ! : \tau}{ + \Gamma \vdash e : [c_1 \sim c_2] \Rightarrow \tau + & \Gamma \vdash c_1 \sim c_2 }$$ \subsection{Pattern Typing}