implementedBy + mutual

Stream: lean4

[Siddharth Bhat]

Consider the program below, ehre we use a mutual clause to create functions even_impl and odd_impl, which supply
implementations for the constants odd and even (This pattern was suggested as a workaround to this issue I had yesterday).

inductive Foo
| mk: Int -> Foo

instance : Inhabited Foo where
  default := Foo.mk 42

constant odd : Int -> Foo
constant even : Int -> Foo

-- | in reality these are partial mutually defined functions.
-- | We use `constant` to evade
-- | `partial mutual...end`
mutual
  def even_impl (i: Int): Foo :=
        match i with
        | 0 => Foo.mk 1
        | n => even (n - 1)

 def odd_impl (i: Int): Foo :=
     match i with
     | 0 => Foo.mk 0
     | n => even (n - 1)
end

attribute [implementedBy odd_impl] odd
attribute [implementedBy even_impl] even

-- | expected output: 1
def main : IO Unit :=
  match even 10 with
   | Foo.mk k => IO.println k

We expect the result to be 1, as 10 is even. However, the answer that is produced 42, which seems to be generated from the Inhabited instance of Foo. Am I misunderstanding what the pattern is supposed to be doing? is this a bug?

LEAN4 version [nightly]:

$ lean --version
Lean (version 4.0.0, commit f4759c9a223f, Release)

[Leonardo de Moura]

This pattern is not necessary. You can write

inductive Foo
  | mk: Int -> Foo
  deriving Inhabited

mutual
  partial def even (i: Int): Foo :=
    match i with
    | 0 => Foo.mk 1
    | n => odd (n - 1)

 partial def odd (i: Int): Foo :=
   match i with
   | 0 => Foo.mk 0
   | n => even (n - 1)
end

def main : IO Unit :=
  match even 10 with
   | Foo.mk k => IO.println k

#eval main
-- 1

[Siddharth Bhat]

Right, it's nice that the bug is fixed so I don't need the workaround anymore!

I was wondering if I misunderstood what implementedBy does, or if the example program exhibits a bug.