easy way to use monad instance of List

Stream: lean4

[Asei Inoue]

Sometimes I want to use a monad instance of List, but I find it tedious to have to create my own instance.

Why not make instances available only with open scoped ListMonad, as follows?

namespace ListMonad

/-- monad instance of `List` -/
scoped instance : Monad List where
  pure := fun {_} a => [a]
  bind := @List.flatMap
  map := @List.map

end ListMonad

open scoped ListMonad

def foo : List Nat := do
  let x ← [1, 2, 3]
  return x

[Mac Malone]

Alternatively, the instance could be a regular def and be enabled via attribute [local instance].

def List.instMonad : Monad List where
  pure := @List.singleton
  bind := @List.flatMap
  map := @List.map

attribute [local instance] List.instMonad

def foo : List Nat := do
  let x ← [1, 2, 3]
  return x

[Mac Malone]

This can even be scoped to a definition like so:

attribute [instance] List.instMonad in
def foo : List Nat := do
  let x ← [1, 2, 3]
  return x

[Asei Inoue]

@Mac Malone nice! Your way enables us to write ListMonad namespace freely..

[Daniel Weber]

Mac Malone said:

This can even be scoped to a definition like so:

attribute [instance] List.instMonad in
def foo : List Nat := do
  let x ← [1, 2, 3]
  return x

This doesn't work correctly, the attribute is registered globally

[François G. Dorais]

Add local