## Stream: general

### Topic: eq.lhs and eq.rhs

#### Johan Commelin (Jul 09 2019 at 07:20):

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 (Jul 09 2019 at 07:20):

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

Last updated: May 16 2021 at 20:13 UTC