The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Simple. Both x_nil and x_not_nil have different types. Those types, indeed, live in Prop, but that's a different story. So you're fixpoint is returning things from different types.

On Thu, Aug 1, 2013 at 6:05 PM, Nuno Gaspar <nmpgaspar AT gmail.com> wrote:

Hello.

Well, I'm having an hard time reproducing an example I was given. I think I can resume it to the following (I'm actually not sure my simplification didn't break the original problem...but heh)

Here follows:

Parameter l : list nat.
Parameter x_nil     : forall n:nat, In n nil.
Parameter x_not_nil : forall (n:nat), In n l.

Fixpoint test l  :=
  match l with
    nil      => x_nil
  | cons e r => x_not_nil
  end.

I imagine you can guess my doubt.. So why doesn't it typecheck? They both live in Prop...  -_-

How would go for making this typecheck? I'm sure it can be done..

Thank you fellas.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.