Comment by solomonb 6 months ago This is why I prefer Agda, where everything comes down to pattern matching. 2 comments solomonb Reply agnishom 6 months 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 6 months 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 6 months 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 6 months 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 6 months 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.