blog: fix typo

aya-prover · Jun 3, 2024 · d742c72 · d742c72
1 parent 8a48fba
commit d742c72
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.