Adding iota

coq · Sep 26, 2023 · 0bf5474 · 0bf5474
1 parent 22c6aec
commit 0bf5474
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/text/match-with-alias.md b/text/match-with-alias.md
@@ -71,4 +71,10 @@ For an inductive type `[... Ii : Δi -> si := {... Cij : Ωij -> Ii δij ...} ..
   ————————————————————————————————————————————————————————————————————————————————————————————————————
                 Γ ⊢ (match t as x in Ii y return P with ... Cij z as w => uij ... end) : P δ
 ```
-Then, for the guard condition, the new variable `w` is considered of the size of `t`.
+and new reduction rule is:
+```
+match (Cij u) as x in Ii y return P with ... Cij z as w => uij ... end
+ →
+uij[z,w:=u,Cij u]
+```
+while, for the guard condition, the new variable `w` is considered of the size of `t`.