Compact definition of ¬¬¬-elim

plfa · Nov 4, 2024 · 89ed5ab · 89ed5ab
1 parent e82750f
commit 89ed5ab
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/plfa/part1/Negation.lagda.md b/src/plfa/part1/Negation.lagda.md
@@ -99,7 +99,7 @@ We cannot show that `¬ ¬ A` implies `A`, but we can show that
   → ¬ ¬ ¬ A
     -------
   → ¬ A
-¬¬¬-elim ¬¬¬x  =  λ x → ¬¬¬x (¬¬-intro x)
+¬¬¬-elim ¬¬¬x x  =  ¬¬¬x (¬¬-intro x)
 ```
 Let `¬¬¬x` be evidence of `¬ ¬ ¬ A`. We will show that assuming
 `A` leads to a contradiction, and hence `¬ A` must hold.