coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Depenednt types and equality proofs

From: Taral <taralx AT gmail.com>
To: Evgeny Makarov <emakarov AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Depenednt types and equality proofs
Date: Mon, 6 Sep 2010 12:27:08 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=Y9EWcwWo0K6wKNpfgH6PA4VbyWGD8xsI8gGB5Y/IuHP68gpDmIsBpjkK0Qa+dlF2II iZnaFhBBXgk838o12YsouzZHbRYAAMt0Z/nCFdPxMkHdXkqCHEC/FFBJ7iAXeTaF5ut7 //8NdhSVcVDhvjci315Ww3GOw7ScRpDUAhXK8=

On Thu, Sep 2, 2010 at 1:54 PM, Evgeny Makarov
<emakarov AT gmail.com>
wrote:
> Lemma mkThing_equal :
> �forall (from to : natSet) (n1 n2 : SignedNat)
> � �(n1_ok : natOK from to n1) (n2_ok : natOK from to n2),
> � � �n1 = n2 -> mkThing n1 n1_ok = mkThing n2 n2_ok.

When I try to inline this lemma, I get all kinds of type problems. Why?

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
� � -- Unknown

[Coq-Club] Depenednt types and equality proofs, Ian Lynagh
- Re: [Coq-Club] Depenednt types and equality proofs, Evgeny Makarov
  - Re: [Coq-Club] Depenednt types and equality proofs, Ian Lynagh
  - Re: [Coq-Club] Depenednt types and equality proofs, Taral