## Stream: new members

### Topic: Only constants and Pi types are supported

#### Nicolò Cavalleri (Jul 30 2020 at 17:32):

If I change the following instance in mathlib

instance continuous_map_semimodule {α : Type*} [topological_space α]
{R : Type*} [semiring R] [topological_space R]
[semimodule R M] [topological_semimodule R M] :
semimodule R C(α, M) :=
semimodule.of_core ${ smul := (•), smul_add := λ c f g, by ext x; exact smul_add c (f x) (g x), add_smul := λ c₁ c₂ f, by ext x; exact add_smul c₁ c₂ (f x), mul_smul := λ c₁ c₂ f, by ext x; exact mul_smul c₁ c₂ (f x), one_smul := λ f, by ext x; exact one_smul R (f x) }  to instance continuous_map_semimodule {α : Type*} [topological_space α] {R : Type*} [semiring R] [topological_space R] {M : Type*} [topological_space M] [add_comm_monoid M] [has_continuous_add M] [semimodule R M] [topological_semimodule R M] : semimodule R C(α, M) := semimodule.of_core$
{ smul     := (•),
smul_add := λ c f g, by ext x; exact smul_add c (f x) (g x),
add_smul := λ c₁ c₂ f, by ext x; exact add_smul c₁ c₂ (f x),
mul_smul := λ c₁ c₂ f, by ext x; exact mul_smul c₁ c₂ (f x),
one_smul := λ f, by ext x; exact one_smul R (f x) }


(which I was planning to do before the PR but I forgot) I get

/-
only constants and Pi types are supported: ?m_1
state:
α : Type ?,
_inst_1 : topological_space α,
R : Type ?,
_inst_2 : semiring R,
_inst_3 : topological_space R,
M : Type ?,
_inst_4 : topological_space M,
_inst_7 : semimodule R M,
_inst_8 : topological_semimodule R M,
c : ?m_1,
f g : ?m_2
⊢ c • (f + g) = c • f + c • g
-/


What is going wrong?

#### Sebastien Gouezel (Jul 30 2020 at 17:39):

semimodule.of_core requires an add_comm_group M, but you have an add_comm_monoid. It means you should not use semimodule.of_core here, but give a direct proof for all the fields.

#### Nicolò Cavalleri (Jul 30 2020 at 17:48):

Oh again weird error message

#### Nicolò Cavalleri (Jul 30 2020 at 17:49):

Moreover when I did PR that I copied the proof of the subtype. Weird that it was not already in greatest generality

#### Sebastien Gouezel (Jul 30 2020 at 17:50):

Yes, we are improving things slowly by pushing things to the right generality when someone notices that things are not as general as they could be, just like you just did!

#### Sebastien Gouezel (Jul 30 2020 at 17:51):

And yes, the error messages are often pretty bad!

Last updated: May 18 2021 at 17:44 UTC