Should I use `note` invisibly

Stream: metaprogramming / tactics

[Chris Hughes]

If I'm writing a tactic and I have a large proof term that will be used multiple times in the final proof term, is there any point using note to avoid the same duplicate large proof term appearing multiple times in the final proof. The added hypotheses won't be used by the user only internally.

You obviously get exponential blow-up without doing this, but maybe it's okay. I think I remember expr has some efficient representation of proof terms that contain the same subterm lots of times.

[Simon Hudon]

It's a good idea to do it, still. It's easy to undo subtree sharing by careless traversal but with an assumption, you're protected. It's also easier to take advantage of sharing in Lean code with an assumption

[Chris Hughes]

Is there a name for this definition n ← mk_fresh_name, note n none pr? The lack of it made me think that it probably wasn't normal to do this all the time.

[Simon Hudon]

I think you want get_unused_name instead. mk_fresh_name is for declarations.

[Simon Hudon]

I think the most helpful function would be local_proof. It would be good to PR your own function that also generates names for you

[Rob Lewis]

Chris Hughes said:

Is there a name for this definition n ← mk_fresh_name, note n none pr? The lack of it made me think that it probably wasn't normal to do this all the time.

docs#tactic.note_anon

[Simon Hudon]

Nice!