elab_rules

Stream: lean4

[Scott Morrison]

I am struggling with the simplest things using elab_rules, and unfortunately there seem to be few examples to work off.

Can someone explain why

import Lean.Elab.Tactic.Basic

open Lean.Parser.Tactic

syntax (name := ex) "ex" (ppSpace location)? : tactic

elab_rules : tactic | `(tactic| ex $loc:location) => do
  trace[Meta.debug] loc

set_option trace.Meta.debug true

example (h : false) : 1 = 1 := by
  ex h
  sorry

says "unknown tactic" after the ex h? How should I write an elab_rules statement to implement ex h?

[Mario Carneiro]

shouldn't there be an at in there somewhere?

[Mario Carneiro]

iirc location includes the at

[Mario Carneiro]

using ex at h seems to work