Modules -- observers
int empty(list* lst) { return !lst || lst->tag == NIL; } element head(list* l) {require( ! empty(l) ); return l->e; } list* tail(list* l) {
head require( ! empty(l) ); return l->next; } bool equal(list* l, list* m) {
tail switch( l->tag) { case NIL: return empty(m); case CONS: return !empty(m) && head(l) == head(m) && tail(l) == tail(m); } }
equal