First-class patterns, or, patterns-as-objects

[ice1000]

As title. I think this is an interesting idea, and I will discuss this with y'all in the next Walpurgis night.

[ice1000]

\struct Monoid
 | A : \Set
 | \pattern identity : A
 | \infix + (a b : A) : A \with {
  | identity, a => a
  | a, identity => a
 }

[ice1000]

https://github.com/JetBrains/arend-lib/blob/7d2f65b380ed9787963a0c7f9339ec6d8e17d1cb/src/Homotopy/Torus.ard

[ice1000]

I want pattern synonym to be a first-class citizen in the language. We need to have a type for them.

[ice1000]

\struct Monoid
 | A : \Set
 | \pattern identity (x : A) : A
 | \infix + (a b : A) : A \with {
  | identity x, a => a
  | a, identity x => a
 }

[ice1000]

We could start from 'pattern definitions':

\pat one : Nat => suc zero
\pat suc-suc-a (a : Nat) => suc (suc 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.

[ice1000]

Deprecated