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

Fix linearity annotation in take

Browse Source 
Hopefully this fixes the bootstrap build
This commit is contained in:
Edwin Brady 2020-12-27 20:11:06 +00:00
parent ad632d825d
commit 61ba5e086f
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/base/Data/Vect.idr
View File

@ -79,7 +79,7 @@ init (x::y::ys) = x :: init (y::ys)
||| Extract the first `n` elements of a Vect.
public export
take : (1 n : Nat)
take : (n : Nat)
-> ( xs : Vect (n + m) type)
-> Vect n type
take 0 xs = Nil