[Agda] Re: records in mutual blocks
Andreas Abel
andreas.abel at ifi.lmu.de
Wed May 11 18:28:15 CEST 2011
The darcs version does allow this. Otherwise
test/succeed/RecordInMutual.agda
would fail.
Check
make test
Andreas
On 5/11/11 5:58 PM, Thorsten Altenkirch wrote:
> How come that the current version (2.2.11) complains about records in mutual blocks. I though that checks was disabled
> after last AIM?
>
> Thorsten
>
> Prelude> :set -package Agda-2.2.11
> ...
> Prelude Agda.Interaction.GhciTop> ioTCM "/Users/txa/Drafts/OmegaCats/Experimental/Syntax.agda" (Just "/var/folders/ds/dsbEn-JbGfOiTcI0+vCoNU+++TI/-Tmp-/agda2-mode1800Kav") ( cmd_load "/Users/txa/Drafts/OmegaCats/Experimental/Syntax.agda" [".", "/Users/txa/Agda/lib/src/"] )
> agda2_mode_code (agda2-status-action "")
> Checking Syntax (/Users/txa/Drafts/OmegaCats/Experimental/Syntax.agda).
> agda2_mode_code (agda2-info-action
> "*Error*"
> "/Users/txa/Drafts/OmegaCats/Experimental/Syntax.agda:14,3-18,20
> Record types are not allowed in mutual blocks")
> agda2_mode_code (annotation-goto
> '("/Users/txa/Drafts/OmegaCats/Experimental/Syntax.agda" . 242))
> agda2_mode_code (agda2-status-action "")
> *** Exception: ExitFailure 1
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list