44:["$","title",null,{"children":"Lean Utility Functions | Kevin Kappelmann | Observable"}] 4c:[] 48:{"id":"7c8361448d3efe7c","slug":"lean-utility-functions","title":"Lean Utility Functions","thumbnail":"62843da1d0bd4ca2543c30a9e33506776844641057faace05837ada0791ceb79","access_level":"public","create_time":"$D2019-08-18T15:37:34.589Z","update_time":"$D2019-09-13T11:42:45.724Z","view_time":null,"first_public_time":"$D2019-08-18T15:37:37.934Z","has_unpublished_edits":null,"fork":true,"stars":1,"starred":false,"owner":{"type":"team","id":"0618be768f4ffcb8","login":"kappelmann","name":"Kevin Kappelmann","avatar_url":"https://avatars-next.observableusercontent.com/e75b66afb4516626d12ccfaaba6708c7bfa155bfb022eb536d985b746062aafc","tier":"starter_2024","bio":"PhD student interested in interactive theorem proving.","followed_by_you":false,"follows_you":false},"version":1072,"publish_version":1072,"role":null,"authored":false,"authors":[{"type":"individual","id":"ead75660855283dc","login":"kappelmann","name":"Kevin Kappelmann","avatar_url":"https://avatars-next.observableusercontent.com/e75b66afb4516626d12ccfaaba6708c7bfa155bfb022eb536d985b746062aafc","tier":null,"bio":"PhD student interested in interactive theorem proving.","followed_by_you":false,"follows_you":false}],"members":[{"type":"individual","id":"ead75660855283dc","login":"kappelmann","name":"Kevin Kappelmann","avatar_url":"https://avatars-next.observableusercontent.com/e75b66afb4516626d12ccfaaba6708c7bfa155bfb022eb536d985b746062aafc","tier":null,"role":"editor"}],"comments":[],"custom_thumbnail":false,"trashed":false,"lapsed":null,"subscribed":null,"forks":1,"collection":{"id":"6bf4517a11601e83","slug":"lean-utilities","title":"Lean Utilities","owner":{"id":"0618be768f4ffcb8","login":"kappelmann","name":"Kevin Kappelmann"}},"type":"notebook","body":{"titling":"auto","title":"Lean Utility Functions","cells":[{"id":0,"value":"md`# Lean Utility Functions`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"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","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":50,"value":"md`## Variables`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"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","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":643,"value":"leanLibName = LEAN_LIBS.CORE","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":47,"value":"md`## Functions`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":800,"value":"defTemplate = (kind) => (name) => inlinemd`**${kind}**${name ? ` (${name})` : ''}.`","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":383,"value":"thm = defTemplate('Theorem')","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":386,"value":"lem = defTemplate('Lemma')","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":389,"value":"exmpl = defTemplate('Example')","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":814,"value":"prop = defTemplate('Proposition')","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":820,"value":"cor = defTemplate('Corollary')","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":816,"value":"def = defTemplate('Definition')","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":392,"value":"proof = el => inlinemd`*Proof ${el}.*`","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1044,"value":"floatRight = el => html`${el}`","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":395,"value":"qed = () => floatRight(tex`\\square`)","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1054,"value":"justification = el => floatRight(html`(${el})`)","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":501,"value":"details = ({ header, text, className = '' }) => {\n addCSS(leanUtilityFunctionsStyle);\n return html`\n

${header}

${text}\n

`;\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"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","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"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","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"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","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"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","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":463,"value":"md`## Styling`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"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","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":481,"value":"leanUtilityFunctionsStyle = html``","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":26,"value":"md`## Imports`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"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","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"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","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":418,"value":"import {explanationFooter}\nwith {leanLibName, leanEditor, stepEditor}\nfrom '@kappelmann/lean-code-explainer'","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":413,"value":"import {leanEditorWithStorage}\nwith {leanLibName, leanEditor}\nfrom '@kappelmann/lean-editor-with-local-storage'","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"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","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":71,"value":"import {stepEditor}\nwith {leanLibName, leanEditor}\nfrom '@bryangingechen/stepping-through-currying-in-lean'","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"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","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":709,"value":"import {quizMarks}\nwith {leanLibName, leanEditor, leanHL}\nfrom '@kappelmann/lean-quiz'","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1036,"value":"import { inlinemd, mdtex } from '@kappelmann/tag-utilities'","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1040,"value":"import { addCSS } from '@kappelmann/general-utilities'","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":23,"value":"import {responsive_katex} from '@jrus/misc'","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","tool":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"}],"files":"$W4c","stdlib":"1"}} 24:null