Nat.cs

Nat.cs

/*

A type `Nat` is either
   -> Zero
   -> Succ of Nat
 
We can say the same thing in C# 12 (.Net 8)

*/

record Nat<T>();

record Zero : Nat<Zero>;

record Succ<T>(Nat<T> Pred) : Nat<Succ<T>>;

public class Judgements
{
    [Fact]
    public void ZeroToThree()
    {
        Nat<Zero> zero = new Zero();
        Nat<Succ<Zero>> one = new Succ<Zero>(zero);
        Nat<Succ<Succ<Zero>>> two = new Succ<Succ<Zero>>(one);
        Nat<Succ<Succ<Succ<Zero>>>> three = new Succ<Succ<Succ<Zero>>>(two);
    }
}