The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Merlin,

  I guess it’s a type inference issue here, what if you explicitly do [@map A demo] instead?
Cheers,
- Matthieu

Le sam. 20 janv. 2018 à 14:15, Merlin Göttlinger <megoettlinger AT gmail.com> a écrit :

Hi,

when using Program Fixpoint with a measure function the following works (typeckecks):

Program Fixpoint demo {A} (l : list A) {measure (length l)} : nat := 

  match l with

  | nil => 0

  | cons x x0 => fold_right plus 0 (map (fun e => demo e) [[x]; x0])

  end.

whereas the version where demo should be eta-expanded automatically does not work because of the added parameters of the measure function:

Program Fixpoint demo {A} (l : list A) {measure (length l)} : nat := 

  match l with

  | nil => 0

  | cons x x0 => fold_right plus 0 (map demo [[x]; x0])

  end.

Is there a trick to have Coq expand this automatically or a specific reason why it doesn't?

Cheers,

Merlin