eq.lhs and eq.rhs

Stream: general

[Johan Commelin]

Do people think this would be useful?

namespace eq
variables {α : Type*} {a b : α}

@[reducible] def lhs (h : a = b) : α := a

@[reducible] def rhs (h : a = b) : α := b

end eq

[Johan Commelin]

I've been using it to refer to long expressions in my tactic state.