Simplest possible tactic implementation

Stream: Is there code for X?

[Ryan Ziegler]

Hi, I'm new to Lean and have been trying to find a minimal working example of a tactic that doesn't depend on any libraries etc. Something like taking h1 : p and h2 : p -> q and getting q (I know this is easy to do without a tactic, but I'm in search of a minimal example). Any pointers would be great!

[Richard Copley]

There are some good ones in Std.Tactic.Basic.

macro "exfalso" : tactic => `(tactic| apply False.elim)

example (P Q : Prop) (hp : P) (hnp : ¬P) : Q := by
  exfalso
  exact hnp hp

[Ryan Ziegler]

Perfect, thanks!