29:null 2a:["$","title",null,{"children":"Stepping through currying in Lean | Bryan Gin-ge Chen | Observable"}] 2f:T9bf,api = md`To add a footer like this to a Lean editor in your own notebook, import the \`stepEditor\` function from this notebook: \`\`\`js import {stepEditor} from '@bryangingechen/stepping-through-currying-in-lean' \`\`\` Then add \`footer: stepEditor(steps, index)\` to the [options object of \`leanEditor\`](https://observablehq.com/@bryangingechen/hello-lean-prover#CMLeanEditorUsage), where \`steps\` is an array of objects (see below) and \`index\` (optional, set to 0 by default) is the starting index. The function \`stepEditor\` takes two arguments. The first argument must be an array of state objects, which can contain any number of the following fields: - \`value\`: *string*, if present, set the contents of this editor to this string. If undefined, search the preceding state objects in the array until a \`value\` is found and set the contents of the editor to that. If none are found, set the contents of the editor to its initial value (derived from \`opts.value\` or \`opts.docArray\`, where \`opts\` is the \`leanEditor\` option object.) - \`desc\`: *string* or *Node*, if present, display this string or DOM node to the right of the controls in the HTML element. - \`marks\`: *array* of objects with \`from\` and \`to\` fields containing CodeMirror positions, which are objects containing \`line\` and \`ch\` fields with line and column numbers (both 0-indexed – note that the line numbers in the editor (and as returned by the Lean server) are 1-indexed), if present, the given text range is given the \`leanmark\` class (see [style cell below](#leanmarkCSS)). For example, if \`marks\` is set to \`[{from: {line:0, ch:0}, to: {line:2, ch:5}}]\` the text from the 1st column in the 1st row to the 6th column of the 3rd row will be marked like this. - \`cursorPos\`: object containing \`line\` and \`ch\` field with line and column numbers (both 0-indexed). - \`displayMode\`: *0* or *1*, if present, set the display mode of the infoview to "goal"

(if 0) or "messages"

(if 1). The second argument specifies the index of the above array to be displayed first. By default it is set to 0, meaning that the footer starts at the beginning of the above array.`30:Tb18,function stepEditor(arr, start = 0) { if (!Array.isArray(arr) || arr.length < 1) throw new Error( `stepEditor: first argument must be a non-empty array, currently: ${arr}` ); if (start < 0 || start >= arr.length) throw new Error( `stepEditor: second argument must be a valid index, currently: ${start}, array length: ${arr.length}` ); return function(leanEditorObj) { const { editor, infoView } = leanEditorObj; if (!document.getElementById('leanmarkCSS')) document.body.appendChild(markCSS); const prevButton = html`