ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 03:34:13 +03:00
Code Issues Projects Releases Wiki Activity

Fix borrowed type check

Browse Source 
Actually a borrowed type can be used as many times as you like, it's
just the names inside the pattern that can't be used without being lent
first!
This commit is contained in:
Edwin Brady 2014-08-22 00:12:58 +01:00
parent b37dcbeab3
commit ddf9779f87
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Idris/Core/Typecheck.hs
View File

@ -271,7 +271,7 @@ checkUnique borrowed ctxt env tm
then put ((n, (LendOnly, NullType)) : ns)
else put ((n, (Once, UniqueType)) : ns)
UType NullType -> do ns <- get
put ((n, (LendOnly, NullType)) : ns)
put ((n, (Many, NullType)) : ns)
UType AllTypes -> do ns <- get
put ((n, (Once, AllTypes)) : ns)
_ -> return ()

2
test/unique001/unique001d.idr
View File

@ -1,3 +1,3 @@
steal : {a : UniqueType} -> Borrowed a -> a
steal x = x
steal (Read x) = x