mysterious monoid.one

Stream: maths

[Patrick Massot]

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?

[Johannes Hölzl]

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.

[Patrick Massot]

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

[Patrick Massot]

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: ?

[Mario Carneiro]

It's just a bug in lean 3

[Mario Carneiro]

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