Module Smyth.Sugar
val nat : Lang.exp -> int option
nat
deconstructs the expressionS (... S (Z ()) ...)
into the integern
, where theS
constructor is nestedn
times (i.e.,S
n
(Z ())
).
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., S
n
(Z ())
).