one-symbol "by assumption"

Stream: general

[Johan Commelin]

How would people feel about a 1-symbol version of by assumption? I now often have hypotheses with unenlightening names H1 ... H5, and these labels are all over the place in my proofs. But they don't really convey any information. I could use the french quotes to tell Lean the type, and it will start looking for a fitting assumption. But often I find that pretty verbose. Because usually, it's just an annoying proof obligation that we want to get rid of. How about !, or maybe the unicode …?

[Patrick Massot]

I can see you are tempted by the SSReflect cabalistic road...

[Patrick Massot]

I think this is part of what SSReflect // does

[Johan Commelin]

I can see you are tempted by the SSReflect cabalistic road...

I know of a guild that doesn't write anything when it comes to these proof obligations... it's completely transparent to them.

[Patrick Massot]

Great, let's have a transparent unicode character! Let's take the one we use in real world math papers.

[Andrew Ashworth]

I am not a huge fan of this being a mathlib standard. Maybe in your personal code, you can make your own meta def, and then when you PR, you can search and replace?

[Andrew Ashworth]

Or a VSCode tab-completion when you start writing by a

[Reid Barton]

If H3 is uninformative, wouldn't ! be even more uninformative?

[Reid Barton]

At least with H3 the IDE will tell you the type

[Johan Commelin]

After a bit more thought, maybe the most most user-friendly version (both for reading and writing) would be to have a VScode keyboard shortcut that looks at the type of the current _ and replaces it with \f< the_type \f>. It really is a pity that we can't invoke hole commands on bare _. Otherwise a hole command would be perfect.

[Mario Carneiro]

a simple available compromise is \f<_\f>

[Mario Carneiro]

I would also be happy if \f<\f> worked but I think that requires a bit more parsing magic

[Reid Barton]

After a bit more thought, maybe the most most user-friendly version (both for reading and writing) would be to have a VScode keyboard shortcut that looks at the type of the current _ and replaces it with \f< the_type \f>. It really is a pity that we can't invoke hole commands on bare _. Otherwise a hole command would be perfect.

I would agree with this. I imagine the VSCode extension could just replace the _ with a {! _ !} and then invoke the hole command--we shouldn't be limited by Lean here.

[Mario Carneiro]

I would prefer it just replace the hole with a reference to the actual hypothesis

[Johan Commelin]

Why not the \f< the_type \f> version? It is less "Lean-explicit" but it is a whole lot more "math-explicit".