Natural numbers and vectors in C# , the Idris way

Nat.cs

// Data Nat = Z | S Nat
// 
// plus : Nat -> Nat -> Nat
// plus Z y = y
// plus (S k) y = S (plus k y)

abstract class Nat {
}

class Zero : Nat {
	Zero() {}
}

class Successor : Nat {
	Nat prev;
	Successor(Nat prev) {this.prev = prev}
}

var _0 = new Zero()
var _1 = new Successor(_0)
var _2 = new Successor(_1)
var _2 = new Successor(new Successor(_0))

Nat plus(Nat x, Nat y) {
	if (typeof(Zero)  == x.GetType()) {
		return y;
	} else {
		var succ = (Successor)x;
		return new Successor(plus(succ.prev,y))
	}
}

Vector0 = {}
Vector1 = {A = "Tom"}
Vector2 = {A = "Jef", B = "Greg"}
Vector1 ++ Vector2 = {A = "Tom", B= "Jef", C "Greg"}