Reducing match expressions in expression

Stream: metaprogramming / tactics

[Leni Aniva]

If I have an expression of the form

(match x.succ, n.succ with
    | a, Nat.zero => a
    | a, b.succ => (a.add b).succ) =
    (x.add n.succ).succ

Is there a function that can reduce this expression by evaluating the match? I tried Meta.whnf and Core.betaReduce and they could not change the expression.

[Aaron Liu]

it's already in whnf so that won't do anything

[Leni Aniva]

Aaron Liu said:

it's already in whnf so that won't do anything

Is there anything else that can perform the reduction? I also tried to programatically delta-expand matchers and beta reduce, and the furthest I could get was

(Nat.casesOn n.succ x.succ fun n => (x.succ.add n).succ) = (x.add n.succ).succ

which still has a recursor, while the match above could be reduced to (x.succ.add n).succ

[Robin Arnez]

lhs then whnf?

[Leni Aniva]

Robin Arnez said:

lhs then whnf?

seems like this is the best way to do it