linArray.idr

-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:

module Main
import Data.Maybe
import Decidable.Equality
import Data.Vect
import Data.List
import Data.Linear.Array

dupArr : (LinArray Int, LinArray Int)
dupArr = 
  let x = newArray 3 (\x => x)
  in (x, x)
  
writeTwice : LinArray Int -> (LinArray Int, LinArray Int)
writeTwice la = 
  let x = write la 2 4
  in (case x of _ # a => 
                  case (write a 3 3) of 
                    _ # b => b
     ,case x of _ # a => a)