[Agda] How to typecheck "How to keep your Neighbours in Order" in the latest version of Agda

[Martin Stone Davis]

Thanks for that. Unfortunately, even with those modifications (updated here
<http://lpaste.net/143728>), it's still not quite right. The first error is:

Pivotal.lagda:213,5: Parse error
> constructor<ERROR>
>  it  -- no fields!
> \end{code}
> ...
>

--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com

On Thu, Oct 22, 2015 at 8:07 PM, effectfully <effectfully at gmail.com> wrote:

> See here
> https://lists.chalmers.se/pipermail/agda-dev/2015-January/000048.html
>
> 2015-10-23 5:38 GMT+03:00, Martin Stone Davis <
> martin.stone.davis at gmail.com>:
> > Would someone help me get Conor's McBride's code to typecheck? I'm trying
> > to follow "How to keep your Neighbours in Order", but, unfortunately, the
> > following definition does not work in Agda 2.4.2.4:
> >
> > _:-_ : forall {P T} -> <P P P> -> (P => T) -> T
> >> ! :- t = t
> >>
> >
> > The error is:
> >
> > Instance search can only be used to find elements in a named type
> >> when checking that the expression t has type .T
> >>
> >
> > The complete source can be found in
> > https://github.com/pigworker/Pivotal/blob/master/Pivotal.lagda; the
> > particular definition at line 266. In case it helps, I've made a copy
> here
> > <http://lpaste.net/143668>.
> > --
> > Martin Stone Davis
> > ps
> > Postal/Residential:
> > 1223 Ferry St
> > Apt 5
> > Eugene, OR 97401
> > Talk / Text / Voicemail: (310) 699-3578 <3106993578>
> > Electronic Mail: martin.stone.davis at gmail.com
> > Website: martinstonedavis.com
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151023/3fdb68ff/attachment.html