31:T6b2,function deduce (...ts) { ts = ts.map(t => (t._proof || t.nodeName) ? t : html`

${t}

`); const proof = html`

`; // add conclusion // '.proof > .conclusion > .ct' const conclusion = ts.pop(); proof.children[1].children[1].appendChild(conclusion); // add premises const prem = proof.children[0]; ts.forEach((t, i) => { // add premiss prem.appendChild(t); // if the premiss is a sub-tree, white-out parts of the horizontal bar for aesthetic reasons if (t._proof) { if (i == 0) { // '.proof > .conclusion > .le' t.children[1].children[0].style['border-bottom'] = '2px solid #fff'; } else if (i+1 == ts.length) { // '.proof > .conclusion > .ri' t.children[1].children[2].style['border-bottom'] = '2px solid #fff'; } } // add a bit of spacing between premises if (i + 1 < ts.length) { prem.appendChild(html`

`); } }); // so that future runs of this function can check that the node is a proof tree proof._proof = true; return proof; }32:[] 2f:{"title":"Deduction trees","cells":[{"id":0,"value":"md`# Deduction trees`","pinned":false,"hidden":false,"mode":"ojs"},{"id":687,"value":"md`![Example](https://i.imgur.com/sqGFShb.png)`","pinned":false,"hidden":false,"mode":"ojs"},{"id":530,"value":"md`## 1) Usage`","pinned":false,"hidden":false,"mode":"ojs"},{"id":562,"value":"md`Use deduce(p0, p1, ... pn, c) to create a single inference, where the arguments may be either DOM nodes (which will be kept untouched), or just strings (which will be converted to a DOM node with html\\`\\`).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":557,"value":"deduce(tex`p_0`, tex`p_1`, tex`...`, tex`p_n`, tex`c`)","pinned":false,"hidden":false,"mode":"ojs"},{"id":555,"value":"md`To create larger trees, just recurse.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":539,"value":"deduce(\n deduce('lsdfs', 'sdf', 'Evangelic'),\n deduce(\n deduce(\n deduce('Axiom'),\n deduce('Apple', 'Bananas'),\n 'Ceylon'\n ),\n 'Demon',\n 'Fast'\n ),\n 'Gibraltar'\n)","pinned":false,"hidden":false,"mode":"ojs"},{"id":528,"value":"md`## 2) Examples`","pinned":false,"hidden":false,"mode":"ojs"},{"id":626,"value":"md`Type theory`","pinned":false,"hidden":false,"mode":"ojs"},{"id":9,"value":"deduce(tex`\\Gamma\\vdash t \\in \\Pi_{x:A} B`, deduce(tex`y^A \\in \\Gamma`, tex`\\Gamma \\vdash y \\in A`), tex`\\Gamma \\vdash \\text{app}(t,y) \\in B[x := y]`)","pinned":false,"hidden":false,"mode":"ojs"},{"id":623,"value":"md`You can also import all kinds of interesting sketches, and include them in your deduction trees, because the DOM nodes that you feed to the deduction tree are left untouched :)`","pinned":false,"hidden":false,"mode":"ojs"},{"id":422,"value":"deduce(deduce('Triangles', deduce(deduce('Hello'), deduce('Set the stop split chance:', ssc.stopSplitChance), 'Mathematics'), pad(canvas)), deduce(tex`\\Gamma\\vdash t \\in \\Pi_{x:A} B`, deduce(tex`y^A \\in \\Gamma`, tex`\\Gamma \\vdash y \\in A`), tex`\\Gamma \\vdash \\text{app}(t,y) \\in B[x := y]`), growingCir)","pinned":false,"hidden":false,"mode":"ojs"},{"id":526,"value":"md`## 3) Implementation`","pinned":false,"hidden":false,"mode":"ojs"},{"id":126,"value":"md`The CSS trickery is due to [https://jsfiddle.net/qujoopkt/].`","pinned":false,"hidden":false,"mode":"ojs"},{"id":424,"value":"$31","pinned":true,"hidden":false,"mode":"ojs"},{"id":149,"value":"import { tunnelCir, growingCir } with { dimensions } from '@proquestionasker/playing-with-concentric-circles'","pinned":false,"hidden":false,"mode":"ojs"},{"id":402,"value":"width = 300","pinned":false,"hidden":false,"mode":"ojs"},{"id":404,"value":"height = 150","pinned":false,"hidden":false,"mode":"ojs"},{"id":659,"value":"dimensions = ({ width: 400, height: 320 })","pinned":false,"hidden":false,"mode":"ojs"},{"id":397,"value":"import { canvas } with { width, height, stopSplitChance } from '@justindsmith/triangle-subdivision'","pinned":false,"hidden":false,"mode":"ojs"},{"id":693,"value":"ssc = ({ stopSplitChance: html`` })","pinned":false,"hidden":false,"mode":"ojs"},{"id":697,"value":"stopSplitChance = Generators.input(ssc.stopSplitChance)","pinned":false,"hidden":false,"mode":"ojs"},{"id":414,"value":"function pad (el) {\n const padded = DOM.element('div', { style: 'padding: 10px 20px;' });\n padded.appendChild(el);\n return padded;\n}","pinned":false,"hidden":false,"mode":"ojs"}],"files":"$W32","stdlib":"1","titling":"auto"}