alt Hacker NewsYou can absolutely use pattern matching in Lean instead of tactics, if you prefer to write the proof that is closer to "what is going on under the hood"
You can absolutely use pattern matching in Lean instead of tactics, if you prefer to write the proof that is closer to "what is going on under the hood"
yeah i didn't mean to imply you cannot do that, but tactics seem to be highly encouraged.
I'm actually a big fan of Lean, I just like it more as a programming language for writing programs with dependent types then as a proof checker.