lean for language specs

Stream: lean4

[Xiyu Zhai]

Hi, everyone. I'm writing my own programming language (https://github.com/ancient-software/husky) and using Lean4 to write language specs and automatically generate tests for Rust. Combined with Rust, I believe this can eliminate both memory and logic bugs.

I would like to include Lean4 error checking in CI.

My question: what is the lake equivalence of cargo check?

lake seems to be able to compile even if syntactic errors exist.

[Notification Bot]

Xiyu Zhai has marked this topic as resolved.

[Notification Bot]

Xiyu Zhai has marked this topic as unresolved.