Making sense of the output from #print

Stream: lean4

[Brandon Brown]

If I define a function or theorem and then #print it, it gives the elaborated lambda expression, but when I copy and paste it as the definition of the function it doesn't type check. Is this a whitespace issue or am I just misunderstanding something basic?

inductive nat : Type where
| zero : nat
| succ : nat → nat

open nat

protected def nat.add : nat → nat → nat :=
fun a b =>
  match a, b with
  | a, zero => a
  | a, succ b => succ (nat.add a b)

#print nat.add

/-
protected def nat.add : nat → nat → nat :=
fun (a b : nat) =>
  nat.brecOn b
    (fun (b : nat) (f : nat.below b) (a : nat) =>
      (match a, b with
        | a, zero => fun (x : nat.below zero) => a
        | a, succ b => fun (x : nat.below (succ b)) => succ (PProd.fst x.fst a))
        f)
    a
-/

-- this gives an error:
protected def nat.add' : nat → nat → nat :=
fun (a b : nat) =>
  nat.brecOn b
    (fun (b : nat) (f : nat.below b) (a : nat) =>
      (match a, b with
        | a, zero => fun (x : nat.below zero) => a
        | a, succ b => fun (x : nat.below (succ b)) => succ (PProd.fst x.fst a))
        f)
    a

[Daniel Selsam]

Known issue: https://github.com/leanprover/lean4/issues/368

[Brandon Brown]

Ok, thanks