[Agda] records in mutual blocks

Thorsten Altenkirch txa at Cs.Nott.AC.UK
Wed May 11 17:58:01 CEST 2011


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


More information about the Agda mailing list