coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] an inductive types question (2)

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Coq Club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] an inductive types question (2)
Date: Tue, 20 Oct 2009 12:24:36 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Given an inductive type such as

Inductive two_el := el_1 | el_2 .

are there closed terms of type two_el which do not reduce to either el_1 or el_2 ?

Vladimir.

[Coq-Club] A not so FSet specific question about destruction, Thomas Braibant
- Re: [Coq-Club] A not so FSet specific question about destruction, St�phane Lescuyer
  - Re: [Coq-Club] A not so FSet specific question about destruction, Guillaume Melquiond
    - Re: [Coq-Club] A not so FSet specific question about destruction, St�phane Lescuyer
- Re: [Coq-Club] A not so FSet specific question about destruction, Matthieu Sozeau
- [Coq-Club] an inductive types question (2), Vladimir Voevodsky
  - Re: [Coq-Club] an inductive types question (2), Adam Chlipala
  - Re: [Coq-Club] an inductive types question (2), Cody Roux
    - Re: [Coq-Club] an inductive types question (2), Vladimir Voevodsky
      - Re: [Coq-Club] an inductive types question (2), Cody Roux
        
        Re: [Coq-Club] an inductive types question (2), Vladimir Voevodsky
        
        Re: [Coq-Club] an inductive types question (2), muad
        
        Re: [Coq-Club] an inductive types question (2), Cody Roux