Module Smyth.Sugar

val nat : Lang.exp -> int option

nat deconstructs the expression S (... S (Z ()) ...) into the integer n, where the S constructor is nested n times (i.e., Sn(Z ())).

val listt : Lang.exp -> (Lang.exp list * Lang.typ list) option

listt deconstructs the expression

Cons<taus> (e0, ... Cons<taus> (eN, Nil<taus>))

into the pair ([e0, ..., eN], taus).