coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Finite set to list

From: Marco Servetto <marco.servetto AT gmail.com>
To: Christian Doczkal <doczkal AT ps.uni-saarland.de>
Cc: Vincent BENAYOUN <benayoun.vincent AT gmail.com>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Finite set to list
Date: Tue, 30 Apr 2013 07:08:03 +1200

I do not understand two things here:
First
>>Definition X (n : nat) : Ensemble unit
>>:= fun _ => …
>> (*stating that the nth Turing Machine halts on any input *).
How can such function be accepted by coq? i.e. only provable
terminable functions can be defined, thus the halting problem stop us
here.

Second:
Is not a finite set (over elements with ordering) isomorph to an
ordered list with no repetition?
Marco.

[Coq-Club] Finite set to list, Vincent BENAYOUN, 04/25/2013
- Re: [Coq-Club] Finite set to list, AUGER Cédric, 04/25/2013
- Re: [Coq-Club] Finite set to list, Christian Doczkal, 04/25/2013
  - Re: [Coq-Club] Finite set to list, Marco Servetto, 04/29/2013
    - Re: [Coq-Club] Finite set to list, Daniel Schepler, 04/30/2013
- Re: [Coq-Club] Finite set to list, Daniel Schepler, 04/25/2013
- Re: [Coq-Club] Finite set to list, Pierre Courtieu, 04/25/2013
- Re: [Coq-Club] Finite set to list, Frédéric Blanqui, 04/26/2013