I am browsing through the standard library of Idris 2 and I stumbled upon this:
export
MArray LinArray where
newArray size k = k (MkLinArray (unsafePerformIO (newArray size)))
write (MkLinArray a) i el
= unsafePerformIO (do ok <- writeArray a i el
pure (ok # MkLinArray a))
msize (MkLinArray a) = max a # MkLinArray a
mread (MkLinArray a) i
= unsafePerformIO (readArray a i) # MkLinArray a
What does the pound sign mean?
The REPL reports:
Main> :t (#)
Builtin.(#) : (1 _ : a) -> (1 _ : b) -> LPair a b
Builtin.DPair.(#) : (val : a) -> (1 _ : t val) -> Res a t
So I suppose it is related to linear pairs. How are linear pairs used with linear arrays?