From baf526316881ea681ced9c50323ea2add2f5ea34 Mon Sep 17 00:00:00 2001 From: Thomas Porter Date: Mon, 10 Jun 2024 20:45:05 -0400 Subject: [PATCH] Update typo in index-unification.md --- src/blog/index-unification.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/blog/index-unification.md b/src/blog/index-unification.md index d00e46f..42373ff 100644 --- a/src/blog/index-unification.md +++ b/src/blog/index-unification.md @@ -2,7 +2,7 @@ [#198]: https://github.com/aya-prover/aya-dev/pull/198 -Aya implements a version of index unification algorithm that allows emission of obvious patterns. Here's an example. +Aya implements a version of index unification algorithm that allows omission of obvious patterns. Here's an example. Consider the famous "sized-vector" `Vec (n : Nat) (A : Type)` definition, and we can perform some pattern matching: