Noncomputable inv / div

Stream: new members

[Alex Meiburg]

The following snippet of code compiles floobOk fine, but complains that floobBad is noncomputable and so can't be compiled:

inductive Floob (x : ℝ) where
  | floob : Floob x

def floobOk (x : ℝ) : Floob (x⁻¹) :=
  ⟨⟩

def floobBad (x : ℝ) : Floob (1/x) :=
  ⟨⟩

To be precise, it says:

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instLinearOrderedFieldReal', and it does not have executable code

which makes sense. But why does floobOk work? It depends on Real.instInvReal (which I can confirm by turning off the pretty-printer), and that is also noncomputable -- for instance, running

#eval (5:ℝ)⁻¹

fails in the way I expect and says, failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instInvReal', and it does not have executable code.

I don't understand why FloobOk compiles.

[Daniel Weber]

I might be wrong, but IIRC the compiler erases types, and the only noncomputable part in floobOk is the type (you can try adding deriving Repr to Floob and #eval-ing it to see this), but that doesn't explain why floobBad fails