Stream: new members

Topic: Coercion from a submodule to its underlying set

Joe (Jul 30 2019 at 14:13):

A coercion from a submodule to its underlying set is defined in algebra/module:

instance : has_coe (submodule α β) (set β) := ⟨submodule.carrier⟩


However, the type inference system doesn't seem to use it. Instead, it is looking for has_coe_to_fun (submodule α β). This sometimes results in a timeout. See the following example.

import analysis.normed_space.basic

variables {α : Type*} {β : Type*}
(x : α) (K : submodule ℝ α)

#check (K : set α) -- (deterministic) timeout
-- [class_instances] (0) ?x_3 : has_coe_to_fun
-- (@submodule ℝ α (@normed_ring.to_ring ℝ (@normed_field.to_normed_ring ℝ real.normed_field)) _inst_1
-- (@vector_space.to_module ℝ α (@normed_field.to_discrete_field ℝ real.normed_field) _inst_1 _inst_2))
-- ...


Does that mean we need to add the following instance?

instance : has_coe_to_fun (submodule ℝ α) := ⟨_, submodule.carrier⟩


Mario Carneiro (Jul 30 2019 at 23:08):

did you try writing (\u K : set A)?

Last updated: May 12 2021 at 23:13 UTC