edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-05 11:32:15 +03:00
Code Issues Projects Releases Wiki Activity

Fix build!

Browse Source
This commit is contained in:
Edwin Brady 2020-01-11 23:08:30 +00:00
parent 4ce469cc03
commit 62a86db1d5
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/TTImp/Elab/Hole.idr
View File

@ -42,7 +42,7 @@ checkHole rig elabinfo nest env fc n_in (Just gexpty)
addUserHole nm addUserHole nm
pure (metaval, gexpty) pure (metaval, gexpty)
checkHole rig elabinfo nest env fc n_in exp checkHole rig elabinfo nest env fc n_in exp
= do nmty <- genName ("type_of_" ++ nameRoot n_in) = do nmty <- genName ("type_of_" ++ n_in)
let env' = letToLam env let env' = letToLam env
ty <- metaVar fc Rig0 env' nmty (TType fc) ty <- metaVar fc Rig0 env' nmty (TType fc)
nm <- inCurrentNS (UN n_in) nm <- inCurrentNS (UN n_in)