"Are you using lean as a general purpose functional language and not really touching the theorem prover" Yeah why not, it's fun!!