idris-1.3.3: test/records002/expected.out

42, 20
10, 42