produce identW when needed

This commit is contained in:
Krasimir Angelov
2026-01-20 07:40:07 +01:00
parent 80524bdec9
commit 307a4481f3
+2 -1
View File
@@ -73,7 +73,8 @@ lookupIdentInfo (m,ModPGF{mpgf=pgf}) i =
appHypos [] xs t es =
foldl (appExpr xs) t es
appHypos ((bt, v, ty):hypos) xs t es =
let x = identS v in Prod bt x (cnvType xs ty) (appHypos hypos (x:xs) t es)
let x = if v == "_" then identW else identS v
in Prod bt x (cnvType xs ty) (appHypos hypos (x:xs) t es)
appExpr xs t e = App t (cnvExpr xs e)