Google Git Google Git
Sign in
fuchsia/third_party/github.com/leanprover/lean4/refs/heads/upstream/Array.mapIdx/./tests/lean/attrCmd.lean
blob: dbf13411dd402d5082341c1d52b0a1348be08543 [file] [edit]
def M := StateM Nat
def f1 : M Nat :=
pure 0 -- failed to synthesize `Pure M`
attribute [reducible] M
def f2 : M Nat :=
pure 0