don't know how to synthesize placeholder

Stream: maths

[Maxwell Thum]

I guess I don't understand how Lean 3 synthesizes placeholders. When I try to take star S, where star is of the following type:

abstract_simplicial_complex.star : Π {A : Type u_1} {K : abstract_simplicial_complex A} (S : set (finset A)) [_inst_1 : subset_asc S K], set (finset A)

I get the following error:

don't know how to synthesize placeholder
context:
A : Type u_1,
K : abstract_simplicial_complex A,
S : set (finset A),
_inst_1 : subset_asc S K
⊢ abstract_simplicial_complex A

For some more context, abstract_simplicial_complex is a class which takes one argument, (A : Type*).

It seems very obvious to me to use K in this context, so am I missing something?

[Kevin Buzzard]

Unification doesn't look at your local context. Inputs in {} brackets should just be inferrable from other inputs. Is abstract_simplicial_complex.star your own definition?

[Kevin Buzzard]

docs#abstract_simplicial_complex

[Kevin Buzzard]

An example of how {} works is id {X : Type} (a : X) : X where lean can figure out X from a. Imagine the chaos if it looked in your local context and just threw in the first type it found!

[Kevin Buzzard]

Oh wait -- you say it's a class? Then use [] brackets, that's exactly what they're for

[Reid Barton]

made up alternate error, following Kevin:

don't know how to synthesize placeholder
context:
A : Type u_1,
K1 : abstract_simplicial_complex A,
K2 : abstract_simplicial_complex A,
S : set (finset A),
_inst_1 : subset_asc S K1
_inst_2 : subset_asc S K2
⊢ abstract_simplicial_complex A

[Kevin Buzzard]

But if this thing is (a) a class and (b) supposed to be a class, then that won't happen.

[Reid Barton]

(b) seems unbelievable, but yes.

[Kevin Buzzard]

I think that the way to proceed with this conversation is that you post a #mwe

[Maxwell Thum]

Kevin Buzzard said:

Oh wait -- you say it's a class? Then use [] brackets, that's exactly what they're for

Ahhh, that works (for that issue, at least)

[Kevin Buzzard]

It also guarantees that for every type A, there will be at most one term of type abstract_simplicial_complex A, or your code will break (for basically the same reason as Reid's example above)