Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Allowing multiple targets in `case`


view this post on Zulip Eric Wieser (Dec 18 2020 at 11:01):

Is this a good idea? I can't post a mwe because I rely on private meta defs visible only within core lean, but a PR is at https://github.com/leanprover-community/lean/pull/508.

This enables syntax like:

example (α β : Type*) (i j : α  β) :  :=
begin
  with_cases {cases hi : i; cases hj : j},
  case [sum.inl sum.inl : i j, sum.inr sum.inr : i j] {
    exact 1,
    exact 1,
  },
  case [sum.inl sum.inr : i j, sum.inr sum.inl : i j] {
    exact 2,
    exact 2,
  },
end

Last updated: May 09 2021 at 22:13 UTC