Agda2> (agda2-status-action "") (agda2-info-action "*Type-checking*" "" nil) (agda2-highlight-clear) (agda2-info-action "*Type-checking*" "Checking Issue373 (Issue373.agda).\n" t) (agda2-info-action "*Type-checking*" "Finished Issue373.\n" t) (agda2-info-action "*Type-checking*" "Compiling Agda.Primitive in agda-default-include-path/Agda/Primitive.agdai to MAlonzo/Code/Agda/Primitive.hs\n" t) (agda2-info-action "*Type-checking*" "Compiling Issue373 in Issue373.agdai to MAlonzo/Code/Issue373.hs\n" t) (agda2-info-action "*Type-checking*" "Calling: ghc -O -o Issue373 -Werror -i -main-is MAlonzo.Code.Issue373 MAlonzo/Code/Issue373.hs --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns\n" t) (agda2-info-action "*Type-checking*" "[1 of 3] Compiling MAlonzo.RTE ( MAlonzo/RTE.hs, MAlonzo/RTE.o )\n" t) (agda2-info-action "*Type-checking*" "[2 of 3] Compiling Imports.Nat ( Imports/Nat.hs, Imports/Nat.o )\n" t) (agda2-info-action "*Type-checking*" "[3 of 3] Compiling MAlonzo.Code.Issue373 ( MAlonzo/Code/Issue373.hs, MAlonzo/Code/Issue373.o )\n" t) (agda2-info-action "*Type-checking*" "Linking Issue373 ...\n" t) (agda2-status-action "Checked") (agda2-info-action "*Compilation result*" "The module was successfully compiled." nil) ((last . 1) . (agda2-goals-action '())) Agda2> ok