Mercurial > cpdt > repo
comparison src/Subset.v @ 533:8921cfa2f503
Use TeX magic to prevent -- from being displayed as an en dash
| author | Cl?ment Pit--Claudel <clement.pitclaudel@live.com> |
|---|---|
| date | Tue, 07 Apr 2015 18:59:24 -0400 |
| parents | b7419a10e52e |
| children | ed829eaa91b2 |
comparison
equal
deleted
inserted
replaced
| 532:aed0fcfabdbd | 533:8921cfa2f503 |
|---|---|
| 669 Defined. | 669 Defined. |
| 670 (* end thide *) | 670 (* end thide *) |
| 671 | 671 |
| 672 (** We can build a [sumor] version of the "bind" notation and use it to write a similarly straightforward version of this function. %Again, the notation definition exposes the ASCII syntax with an operator \texttt{<-{}-}, while the later code uses a nicer long left arrow $\longleftarrow$.% *) | 672 (** We can build a [sumor] version of the "bind" notation and use it to write a similarly straightforward version of this function. %Again, the notation definition exposes the ASCII syntax with an operator \texttt{<-{}-}, while the later code uses a nicer long left arrow $\longleftarrow$.% *) |
| 673 | 673 |
| 674 (** %\def\indash{-}\catcode`-=13\def-{\indash\kern0pt }% *) | |
| 675 | |
| 674 Notation "x <-- e1 ; e2" := (match e1 with | 676 Notation "x <-- e1 ; e2" := (match e1 with |
| 675 | inright _ => !! | 677 | inright _ => !! |
| 676 | inleft (exist x _) => e2 | 678 | inleft (exist x _) => e2 |
| 677 end) | 679 end) |
| 678 (right associativity, at level 60). | 680 (right associativity, at level 60). |
| 679 | 681 |
| 682 (** %\catcode`-=12% *)(* *) | |
| 680 (** printing * $\times$ *) | 683 (** printing * $\times$ *) |
| 681 | 684 |
| 682 (* EX: Write a more expressively typed version of the last exercise. *) | 685 (* EX: Write a more expressively typed version of the last exercise. *) |
| 683 | 686 |
| 684 (* begin thide *) | 687 (* begin thide *) |