Clarity for Tactic chapter

[winston-h-zhang]

Note: I'm raising this issue mostly for bookkeeping purposes -- if someone wants to address them please feel free to! (Anyways, I'm probably going to come back and add these in myself sometime in the future)

1. Make clear goalDecl.type and Lean.Meta.getMVarType goal are the same -- possible confusion from two options.

2. Similarly, what is the difference between Lean.Meta.inferType declExpr and decl.type?

3. Also this

syntax "custom_tactic" : tactic
macro_rules
| `(tactic| custom_tactic) => `(tactic| rfl)
macro_rules
| `(tactic| custom_tactic) => `(tactic| apply And.intro <;> custom_tactic)

has and-then failure behavior; if the first rule fails then the second is applied. However, this

syntax "custom_tactic" : tactic
macro_rules
| `(tactic| custom_tactic) => `(tactic| rfl)
| `(tactic| custom_tactic) => `(tactic| apply And.intro <;> custom_tactic)

does not work. This could be pointed out in the text.