5 ms·
Could somebody explain me, please, what is the annotation block and how do I use it?
by zyzor 11y ago
Could somebody explain me, please, what is the annotation block and how do I use it?
- Houshalter 11y agoIt lets you make assumptions. Assumptions let you prove implications. Say you have A->B->C and B. And you want to prove A->C. Then you can assume A, and do a regular proof that proves C. Then you use that other weird block, with the A, B, and implication sign on it. You connect the assumption you made to the "A", and the result, to the "B", and then it lets you prove "A->C".
- zyzor 11y agoOk, so the input socket of this block is the fact that I assume. And what's the meaning of the input socket of this block?
- zyzor 11y agoHm, the more I play with this block, the less I understand it. As far as I can see, the input of this block equals its output, and I can decide what's its input and output.
- dllthomas 11y agoThink of it like type annotation in Haskell. It doesn't change things, but it lets you pin things down where you know them to make it easier to figure out the bits you don't know (and lets you resolve ambiguity).
- zyzor 11y agoOh, maybe the block I talk about is not called "annotate block"? I talk about the block that from the very beginning of the game is in the "helper blocks" region and which has a pencil icon on it.
- Houshalter 11y agoNo the helper block is the assumption block. The input to the block connects to the first output of the implication block. The output is the assumption, i.e. whatever you typed into it. You can use that to prove more things. Then use the implication block to show that the assumption implies those things.