feat: add Rubik's cube

leanprover-community · Feb 2, 2023 · aa4bec8 · aa4bec8
1 parent 87dcb60
commit aa4bec8
Show file tree

Hide file tree

Showing 5 changed files with 1,259 additions and 15 deletions.
diff --git a/WidgetKit/Demos/Rubiks.lean b/WidgetKit/Demos/Rubiks.lean
@@ -0,0 +1,16 @@
+import WidgetKit.Component.HtmlDisplay
+
+open Lean WidgetKit
+open scoped WidgetKit.Jsx
+
+structure RubiksProps where
+  seq : Array String := #[]
+  deriving ToJson, FromJson, Inhabited
+
+@[widget_module]
+def Rubiks : Component RubiksProps where
+  javascript := include_str ".." / ".." / "build" / "js" / "rubiks.js"
+
+def eg := #["L", "L", "D⁻¹", "U⁻¹", "L", "D", "D", "L", "U⁻¹", "R", "D", "F", "F", "D"]
+
+#html <Rubiks seq={eg} />