Declare instances as being instances

[wenkokke]

Shouldn't all values, such as Data.List.monad now be declared as instances?

instance
    monad : ∀ {ℓ} → RawMonad (List {ℓ})
    monad = record
      { return = λ x → x ∷ []
      ; _>>=_  = λ xs f → concat (map f xs)
      }

Or am I supposed to declare these values as instances locally?

import Data.List as List
private
    instance
        ListMonad = List.monad

[MatthewDaggitt]

Apologies for the very late reply. The standard library tries to use only the core features of Agda, and therefore there are no current plans to incorporate instance arguments at the moment. Declaring them locally seems the best bet.