Custom block is unexpectedly complicated

[tekhnus]

Hi! I have a problem with creating custom blocks.

What did I do: I completed a task and I would like to represent the whole theorem as a custom block for later usage. Expectations: I hit Ctrl+A, and I expect to get an option to create a custom block which exactly represents the whole theorem. Reality: the proposed custom block is weird, it has more premises and more variables than the theorem.

[nomeata]

You can't really include an assumption in the custom block (it wouldn't exist in other tasks), so it's as if it wasn't selected, and you get the more general custom block you see

If you want a single input, maybe try adding a helper block right after the assumption and include that in your custom block?

[tekhnus]

I did what you proposed and indeed managed to get the desired block; but when I try to use it, it doesn't seem to work:

[nomeata]

Hmm, it seems it doesn't generalize the variables enough. Probably the helper block ties the variables down.

You could try to work around it by constructing an identity block first (X->X), and using that instead of the helper block.

[nomeata]

This is what I have in mind

[tekhnus]

Yeah, that works for me, thanks for the advice! I hope it will eventually work properly without workarounds.