search

leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
211 stars 50 forks source link

Clarity for Tactic chapter #61

Open winston-h-zhang opened 2 years ago

winston-h-zhang commented 2 years ago

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.