Commit 88cbb6b8 authored by Clément Pit--Claudel's avatar Clément Pit--Claudel

Use TeX magic to prevent -- from being displayed as an en dash

parent 00cbd4c1
......@@ -671,12 +671,15 @@ Defined.
(** 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. *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment