nasty diamond

Stream: general

[Sebastien Gouezel]

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]

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