Type-level natural number addition using Conditional Types in TypeScript 2.8

condTypes.ts

type Nat = 0 | { succ: Nat };

type Succ<T extends Nat> = { succ: T };

type N0  = 0;
type N1  = Succ<N0>;
type N2  = Succ<N1>;
type N3  = Succ<N2>;
type N4  = Succ<N3>;
type N5  = Succ<N4>;
type N6  = Succ<N5>;
type N7  = Succ<N6>;
type N8  = Succ<N7>;
type N9  = Succ<N8>;
type N10 = Succ<N9>;

// type-level add operation
type Add<X extends Nat, Y extends Nat> =
    X extends Succ<infer R> ? { succ: Add<R, Y> } : Y;

// type-level assertion
type Assert<X extends Nat, Y extends Nat> = X extends Y ? any : never;

// test
const t1: Assert<Add<N4, N5>, N9> = {}; // pass
const t2: Assert<Add<N1, N3>, N4> = {}; // pass
const t3: Assert<Add<N1, N3>, N5> = {}; // compile error