How to use do notation

Stream: general

[Konstantin Weitz]

I'm trying to get do notation to work, but even a simple example like this one fails for me:

def State T := StateM Nat T

def inc : State Unit :=
  fun n => ((), n+1)

def get : State Nat :=
  fun n => (n, n)

def program : State Nat := do
  inc
  get

with this error message for the inc call.

failed to synthesize
Bind State
Lean 4

What am I doing wrong?

[Aaron Liu]

make def State into abbrev State

[Aaron Liu]

this will allow typeclass to see through its definition

[Konstantin Weitz]

Wonderful, that worked, thanks!