The Coq mailing list

[Benoit Montagu <benoit.montagu AT m4x.org>]

> Definition mapp (l:ZZNZ) (m:Map l) (r:ZZNZ) (n:Map zr) :
>                           Map (mappIndx l r) :=
>    match l, r return Map (mappIndx l r) with
>      | ZZ, ZZ => mx0
>      | NZ, ZZ => mconsl m n
>      | ZZ, NZ => mconsr m n
>      | NZ, NZ => mconsb m n
>    end.
>
> This last definition is not accepted.  How should this be defined?

The following definition works:

Definition mapp (l:ZZNZ) (m:Map l) (r:ZZNZ) (n:Map r) :
                         Map (mappIndx l r) :=
  match m in Map l', n in Map r' return Map (mappIndx l' r') with
    | mx0, mx0 => mx0
    | m', mx0 as n' => mconsl m' n'
    | mx0 as m', n' => mconsr m' n'
    | m', n' => mconsb m' n'
  end.

-- Benoit