The avatar for @bryangingechen
Bryan Gin-ge Chen
here to learn
Published
Edited
Jan 26, 2021
2 forks
Importers
37 stars
Ingredients
mathjax-editing.jshighlightjs for LeanConnect Observable notebooks to Lean on your computer with websocketdCindyJS import exampleTOCD3 ScatterplotD3 Log-Scaled HistogramLean exercise boxStepping through currying in Lean
Hello, Lean prover!
MathJaxPolygon inputHello, cubic-spline!Brython in observableHello, Bokeh.js!commentOnLabeling connected componentsDrag to re-arrange (vertical edition)Dynamic import polyfillHello, R on OpenCPU!Hello, noUiSlider!Hello, CindyJS!Hello, chess!Grid inputs
Also listed in…
Lean
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
test0.msgs
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
setLeanURL = resolveLeanURL('init/data/set')
Insert cell
Insert cell
setLean = fetch(setLeanURL).then(res => res.text())
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
// If the server is alive and the results array is empty, try rerunning this cell
Promises.delay(100, null).then(() => server.search('and'))
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
testFile = new LeanFile({
fileName: 'testLeanFile.lean',
value: `#eval 8+8
#eval [1, 2, 4+4]
#eval g`,
}, invalidation).sync()
Insert cell
Insert cell
// requests info at line 1, column 7
// (recall that the Lean server works with line numbers that start from 1 and columns that start from 0)
testFile.info(1,7)
Insert cell
Insert cell
Insert cell
Insert cell
parseLeanMsgs(testFile.msgs.filter(({caption}) => caption === 'eval result'))
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
viewof minimalEditor = leanEditor({}, invalidation)
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
minimalEditor
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
setLeanArray = setLean.split('\n\n')
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
setLeanEditor = leanEditorFrom({
docArray: setLeanArray,
fileName: 'set.lean',
readOnly: true,
height: '60px',
})
Insert cell
Insert cell
setLeanEditor(10, invalidation)
Insert cell
Insert cell
viewof set2a = setLeanEditor(2, invalidation)
Insert cell
viewof set2b = setLeanEditor(2, invalidation)
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell

One platform to build and deploy the best data apps

Experiment and prototype by building visualizations in live JavaScript notebooks. Collaborate with your team and decide which concepts to build out.
Use Observable Framework to build data apps locally. Use data loaders to build in any language or library, including Python, SQL, and R.
Seamlessly deploy to Observable. Test before you ship, use automatic deploy-on-commit, and ensure your projects are always up-to-date.
Learn more