Hackeython Working Group: ADT Observers

Shepard: Mattias

Motivation

Alexander @wadoon has recently introduced ADTs to KeY. That is great!

One little feature that has been left out is the constructor arguments should result in observer or destructor function symbols axiomatised with the respective taclets. Like:

\datatypes {
  MyList = MNil | MCons(any head, MyList tail);
}

will introduce two functions any head(MyList) and MyList tail(MyList) with the rewriting rules head(MCons(h, t)) = h and tail(MCons(h, t)) = t in taclet form.

There are a few technical details to be discussed on site.