refl with ideals

Stream: general

[Kenny Lau]

import ring_theory.ideals

example (s : ideal ℤ) : s ≤ s := by refl

[Kenny Lau]

invalid apply tactic, failed to unify
  s ≤ s
with
  ∀ [_inst_1 : preorder ?m_1] (a : ?m_1), a ≤ a
state:
s : ideal ℤ
⊢ s ≤ s

[Kenny Lau]

why doesn't refl close the goal?

[Reid Barton]

Guessing the apply bug

[Reid Barton]

it looks like apply tried to supply the wrong number of parameters, and I bet le for ideal is some forall/Pi-type which would account for this

[Floris van Doorn]

I think we have refl' for this.

[Kenny Lau]

works like a charm!