Indexing hypothesis observations

Stream: lean4

[Tom]

I am working through some code that tries to use for h: ... and if h: ... etc. I noticed a few minor things which could be QoL improvements for code that currently exists in the Lean4 codebase.

1. unless doesn't seem to support the unless h : ... syntax
2. It may be useful to be able to associate the hypothesis with a subexpression rather than with the full expression. eg. in Lean/Util/Diff.lean on line 174 the code says

 while i < original.size && original[i]! != d do

if would be convenient to be able to say

while (h : i < original.size) && original[i] != d do -- notice the missing `!`

I've noticed this before with other compound expressions e.g. in if statements, where I e.g. wish to write

if cond1 && cond2 then ...
else ...

but if I want to use a hypothesis, AFAICS, I have to switch to if h: cond1 ∧ cond2 then

[Damiano Testa]

The second point requires knowing a lot about truth tables: if you had and or what should it do?

[Tom]

That's a great observation! I can see how that would get complicated with short-circuiting operators.

[Daniel Weber]

You can use ∃ h : i < original.size, original[i] != d, although I'm not sure if it short-circuits correctly