Zulip Chat Archive

Stream: new members

Topic: Elaborating the type of a constant


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Dec 01 2020 at 09:47):

@u_foo F _ would be shorter than the type annotations

view this post on Zulip 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: May 17 2021 at 22:15 UTC