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

check for implicit

Browse Source
This commit is contained in:
Steve Dunham
2024-10-28 21:37:02 -07:00
parent e54aced733
commit 16e6325df3
1 changed files with 2 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/Lib/Elab.idr
View File

@@ -833,6 +833,8 @@ check ctx tm ty = case (tm, !(forceType ty)) of
sc <- check (extend ctx nm' a) tm ty' sc <- check (extend ctx nm' a) tm ty'
pure $ Lam (getFC tm) nm' sc pure $ Lam (getFC tm) nm' sc
(RImplicit fc, ty) => freshMeta ctx fc ty Normal
(RLet fc nm ty v sc, rty) => do (RLet fc nm ty v sc, rty) => do
ty' <- check ctx ty (VU emptyFC) ty' <- check ctx ty (VU emptyFC)
vty <- eval ctx.env CBN ty' vty <- eval ctx.env CBN ty'