Zulip Chat Archive

Stream: general

Topic: Another bug in calc


view this post on Zulip Yury G. Kudryashov (Mar 14 2021 at 06:18):

The following #mwe fails:

example {n : } : n  (univ : set ) :=
calc n  univ : trivial
...  univ : subset.rfl
... = univ : rfl

view this post on Zulip Mario Carneiro (Mar 14 2021 at 06:44):

trans_rel_left appears to only work on relations on the same type

theorem trans_rel_left :  {α : Sort u} {a b c : α} (r : α  α  Prop), r a b  b = c  r a c :=

view this post on Zulip Mario Carneiro (Mar 14 2021 at 06:44):

I didn't even know that calc allowed things like a \in b \subset c as trans rules

view this post on Zulip Mario Carneiro (Mar 14 2021 at 06:45):

(I suspect the author of calc also didn't)

view this post on Zulip Yury G. Kudryashov (Mar 14 2021 at 07:40):

Thanks! I'll look into fixing this tomorrow or on Monday.


Last updated: May 08 2021 at 03:17 UTC