Types.New+.dscr

//'Types.New' with property key syntax sugar.
//Uses ambiguous matches - might change in future.
//Separates values into 'Value[a] | Type[a]'.

Res[rec, prim].

//The type system
Value[a]. //An untyped value.
Type[a]. //A value's type.

//Values
Zero[].
Succ[prev].
Add[a, b].
Fib[a].
Fib3[a].

//Types
Nat[].

//Type signatures
Add[Type[Nat[]], Type[Nat[]]]: Type[Nat[]]
Fib[Type[Nat[]]]: Type[Nat[]]
Fib3[Type[Nat[]]]: Type[Nat[]]

//Untyped functions
Add[Value[Zero[]], Value[a]]: Value[b>a]
Add[Value[Succ[prev]], Value[a]]: Add[
  Value[a>a>prev]
  Value[Succ[prev: b<Add>a<Value]]
]
Fib[Value[Zero[]]]: Value[Succ[Zero[]]]
Fib[Value[Succ[Zero[]]]]: Value[Succ[Zero[]]]
Fib[Value[Succ[Succ[prev]]]]: Add[
  Fib[Value[a>a>prev]]
  Fib[Value[a>a>prev>prev]]
]
Fib3[Value[a]]: Fib[Fib[Fib[Value[a>a]]]]

//Alternate number representation
Add[Value[#Number[]], Value[#Number[]]]: Value[#Add[a>a, b>a]]
Fib[Value[0]]: Value[1]
Fib[Value[1]]: Value[1]
Fib[Value[#Number[]]]: Add[
  Fib[Value[#Add[a>a, -1]]]
  Fib[Value[#Add[a>a, -2]]]
]

//Query
Res[
  rec: Fib3[Type[Nat[]] | Value[Succ[Succ[Succ[Succ[Zero[]]]]]]]
  prim: Fib3[Type[Nat[]] | Value[4]]
]?