compiler IR check failed at 'List.filterTR.loop._at

Stream: lean4

[Lewis]

How to fix the error:

compiler IR check failed at 'List.filterTR.loop._at.l0_norm._spec_3', error: unknown declaration 'Real.decidableEq'

-- Define the ℓ₀-norm (number of non-zero entries) of a vector

def l0_norm {n : ℕ} (v : Vec n) : ℕ :=

  (Finset.univ.filter (λ i => v i ≠ 0)).card

Thanks.

[Kevin Buzzard]

Put noncomputable before def and then if there's an open GitHub issue about this annoying thing then give it an upvote

[Bhavik Mehta]

https://github.com/leanprover/lean4/issues/1785

[Lewis]

How to fix the Lean code? Thanks a lot.

[Kim Morrison]

Kevin has answered above.

[Oliver]

(deleted)

[Lewis]

Kim Morrison said:

Kevin has answered above.

Why does it stll say "compiler IR check failed at 'List.filterTR.loop._at.l0_norm._spec_3', error: unknown declaration 'Real.decidableEq'" after putting noncomputable before def? Thanks

[Damiano Testa]

For me, it says

function expected at
  Vec
term has type
  ?m.9

at Vec n.

[Kevin Buzzard]

Lewis if you're still having the problem then can you post a #mwe ?