Quotient-like match pattern

Stream: metaprogramming / tactics

[Robert Maxton]

Suppose I have a (non-canonical, not-an-inductive-constructor) function that makes values of some type τ:

@[match_pattern]
def myMk  (a : α) (b : β) : τ := ...

And a proof/def that considering only elements that can be made by myMk is sufficient to prove/generate data for everything in τ:

@[elab_as_elim]
def myRecOn {C : τ → Sort u} (t : τ) (mkMk : ∀ a b, C (myMk a b)) : C t := ...

What's the cleanest way to turn myMk into something that can be matched against, used in destructuring assignment, and so on? I vaguely believe this is possible because there are notes to that effect in e.g. Finset.sum's documentation, but I'm not entirely sure.

[Robert Maxton]

I've started with the attributes already included above, but in my specific use case trying to do fun (myMk a b) => ... with just the above results in the compiler complaining invalid patterns, `a` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching. Which doesn't exactly surprise me -- that's essentially why I had to write myRecOn, after all -- but I don't really know where to go from here.

[Aaron Liu]

@[match_pattern] is probably not going to work for anything complicated, but if myMk is simple enough, then you could do that.

[Robert Maxton]

It's not terribly complicated, but it has a Quot.mk in it, so depending on where I put the attribute, either the pattern isn't recognized when I try to use it, or the parameter ends up in an inaccessible pattern and can't be used.