michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #299 from h4iku/sentence-patch

Browse source 
DeBruijn: Removed a redundant sentence
This commit is contained in:
Philip Wadler 2019-06-19 12:00:36 -03:00 committed by GitHub
commit 41dc0ba78d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/plfa/DeBruijn.lagda
View file

@ -360,8 +360,7 @@ data _⊢_ : Context → Type → Set where
The definition exploits the close correspondence between the The definition exploits the close correspondence between the
structure of terms and the structure of a derivation showing structure of terms and the structure of a derivation showing
that it is well-typed: now we use the derivation _as_ the that it is well-typed: now we use the derivation _as_ the
term. For example, consider the following three terms, term.
building up the Church numeral two.
For example, consider the following old-style typing For example, consider the following old-style typing
judgments: judgments: