diff src/Subset.v @ 392:4b1242b277b2

Typo fixes
author Adam Chlipala <adam@chlipala.net>
date Fri, 20 Apr 2012 12:49:47 -0400
parents 31fa03bc0f18
children 05efde66559d
line wrap: on
line diff
--- a/src/Subset.v	Thu Apr 12 18:46:55 2012 -0400
+++ b/src/Subset.v	Fri Apr 20 12:49:47 2012 -0400
@@ -651,7 +651,7 @@
 Defined.
 (* end thide *)
 
-(** We can build a [sumor] version of the %``%#"#bind#"#%''% notation and use it to write a similarly straightforward version of this function. *)
+(** 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.% *)
 
 (** printing <-- $\longleftarrow$ *)
 
@@ -676,6 +676,8 @@
 Defined.
 (* end thide *)
 
+(** This example demonstrates how judicious selection of notations can hide complexities in the rich types of programs. *)
+
 
 (** * A Type-Checking Example *)