One thing I don’t understand is the table at the end. It says Rust requires 30 lines of code for a type state pattern, and I’m sure that Rust will be more verbo

One thing I don’t understand is the table at the end. It says Rust requires 30 lines of code for a type state pattern, and I’m sure that Rust will be more verbose than Lean here, but wouldn’t all the typing shown in the article count as lines for Lean? I don’t see how it’s 0.