wiki:TypeNats/RuleNotation

Version 1 (modified by diatchki, 4 years ago) (diff)

--

Variable names:

m,n,k:  natural numbers
a,b,c:  types of kind Nat

When overlapping, earlier rules take precedence (as in Haskell multi-equation definitions).

{ expr } is the value of the Haskell expression expr.