neither computable nor noncomputable

(Unfortunately I haven't minimised this to the point we can avoid mathlib.)

import set_theory.ordinal

inductive G : Type 1
| mk : ∀ α : Type, (α → G) → G

noncomputable def N : ordinal → G
| O₁ := ⟨ O₁.out.α,
  λ O₂, have hwf : (ordinal.typein O₁.out.r O₂) < O₁ := sorry,
    N (ordinal.typein O₁.out.r O₂) ⟩
using_well_founded {dec_tac := tactic.assumption}

gives a warning definition 'N' was incorrectly marked as noncomputable, while

import set_theory.ordinal

inductive G : Type 1
| mk : ∀ α : Type, (α → G) → G

def N : ordinal → G
| O₁ := ⟨ O₁.out.α,
  λ O₂, have hwf : (ordinal.typein O₁.out.r O₂) < O₁ := sorry,
    N (ordinal.typein O₁.out.r O₂) ⟩
using_well_founded {dec_tac := tactic.assumption}

gives an error rec_fn_macro only allowed in meta definitions

Zulip thread

Reproduce the two definitions using the set_theory.ordinal import and compare the handling of noncomputable definitions, recursive definitions, and using_well_founded. Start at the rec_fn_macro and noncomputable checks mentioned by the diagnostics; done means the example has consistent, tested behavior rather than conflicting warnings and errors.