-definition minus:
- nat \to (nat \to nat)
-\def
- let rec minus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n
-with [O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k)
-| (S l) \Rightarrow (minus k l)])])) in minus.
+let rec minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with
+[O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k) | (S
+l) \Rightarrow (minus k l)])]).