Testing has_repr

Stream: metaprogramming / tactics

[Eric Wieser]

In #8170, I suggested writing a test for a has_repr instance. Ideally the test would just be #eval ... and the test runner would just check the output, but it seems that unlike the core lean tests, the mathlib tests don't work that way.

So how can I run eval from within a tactic block? My naive attempt is something like

run_cmd
do x ← to_expr ``(↑[2, 1, 4, 3] : cycle ℕ),
   let s := "{repr x}",
   if s = "c[2, 1, 4, 3]" then
     pure ()
   else
     failure

but I can't work out how to actually call repr.

[Eric Wieser]

Ah, found docs#tactic.eval_expr. Is there a more idiomatic way than this?

run_cmd
do x ← to_expr ``(repr (↑[2, 1, 4, 3] : cycle ℕ)),
   "c[1, 4, 3, 2]" ← eval_expr string x,
   pure ()

[Chris Hughes]

Doesn't this have the same effect? I don't understand exactly what you're trying to do.

run_cmd
do
   "c[1, 4, 3, 2]" ← pure (repr (↑[2, 1, 4, 3] : cycle ℕ)),
   pure ()

I guess in your application you want x to be an arbitrary expression? If so, then I don't know a better way.

[Eric Wieser]

You're right, I think I forgot that meta code runs in the VM anyway

[Eric Wieser]

run_cmd guard ("c[1, 4, 3, 2]" = repr (↑[2, 1, 4, 3] : cycle ℕ))

seems like it's probably the spelling I want