This syntax looks much more friendly than Lean! Could be really great. Complaint about their Live Code environment. I tried running the code on their front-page

This syntax looks much more friendly than Lean! Could be really great. Complaint about their Live Code environment. I tried running the code on their front-page in the live environment and it gave me `input.pf:2.9-2.12: undefined variable: Nat` which immediately makes me bounce off.