The avatar for @bryangingechen
Bryan Gin-ge Chen
here to learn
Published
Edited
Jan 29, 2021
1 fork
14 stars
Lean
Hello, Lean prover!
Fibonacci formalized 1: some sums
Fibonacci formalized 2: bees and carsConnect Observable notebooks to Lean on your computer with websocketdStepping through currying in LeanLean exercise boxStandalone Lean editorGitHub Lean doc previewhighlightjs for LeanGitHub Lean file viewer
Also listed in…
Meals
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

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