Zulip Chat Archive

Stream: general

Topic: refl with ideals


view this post on Zulip Kenny Lau (Jul 02 2020 at 14:35):

import ring_theory.ideals

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

view this post on Zulip Kenny Lau (Jul 02 2020 at 14:35):

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

view this post on Zulip Kenny Lau (Jul 02 2020 at 14:35):

why doesn't refl close the goal?

view this post on Zulip Reid Barton (Jul 02 2020 at 15:00):

Guessing the apply bug

view this post on Zulip Reid Barton (Jul 02 2020 at 15:00):

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

view this post on Zulip Floris van Doorn (Jul 02 2020 at 15:04):

I think we have refl' for this.

view this post on Zulip Kenny Lau (Jul 02 2020 at 15:21):

works like a charm!


Last updated: May 08 2021 at 10:12 UTC