edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-20 11:21:43 +03:00
Code Issues Projects Releases Wiki Activity

Don't pass let bound things to with function

Browse Source 
These are let bound things in the local environment, which could happen
if the with clause is in a where block.
This commit is contained in:
Edwin Brady 2019-07-09 16:51:54 +02:00
parent 046498f926
commit 1119c089bf
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/TTImp/ProcessDef.idr
View File

@ -278,7 +278,12 @@ bindReq : {vs : _} ->
List (PiInfo, Name) -> List (PiInfo, Name) ->
Term pre -> Maybe (List (PiInfo, Name), List Name, ClosedTerm) Term pre -> Maybe (List (PiInfo, Name), List Name, ClosedTerm)
bindReq {vs} fc env SubRefl ns tm bindReq {vs} fc env SubRefl ns tm
= pure (ns, reverse vs, abstractEnvType fc env tm) = pure (ns, notLets [] _ env, abstractEnvType fc env tm)
where
notLets : List Name -> (vars : List Name) -> Env Term vars -> List Name
notLets acc [] _ = acc
notLets acc (v :: vs) (Let _ _ _ :: env) = notLets acc vs env
notLets acc (v :: vs) (_ :: env) = notLets (v :: acc) vs env
bindReq {vs = n :: _} fc (b :: env) (KeepCons p) ns tm bindReq {vs = n :: _} fc (b :: env) (KeepCons p) ns tm
= do b' <- shrinkBinder b p = do b' <- shrinkBinder b p
bindReq fc env p ((plicit b, n) :: ns) bindReq fc env p ((plicit b, n) :: ns)