dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

better fc in missing case

Browse Source
This commit is contained in:
Steve Dunham
2025-01-11 17:40:24 -08:00
parent 363f85710f
commit 1a9a8d3312
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
port/Lib/Elab.newt
View File

@@ -1361,7 +1361,7 @@ check ctx tm ty = do
pure $ MkClause (getFC pat) ((scnm, pat') :: Nil) Nil rawRHS pure $ MkClause (getFC pat) ((scnm, pat') :: Nil) Nil rawRHS
-- buildCase expects scrutinee to be a name in the context, so we need to let it. -- buildCase expects scrutinee to be a name in the context, so we need to let it.
-- if it's a Bnd and not shadowed we could skip the let, but that's messy. -- if it's a Bnd and not shadowed we could skip the let, but that's messy.
let ctx' = extend ctx scnm scty let ctx' = withPos (extend ctx scnm scty) (getFC tm)
tree <- buildTree ctx' $ MkProb clauses ty tree <- buildTree ctx' $ MkProb clauses ty
pure $ Let fc scnm sc tree pure $ Let fc scnm sc tree