← Back to context Comment by solomonb 3 days ago This is why I prefer Agda, where everything comes down to pattern matching. 2 comments solomonb Reply agnishom 3 days ago 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" solomonb 3 days ago 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.
agnishom 3 days ago 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" solomonb 3 days ago 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.
solomonb 3 days ago 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.
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.