coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Question about encoding type system in Coq

From: Nadeem Abdul Hamid <nadeem AT acm.org>
To: David Nowak <David.Nowak AT lsv.ens-cachan.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: Question about encoding type system in Coq
Date: Thu, 06 Sep 2001 09:15:22 -0400
Organization: Yale University

> What's the type of alpha?

The type of alpha is nat. That is, ideally, I would want to do
something like this:

< Parameter alpha : nat.
< Eval Compute in (select ((alpha, 1)::nil) alpha).

and have it result in 1. Of course, the way select is currently
written, it won't do this. Maybe I can use some sort of
equality-related reasoning to define select, instead of cases and
"ifeq", but I don't know?

--- nadeem

Question about encoding type system in Coq, Nadeem Abdul Hamid
- Message not available
  - Re: Question about encoding type system in Coq, Nadeem Abdul Hamid