Mercurial > urweb

comparison doc/manual.tex @ 573:33500a15b872

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More manual bug reports from megacz
author Adam Chlipala <adamc@hcoop.net>
date Wed, 24 Dec 2008 10:48:31 -0500
parents af0df56ecc2c
children 9db6880184d0
comparison
equal deleted inserted replaced
572:57018f21cd5c 573:33500a15b872
433 & \Gamma \vdash c_1 \sim c_2 433 & \Gamma \vdash c_1 \sim c_2
434 }$$ 434 }$$
435 435
436 $$\infer{\Gamma \vdash \mt{fold} :: ((\mt{Name} \to \kappa_1 \to \kappa_2 \to \kappa_2) \to \kappa_2 \to \{\kappa_1\} \to \kappa_2}{}$$ 436 $$\infer{\Gamma \vdash \mt{fold} :: ((\mt{Name} \to \kappa_1 \to \kappa_2 \to \kappa_2) \to \kappa_2 \to \{\kappa_1\} \to \kappa_2}{}$$
437 437
438 $$\infer{\Gamma \vdash (\overline c) :: (k_1 \times \ldots \times k_n)}{ 438 $$\infer{\Gamma \vdash (\overline c) :: (\kappa_1 \times \ldots \times \kappa_n)}{
439 \forall i: \Gamma \vdash c_i :: k_i 439 \forall i: \Gamma \vdash c_i :: \kappa_i
440 } 440 }
441 \quad \infer{\Gamma \vdash c.i :: k_i}{ 441 \quad \infer{\Gamma \vdash c.i :: \kappa_i}{
442 \Gamma \vdash c :: (k_1 \times \ldots \times k_n) 442 \Gamma \vdash c :: (\kappa_1 \times \ldots \times \kappa_n)
443 }$$ 443 }$$
444 444
445 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c :: \kappa}{ 445 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c :: \kappa}{
446 \Gamma \vdash c_1 :: \{\kappa'\} 446 \Gamma \vdash c_1 :: \{\kappa'\}
447 & \Gamma \vdash c_2 :: \{\kappa'\} 447 & \Gamma \vdash c_2 :: \{\kappa'\}
582 \Gamma \vdash e : \$([c = \tau] \rc c') 582 \Gamma \vdash e : \$([c = \tau] \rc c')
583 } 583 }
584 \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{ 584 \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
585 \Gamma \vdash e_1 : \$c_1 585 \Gamma \vdash e_1 : \$c_1
586 & \Gamma \vdash e_2 : \$c_2 586 & \Gamma \vdash e_2 : \$c_2
587 & \Gamma \vdash c_1 \sim c_2
587 }$$ 588 }$$
588 589
589 $$\infer{\Gamma \vdash e \rcut c : \$c'}{ 590 $$\infer{\Gamma \vdash e \rcut c : \$c'}{
590 \Gamma \vdash e : \$([c = \tau] \rc c') 591 \Gamma \vdash e : \$([c = \tau] \rc c')
591 } 592 }
607 \quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{ 608 \quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{
608 \forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau' 609 \forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau'
609 & \Gamma_i \vdash e_i : \tau 610 & \Gamma_i \vdash e_i : \tau
610 }$$ 611 }$$
611 612
612 $$\infer{\Gamma \vdash [c_1 \sim c_2] \Rightarrow e : [c_1 \sim c_2] \Rightarrow \tau}{ 613 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : \lambda [c_1 \sim c_2] \Rightarrow \tau}{
613 \Gamma \vdash c_1 :: \{\kappa\} 614 \Gamma \vdash c_1 :: \{\kappa\}
614 & \Gamma \vdash c_2 :: \{\kappa\} 615 & \Gamma \vdash c_2 :: \{\kappa\}
615 & \Gamma, c_1 \sim c_2 \vdash e : \tau 616 & \Gamma, c_1 \sim c_2 \vdash e : \tau
616 }$$ 617 }$$
617 618