type Integer { Integer succ(); Integer plus(Integer y); Integer times(Integer y); } class Zero() : Integer impl Integer { Integer plus(Integer y) { return y; } Integer times(Integer y) { return (this : Integer); } Integer succ() { return new Positive : Integer(pred = (this : Integer)); } export Integer : plus, times, succ; } class Positive() : Integer impl Integer { init Integer pred; Integer plus(Integer y) { return pred.plus(y.succ()); } Integer times(Integer y) { return pred.times(y).plus(y); } Integer succ() { return new Positive : Integer(pred = (this : Integer)); } export Integer : plus, times, succ; } Integer main() { Integer zero = new Zero : Integer(); Integer one = new Positive : Integer(pred = zero); Integer two = new Positive : Integer(pred = one); Integer three = one.plus(two); Integer four = two.times(two); Integer five = four.plus(one); Integer six = two.plus(four); Integer seven = one.plus(two.plus(four)); Integer eight = two.times(two); Integer nine = three.times(three); return nine.plus(one); }