I started one such tutorial: https://agentultra.github.io/lean-for-hackers/ https://agentultra.github.io/lean-for-hackers/ I haven't gotten to the dependent ty

I started one such tutorial: https://agentultra.github.io/lean-for-hackers/ https://agentultra.github.io/lean-for-hackers/ I haven't gotten to the dependent types part yet. I find most tutorials one these languages start with the theory up front. I'm taking a more pragmatic tack by demonstrating the language through examples building on familiar learning patterns of writing simple programs first and working your way up. It is a neat way to write programs!