Skip to content

Commit

Permalink
[ fix ] build
Browse files Browse the repository at this point in the history
  • Loading branch information
gallais committed Nov 29, 2023
1 parent 3850df5 commit 897f2f7
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions src/Compiler/LambdaLift.idr
Original file line number Diff line number Diff line change
Expand Up @@ -425,6 +425,11 @@ mutual
pure $ LUnderApp fc n (length bound) (allVars fc vars unused)
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
-- the resulting function
Expand Down

0 comments on commit 897f2f7

Please sign in to comment.