2f:T8bd,function formatGoal(goal, line, ch) { const { text, doc, type, state } = goal; const goalDiv = html`

`; if (state) { if (state.startsWith('⊢ solution_from ')) { goalDiv.appendChild( html`

${line}:${ch}: state

` ); const parsedState = state .match(/^⊢ solution_from (.*)/)[1] .replace(/([a-z]+) :=/g, '"$1":') .replace(/tt|right_shore/g, 'true') .replace(/ff|left_shore/g, 'false'); goalDiv.appendChild(drawParsed(JSON.parse(parsedState))); goalDiv.appendChild( html`

${leanHLSpan`${state}`}

` ); } else if (state.startsWith('no goals')) { goalDiv.appendChild( html`

${line}:${ch}: state

` ); goalDiv.appendChild( drawParsed({ wolf: true, goat: true, farmer: true, cabbage: true }) ); goalDiv.appendChild( html`

🎉 All done!

` ); } else { goalDiv.appendChild( html`

${line}:${ch}: goal

` ); goalDiv.appendChild( html`

${leanHLSpan`${state}`}

` ); } } if (text) { goalDiv.appendChild(html`

tactic ${leanHLSpan`${text}`}

`); } else if (type) { goalDiv.appendChild(html`

${line}:${ch}: type ${ goal['full-id'] ? `of ${goal['full-id']}` : `` }

`); goalDiv.appendChild( html`

${leanHLSpan`${type}`}

` ); } if (doc) { goalDiv.appendChild(formatDoc(doc)); } return goalDiv; }30:T59b,function drawParsed({ wolf, goat, cabbage, farmer }) { let topL = 28; let topR = 33; const wolfTop = !wolf ? topL : topR; const wolfLeft = !wolf ? 5 : 80; if (!wolf) topL += 14; else topR += 14; const farmerTop = !farmer ? topL : topR; const farmerLeft = !farmer ? 2 : 80; if (!farmer) topL += 19; else topR += 19; topL = Math.max(topL, 35); topR = Math.max(topR, 40); const cabbageTop = !cabbage ? topL : topR; const cabbageLeft = !cabbage ? 6 : 85; if (!cabbage) topL += 8; else topR += 8; const goatTop = !goat ? topL : topR; const goatLeft = !goat ? 3 : 80; return html`

`; }31:[] 2d:{"title":"Cabbage, goat and wolf","cells":[{"id":0,"value":"md`# Cabbage, goat and wolf`","pinned":false,"hidden":false,"mode":"ojs"},{"id":21,"value":"viewof solution = {\n const view = puzzleMaker(1, invalidation);\n view.value.editor.setCursor(3,2);\n return view;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":240,"value":"viewof showSolution = {\n const check = html``;\n const label = html`${check} Show solution`;\n function update() {\n label.value = check.checked;\n }\n check.addEventListener('click', update);\n label.value = check.checked;\n update();\n return label;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":227,"value":"md`## Resources`","pinned":false,"hidden":false,"mode":"ojs"},{"id":266,"value":"md`[Lean code by Mario Carneiro](https://leanprover-community.github.io/archive/116395maths/44057wolfgoatcabbage.html#174610029) in response to [a thread on the Lean Prover Zulip chat by Johan Commelin](https://leanprover-community.github.io/archive/116395maths/44057wolfgoatcabbage.html).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":4,"value":"script = fetch(\n 'https://gistcdn.githack.com/bryangingechen/22846c52fc6e5fc2bcdf40c5c89aacef/raw/fd265dd41099280be30bed21de8d5efd67f82749/puzzle.lean'\n)\n .then(res => res.text())\n .then(s => s.split('\\n---\\n'))","pinned":false,"hidden":false,"mode":"ojs"},{"id":42,"value":"md`Image credits: \n- [Freepik](https://www.flaticon.com/authors/freepik) at [Flaticon](https://www.flaticon.com):\n - [\\`wolf.svg\\`](https://www.flaticon.com/free-icon/wolf_185704)

\n - [\\`goat.svg\\`](https://www.flaticon.com/free-icon/goat_616714)

\n - [\\`cabbage.svg\\`](https://www.flaticon.com/free-icon/cabbage_765618)

\n - [\\`river.svg\\`](https://www.flaticon.com/free-icon/river_2087298)

\n- [Darius Dan](https://www.flaticon.com/authors/darius-dan) at [Flaticon](https://www.flaticon.com):\n - [\\`farmer.svg\\`](https://www.flaticon.com/free-icon/farmer_1983208)

`","pinned":false,"hidden":false,"mode":"ojs"},{"id":47,"value":"wolfsvg = 'https://gistcdn.githack.com/bryangingechen/22846c52fc6e5fc2bcdf40c5c89aacef/raw/0c3386d8b235a96dc97b7f5264206b4a4d2a2f42/wolf.svg'","pinned":false,"hidden":false,"mode":"ojs"},{"id":51,"value":"goatsvg = 'https://gistcdn.githack.com/bryangingechen/22846c52fc6e5fc2bcdf40c5c89aacef/raw/0c3386d8b235a96dc97b7f5264206b4a4d2a2f42/goat.svg'","pinned":false,"hidden":false,"mode":"ojs"},{"id":53,"value":"farmersvg = 'https://gistcdn.githack.com/bryangingechen/22846c52fc6e5fc2bcdf40c5c89aacef/raw/d168f503068fc2db0dcb7c002d4ae32584e0a824/farmer.svg'","pinned":false,"hidden":false,"mode":"ojs"},{"id":55,"value":"cabbagesvg = 'https://gistcdn.githack.com/bryangingechen/22846c52fc6e5fc2bcdf40c5c89aacef/raw/0c3386d8b235a96dc97b7f5264206b4a4d2a2f42/cabbage.svg'","pinned":false,"hidden":false,"mode":"ojs"},{"id":73,"value":"riversvg = 'https://gistcdn.githack.com/bryangingechen/22846c52fc6e5fc2bcdf40c5c89aacef/raw/d2f2668f6af05a3b59c7b3fd8b2c97920b979d2f/river.svg'","pinned":false,"hidden":false,"mode":"ojs"},{"id":68,"value":"md`## Code`","pinned":false,"hidden":false,"mode":"ojs"},{"id":16,"value":"scriptToSolve = {\n const s = script.slice();\n s[1] = `theorem solution : solution_from ⟨ff, ff, ff, ff⟩ :=\nbegin\n \nend`\n return s;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":11,"value":"leanLibName = 'library'","pinned":false,"hidden":false,"mode":"ojs"},{"id":35,"value":"$2f","pinned":false,"hidden":false,"mode":"ojs"},{"id":41,"value":"$30","pinned":false,"hidden":false,"mode":"ojs"},{"id":6,"value":"import {leanEditorFrom, formatDoc, CSS_CLASSES, leanHLSpan} with {leanLibName, formatGoal} from '@bryangingechen/hello-lean-prover'","pinned":false,"hidden":false,"mode":"ojs"},{"id":8,"value":"puzzleMaker = leanEditorFrom({\n fileName: 'puzzle.lean',\n docArray: showSolution ? script : scriptToSolve,\n height: '480px',\n})","pinned":false,"hidden":false,"mode":"ojs"}],"files":"$W31","stdlib":"1","titling":"auto"}