Skip to content

Commit

Permalink
[ cleanup ]
Browse files Browse the repository at this point in the history
  • Loading branch information
gallais committed Nov 28, 2023
1 parent f9206e2 commit b726a32
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 6 deletions.
4 changes: 0 additions & 4 deletions src/Compiler/LambdaLift.idr
Original file line number Diff line number Diff line change
Expand Up @@ -368,10 +368,6 @@ mutual
update Lifts { defs $= ((n, MkLFun (used us) bound scl') ::) }
pure $ LUnderApp fc n (length bound) (allVars fc vars us)
where
allPrfs : (vs : List Name) -> (unused : Vect (length vs) Bool) -> List (Var vs)
allPrfs [] _ = []
allPrfs (v :: vs) (False::uvs) = MkVar First :: map weaken (allPrfs vs uvs)
allPrfs (v :: vs) (True::uvs) = map weaken (allPrfs vs uvs)

-- apply to all the variables. 'First' will be first in the last, which
-- is good, because the most recently bound name is the first argument to
Expand Down
4 changes: 2 additions & 2 deletions src/Core/TT/Var.idr
Original file line number Diff line number Diff line change
Expand Up @@ -521,8 +521,8 @@ usedIsVar :
usedIsVar (False :: bs) First = assert_total $
idris_crash "INTERNAL ERROR: Referenced variable marked as unused"
usedIsVar (True :: bs) First = MkNVar First
usedIsVar (False :: bs) (Later p) = usedIsVar (bs) p
usedIsVar (True :: bs) (Later p) = later (usedIsVar (bs) p)
usedIsVar (False :: bs) (Later p) = usedIsVar bs p
usedIsVar (True :: bs) (Later p) = later (usedIsVar bs p)

export
usedNVar : (us : Used vars) -> NVar nm vars -> NVar nm (used us)
Expand Down

0 comments on commit b726a32

Please sign in to comment.