Zulip Chat Archive

Stream: general

Topic: expression for undeclared declaration


view this post on Zulip Kenny Lau (May 16 2020 at 19:16):

#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'

view this post on Zulip Kenny Lau (May 16 2020 at 19:17):

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

view this post on Zulip Kenny Lau (May 16 2020 at 19:18):

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

view this post on Zulip Keeley Hoek (May 16 2020 at 19:24):

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

view this post on Zulip Keeley Hoek (May 16 2020 at 19:24):

Someone just wrote code which checks this

view this post on Zulip Keeley Hoek (May 16 2020 at 19:24):

To catch mistakes

view this post on Zulip Keeley Hoek (May 16 2020 at 19:25):

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

view this post on Zulip Keeley Hoek (May 16 2020 at 19:28):

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)

view this post on Zulip Keeley Hoek (May 16 2020 at 19:28):

They print the same

view this post on Zulip Keeley Hoek (May 16 2020 at 19:31):

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

view this post on Zulip Mario Carneiro (May 16 2020 at 20:07):

The actual equivalent is ```(foo)

view this post on Zulip Mario Carneiro (May 16 2020 at 20:07):

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


Last updated: May 13 2021 at 23:16 UTC