Mercurial > urweb
diff doc/manual.tex @ 662:039ad51cf9c3
Add guard elim rule
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 12 Mar 2009 12:25:05 -0400 |
parents | d5552715db53 |
children | c90906b2f431 |
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}