//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[b].
Fib3[a].

//Types
Nat[].

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

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

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

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