composOp should iterate under ImplArg
This commit is contained in:
1 parent
ee6fdbf68f
commit
f9f2491fcc
1 file changed
+4
@@ -534,6 +534,10 @@ composOp co trm =
|
|||||||
ELin c ty ->
|
ELin c ty ->
|
||||||
do ty' <- co ty
|
do ty' <- co ty
|
||||||
return (ELin c ty')
|
return (ELin c ty')
|
||||||
|
|
||||||
|
ImplArg t ->
|
||||||
|
do t' <- co t
|
||||||
|
return (ImplArg t')
|
||||||
|
|
||||||
_ -> return trm -- covers K, Vr, Cn, Sort, EPatt
|
_ -> return trm -- covers K, Vr, Cn, Sort, EPatt
|
||||||
|
|
||||||
|
|||||||
Reference in new issue
Block a user