## Stream: new members

### Topic: Elaborating the type of a constant

#### Bolton Bailey (Dec 01 2020 at 05:49):

Hello, something came up in my project that confused me, so I thought I would post it here. The MWE is

universes u

variables {F : Type u}
variables [field F]

constants n_foo n_bar : ℕ

constant u_foo : vector (polynomial F) n_foo
constant u_bar : vector (polynomial F) n_bar

constant a_foo : vector F n_foo

def my_property (a_bar : vector F n_bar) :
((vector.map₂ has_scalar.smul a_bar u_bar).to_list.sum + (vector.map₂ has_scalar.smul a_foo u_foo).to_list.sum)
= 0
:=
sorry


This code complains of "don't know how to synthesize placeholder" on a_foo and u_foo. It gets fixed by elaborating the type of a_foo and u_foo

import data.mv_polynomial.basic
import data.polynomial.div

universes u

variables {F : Type u}
variables [field F]

constants n_foo n_bar : ℕ

constant u_foo : vector (polynomial F) n_foo
constant u_bar : vector (polynomial F) n_bar

constant a_foo : vector F n_foo

def my_property (a_bar : vector F n_bar) :
((vector.map₂ has_scalar.smul a_bar u_bar).to_list.sum + (vector.map₂ has_scalar.smul (a_foo : vector F n_foo) (u_foo : vector (polynomial F) n_foo)).to_list.sum)
= 0
:=
sorry


This latter code has no errors. But I can't figure out why it is necessary to elaborate the type when it's specified right on line 20.

#### Reid Barton (Dec 01 2020 at 09:43):

The constants u_foo, etc. depend on the variable F, which might not mean what you think.
I would recommend not using constant at all.

#### Eric Wieser (Dec 01 2020 at 09:47):

@u_foo F _ would be shorter than the type annotations

#### Reid Barton (Dec 01 2020 at 09:50):

What's going on is slightly complicated but the basic issue is you have effectively a separate constant u_foo for each field

Last updated: Dec 20 2023 at 11:08 UTC