leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

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 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll