[Agda] More aggressive `with`: Please check your Agda-2.4.2
developments!
Andrés Sicard-Ramírez
asr at eafit.edu.co
Mon Nov 30 03:30:48 CET 2015
On 22 November 2015 at 09:53, Sergei Meshveliani <mechvel at botik.ru> wrote:
> I have tried it on docon-A-0.03
> (see
> http://www.botik.ru/pub/local/Mechveliani/docon-A/0.03/
> ).
>
>
> agda-2.4.2.5 $agdaLibOpt +RTS -M3G -RTS Structures0.agda
>
> reports
>
> ------------
> ...
> Skipping OfMaps (/home/mechvel/doconA/0.03/source/OfMaps.agdai).
> piApply t = El {_getSort = Type (Max [Plus 1 (UnreducedLevel (Var 1
> []))]), unEl = Sort (Type (Max [Plus 0 (UnreducedLevel (Var 1 []))]))}
> args = [[]r(Var 0 [Proj Structures0.UpMagma.magma])]
> An internal error has occurred. Please report this as a bug.
> Location of the error: src/full/Agda/TypeChecking/Substitute.hs:374
I reported the issue in
https://github.com/agda/agda/issues/1725
--
Andrés
More information about the Agda
mailing list