De Bruijn: Fix a verb form (#527)
This commit is contained in:
parent
a78889398d
commit
adab54f36d
1 changed files with 1 additions and 1 deletions
|
@ -756,7 +756,7 @@ The logician Haskell Curry observed that getting the
|
|||
definition of substitution right can be a tricky business. It
|
||||
can be even trickier when using de Bruijn indices, which can
|
||||
often be hard to decipher. Under the current approach, any
|
||||
definition of substitution must, of necessity, preserves
|
||||
definition of substitution must, of necessity, preserve
|
||||
types. While this makes the definition more involved, it
|
||||
means that once it is done the hardest work is out of the way.
|
||||
And combining definition with proof makes it harder for errors
|
||||
|
|
Loading…
Reference in a new issue