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

Fix whitespace error

Browse Source
This commit is contained in:
Edwin Brady 2021-04-29 13:47:31 +01:00
parent c3e5689a62
commit 3bb4333ac3
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/Compiler/CaseOpts.idr
View File

@ -39,7 +39,7 @@ shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)
shiftVar : {outer, args : _} ->
{idx : _} ->
{idx : _} ->
(0 p : IsVar n idx (outer ++ (x :: args ++ vars))) ->
NVar n (outer ++ (args ++ x :: vars))
shiftVar {outer = []} p = shiftUnder p