31:[] 2f:{"title":"Lean Utility Functions","cells":[{"id":0,"value":"md`# Lean Utility Functions`","pinned":false,"hidden":false,"mode":"ojs"},{"id":428,"value":"md`Collection of utility methods to write great Lean tutorials. Just import whatever you like using\n\\`\\`\\`javascript\nimport {} with {leanLibName} from '@kappelmann/lean-utility-functions'\n\\`\\`\\`\nwhere \\`leanLibName\\` specifies the lean library you want to use. You can use\n\\`\\`\\`javascript\nimport {LEAN_LIBS} from '@kappelmann/lean-configuration'\nleanLibName = LEAN_LIBS.MATHLIB // or LEAN_LIBS.CORE\n\\`\\`\\`\n`","pinned":false,"hidden":false,"mode":"ojs"},{"id":50,"value":"md`## Variables`","pinned":false,"hidden":false,"mode":"ojs"},{"id":636,"value":"md`The next cell determines which libraray to use. For mathlib use \\`LEAN_LIBS.MATHLIB\\` and for core use \\`LEAN_LIBS.CORE\\`.`","pinned":false,"hidden":false,"mode":"ojs"},{"id":643,"value":"leanLibName = LEAN_LIBS.CORE","pinned":false,"hidden":false,"mode":"ojs"},{"id":47,"value":"md`## Functions`","pinned":false,"hidden":false,"mode":"ojs"},{"id":800,"value":"defTemplate = (kind) => (name) => inlinemd`**${kind}**${name ? ` (${name})` : ''}.`","pinned":true,"hidden":false,"mode":"ojs"},{"id":383,"value":"thm = defTemplate('Theorem')","pinned":true,"hidden":false,"mode":"ojs"},{"id":386,"value":"lem = defTemplate('Lemma')","pinned":true,"hidden":false,"mode":"ojs"},{"id":389,"value":"exmpl = defTemplate('Example')","pinned":true,"hidden":false,"mode":"ojs"},{"id":814,"value":"prop = defTemplate('Proposition')","pinned":true,"hidden":false,"mode":"ojs"},{"id":820,"value":"cor = defTemplate('Corollary')","pinned":true,"hidden":false,"mode":"ojs"},{"id":816,"value":"def = defTemplate('Definition')","pinned":true,"hidden":false,"mode":"ojs"},{"id":392,"value":"proof = el => inlinemd`*Proof ${el}.*`","pinned":true,"hidden":false,"mode":"ojs"},{"id":1044,"value":"floatRight = el => html`${el}`","pinned":true,"hidden":false,"mode":"ojs"},{"id":395,"value":"qed = () => floatRight(tex`\\square`)","pinned":true,"hidden":false,"mode":"ojs"},{"id":1054,"value":"justification = el => floatRight(html`(${el})`)","pinned":true,"hidden":false,"mode":"ojs"},{"id":501,"value":"details = ({ header, text, className = '' }) => {\n addCSS(leanUtilityFunctionsStyle);\n return html`\n

${header}

${text}\n

`;\n}","pinned":true,"hidden":false,"mode":"ojs"},{"id":444,"value":"question = (question, answer) => details({\n header: html`❓ ${question}`,\n text: answer,\n className: CSS_CLASSES.QUESTION\n})","pinned":true,"hidden":false,"mode":"ojs"},{"id":491,"value":"warning = (warning, explanation) => details({\n header: html`⚠️ ${warning}`,\n text: explanation,\n className: CSS_CLASSES.WARNING\n})","pinned":true,"hidden":false,"mode":"ojs"},{"id":825,"value":"info = (info, explanation) =>\n details({\n header: html`❗ ${info}`,\n text: explanation,\n className: CSS_CLASSES.INFORMATION\n })","pinned":true,"hidden":false,"mode":"ojs"},{"id":5,"value":"function examplesTable({examples, editor, invalidation, offset = 0}) {\n if (!(invalidation instanceof Promise))\n throw new Error(`examplesTable: invalidation be a promise (currently: ${invalidation})`);\n return html`\n \n \n \n \n \n ${examples.map((el, i) => html`\n \n \n \n `\n )}\n

Example	Lean Proof
${responsive_katex(invalidation, tex`${el}`)}	${editor(i + offset, invalidation)}

`\n}","pinned":true,"hidden":false,"mode":"ojs"},{"id":463,"value":"md`## Styling`","pinned":false,"hidden":false,"mode":"ojs"},{"id":468,"value":"CSS_CLASSES = ({\n INFORMATION: 'information',\n QUESTION: 'question',\n WARNING: 'warning',\n ...BASE_CSS_CLASSES\n})","pinned":false,"hidden":false,"mode":"ojs"},{"id":481,"value":"leanUtilityFunctionsStyle = html``","pinned":true,"hidden":false,"mode":"ojs"},{"id":26,"value":"md`## Imports`","pinned":false,"hidden":false,"mode":"ojs"},{"id":614,"value":"import {\n LEAN_LIBS,\n COLOURS,\n INTERNAL_CSS,\n leanEditorConfig,\n CSS_CLASSES as BASE_CSS_CLASSES,\n SPACING_BASELINE\n} from '@kappelmann/lean-configuration'","pinned":true,"hidden":false,"mode":"ojs"},{"id":608,"value":"import {leanEditor, leanEditorFrom, leanHL, InfoView}\nwith {leanLibName, INTERNAL_CSS, leanEditorConfig as config} \nfrom '@bryangingechen/hello-lean-prover'","pinned":true,"hidden":false,"mode":"ojs"},{"id":418,"value":"import {explanationFooter}\nwith {leanLibName, leanEditor, stepEditor}\nfrom '@kappelmann/lean-code-explainer'","pinned":true,"hidden":false,"mode":"ojs"},{"id":413,"value":"import {leanEditorWithStorage}\nwith {leanLibName, leanEditor}\nfrom '@kappelmann/lean-editor-with-local-storage'","pinned":true,"hidden":false,"mode":"ojs"},{"id":89,"value":"import {proofView, proofCreatorFooter, observeProofObject, convertMathsEntryRaw}\nwith {leanLibName, leanEditor, leanEditorFrom, leanHL, InfoView}\nfrom '@kappelmann/lean-proof-view'","pinned":true,"hidden":false,"mode":"ojs"},{"id":71,"value":"import {stepEditor}\nwith {leanLibName, leanEditor}\nfrom '@bryangingechen/stepping-through-currying-in-lean'","pinned":true,"hidden":false,"mode":"ojs"},{"id":424,"value":"import {stepsCreatorFooter, observeStepsObject, convertDescRaw}\nwith {leanLibName, leanEditor, explanationFooter, stepEditor}\nfrom '@kappelmann/lean-step-editor-steps-creator'","pinned":true,"hidden":false,"mode":"ojs"},{"id":709,"value":"import {quizMarks}\nwith {leanLibName, leanEditor, leanHL}\nfrom '@kappelmann/lean-quiz'","pinned":true,"hidden":false,"mode":"ojs"},{"id":1036,"value":"import { inlinemd, mdtex } from '@kappelmann/tag-utilities'","pinned":true,"hidden":false,"mode":"ojs"},{"id":1040,"value":"import { addCSS } from '@kappelmann/general-utilities'","pinned":true,"hidden":false,"mode":"ojs"},{"id":23,"value":"import {responsive_katex} from '@jrus/misc'","pinned":false,"hidden":false,"mode":"ojs"}],"files":"$W31","stdlib":"1","titling":"auto"}