From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <lukstafi@gmail.com>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83])
	by sympa.inria.fr (Postfix) with ESMTPS id 600AA7EE99
	for <caml-list@sympa.inria.fr>; Tue, 10 Dec 2013 14:20:51 +0100 (CET)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  lukstafi@gmail.com) identity=pra; client-ip=74.125.82.174;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="lukstafi@gmail.com";
  x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible
Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of
  lukstafi@gmail.com designates 74.125.82.174 as permitted
  sender) identity=mailfrom; client-ip=74.125.82.174;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="lukstafi@gmail.com";
  x-sender="lukstafi@gmail.com"; x-conformance=sidf_compatible;
  x-record-type="v=spf1"
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@mail-we0-f174.google.com) identity=helo;
  client-ip=74.125.82.174;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="lukstafi@gmail.com";
  x-sender="postmaster@mail-we0-f174.google.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Ag8DAMsUp1JKfVKulGdsb2JhbABZhBK5GoETCBYOAQEBAQcLCwkSKoIcCQEBBAFAARseAwELBgUDAQc7IQEBEQEFARwGE4dvAQMJBqUUjFmDCYRCChknDWSGAxEBBQyMZ4IZhDQElimBa4xag0wYKYRWOw
X-IPAS-Result: Ag8DAMsUp1JKfVKulGdsb2JhbABZhBK5GoETCBYOAQEBAQcLCwkSKoIcCQEBBAFAARseAwELBgUDAQc7IQEBEQEFARwGE4dvAQMJBqUUjFmDCYRCChknDWSGAxEBBQyMZ4IZhDQElimBa4xag0wYKYRWOw
X-IronPort-AV: E=Sophos;i="4.93,865,1378850400"; 
   d="scan'208";a="48047238"
Received: from mail-we0-f174.google.com ([74.125.82.174])
  by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 10 Dec 2013 14:20:51 +0100
Received: by mail-we0-f174.google.com with SMTP id q58so4975552wes.33
        for <caml-list@inria.fr>; Tue, 10 Dec 2013 05:20:50 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=mime-version:in-reply-to:references:from:date:message-id:subject:to
         :content-type;
        bh=AmEfmhHnwxo0C8goh+tr9yIE00u18b5DcpMFV+CdkZQ=;
        b=DXDyUITdRrIeX/HnD2eSBlgR739VLrRZcSxn+5jI4Jc9OngGoxXEVSbClsoipPrPvY
         ZxI+3I/epAek46D8KhW6FkOiAuF/wCUycViOcjzG17cGIugq3+zTJoNYtGoQk1GBBBjB
         XuZDPZMcIlMMz+rYquihXdSSwSkE70AgaBTL/wT5dOqFigUJkBsUyvIuTbeB5AX6IHRu
         JgR74fIm+CHPxF/eJ4Euuzz59KfqjuSGdWNO7UoCdq4pIm3dGdqLDwFsOTcvr7JzXBcz
         ltdaf0Jh37xJQWK4HT2HjEs3lhPZIHiHViCUbPDvYo/ORfrjFheNtnisu42QlLoMdp8J
         gMtw==
X-Received: by 10.180.108.132 with SMTP id hk4mr19592547wib.12.1386681650340;
 Tue, 10 Dec 2013 05:20:50 -0800 (PST)
MIME-Version: 1.0
Received: by 10.227.36.201 with HTTP; Tue, 10 Dec 2013 05:20:30 -0800 (PST)
In-Reply-To: <CAJMfKEWEcbFaQs2fPRj9xah+RTSkpmywpg2fsbusmacndViXQg@mail.gmail.com>
References: <CAJMfKEWLZdj8ceGxOUU=uUFdrH8aE+emiY5_eLfOHzfqoPwpqA@mail.gmail.com>
 <CAJMfKEU6=ddcuFHj909L9kU0B1jN3kYm-aXY24th8b6vtaV9_A@mail.gmail.com> <CAJMfKEWEcbFaQs2fPRj9xah+RTSkpmywpg2fsbusmacndViXQg@mail.gmail.com>
From: Lukasz Stafiniak <lukstafi@gmail.com>
Date: Tue, 10 Dec 2013 14:20:30 +0100
Message-ID: <CAJMfKEUWRYj5w23-3EOSJuoMGhuAX+164rAE_+fKwvArfYA4hw@mail.gmail.com>
To: Caml <caml-list@inria.fr>
Content-Type: multipart/alternative; boundary=e89a8f3baad52f6c4a04ed2dfbbf
Subject: Re: [Caml-list] Polymorphic recursion and GADTs

--e89a8f3baad52f6c4a04ed2dfbbf
Content-Type: text/plain; charset=ISO-8859-1

On Mon, Dec 9, 2013 at 10:34 PM, Lukasz Stafiniak <lukstafi@gmail.com>wrote:

> The annotation needs to be directly at the "function" node:
>
>
Even better: no (additional) annotation is needed if I export the
beta-redex as a match clause.

--e89a8f3baad52f6c4a04ed2dfbbf
Content-Type: text/html; charset=ISO-8859-1

<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Mon, Dec 9, 2013 at 10:34 PM, Lukasz Stafiniak <span dir="ltr">&lt;<a href="mailto:lukstafi@gmail.com" target="_blank">lukstafi@gmail.com</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">The annotation needs to be directly at the &quot;function&quot; node:<div><br></div></div></blockquote>
<div>
<br></div><div>Even better: no (additional) annotation is needed if I export the beta-redex as a match clause.</div></div></div></div>

--e89a8f3baad52f6c4a04ed2dfbbf--