mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-13 13:55:57 +03:00
Be explicit about multiplicity in Array
The bootstrap version can't infer it!
This commit is contained in:
parent
c3c556f192
commit
84adbe6dc8
@ -68,7 +68,7 @@ copyArray newsize a
|
||||
= if pos < 0
|
||||
then (a, a')
|
||||
else let val # a = mread a pos
|
||||
a' = case val of
|
||||
1 a' = case val of
|
||||
Nothing => a'
|
||||
Just v => write a' pos v in
|
||||
copyContent (pos - 1) a a'
|
||||
|
Loading…
Reference in New Issue
Block a user