Zulip Chat Archive

Stream: general

Topic: nasty diamond


Sebastien Gouezel (May 07 2021 at 11:04):

Lean is completely stuck on this:

import topology.continuous_function.bounded

open_locale bounded_continuous_function

example {α : Type*} [topological_space α] : semi_normed_space  (α →ᵇ ) :=
@normed_space.to_semi_normed_space  (α →ᵇ ) (by apply_instance) (by apply_instance)
(by apply_instance)

I don't know how to investigate this kind of stuff.

Update: replacing Type* with Type u solves it, so this is a universe unification issue.

Kevin Buzzard (May 07 2021 at 12:20):

Oh good catch! This sort of thing is happening more and more nowadays.


Last updated: Dec 20 2023 at 11:08 UTC