Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • 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!




Archive powered by MhonArc 2.6.16.

Top of Page