expression for undeclared declaration

Stream: general

[Kenny Lau]

#check `[rw foo]
/-
has_bind.seq (tactic.save_info {line := 102, column := 9})
  (tactic.step
     (tactic.interactive.rw
        {rules := [{pos := {line := 102, column := 12}, symm := ff, rule := ``(foo)}], end_pos := none pos}
        (interactive.loc.ns [none]))) :
  tactic unit
-/

#check ``(foo) -- unknown identifier 'foo'

[Kenny Lau]

why can I have ``(foo) inside rewrite but not by itself?

[Kenny Lau]

and what exactly does it do? I tried pp.all but it's still ``(foo)

[Keeley Hoek]

You could have ``(foo) directly, but lean doesn't let you on purpose

[Keeley Hoek]

Someone just wrote code which checks this

[Keeley Hoek]

To catch mistakes

[Keeley Hoek]

And it is convenient when, while you're writing your tactic, to write ``(foo) and mean the foo which is currently in-scope, so lean secretly does the replacement foo -> my.namspace.foo

[Keeley Hoek]

See:

lemma foo: unit := ()

run_cmd (do tactic.trace ((@expr.const ff `foo [])).to_raw_fmt)
run_cmd (do tactic.trace ``(foo).to_raw_fmt)

[Keeley Hoek]

They print the same

[Keeley Hoek]

Without the to_raw_fmts they print differently, but just because of secret macros wrapped around the latter (is my understanding)

[Mario Carneiro]

The actual equivalent is ```(foo)

[Mario Carneiro]

to do the same as `[rw foo] would be something like to_expr ```(foo) >>= \lam h, rewrite_goal h