coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: frank maltman <frank.maltman AT googlemail.com>
- To: Brandon Moore <brandon_m_moore AT yahoo.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Length indexed vector 'index'
- Date: Tue, 17 May 2011 03:51:30 +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=Uzx3JiVUm0q7zJC60g5dj4g5DGBGiD9qMWIVs76E6nAnitk5ON9XthzFFCVqBdeO4F m+ponYgQePtaMw0dL5m6KbAAG8LGCH6Yf9SfuB0cmfOJJ3ija9Rgbvkgb3dfgwoJcCCj xWUxTfylcZrViJo3yv/BJQnPVR2GzScnUrM64=
On Mon, 16 May 2011 12:52:12 -0700 (PDT)
Brandon Moore
<brandon_m_moore AT yahoo.com>
wrote:
>
> It might be a little more comprehensible if you write it out with more
> parentheses.
>
> You turn
>
> > fun i =>
> > ((match i in (F.finite b') return ((F.finite (pred b') -> A)
> > -> A) with
> > | F.FO _ => fun _ => x
> > | F.FS _ f' => fun index' => index' f'
> > end) (index xs))
>
> into
>
> > (fun i =>
> > (match i in (F.finite b') return ((F.finite (pred b') -> A)
> > -> A) with
> > | F.FO _ => fun _ => x
> > | F.FS _ f' => fun index' => index' f'
> > end)) (index xs)
>
> I hope it's less surprising that (fun x => (E g))
> can be rather different from (fun x => E), which is E[g/x]
Yes, I understand. 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
- Message not available
- 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
- Re: [Coq-Club] Length indexed vector 'index',
Adam Chlipala
- Re: [Coq-Club] Length indexed vector 'index',
frank maltman
- Re: [Coq-Club] Length indexed vector 'index',
Adam Chlipala
Archive powered by MhonArc 2.6.16.