max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: allow LCNF discriminant to have any type

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-01 17:28:02 -07:00
parent 30c75b4b88
commit 61edf19334
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Compiler/LCNF/Check.lean
View file

@ -150,9 +150,10 @@ partial def checkCases (c : Cases) : CheckM Expr := do
let mut hasDefault := false
checkFVar c.discr
let discrType ← inferFVarType c.discr
let .const declName _ := discrType.headBeta.getAppFn | throwError "unexpected LCNF discriminant type {discrType}"
unless c.typeName == declName do
throwError "invalid LCNF `{c.typeName}.casesOn`, discriminant has type{indentExpr discrType}"
unless discrType.isAnyType do
let .const declName _ := discrType.headBeta.getAppFn | throwError "unexpected LCNF discriminant type {discrType}"
unless c.typeName == declName do
throwError "invalid LCNF `{c.typeName}.casesOn`, discriminant has type{indentExpr discrType}"
for alt in c.alts do
let type ←
match alt with