We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent a788893 commit adab54fCopy full SHA for adab54f
src/plfa/part2/DeBruijn.lagda.md
@@ -756,7 +756,7 @@ The logician Haskell Curry observed that getting the
756
definition of substitution right can be a tricky business. It
757
can be even trickier when using de Bruijn indices, which can
758
often be hard to decipher. Under the current approach, any
759
-definition of substitution must, of necessity, preserves
+definition of substitution must, of necessity, preserve
760
types. While this makes the definition more involved, it
761
means that once it is done the hardest work is out of the way.
762
And combining definition with proof makes it harder for errors
0 commit comments