DecimalLiterals (N): trait % A built-in trait schema given here % for documentation only introduces 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 %, ... : -> N succ: N -> N asserts equations 1 == succ(0); 2 == succ(1); 3 == succ(2); % ... as far as needed for any literals % of sort N appearing in the including trait[Table of Contents] [Index]