ssreflect - Re: [ssreflect] Canonical Structure not so canonical

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Canonical Structure not so canonical

From: Enrico Tassi <>
To:
Subject: Re: [ssreflect] Canonical Structure not so canonical
Date: Mon, 9 May 2016 17:04:26 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=None ; spf=None
Ironport-phdr: 9a23:UXsHih8fo6jya/9uRHKM819IXTAuvvDOBiVQ1KB91+IcTK2v8tzYMVDF4r011RmSDdSdsqgP1LqempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lS8iL1Y/oh6ibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V07NVaXKv+cq8kZblDFnEnNXo07YvqswPCRE2B/CgySGITxzdOGQnO61nGV4zqs2Ouu+xn2SKde9H/Vqs1cTWk9aZiDhHy3nRUfwUl+X3a35QjxJlQpwis8kRy

On Mon, May 09, 2016 at 12:57:33PM +0000, Georges Gonthier wrote:
> This way of proceeding lets you specify the structure with a
> regular type cast (or variable type declaration), which I think is
> more natural.

Are there other mechanisms that would be practical in your opinion? I
mean, even changing the system.

Maybe another way to put it is the following one.
Which is the natural notion of "context" that should drive inference?
The surrounding terms? Type annotations? Proof context? Variable
names?

Sorry for hijacking the thread...

Best,
--
Enrico Tassi

[ssreflect] Canonical Structure not so canonical, Florent Hivert, 05/08/2016
- RE: [ssreflect] Canonical Structure not so canonical, Georges Gonthier, 05/09/2016
  - Re: [ssreflect] Canonical Structure not so canonical, Enrico Tassi, 05/09/2016
  - Re: [ssreflect] Canonical Structure not so canonical, Florent Hivert, 05/09/2016
    - RE: [ssreflect] Canonical Structure not so canonical, Georges Gonthier, 05/09/2016
      - Re: [ssreflect] Canonical Structure not so canonical, Florent Hivert, 05/09/2016
        
        RE: [ssreflect] Canonical Structure not so canonical, Georges Gonthier, 05/10/2016

List archive

Re: [ssreflect] Canonical Structure not so canonical