Fixes a verb plural error (#512)

This commit is contained in:
Marko Dimjašević 2020-09-10 07:39:40 +02:00 committed by GitHub
parent 12d87f4198
commit ebdd29865b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -329,7 +329,7 @@ We write
Γ ⊢ A Γ ⊢ A
for terms which in context `Γ` has type `A`. for terms which in context `Γ` have type `A`.
The judgement is formalised by a datatype indexed The judgement is formalised by a datatype indexed
by a context and a type. by a context and a type.
It looks exactly like the old typing judgment, but It looks exactly like the old typing judgment, but