2c:null 2d:["$","title",null,{"children":"Lean exercise box | Bryan Gin-ge Chen | Observable"}] 32:[] 30:{"id":"19ee268ae091d706","slug":"lean-exercise-box","title":"Lean exercise box","thumbnail":"25255b749130cb07f15db5be32d26d24767d14c5172195b2b09a7db92f5ec0ef","access_level":"public","create_time":"$D2019-07-19T19:40:01.127Z","update_time":"$D2019-08-15T16:12:49.885Z","view_time":null,"first_public_time":"$D2019-07-28T19:36:08.468Z","fork":false,"stars":1,"starred":false,"owner":{"type":"team","id":"d2fd23101beb2a61","login":"bryangingechen","name":"Bryan Gin-ge Chen","avatar_url":"https://avatars-next.observableusercontent.com/73f0dccc0b7fc5c845e6a52a58e01a2ae432cc529aaada0d10ab602137e603c0","tier":"starter_2024"},"version":83,"publish_version":83,"role":null,"authored":false,"authors":[{"type":"individual","id":"5c13a1a27cf52564","login":"bryangingechen","name":"Bryan Gin-ge Chen","avatar_url":"https://avatars-next.observableusercontent.com/73f0dccc0b7fc5c845e6a52a58e01a2ae432cc529aaada0d10ab602137e603c0","tier":null}],"members":[{"type":"individual","id":"5c13a1a27cf52564","login":"bryangingechen","name":"Bryan Gin-ge Chen","avatar_url":"https://avatars-next.observableusercontent.com/73f0dccc0b7fc5c845e6a52a58e01a2ae432cc529aaada0d10ab602137e603c0","tier":null,"role":"editor"}],"comments":[],"custom_thumbnail":true,"trashed":false,"subscribed":null,"forks":2,"collection":{"id":"68b035771823d0b5","slug":"lean","title":"Lean","owner":{"id":"d2fd23101beb2a61","login":"bryangingechen","name":"Bryan Gin-ge Chen"}},"type":"notebook","body":{"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","author":"$undefined","summary":"$undefined"},{"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","author":"$undefined","summary":"$undefined"},{"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","author":"$undefined","summary":"$undefined"},{"id":18,"value":"function exerciseControls(hint, solution) {\n return function({editor}) {\n const hintButton = html`