31:[] 2f:{"title":"Lean exercise box","cells":[{"id":0,"value":"md`# Lean exercise box\n\nThis notebook demonstrates a custom footer function for the [Lean editor](https://observablehq.com/@bryangingechen/hello-lean-prover) which adds \"hint\" and \"solution\" buttons. Here it is used to make an \"exercise box\".`","pinned":false,"hidden":false,"mode":"ojs"},{"id":22,"value":"{\n style3;\n const fileName = 'exercise.lean';\n const iv = new InfoView({ \n class: 'infoview3',\n filterMode: 1,\n displayMode: 1,\n }, invalidation);\n const le = leanEditorFrom({\n fileName,\n docArray, \n infoView: iv,\n });\n const statement = le(0, invalidation, {\n readOnly: true,\n height: '30px',\n header: html`TPiL, Exercise 3.7.1 (done with tactics):`,\n });\n const inputEditor = le(1, invalidation, {\n header: html`Fill in a proof of the above statement, using tactics:`,\n footer: exerciseControls(hint, solution),\n });\n return html`

${statement}${inputEditor}

${iv.node}`;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":5,"value":"md`Calling \\`exerciseControls\\` with a \\`hint\\` string and \\`solution\\` string creates a function which is suitable for being passed to the \\`footer\\` option in \\`leanEditor\\`:`","pinned":false,"hidden":false,"mode":"ojs"},{"id":18,"value":"function exerciseControls(hint, solution) {\n return function({editor}) {\n const hintButton = html`