[Agda] change in operator syntax

[Sergei Meshveliani]

My current adventure is as follows.
I need my application to type-check in  14 Gb  in a reasonable time.
Among other attempts, I need to try  --sharing.  
And Kahl wrote that it has an effect in Development version
(what about Maint, Master ?).

I tried  Development. But its type checker reports a certain  internal
error
-- of which I reported today to Guthub.
This line is stuck, so far.
And I think now of returning to Agda 2.4.2.3.
Need I to try Maint ?

Also Development version suggests another treating of the operator
fixities.
It needs about 2 hours to modify my whole application code respectively.
But I have an impression that 
1) in Agda 2.4.2.3 they are treated in a (slightly) better way,
2) the Agda developers also have such impression (have they?).

Regards,

------
Sergei


On Fri, 2015-08-14 at 13:57 +0200, Andrea Vezzosi wrote:
> If you want to try the devel version of Agda without having to change
> too much about fixities you can pull from the freshly made
> def-fixities branch.
> 
> https://github.com/agda/agda/tree/def-fixities
> 
> I haven't merged this in the master because it breaks some of the test
> suite at the moment.
> However the general plan is to have default fixities back.
> 
> Cheers,
> Andrea
> 
> On Fri, Aug 14, 2015 at 11:22 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> > On Thu, 2015-08-13 at 16:21 -0400, Wolfram Kahl wrote:
> >> On Thu, Aug 13, 2015 at 11:06:31PM +0400, Sergei Meshveliani wrote:
> >> > I am trying the  Development Agda of  August 13, 2015.
> >> >
> >> > The attached code (25 nonempty lines) produces the report
> >> >
> >> > -----------------
> >> > Don't know how to parse _~_ Respects2 _≈_. Could mean any one of:
> >> >   _Respects2_ _~_ _≈_
> >> >   _Respects2_ _~_ _≈_
> >> >   _Respects2_ _~_ _≈_
> >> >   _Respects2_ _~_ _≈_
> >> > Operators used in the grammar:
> >> >   Respects2  (infix operator, unrelated)           [_Respects2_
> >> >   ...
> >> >   ...
> >> > -----------------
> >> >
> >> > What can be the matter about this?
> >>
> >> As far as I know, operator parsing in the development version is
> >> not yet settled, so it may change.
> >>
> >> The main effect of the current state that I can see is that infix operators
> >> without fixity declaration appear to be almost unusable.
> >> >From the ``unrelated'' in the message above,
> >> you see that Respects2 has no fixity declaration ---
> >> if you use your own version of _Respects2_ , just add a fixity declaration.
> >> If not, use the prefix application ``_Respects2_ _~_ _≈_''.
> >> (In some cases, additional parentheses are required, too.)
> >>
> >> (There seems to be no way to attach fixities to infix operators
> >>  used as variables in pattern / as arguments.)
> >>
> >>
> >> Hope this helps!
> >
> > Thank you.
> >
> > Now, I add
> >            infix 4 _Respects2_
> >
> > But it cannot parse  _~_ and _≈_  in  Respects2←→Respects₂gen, where
> > _~_ and _≈_  are given as variable arguments in a function.
> > Then I remove their fixity changing them to  ~ and ≈,  and this is
> > parsed.
> >
> > But generally:  if  _~_  is a variable argument in a function, then is
> > the programmer supposed to change it to  ~  and write (~ x y) instead of
> > (x ~ y)  everywhere in the body?
> >
> > Regards,
> >
> > ------
> > Sergei
> >
> >
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>