Typed Evaluation

In the normal type-theory based formulation of programming languages, we would introduce a typing judgement like \[\frac{a:Nat \quad b:Nat}{\texttt{plus}(a,b):Nat}\] stating that addition of two natural numbers is a term of type natural number. In Lynx, we make a weaker claim. We say that (for total functions) addition can be equal to other expressions in type \(Nat\) or can be evaluated in type \(Nat\) but not that it is of type \(Nat\). Type expressions are formed in terms of evaluation: \[\frac{a:Nat \quad b:Nat}{\texttt{plus}(a,b) \Downarrow_Nat Nat}\]