Skip to content

Commit cc90d82

Browse files
committed
[spectec] Add missing side condition on
1 parent d8fc833 commit cc90d82

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

spectec/doc/semantics/il/4-subst.spectec

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -137,6 +137,7 @@ def $subst_typ(s, VAR x a*) = VAR x $subst_arg(s, a)* -- otherwise
137137
def $subst_typ(s, optyp) = optyp
138138
def $subst_typ(s, TUP tb*) = TUP $subst_typbind(s, tb)*
139139
def $subst_typ(s, ITER t it) = ITER $subst_typ(s ++ s', t) $subst_iter(s, it')
140+
-- if (it', s') = $refresh_iter(it)
140141
def $subst_typ(s, MATCH x a* WITH inst*) = MATCH x $subst_arg(s, a)* WITH $subst_inst(s, inst)*
141142

142143
def $subst_deftyp(subst, deftyp) : deftyp

0 commit comments

Comments
 (0)