[Agda] installing/using 2.6.0-207bde6

[G. Allais]

Hi Sergey,

The problem does not lie with Ulf's Prelude or Agda's standard
library but rather with Agda itself. You need to upgrade to
(at least) the commit Ulf is pointing at.

Alternatively you could wait a bit and port your library to the
next stable version which is about to be released. The installation
instructions for your users will then be a lot simpler (basically:
cabal install Agda-2.5.3).

Cheers,
--
gallais

On 14/08/17 17:32, Sergei Meshveliani wrote:
> On Mon, 2017-08-14 at 16:41 +0200, Ulf Norell wrote:
>>
>>
>> On Mon, Aug 14, 2017 at 2:46 PM, Sergei Meshveliani <mechvel at botik.ru>
>> wrote:
>>         
>>            and added there import of `compare' and DivMod of Agda
>>         Prelude.
>>         
>>         This caused the necessity to add
>>              import Prelude.String
>>              import Prelude.Nat
>>         
>>         to many files in the application.
>>
>>
>> This problem was fixed in issue #2641 [1] (commit 64cc2b3). You should
>> no longer need the imports of the Prelude modules.
>>
>>
>> / Ulf
>>
>>
>> [1] https://github.com/agda/agda/issues/2641 
> 
> 
> My  install.txt  needs to explain plainly:  
> where to take this needed (improved) Agda Prelude version 
> (for Agda 2.6.0-207bde6).
> 
> Is it by 
>       git clone https://github.com/UlfNorell/agda-prelude
> ?
> 
> Thanks,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170815/7d718453/attachment.sig>