Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/src/Subset.v Fri Nov 21 11:21:37 2014 -0500 +++ b/src/Subset.v Tue Apr 07 18:59:24 2015 -0400 @@ -671,12 +671,15 @@ (** 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$.% *) +(** %\def\indash{-}\catcode`-=13\def-{\indash\kern0pt }% *) + Notation "x <-- e1 ; e2" := (match e1 with | inright _ => !! | inleft (exist x _) => e2 end) (right associativity, at level 60). +(** %\catcode`-=12% *)(* *) (** printing * $\times$ *) (* EX: Write a more expressively typed version of the last exercise. *)