Zulip Chat Archive

Stream: maths

Topic: mysterious monoid.one


view this post on Zulip Patrick Massot (Mar 03 2019 at 15:33):

I'm moving stuff around in topology/algebra and suddenly trying to get an instance of is_ring_hom shows goals like completion.extension f 1 = monoid.one β which used to be completion.extension f 1 = 1. It's only one more refl to type but I'm perplexed. Any idea?

view this post on Zulip Johannes Hölzl (Mar 03 2019 at 15:59):

the structure mechanism, i.e. { x := _, .. _ } sometimes produces strange results. It looks like it unfolds too much. Sometimes a solution is to fix all universe meta variables.

view this post on Zulip Patrick Massot (Mar 03 2019 at 16:22):

Thank you Johannes. That's consistent with the fact that I minimized problems elsewhere by transforming a bunch of Type u by Type*

view this post on Zulip Patrick Massot (Mar 03 2019 at 16:23):

And indeed reverting one of those Type* to Type u fixes the weird goal. This is really weird. @Sebastian Ullrich any hope in :four_leaf_clover: ?

view this post on Zulip Mario Carneiro (Mar 03 2019 at 16:24):

It's just a bug in lean 3

view this post on Zulip Mario Carneiro (Mar 03 2019 at 16:24):

I recall Sebastian diagnosing it and it should be an easy fix


Last updated: May 19 2021 at 02:10 UTC