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

Removed a redundant sentence

Browse source
This commit is contained in:
Reza Gharibi 2019-06-19 18:41:01 +04:30 committed by GitHub
parent e5f68a47ac
commit 4119cde3c8
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: