Reid Barton

Toy example: ```lean import tactic.ext @[ext] structure foo (α : Type*) := (a : α) (b : unit) #check @foo.ext ``` The generated lemma has type `foo.ext : ∀ {α...