let rec example

[helm.git] / helm / matita / tests / letrec.ma

definition plus: nat \to nat \to nat \def
  let rec plus (n,m:nat) \def
    match n with
    [ O \Rightarrow m
    | (S x) \Rightarrow S (plus x m) ]
  in
  plus.