The avatar for @bryangingechen
Bryan Gin-ge Chen
here to learn
Published
Edited
Jan 26, 2021
2 forks
Importers
37 stars
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

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