Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] should typecheck... right

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] should typecheck... right


Chronological Thread 
  • From: Beta Ziliani <beta AT mpi-sws.org>
  • To: Nuno Gaspar <nmpgaspar AT gmail.com>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] should typecheck... right
  • Date: Thu, 1 Aug 2013 18:18:12 +0200

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.




Archive powered by MHonArc 2.6.18.

Top of Page