coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: roconnor AT theorem.ca
- To: Adam Chlipala <adamc AT cs.berkeley.edu>
- Cc: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Dependently-typed binary operators
- Date: Tue, 13 Sep 2005 01:23:09 -0400 (EDT)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Mon, 12 Sep 2005, Adam Chlipala wrote:
> e1 : Bvector 32
> e2 : Bvector 32
> ============================
> (beven e1 || beven e2) = beven (band32 e1 e2)
>
> destruct e1.
>
> I get the error:
>
> User error: Cannot solve a second-order unification problem
>
> Can anyone suggest how I might go about proving this goal?
Think about what the two goals will be after the destruct. Write out what
they are. Then you will realize it will be neccesary to
unfold band32.
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
- [Coq-Club] Dependently-typed binary operators, Adam Chlipala
- Re: [Coq-Club] Dependently-typed binary operators, roconnor
- Re: [Coq-Club] Dependently-typed binary operators,
roconnor
- Re: [Coq-Club] Dependently-typed binary operators, Pierre Casteran
- Re: [Coq-Club] Dependently-typed binary operators,
Conor McBride
- Re: [Coq-Club] Dependently-typed binary operators,
roconnor
- Re: [Coq-Club] Dependently-typed binary operators, Conor McBride
- Re: [Coq-Club] Dependently-typed binary operators,
roconnor
- Re: [Coq-Club] Dependently-typed binary operators,
roconnor
- Re: [Coq-Club] Dependently-typed binary operators, Frederic Blanqui
- Re: [Coq-Club] Dependently-typed binary operators, roconnor
Archive powered by MhonArc 2.6.16.