The avatar for @bryangingechen
Bryan Gin-ge Chen
here to learn
Published
Edited
Jan 29, 2021
1 fork
14 stars
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
parseLeanMsgs(fEval.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
import {leanEditor, leanEditorFrom, leanControl, leanHL, parseLeanMsgs} with {transportOpts} from '@bryangingechen/hello-lean-prover'
Insert cell
Insert cell
// leanControl
Insert cell
Insert cell
transportOpts = {
const prefix = 'https://bryangingechen.github.io/lean/lean-web-editor/';
return {
javascript: prefix+'lean_js_js.js', // Lean server compiled to asm.js with Emscripten (won't be downloaded or used unless your browser doesn't support WASM)
webassemblyJs: prefix+'lean_js_wasm.js', // JS code generated by Emscripten to call...
webassemblyWasm: prefix+'lean_js_wasm.wasm', // Lean server compiled to WASM by Emscripten
libraryZip: prefix+'libfib.zip', // bundle of .olean files
};
}
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