Strange behaviour after proving well foundedness

Stream: new members

[Julian Sutherland]

After defining the following function:

def floor_root_helper (e : ℕ) (n : ℕ) : ℕ → ℕ
| m :=
  if m ^ e ≤ n ∧ n < (m + 1) ^ e
  then m
  else floor_root_helper (m + 1)
  using_well_founded { rel_tac := λ _ _, `[exact ⟨_, measure_wf $ λ n, n - m ^ e⟩]` }

Although Lean 3 gives me no errors, it seems that floor_root_helper is not added into the namespace after this definition.
Can anyone see what's going wrong here?

Thanks in advance!

[Reid Barton]

The last ` should not be there

[Patrick Johnson]

You can't use m in the termination proof. Your indentation confuses you. using_well_founded applies to all cases.
It should be like this (although I'm not sure this is what you want):

def floor_root_helper (e : ℕ) (n : ℕ) : ℕ → ℕ
| m :=
  if h : m ^ e ≤ n ∧ n < (m + 1) ^ e then m
  else have n - (m + 1) ^ e < n - m ^ e, by sorry,
    floor_root_helper (m + 1)
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, measure_wf $ λ k, n - k ^ e⟩] }