lean4-samples

lean4-samples copied to clipboard

Rubiks Cube doesn't build for me (Lean4 dev novice here)

1

``` PS C:\Users\fruit\OneDrive\Desktop\Lean4Widgets> cd C:\Users\fruit\OneDrive\Desktop\Lean4Widgets\lean4-samples\RubiksCube PS C:\Users\fruit\OneDrive\Desktop\Lean4Widgets\lean4-samples\RubiksCube> dir Directory: C:\Users\fruit\OneDrive\Desktop\Lean4Widgets\lean4-samples\RubiksCube Mode LastWriteTime Length Name ---- ------------- ------ ---- d----- 9/3/2022 11:58 AM images d----- 9/3/2022 11:58 AM widget -a---- 9/3/2022...

enjoysmath

add quine example

1

mo271

Rubik's cube with Gitpod needs extra shell commands to build

1

I have the Chrome Gitpod extension installed, and when I click on the Gitpod button that appears on the page, it opens up a VSCode environment, showing the following messages...

crisperdue

Incorrect proof in NaturalNumbers

1

In level 4 of Advanced Multiplication World there is a proof of: ``` theorem mul_left_cancel (a b c : MyNat) (ha : a ≠ 0) : a * b =...

paulch42