From d742c725b7b49c2a856d566776601e93a58db31a Mon Sep 17 00:00:00 2001
From: Hoshino Tented <hoshinotented@qq.com>
Date: Mon, 3 Jun 2024 21:21:00 +0800
Subject: [PATCH] blog: fix typo

---
 aya/blog/extended-pruning.aya.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/aya/blog/extended-pruning.aya.md b/aya/blog/extended-pruning.aya.md
index b7801c7..1a31d36 100644
--- a/aya/blog/extended-pruning.aya.md
+++ b/aya/blog/extended-pruning.aya.md
@@ -84,7 +84,7 @@ Then, we get the following tycking problems, according to the rules of PathP:
 
 ```
 vecA : Vec (+-assoc {?a Γ 0} {?b Γ 0} {?c Γ 0} 0) Nat
-vecB : Vec (+-assoc {?a Γ 1} {?b Γ 1} {?c Γ 1} 0) Nat
+vecB : Vec (+-assoc {?a Γ 1} {?b Γ 1} {?c Γ 1} 1) Nat
 ```
 
 Look at the spines of all of these metavariables. None of them are in pattern fragment.