The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hi Nathanaël,

I am not an expert on universe issues. But this is very strange, because 
it seems somehow specific to "map". I do not understand why.

Here is a little variant of your code that is accepted by Coq: it uses 
"fold_right" instead of "map".

Require Import Vpl.ImpureConfig.
Require Import Vpl.PedraQ.
Require Import List.
Definition f (x : unit) : imp unit := pure x.

Definition g := fold_right (fun x l => (f x)::l).

A variant with "fold_left" also works !

Moreover, the VPL already uses some higher-order iterator, see 
"swithAll" in
  https://github.com/VERIMAG-Polyhedra/VPL/blob/master/coq/AssignD.v

So, I do not understand where this issue comes from. I am also 
interested in any hint about this...

Thanks,

Sylvain.


Le 20/06/2018 à 10:09, Nathanaël Courant a écrit :
> Require Import ImpureConfig.
> Require Import PedraQ.
> Require Import List.
> Definition f (x : unit) : imp unit := pure x.
> Definition g l := map f l.