coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Length indexed vector 'index'

From: frank maltman <frank.maltman AT googlemail.com>
To: Adam Chlipala <adam AT chlipala.net>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Length indexed vector 'index'
Date: Tue, 17 May 2011 13:46:40 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:cc:subject:message-id:in-reply-to:references:x-mailer :mime-version:content-type:content-transfer-encoding; b=x2wCQyEqFC1rua0Oe2pUrysT4v9NiwffSmdO1Emnkqjf9N9fcivKf+JVHgZ5JpUEVm w3PS393DeGnr8iFA95AODkQhDzcW9ZBJW9ZUOaKjJjurY2BBwqRUkOpL7IR+DXdJJaTy 0itktVzkCRVIiOt8QQzLALeAV/lsNXk2ZBFHQ=

On Tue, 17 May 2011 09:36:39 -0400
Adam Chlipala
<adam AT chlipala.net>
wrote:
>
> Yup, and here's one way of doing so:
>

Argh! I'm an idiot...

> Definition get {A : Set} (f : finite 4) (c : contrived A) : A :=
>    match c with
>      | C n0 n1 n2 n3 =>
>        match finite_nat f as n return n < 4 -> A with
                                        ^^^^^
I kept writing 'finite_nat f' instead of just 'n' as the
term. Obviously this didn't match what the theorem expected
as an argument...

Thanks!

[Coq-Club] Length indexed vector 'index', frank maltman
- Re: [Coq-Club] Length indexed vector 'index', Adam Chlipala
  - Re: [Coq-Club] Length indexed vector 'index', frank maltman
    - Message not available
      - Re: [Coq-Club] Length indexed vector 'index', frank maltman
  - Re: [Coq-Club] Length indexed vector 'index', frank maltman
    - Re: [Coq-Club] Length indexed vector 'index', Matthieu Sozeau
    - Re: [Coq-Club] Length indexed vector 'index', Brandon Moore
      - Re: [Coq-Club] Length indexed vector 'index', frank maltman
  - Re: [Coq-Club] Length indexed vector 'index', frank maltman
    - Re: [Coq-Club] Length indexed vector 'index', Adam Chlipala
      - Re: [Coq-Club] Length indexed vector 'index', frank maltman