The avatar for @kappelmann
Kevin Kappelmann
PhD student interested in interactive theorem proving.
Published
Lean Utilities
Edited
Sep 12, 2019
Importers
1 star
Lean Utilities
Lean Code ExplainerLean Step Editor Steps CreatorLean Editor With Local StorageLean Quiz
Lean Utility Functions
Lean Proof ViewLean Configuration
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
defTemplate = (kind) => (name) => inlinemd`**${kind}**${name ? ` (${name})` : ''}<strong>.</strong>`
Insert cell
thm = defTemplate('Theorem')
Insert cell
lem = defTemplate('Lemma')
Insert cell
exmpl = defTemplate('Example')
Insert cell
prop = defTemplate('Proposition')
Insert cell
cor = defTemplate('Corollary')
Insert cell
def = defTemplate('Definition')
Insert cell
proof = el => inlinemd`*Proof ${el}.*`
Insert cell
floatRight = el => html`<span style="float: right">${el}</span>`
Insert cell
qed = () => floatRight(tex`\square`)
Insert cell
justification = el => floatRight(html`(${el})`)
Insert cell
details = ({ header, text, className = '' }) => {
addCSS(leanUtilityFunctionsStyle);
return html`
<details class="${className}">
<summary>${header}</summary>${text}
</details>`;
}
Insert cell
question = (question, answer) => details({
header: html`❓ ${question}`,
text: answer,
className: CSS_CLASSES.QUESTION
})
Insert cell
warning = (warning, explanation) => details({
header: html`⚠️ ${warning}`,
text: explanation,
className: CSS_CLASSES.WARNING
})
Insert cell
info = (info, explanation) =>
details({
header: html`❗ ${info}`,
text: explanation,
className: CSS_CLASSES.INFORMATION
})
Insert cell
function examplesTable({examples, editor, invalidation, offset = 0}) {
if (!(invalidation instanceof Promise))
throw new Error(`examplesTable: invalidation be a promise (currently: ${invalidation})`);
return html`
<table style="min-width: 100%">
<tr>
<th>Example</th>
<th>Lean Proof</th>
</tr>
${examples.map((el, i) => html`
<tr>
<td>${responsive_katex(invalidation, tex`${el}`)}</td>
<td>${editor(i + offset, invalidation)}</td>
</tr>`
)}
</table>`
}
Insert cell
Insert cell
Insert cell
leanUtilityFunctionsStyle = html`<style id="lean-utility-functions">

details {
border: dotted 1px black;
}

details > * {
padding: ${SPACING_BASELINE};
}

details summary {
cursor: pointer;
}

details[open] summary {
background: ${COLOURS.ACTIVE};
}

details:not([open]) summary:hover {
background: ${COLOURS.HOVER};
}

</style>`
Insert cell
Insert cell
import {
LEAN_LIBS,
COLOURS,
INTERNAL_CSS,
leanEditorConfig,
CSS_CLASSES as BASE_CSS_CLASSES,
SPACING_BASELINE
} from '@kappelmann/lean-configuration'
Insert cell
import {leanEditor, leanEditorFrom, leanHL, InfoView}
with {leanLibName, INTERNAL_CSS, leanEditorConfig as config}
from '@bryangingechen/hello-lean-prover'
Insert cell
import {explanationFooter}
with {leanLibName, leanEditor, stepEditor}
from '@kappelmann/lean-code-explainer'
Insert cell
import {leanEditorWithStorage}
with {leanLibName, leanEditor}
from '@kappelmann/lean-editor-with-local-storage'
Insert cell
import {proofView, proofCreatorFooter, observeProofObject, convertMathsEntryRaw}
with {leanLibName, leanEditor, leanEditorFrom, leanHL, InfoView}
from '@kappelmann/lean-proof-view'
Insert cell
import {stepEditor}
with {leanLibName, leanEditor}
from '@bryangingechen/stepping-through-currying-in-lean'
Insert cell
import {stepsCreatorFooter, observeStepsObject, convertDescRaw}
with {leanLibName, leanEditor, explanationFooter, stepEditor}
from '@kappelmann/lean-step-editor-steps-creator'
Insert cell
import {quizMarks}
with {leanLibName, leanEditor, leanHL}
from '@kappelmann/lean-quiz'
Insert cell
import { inlinemd, mdtex } from '@kappelmann/tag-utilities'
Insert cell
import { addCSS } from '@kappelmann/general-utilities'
Insert cell
Insert cell

Purpose-built for displays of data

Observable is your go-to platform for exploring data and creating expressive data visualizations. Use reactive JavaScript notebooks for prototyping and a collaborative canvas for visual data exploration and dashboard creation.
Learn more