Mercurial > cpdt > repo

comparison src/Subset.v @ 392:4b1242b277b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Typo fixes
author Adam Chlipala <adam@chlipala.net>
date Fri, 20 Apr 2012 12:49:47 -0400
parents 31fa03bc0f18
children 05efde66559d
comparison
equal deleted inserted replaced
391:fd3f1057685c 392:4b1242b277b2
649 m2 <- pred_strong7 n2; 649 m2 <- pred_strong7 n2;
650 [|(m1, m2)|]); tauto. 650 [|(m1, m2)|]); tauto.
651 Defined. 651 Defined.
652 (* end thide *) 652 (* end thide *)
653 653
654 (** We can build a [sumor] version of the %``%#"#bind#"#%''% notation and use it to write a similarly straightforward version of this function. *) 654 (** We can build a [sumor] version of the %``%#"#bind#"#%''% notation and use it to write a similarly straightforward version of this function. %The operator rendered here as $\longleftarrow$ is noted in the source as a less-than character followed by two hyphens.% *)
655 655
656 (** printing <-- $\longleftarrow$ *) 656 (** printing <-- $\longleftarrow$ *)
657 657
658 Notation "x <-- e1 ; e2" := (match e1 with 658 Notation "x <-- e1 ; e2" := (match e1 with
659 | inright _ => !! 659 | inright _ => !!
673 m1 <-- pred_strong8 n1; 673 m1 <-- pred_strong8 n1;
674 m2 <-- pred_strong8 n2; 674 m2 <-- pred_strong8 n2;
675 [||(m1, m2)||]); tauto. 675 [||(m1, m2)||]); tauto.
676 Defined. 676 Defined.
677 (* end thide *) 677 (* end thide *)
678
679 (** This example demonstrates how judicious selection of notations can hide complexities in the rich types of programs. *)
678 680
679 681
680 (** * A Type-Checking Example *) 682 (** * A Type-Checking Example *)
681 683
682 (** We can apply these specification types to build a certified type checker for a simple expression language. *) 684 (** We can apply these specification types to build a certified type checker for a simple expression language. *)