multiple reverts delete hypotheses

Stream: lean4

[Arien Malec]

def Thing (α : Type u) : Type u := sorry

theorem foo {R : α → β → Prop} (C : Thing α → Thing β → Prop)
    (H : ∀ {ca cb}, C ca cb → ca = cb) (Hc : C ca cb)
    (ha : True) : ca = cb := by
    revert ca cb; sorry

For this example, the hypothesis Hc is in the tactic state before the revert, and gone after

[Arien Malec]

I don't know if the Thing shenanigans are strictly necessary.

[Arien Malec]

De-Thinged

theorem foo {R : α → β → Prop} {a a' : α} {b b' : β} (C :  α →  β → Prop)
    (H : ∀ {ca cb}, C ca cb → a = a') (Hc : C ca cb)
    (ha : True) : b = b' := by
    revert ca cb; sorry

Same behavior.

[Arien Malec]

Also revert ca; revert cb; sorry has the same issues.

[Gabriel Ebner]

If you look closely Hc has been reverted as well.

[Gabriel Ebner]

You can't keep Hc after reverting: it's type depends on ca and cb. So it either needs to be deleted or reverted.

[Arien Malec]

ahh... I see it. and since it's dependent, it has to come after the \foralls. Thanks!