Skip to content
This repository has been archived by the owner on Oct 19, 2023. It is now read-only.

Latest commit

 

History

History
20 lines (13 loc) · 801 Bytes

README.md

File metadata and controls

20 lines (13 loc) · 801 Bytes
Raw

A screenshot showing the Rubik's cube in operation.

Rubik's cube visualiser

This project is a demo of the user widgets system. It displays a Rubik's cube in the Lean infoview. Inspired by the rubiks-cube-group from Kendal Frey.

The purpose of this example is to show how to build widgets using TypeScript and bundled NPM libraries.

Running

In order to build you need Lean 4 and Node.js. You also need to be using VSCode (or a Gitpod). First run

lake build rubiksJs

and then open Rubiks.lean in the editor. Put your cursor over the #widget command and you should see an interactive Rubik's cube in the infoview.