contracts-conformance.json (78227B)
1 { 2 "compilerBundleSha256": "9c61d59cd76036000691da6ff5e2e9f641cf5c614b424d7280e052cfcb716e75", 3 "hostSha256": "662fcf80231c070e4aa15dff1438aa1f5c99fb27a905f46a62efaff46c49f668", 4 "contractsSourceSha256": "8f69b32c50461edd5db536becb6faedd5ba33945bf774534592034350702600a", 5 "bindings": { 6 "matchResult": "base.matchResult", 7 "withContract": "base.withContract", 8 "err": "base.err", 9 "ok": "base.ok", 10 "check": "base.check", 11 "checkContract": "base.checkContract", 12 "contractOk": "base.contractOk", 13 "contractErr": "base.contractErr", 14 "anyC": "base.anyC", 15 "neverC": "base.neverC", 16 "guardC": "base.guardC", 17 "nat?": "base.nat?", 18 "nonZero?": "base.nonZero?", 19 "bool?": "base.bool?", 20 "andC": "base.andC", 21 "orC": "base.orC", 22 "notC": "base.notC", 23 "mapC": "base.mapC", 24 "bindC": "base.bindC", 25 "listOf": "base.listOf", 26 "nonEmptyListOf": "base.nonEmptyListOf", 27 "pairOf": "base.pairOf", 28 "fnContract": "base.fnContract", 29 "fn2": "base.fn2", 30 "bindResult": "base.bindResult", 31 "mapResult": "base.mapResult", 32 "resultMapErr": "base.resultMapErr", 33 "resultIsOk": "base.resultIsOk", 34 "resultIsErr": "base.resultIsErr", 35 "pureE": "base.pureE", 36 "bindE": "base.bindE", 37 "exceptE": "base.exceptE", 38 "pureM": "base.pureM", 39 "bindM": "base.bindM", 40 "checkM": "base.checkM", 41 "liftM": "base.liftM", 42 "runM": "base.runM", 43 "handleM": "base.handleM" 44 }, 45 "backend": "stable", 46 "cases": [ 47 { 48 "source": "id =@nat? (x : x)", 49 "export": "id", 50 "arguments": [], 51 "failure": "not a natural number", 52 "definitions": { 53 "id": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000" 54 }, 55 "result": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000", 56 "expected": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000" 57 }, 58 { 59 "source": "id x =@nat? x", 60 "export": "id", 61 "arguments": [ 62 "2021020210202100" 63 ], 64 "expected": "2021020210202100", 65 "definitions": { 66 "id": "21212120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002020020212010211002121202121200212002121200212002120112020202121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202110020212120021200212011202120112011021212002120021201021200211002021100212010211002021100211002120102110020211002121200212002121200212002120102110020211002020020212120021200212120021200212011200212011200212120021200212011200212011200212011212002120021201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212011212021212002120021201120212011201021212002120021201021200211002021100212010211002021100202202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210002120102110021201120102121200212002120102120021200212011202121200212002120112021201120110212120021200212010212002110020211002120102110020211002120102110020212010211002120112010212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110020202110021201120212120212110021100202120212120021200212011212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100201020200212010212120021200212010212002120021212002120021201120021201120021212002120021201120021201120021212002120021201120021201120021201120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021212002120021201120021201120021201120102121200212002120112002120112002121200212002120112002120112002120112011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020021201120102121200212002120102120021200212010211002021201021100212011201021201120102121200212002120102120021200212010211002021201021100202021100202120102110021201120102121200212002120112002120112002121200212002120112002120112002120112010212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212011201120112021211002002121200212002120112002120112002120112011200212011201120021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120102110020212010212120021200212010212002120021201021100202120102110020202120102121200212002120112002120112002120112010212011200212011200212120021200212010212002120021201021100202120102110020202120102110020202021100212011201021212002120021201021200212002120102110020212010211002020212120021200212010211002020020202120102121200212002120102110020200202021201021100202020200202020202002020211002021201021100202110021212021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002021211002110021100211002120102110021100" 67 }, 68 "result": "2021020210202100" 69 }, 70 { 71 "source": "id x =@nat? x", 72 "export": "id", 73 "arguments": [ 74 "10" 75 ], 76 "failure": "not a natural number", 77 "definitions": { 78 "id": "21212120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002020020212010211002121202121200212002121200212002120112020202121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202110020212120021200212011202120112011021212002120021201021200211002021100212010211002021100211002120102110020211002121200212002121200212002120102110020211002020020212120021200212120021200212011200212011200212120021200212011200212011200212011212002120021201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212011212021212002120021201120212011201021212002120021201021200211002021100212010211002021100202202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210002120102110021201120102121200212002120102120021200212011202121200212002120112021201120110212120021200212010212002110020211002120102110020211002120102110020212010211002120112010212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110020202110021201120212120212110021100202120212120021200212011212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100201020200212010212120021200212010212002120021212002120021201120021201120021212002120021201120021201120021212002120021201120021201120021201120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021212002120021201120021201120021201120102121200212002120112002120112002121200212002120112002120112002120112011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020021201120102121200212002120102120021200212010211002021201021100212011201021201120102121200212002120102120021200212010211002021201021100202021100202120102110021201120102121200212002120112002120112002121200212002120112002120112002120112010212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212011201120112021211002002121200212002120112002120112002120112011200212011201120021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120102110020212010212120021200212010212002120021201021100202120102110020202120102121200212002120112002120112002120112010212011200212011200212120021200212010212002120021201021100202120102110020202120102110020202021100212011201021212002120021201021200212002120102110020212010211002020212120021200212010211002020020202120102121200212002120102110020200202021201021100202020200202020202002020211002021201021100202110021212021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002021211002110021100211002120102110021100" 79 }, 80 "result": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000", 81 "expected": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000" 82 }, 83 { 84 "source": "id x =@nat? x", 85 "export": "id", 86 "arguments": [ 87 "200" 88 ], 89 "failure": "not a natural number", 90 "definitions": { 91 "id": "21212120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002020020212010211002121202121200212002121200212002120112020202121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202110020212120021200212011202120112011021212002120021201021200211002021100212010211002021100211002120102110020211002121200212002121200212002120102110020211002020020212120021200212120021200212011200212011200212120021200212011200212011200212011212002120021201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212011212021212002120021201120212011201021212002120021201021200211002021100212010211002021100202202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210002120102110021201120102121200212002120102120021200212011202121200212002120112021201120110212120021200212010212002110020211002120102110020211002120102110020212010211002120112010212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110020202110021201120212120212110021100202120212120021200212011212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100201020200212010212120021200212010212002120021212002120021201120021201120021212002120021201120021201120021212002120021201120021201120021201120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021212002120021201120021201120021201120102121200212002120112002120112002121200212002120112002120112002120112011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020021201120102121200212002120102120021200212010211002021201021100212011201021201120102121200212002120102120021200212010211002021201021100202021100202120102110021201120102121200212002120112002120112002121200212002120112002120112002120112010212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212011201120112021211002002121200212002120112002120112002120112011200212011201120021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120102110020212010212120021200212010212002120021201021100202120102110020202120102121200212002120112002120112002120112010212011200212011200212120021200212010212002120021201021100202120102110020202120102110020202021100212011201021212002120021201021200212002120102110020212010211002020212120021200212010211002020020202120102121200212002120102110020200202021201021100202020200202020202002020211002021201021100202110021212021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002021211002110021100211002120102110021100" 92 }, 93 "result": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000", 94 "expected": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000" 95 }, 96 { 97 "source": "id x@nat? =@nat? x", 98 "export": "id", 99 "arguments": [ 100 "2102102100" 101 ], 102 "expected": "2102102100", 103 "definitions": { 104 "id": "2121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202002021201121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202002021201021100212011212021212002120021212002120021201120202021212120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002021100202121200212002120112021201120110212120021200212010212002110020211002120102110020211002110021201021100202110021212002120021212002120021201021100202110020200202121200212002121200212002120112002120112002121200212002120112002120112002120112120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120112120212120021200212011202120112010212120021200212010212002110020211002120102110020211002022021021021020210210022102102102102021021002202021020210210210022020202020210022102020202021021002202020202021002202102102102021021002210202020202102100220202102021021021002210202102021021021002202102020210210210022102020202021021002202021021020210210022020202020210022021021021020210210022102021020210210210022102021021020210210022021020202021021002210202102020210210022021020202102102100021201021100212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110021201120102120112010212120021200212010212002120021201120212120021200212011202120112011021212002120021201021200211002021100212010211002021100212010211002021201021100202021100212011202121202121100211002021202121200212002120112121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002010202002120102121200212002120102120021200212120021200212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212120021200212011200212011200212011201021212002120021201120021201120021212002120021201120021201120021201120112120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200212011201021212002120021201021200212002120102110020212010211002120112010212011201021212002120021201021200212002120102110020212010211002020211002021201021100212011201021212002120021201120021201120021212002120021201120021201120021201120102120112002120112002121200212002120112002120112002121200212002120112002120112002120112011202120112011201120212110020021212002120021201120021201120021201120112002120112011200212120021200212011200212011200212011201021201120021201120021212002120021201021200212002120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021201021100202120102121200212002120102120021200212010211002021201021100202021201021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212010211002021201021100202021201021100202020211002120112010212120021200212010212002120021201021100202120102110020202121200212002120102110020200202021201021212002120021201021100202002020212010211002020202002020202020020202110020212010211002021100212120212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020212110021100211002110021201021100212010211002121202121200212002121200212002120112020202121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202110020212120021200212011202120112011021212002120021201021200211002021100212010211002021100211002120102110020211002121200212002121200212002120102110020211002020020212120021200212120021200212011200212011200212120021200212011200212011200212011212002120021201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212011212021212002120021201120212011201021212002120021201021200211002021100212010211002021100202202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210002120102110021201120102121200212002120102120021200212011202121200212002120112021201120110212120021200212010212002110020211002120102110020211002120102110020212010211002120112010212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110020202110021201120212120212110021100202120212120021200212011212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100201020200212010212120021200212010212002120021212002120021201120021201120021212002120021201120021201120021212002120021201120021201120021201120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021212002120021201120021201120021201120102121200212002120112002120112002121200212002120112002120112002120112011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020021201120102121200212002120102120021200212010211002021201021100212011201021201120102121200212002120102120021200212010211002021201021100202021100202120102110021201120102121200212002120112002120112002121200212002120112002120112002120112010212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212011201120112021211002002121200212002120112002120112002120112011200212011201120021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120102110020212010212120021200212010212002120021201021100202120102110020202120102121200212002120112002120112002120112010212011200212011200212120021200212010212002120021201021100202120102110020202120102110020202021100212011201021212002120021201021200212002120102110020212010211002020212120021200212010211002020020202120102121200212002120102110020200202021201021100202020200202020202002020211002021201021100202110021212021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002021211002110021100211002120102110021100" 105 }, 106 "result": "2102102100" 107 }, 108 { 109 "source": "id x@nat? =@nat? x", 110 "export": "id", 111 "arguments": [ 112 "2202102020202102100221020202020210210022020210202021021000" 113 ], 114 "failure": "not a natural number", 115 "definitions": { 116 "id": "2121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202002021201121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202002021201021100212011212021212002120021212002120021201120202021212120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002021100202121200212002120112021201120110212120021200212010212002110020211002120102110020211002110021201021100202110021212002120021212002120021201021100202110020200202121200212002121200212002120112002120112002121200212002120112002120112002120112120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120112120212120021200212011202120112010212120021200212010212002110020211002120102110020211002022021021021020210210022102102102102021021002202021020210210210022020202020210022102020202021021002202020202021002202102102102021021002210202020202102100220202102021021021002210202102021021021002202102020210210210022102020202021021002202021021020210210022020202020210022021021021020210210022102021020210210210022102021021020210210022021020202021021002210202102020210210022021020202102102100021201021100212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110021201120102120112010212120021200212010212002120021201120212120021200212011202120112011021212002120021201021200211002021100212010211002021100212010211002021201021100202021100212011202121202121100211002021202121200212002120112121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002010202002120102121200212002120102120021200212120021200212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212120021200212011200212011200212011201021212002120021201120021201120021212002120021201120021201120021201120112120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200212011201021212002120021201021200212002120102110020212010211002120112010212011201021212002120021201021200212002120102110020212010211002020211002021201021100212011201021212002120021201120021201120021212002120021201120021201120021201120102120112002120112002121200212002120112002120112002121200212002120112002120112002120112011202120112011201120212110020021212002120021201120021201120021201120112002120112011200212120021200212011200212011200212011201021201120021201120021212002120021201021200212002120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021201021100202120102121200212002120102120021200212010211002021201021100202021201021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212010211002021201021100202021201021100202020211002120112010212120021200212010212002120021201021100202120102110020202121200212002120102110020200202021201021212002120021201021100202002020212010211002020202002020202020020202110020212010211002021100212120212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020212110021100211002110021201021100212010211002121202121200212002121200212002120112020202121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202110020212120021200212011202120112011021212002120021201021200211002021100212010211002021100211002120102110020211002121200212002121200212002120102110020211002020020212120021200212120021200212011200212011200212120021200212011200212011200212011212002120021201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212011212021212002120021201120212011201021212002120021201021200211002021100212010211002021100202202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210002120102110021201120102121200212002120102120021200212011202121200212002120112021201120110212120021200212010212002110020211002120102110020211002120102110020212010211002120112010212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110020202110021201120212120212110021100202120212120021200212011212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100201020200212010212120021200212010212002120021212002120021201120021201120021212002120021201120021201120021212002120021201120021201120021201120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021212002120021201120021201120021201120102121200212002120112002120112002121200212002120112002120112002120112011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020021201120102121200212002120102120021200212010211002021201021100212011201021201120102121200212002120102120021200212010211002021201021100202021100202120102110021201120102121200212002120112002120112002121200212002120112002120112002120112010212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212011201120112021211002002121200212002120112002120112002120112011200212011201120021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120102110020212010212120021200212010212002120021201021100202120102110020202120102121200212002120112002120112002120112010212011200212011200212120021200212010212002120021201021100202120102110020202120102110020202021100212011201021212002120021201021200212002120102110020212010211002020212120021200212010211002020020202120102121200212002120102110020200202021201021100202020200202020202002020211002021201021100202110021212021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002021211002110021100211002120102110021100" 117 }, 118 "result": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000", 119 "expected": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000" 120 }, 121 { 122 "source": "id @nat? =@nat? (x : x)", 123 "export": "id", 124 "arguments": [ 125 "21020202100" 126 ], 127 "expected": "21020202100", 128 "definitions": { 129 "id": "21212120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002020020212011212120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002020020212010211002120112120212120021200212120021200212011202020212121202121200212002120112002120112002120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201021212002120021201120021201120021201120112002120112011200212011201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112011201021212002120021201120021201120021201120102120112002120112002120112011200212011201120021201121200212002120112002120112002120112011202121200212002120112120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100211002120102120102110021201021201021201021100212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110021201021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002020212010212010211002020202110020202110020212120021200212011202120112010212120021200212010212002110020211002120102110020211002021212002120021201120212011201102121200212002120102120021100202110021201021100202110021100212010211002021100212120021200212120021200212010211002021100202002021212002120021212002120021201120021201120021212002120021201120021201120021201121200212002120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021201121202121200212002120112021201120102121200212002120102120021100202110021201021100202110020220210210210202102100221021021021020210210022020210202102102100220202020202100221020202020210210022020202020210022021021021020210210022102020202021021002202021020210210210022102021020210210210022021020202102102100221020202020210210022020210210202102100220202020202100220210210210202102100221020210202102102100221020210210202102100220210202020210210022102021020202102100220210202021021021000212010211002120112010212120021200212010212002120021201120212120021200212011202120112011021212002120021201021200211002021100212010211002021100212010211002021201021100212011201021201120102121200212002120102120021200212011202121200212002120112021201120110212120021200212010212002110020211002120102110020211002120102110020212010211002020211002120112021212021211002110020212021212002120021201121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020102020021201021212002120021201021200212002121200212002120112002120112002121200212002120112002120112002121200212002120112002120112002120112011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002121200212002120112002120112002120112010212120021200212011200212011200212120021200212011200212011200212011201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002120112010212120021200212010212002120021201021100202120102110021201120102120112010212120021200212010212002120021201021100202120102110020202110020212010211002120112010212120021200212011200212011200212120021200212011200212011200212011201021201120021201120021212002120021201120021201120021212002120021201120021201120021201120112021201120112011202121100200212120021200212011200212011200212011201120021201120112002121200212002120112002120112002120112010212011200212011200212120021200212010212002120021201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212010211002021201021212002120021201021200212002120102110020212010211002020212010212120021200212011200212011200212011201021201120021201120021212002120021201021200212002120102110020212010211002020212010211002020202110021201120102121200212002120102120021200212010211002021201021100202021212002120021201021100202002020212010212120021200212010211002020020202120102110020202020020202020200202021100202120102110020211002121202121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202121100211002110021100212010211002120112021100212010211002121202121200212002121200212002120112020202121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202110020212120021200212011202120112011021212002120021201021200211002021100212010211002021100211002120102110020211002121200212002121200212002120102110020211002020020212120021200212120021200212011200212011200212120021200212011200212011200212011212002120021201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212011212021212002120021201120212011201021212002120021201021200211002021100212010211002021100202202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210002120102110021201120102121200212002120102120021200212011202121200212002120112021201120110212120021200212010212002110020211002120102110020211002120102110020212010211002120112010212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110020202110021201120212120212110021100202120212120021200212011212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100201020200212010212120021200212010212002120021212002120021201120021201120021212002120021201120021201120021212002120021201120021201120021201120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021212002120021201120021201120021201120102121200212002120112002120112002121200212002120112002120112002120112011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020021201120102121200212002120102120021200212010211002021201021100212011201021201120102121200212002120102120021200212010211002021201021100202021100202120102110021201120102121200212002120112002120112002121200212002120112002120112002120112010212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212011201120112021211002002121200212002120112002120112002120112011200212011201120021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120102110020212010212120021200212010212002120021201021100202120102110020202120102121200212002120112002120112002120112010212011200212011200212120021200212010212002120021201021100202120102110020202120102110020202021100212011201021212002120021201021200212002120102110020212010211002020212120021200212010211002020020202120102121200212002120102110020200202021201021100202020200202020202002020211002021201021100202110021212021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002021211002110021100211002120102110021100" 130 }, 131 "result": "21020202100" 132 }, 133 { 134 "source": "id @nat? =@nat? (x : x)", 135 "export": "id", 136 "arguments": [ 137 "10" 138 ], 139 "failure": "not a natural number", 140 "definitions": { 141 "id": "21212120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002020020212011212120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002020020212010211002120112120212120021200212120021200212011202020212121202121200212002120112002120112002120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201021212002120021201120021201120021201120112002120112011200212011201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112011201021212002120021201120021201120021201120102120112002120112002120112011200212011201120021201121200212002120112002120112002120112011202121200212002120112120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100211002120102120102110021201021201021201021100212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110021201021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002020212010212010211002020202110020202110020212120021200212011202120112010212120021200212010212002110020211002120102110020211002021212002120021201120212011201102121200212002120102120021100202110021201021100202110021100212010211002021100212120021200212120021200212010211002021100202002021212002120021212002120021201120021201120021212002120021201120021201120021201121200212002120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021201121202121200212002120112021201120102121200212002120102120021100202110021201021100202110020220210210210202102100221021021021020210210022020210202102102100220202020202100221020202020210210022020202020210022021021021020210210022102020202021021002202021020210210210022102021020210210210022021020202102102100221020202020210210022020210210202102100220202020202100220210210210202102100221020210202102102100221020210210202102100220210202020210210022102021020202102100220210202021021021000212010211002120112010212120021200212010212002120021201120212120021200212011202120112011021212002120021201021200211002021100212010211002021100212010211002021201021100212011201021201120102121200212002120102120021200212011202121200212002120112021201120110212120021200212010212002110020211002120102110020211002120102110020212010211002020211002120112021212021211002110020212021212002120021201121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020102020021201021212002120021201021200212002121200212002120112002120112002121200212002120112002120112002121200212002120112002120112002120112011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002121200212002120112002120112002120112010212120021200212011200212011200212120021200212011200212011200212011201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002120112010212120021200212010212002120021201021100202120102110021201120102120112010212120021200212010212002120021201021100202120102110020202110020212010211002120112010212120021200212011200212011200212120021200212011200212011200212011201021201120021201120021212002120021201120021201120021212002120021201120021201120021201120112021201120112011202121100200212120021200212011200212011200212011201120021201120112002121200212002120112002120112002120112010212011200212011200212120021200212010212002120021201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212010211002021201021212002120021201021200212002120102110020212010211002020212010212120021200212011200212011200212011201021201120021201120021212002120021201021200212002120102110020212010211002020212010211002020202110021201120102121200212002120102120021200212010211002021201021100202021212002120021201021100202002020212010212120021200212010211002020020202120102110020202020020202020200202021100202120102110020211002121202121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202121100211002110021100212010211002120112021100212010211002121202121200212002121200212002120112020202121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202110020212120021200212011202120112011021212002120021201021200211002021100212010211002021100211002120102110020211002121200212002121200212002120102110020211002020020212120021200212120021200212011200212011200212120021200212011200212011200212011212002120021201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212011212021212002120021201120212011201021212002120021201021200211002021100212010211002021100202202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210002120102110021201120102121200212002120102120021200212011202121200212002120112021201120110212120021200212010212002110020211002120102110020211002120102110020212010211002120112010212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110020202110021201120212120212110021100202120212120021200212011212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100201020200212010212120021200212010212002120021212002120021201120021201120021212002120021201120021201120021212002120021201120021201120021201120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021212002120021201120021201120021201120102121200212002120112002120112002121200212002120112002120112002120112011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020021201120102121200212002120102120021200212010211002021201021100212011201021201120102121200212002120102120021200212010211002021201021100202021100202120102110021201120102121200212002120112002120112002121200212002120112002120112002120112010212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212011201120112021211002002121200212002120112002120112002120112011200212011201120021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120102110020212010212120021200212010212002120021201021100202120102110020202120102121200212002120112002120112002120112010212011200212011200212120021200212010212002120021201021100202120102110020202120102110020202021100212011201021212002120021201021200212002120102110020212010211002020212120021200212010211002020020202120102121200212002120102110020200202021201021100202020200202020202002020211002021201021100202110021212021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002021211002110021100211002120102110021100" 142 }, 143 "result": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000", 144 "expected": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000" 145 }, 146 { 147 "source": "first x@nat? y@nat? =@nat? x", 148 "export": "first", 149 "arguments": [ 150 "10", 151 "202100" 152 ], 153 "failure": "not a natural number", 154 "definitions": { 155 "first": "212121202121200212002120112002120112002120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201021212002120021201120021201120021201120112002120112011200212011201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112011201021212002120021201120021201120021201120102120112002120112002120112011200212011201120021201121200212002120112002120112002120112011202121200212002120112120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100211002120102120102110021201021201021201021100212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110021201021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002020212010212010211002020202110020202110020212010212120021200212011202120112010212120021200212010212002110020211002120102110020200202120102121200212002120112120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002020021201021201021201121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202002021201021100212011212021212002120021212002120021201120202021212120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002021100202121200212002120112021201120110212120021200212010212002110020211002120102110020211002110021201021100202110021212002120021212002120021201021100202110020200202121200212002121200212002120112002120112002121200212002120112002120112002120112120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120112120212120021200212011202120112010212120021200212010212002110020211002120102110020211002022021021021020210210022102102102102021021002202021020210210210022020202020210022102020202021021002202020202021002202102102102021021002210202020202102100220202102021021021002210202102021021021002202102020210210210022102020202021021002202021021020210210022020202020210022021021021020210210022102021020210210210022102021021020210210022021020202021021002210202102020210210022021020202102102100021201021100212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110021201120102120112010212120021200212010212002120021201120212120021200212011202120112011021212002120021201021200211002021100212010211002021100212010211002021201021100202021100212011202121202121100211002021202121200212002120112121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002010202002120102121200212002120102120021200212120021200212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212120021200212011200212011200212011201021212002120021201120021201120021212002120021201120021201120021201120112120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200212011201021212002120021201021200212002120102110020212010211002120112010212011201021212002120021201021200212002120102110020212010211002020211002021201021100212011201021212002120021201120021201120021212002120021201120021201120021201120102120112002120112002121200212002120112002120112002121200212002120112002120112002120112011202120112011201120212110020021212002120021201120021201120021201120112002120112011200212120021200212011200212011200212011201021201120021201120021212002120021201021200212002120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021201021100202120102121200212002120102120021200212010211002021201021100202021201021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212010211002021201021100202021201021100202020211002120112010212120021200212010212002120021201021100202120102110020202121200212002120102110020200202021201021212002120021201021100202002020212010211002020202002020202020020202110020212010211002021100212120212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020212110021100211002110021201021100212010211002021212021212002120021212002120021201120202021212120212120021200212011200212011200212011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120102121200212002120112002120112002120112011200212011201120021201120112011202121212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020020021100212011201120102121200212002120112002120112002120112010212011200212011200212011201120021201120112002120112120021200212011200212011200212011201120212120021200212011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021100212010212010211002120102120102120102110021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002120102121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100202021201021201021100202020211002020211002021212002120021201120212011201021212002120021201021200211002021100212010211002021100202121200212002120112021201120110212120021200212010212002110020211002120102110020211002110021201021100202110021212002120021212002120021201021100202110020200202121200212002121200212002120112002120112002121200212002120112002120112002120112120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120112120212120021200212011202120112010212120021200212010212002110020211002120102110020211002022021021021020210210022102102102102021021002202021020210210210022020202020210022102020202021021002202020202021002202102102102021021002210202020202102100220202102021021021002210202102021021021002202102020210210210022102020202021021002202021021020210210022020202020210022021021021020210210022102021020210210210022102021021020210210022021020202021021002210202102020210210022021020202102102100021201021100212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110021201120102120112010212120021200212010212002120021201120212120021200212011202120112011021212002120021201021200211002021100212010211002021100212010211002021201021100202021100212011202121202121100211002021202121200212002120112121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002010202002120102121200212002120102120021200212120021200212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212120021200212011200212011200212011201021212002120021201120021201120021212002120021201120021201120021201120112120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200212011201021212002120021201021200212002120102110020212010211002120112010212011201021212002120021201021200212002120102110020212010211002020211002021201021100212011201021212002120021201120021201120021212002120021201120021201120021201120102120112002120112002121200212002120112002120112002121200212002120112002120112002120112011202120112011201120212110020021212002120021201120021201120021201120112002120112011200212120021200212011200212011200212011201021201120021201120021212002120021201021200212002120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021201021100202120102121200212002120102120021200212010211002021201021100202021201021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212010211002021201021100202021201021100202020211002120112010212120021200212010212002120021201021100202120102110020202121200212002120102110020200202021201021212002120021201021100202002020212010211002020202002020202020020202110020212010211002021100212120212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020212110021100211002110021201021100211002121202121200212002121200212002120112020202121212021212002120021201120021201120021201120112021212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100200200211002120112010212120021200212011200212011200212011201120021201120112002120112011201120212121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002002002110021201120112010212120021200212011200212011200212011201021201120021201120021201120112002120112011200212011212002120021201120021201120021201120112021212002120021201121202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002110021201021201021100212010212010212010211002121200212002120112002120112002121200212002120102120021200212010211002021201021100202021100212010212120021200212011200212011200212120021200212010212002120021201021100202120102110020202110020202120102120102110020202021100202021100202121200212002120112021201120102121200212002120102120021100202110021201021100202110020212120021200212011202120112011021212002120021201021200211002021100212010211002021100211002120102110020211002121200212002121200212002120102110020211002020020212120021200212120021200212011200212011200212120021200212011200212011200212011212002120021201120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100212011212021212002120021201120212011201021212002120021201021200211002021100212010211002021100202202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210002120102110021201120102121200212002120102120021200212011202121200212002120112021201120110212120021200212010212002110020211002120102110020211002120102110020212010211002120112010212011201021212002120021201021200212002120112021212002120021201120212011201102121200212002120102120021100202110021201021100202110021201021100202120102110020202110021201120212120212110021100202120212120021200212011212120212120021200212011200212011200212011201021201120021212002120021201021200211002021100202021100201020200212010212120021200212010212002120021212002120021201120021201120021212002120021201120021201120021212002120021201120021201120021201120112021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110021212002120021201120021201120021201120102121200212002120112002120112002121200212002120112002120112002120112011212021212002120021201120021201120021201120102120112002121200212002120102120021100202110020202110020021201120102121200212002120102120021200212010211002021201021100212011201021201120102121200212002120102120021200212010211002021201021100202021100202120102110021201120102121200212002120112002120112002121200212002120112002120112002120112010212011200212011200212120021200212011200212011200212120021200212011200212011200212011201120212011201120112021211002002121200212002120112002120112002120112011200212011201120021212002120021201120021201120021201120102120112002120112002121200212002120102120021200212011202121200212002120112002120112002120112010212011200212120021200212010212002110020211002020211002120102110020212010212120021200212010212002120021201021100202120102110020202120102121200212002120112002120112002120112010212011200212011200212120021200212010212002120021201021100202120102110020202120102110020202021100212011201021212002120021201021200212002120102110020212010211002020212120021200212010211002020020202120102121200212002120102110020200202021201021100202020200202020202002020211002021201021100202110021212021212002120021201120021201120021212002120021201021200212002120102110020212010211002020211002021211002110021100211002120102110021100" 156 }, 157 "result": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000", 158 "expected": "2022202102102102021021002210210210210202102100220202102021021021002202020202021002210202020202102100220202020202100220210210210202102100221020202020210210022020210202102102100221020210202102102100220210202021021021002210202020202102100220202102102021021002202020202021002202102102102021021002210202102021021021002210202102102021021002202102020202102100221020210202021021002202102020210210210000" 159 }, 160 { 161 "source": "main = check nat? 42", 162 "export": "main", 163 "arguments": [], 164 "expected": "2021020210202100", 165 "definitions": { 166 "main": "2021020210202100" 167 }, 168 "result": "2021020210202100" 169 }, 170 { 171 "source": "main = check (listOf nat?) [1 2]", 172 "export": "main", 173 "arguments": [], 174 "expected": "2210022021000", 175 "definitions": { 176 "main": "2210022021000" 177 }, 178 "result": "2210022021000" 179 } 180 ] 181 }