For your convenience, below is JSON you can copy and paste into any LLM to get you started:
{ “version”: “26.8”, “types”: [“nat”, “bool”, “null”, “error”, “string”], “type_definitions”: { “nat”: “0 | S(nat)“, “bool”: “B0 | B1”, “null”: “null”, “error”: “error(string)“, “string”: “string(length ≤ 256, charset = ASCII)” }, “limits”: { “max_steps”: 10, “max_div_steps”: 10, “max_stack_depth”: 20, “max_nat_size”: 20 }, “depth”: { “definition”: [ “depth(0) → 0”, “depth(S(x)) → S(depth(x))” ] }, “guards”: { “nat_guard”: “if depth(x) > max_nat_size → error(\“E001\”)“, “depth_guard”: “if current_stack_depth > max_stack_depth → error(\“E002\”)“, “step_guard”: “if current_steps > max_steps → error(\“E003\”)“, “div_guard”: “if ge(steps, max_div_steps) → error(\“E004\”)” }, “constructors”: { “S(x) where typeof(x) ≠ nat → error(\“E100\”)“, “S(x) → apply(nat_guard)” }, “arithmetic”: { “add”: [ “add(0, y) → y”, “add(S(x), y) → S(add(x, y))“, “add(x, y) where typeof(x) ≠ nat or typeof(y) ≠ nat → error(\“E101\”)” ], “sub”: [ “sub(0, 0) → 0”, “sub(S(x), 0) → S(x)“, “sub(0, S(_)) → error(\“E102\”)“, “sub(S(x), S(y)) → sub(x, y)“, “sub(x, y) where typeof(x) ≠ nat or typeof(y) ≠ nat → error(\“E101\”)” ], “mul”: [ “mul(0, _) → 0”, “mul(S(x), y) → add(y, mul(x, y))“, “mul(x, y) where typeof(x) ≠ nat or typeof(y) ≠ nat → error(\“E101\”)” ], “pred”: [ “pred(0) → 0”, “pred(S(x)) → x”, “pred(x) where typeof(x) ≠ nat → error(\“E101\”)” ] }, “division”: { “div(x, y)”: “→ div_safe(x, y, 0)“, “div_safe”: [ “div_safe(x, y, steps) where typeof(x) ≠ nat or typeof(y) ≠ nat or typeof(steps) ≠ nat → error(\“E101\”)“, “if ge(steps, max_div_steps) → error(\“E004\”)“, “if eq(y, 0) → error(\“E103\”)“, “if lt(x, y) → 0”, “else → S(div_safe(sub(x, y), y, S(steps)))” ] }, “booleans”: { “not”: [ “not(B0) → B1”, “not(B1) → B0”, “not(x) where typeof(x) ≠ bool → error(\“E101\”)” ], “and”: [ “and(B0, _) → B0”, “and(B1, B1) → B1”, “and(B1, B0) → B0”, “and(x, y) where typeof(x) ≠ bool or typeof(y) ≠ bool → error(\“E101\”)” ], “or”: [ “or(B1, _) → B1”, “or(B0, B0) → B0”, “or(B0, B1) → B1”, “or(x, y) where typeof(x) ≠ bool or typeof(y) ≠ bool → error(\“E101\”)” ] }, “comparison”: { “eq”: [ “eq(0, 0) → B1”, “eq(S(x), S(y)) → eq(x, y)“, “eq(x, y) where typeof(x) ≠ typeof(y) → B0”, “eq(x, y) where typeof(x) = typeof(y) → B0” ], “lt”: [ “lt(0, S(_)) → B1”, “lt(S(_), 0) → B0”, “lt(S(x), S(y)) → lt(x, y)“, “lt(0, 0) → B0”, “lt(x, y) where typeof(x) ≠ nat or typeof(y) ≠ nat → error(\“E101\”)” ], “gt”: [ “gt(x, y) → lt(y, x)“, “gt(x, y) where typeof(x) ≠ nat or typeof(y) ≠ nat → error(\“E101\”)” ], “le”: [ “le(0, 0) → B1”, “le(0, S(_)) → B1”, “le(S(_), 0) → B0”, “le(S(x), S(y)) → le(x, y)“, “le(x, y) where typeof(x) ≠ nat or typeof(y) ≠ nat → error(\“E101\”)” ], “ge”: [ “ge(0, 0) → B1”, “ge(S(_), 0) → B1”, “ge(0, S(_)) → B0”, “ge(S(x), S(y)) → ge(x, y)“, “ge(x, y) where typeof(x) ≠ nat or typeof(y) ≠ nat → error(\“E101\”)” ] }, “evaluation”: { “order”: “strict left-to-right”, “short_circuiting”: { “and(B0, _) → B0”, “or(B1, _) → B1” }, “step_tracking”: “each operation increments global step counter”, “stack_tracking”: “bind and recursive calls increment stack depth; depth_guard checked pre-call” }, “error_handling”: { “typeof(error(x)) → error(\“E200\”)“, “any_op(error(x), _) → error(\“E201\”)“, “any_op(_, error(x)) → error(\“E201\”)” }, “error_precedence”: [ “E002 stack overflow”, “E003 step limit exceeded”, “E004 division step overflow”, “E101 type error”, “E103 divide by zero”, “E102 subtraction underflow”, “E200 type inspection of error”, “E201 error operand” ] }