Ur Ya'arOK folks, let's learn #Lean!
This Number game is exactly what we did in #Logic courses when teaching Hilbert style proof systems, only with different terminology.
Lean's "Tactics" seems to be roughly the same as deduction rules.
Lean's "Tactics" seems to be roughly the same as deduction rules.
Andrej Bauer@yaarur It's more like natural deduction, actually, and the tactics are really little programs that apply one or more deduction rules, sometimes hundreds or thousands.