The Coq mailing list

[Michel Levy <Michel.Levy AT imag.fr>]

I have tried the following definition of minimum of two naturals numbers
(I know it's already defined in Min Module).
Require Compare_dec.
Definition minl :=[n,m:nat] Cases (le_let_dec n m) of
(left x) => n | (right x) => m end.

Extraction "min_opt.ml" minl.
In the program extracted I find 

let le_lt_dec n =
  let rec f = function
    O -> (fun m -> Left)
  | S n1 -> (fun m ->
      let rec f0 = function
        O -> Right
      | S n3 -> (match f n1 n3 with
                   Left -> Left
                 | Right -> Right)
      in f0 m)
  in f n

Why (match f n1 n3 with Left -> Left | Right -> Right) is no replaced by
(f n1 n3) ?


-- 
Michel Levy
36 rue George Sand 38400 Saint Martin d'Hères
email : 
Michel.Levy AT imag.fr
http://www-lsr.imag.fr/users/Michel.Levy/