Our server collects metadata (such as IP address, browser, operating system) and the data that the user enters into the editor. The data is used to compute the Lean output and display it to the user. The information will be stored as long as the user stays on our website and will be deleted immediately afterwards. We keep logs to improve our software, but the contained data is anonymized.
We don't use cookies but you can choose to save the settings in the browser store by activating the option in the settings.
To see the actual Lean version implied by the toolchain above, the following can be pasted into the editor:
#eval Lean.versionString
These settings are stored in the URL as they change the project's setup
Lean Version: Lean-MLIR
Lead character to trigger unicode input mode
Wrap code
Accept Suggestion on Enter
Theme: visual studio lightvisual studio darkhigh contrastcobalt
Mobile layout (vertical)
Compress code in URL
Editor settings and User settings are not preserved unless you opt-in to save them.
Save my settings (in the browser store)
Copy paste a zulip message here to extract code-blocks. (mobile: "copy to clipboard", web: "view message source")
You are in the plain text editorGo back to the Monaco Editor (click ) for the infoview to update!