here to learn
md`# "Natural number game"
Prototyping https://github.com/ImperialCollegeLondon/natural_number_game in Observable
`
import {leanEditor, leanEditorFrom, InfoView, LeanFile, leanControl, leanHL, parseLeanMsgs}
with {transportOpts}
from '@bryangingechen/hello-lean-prover'
// import {leanEditor, leanEditorFrom, InfoView, LeanFile, leanControl, leanHL, parseLeanMsgs}
// from '@bryangingechen/lean-websocketd'
world1Array = fetch('https://raw.githubusercontent.com/bryangingechen/natural_number_game/observable/src/my_solutions/world1_addition.lean').then(res => res.text()).then(s => s.split('\n---\n'))
world1Array[9]
world1Md = world1Array
.filter(s => s.startsWith('/-')) // select block comments
.map(s => {
const arr = s
.slice(2,-2) // remove /- and -/
.split('```');
const str = []; // ordinary markdown
for (let j=0; j<arr.length; j+=2) {
str.push(arr[j].trim());
}
const highlighted = []; // highlighted Lean source blocks
for (let j=1; j<arr.length; j+=2) {
highlighted.push(leanHL`${arr[j]}`);
}
return md(str, ...highlighted);
})
world1Lean = world1Array.filter(s => !s.startsWith('/-')) // everything else
world1Editor = leanEditorFrom({
docArray: world1Lean,
fileName: 'world1.lean',
height: 150,
}, invalidation)
world1Editor(0, invalidation, {height:100, readOnly: true})
world1Md[0]
world1Editor(1, invalidation)
world1Md[1]
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.
