idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-20 10:02:03 +03:00
Code Issues Projects Releases Wiki Activity

Update comment to cover changes

Browse Source
This commit is contained in:
Steve Dunham 2024-06-17 10:37:44 -07:00
parent c9f7f308cf
commit f9d00ea63e
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/TTImp/TTImp.idr
View File

@ -726,8 +726,9 @@ implicitsAs n defs ns tm
Core (List (Name, PiInfo RawImp)) Core (List (Name, PiInfo RawImp))
-- #834 When we are in a local definition, we have an explicit telescope -- #834 When we are in a local definition, we have an explicit telescope
-- corresponding to the variables bound in the parent function. -- corresponding to the variables bound in the parent function.
-- So we first peel off all of the explicit quantifiers corresponding -- Parameter blocks also introduce additional telescope of implicit, auto,
-- to these variables. -- and explicit variables. So we first peel off all of the quantifiers
-- corresponding to these variables.
findImps ns es (_ :: locals) (NBind fc x (Pi _ _ _ _) sc) findImps ns es (_ :: locals) (NBind fc x (Pi _ _ _ _) sc)
= do body <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) = do body <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder))
findImps ns es locals body findImps ns es locals body