Update proofs.md

liamoc · Dec 3, 2014 · 344831c · 344831c
1 parent f22242e
commit 344831c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/pages/proofs.md b/pages/proofs.md
@@ -69,7 +69,7 @@ How does this all relate to Agda?
 
 Agda's types correspond to judgements. If we can construct a value of a certain type, we have
 simultaneously constructed a _proof_ that the theorem encoded by that type holds. As types are
-judgements, and values are theorems, _data constructors_ for a type correspond to _inference rules_
+judgements, and values are their proofs, _data constructors_ for a type correspond to _inference rules_
 for the corresponding proposition. Let's encode the judgement $\textbf{even}$ in Agda, based on
 our definition in natural deduction.