(kernel) declaration has metavariables??

Stream: new members

[Op From The Start]

I have a definition of the ≤ operator and I have proved that it terminates, but now I am getting kernel errors and I am not sure why, or how to fix them.

-- (kernel) declaration has metavariables 'le._unary.eq_def'
noncomputable
-- (kernel) declaration has metavariables 'le._unary'
def le: PreNo → PreNo → Prop :=
  λ x y =>
   match hx:x,hy:y with
   | PreNo.mk xL xR xLS xRS, PreNo.mk yL yR yLS yRS =>
     (∀ (yr: yR), ¬(le (yRS yr) x)) ∧ (∀ (xl: xL), ¬(le y (xLS xl)))
termination_by x y => ...
decreasing_by ...

How can I get rid of these errors?

[Op From The Start]

I used eariler Ordinal instead of Ordinal.{0}, adding the universe fixed it.