What does the pound sign mean in Idris 2?

14 views Asked by At

I am browsing through the standard library of Idris 2 and I stumbled upon this:

Data.Linear.Array:

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?

0

There are 0 answers