Pattern synonyms

[ice1000]

trafficstars

We could start from 'pattern definitions':

\def addN (a, b : Nat) : Nat
 | zero, a => a
 | a, zero => a
 | suc a, b => suc (addN a b)
 | a, suc b => suc (addN a b)

\pat one : Nat => suc zero
\pat suc-suc-a (a : Nat) => addN (suc (suc zero)) a

\def a-2 (a : Nat) : Nat
 | suc-suc-a a => a
 | one => one
 | zero => zero

Note that I want to use \pat definitions as both patterns and functions.

Originally posted by @ice1000 in https://github.com/ice1000/aya-prover/issues/190#issuecomment-809092666

[ice1000]

suc-suc-a should be evaluated to suc (suc a) and it corresponds to the pattern of the same form.

[ice1000]

\pat fail (a, b : Nat) => addN b a

Stuck application should fail to be a pattern object, so the above code should fail.

[re-xyr]

Can we write \impossible in pattern functions? Will it be able to be used as an ordinary function then?

[ice1000]

Can we write \impossible in pattern functions? Will it be able to be used as an ordinary function then?

Interesting question! I think we don't have to. Reason: if you want to synonym a single \impossible, that just doesn't make sense -- it's not very long and doesn't need to be aliased. If you want to do x (y z \impossible) w, you can have a synonym parameterized by the \impossible part, and use \impossible in the patterns. With this workaround provided I'd say it's unnecessary to do so.