Comment by ctmnt

Yes, it isn’t performant. Lean isn’t a language for writing software, though you technically can; it’s a language for proving math.