Directory listing for Agda-2.3.2.2 source tarball
Agda-2.3.2.2/test/fail/
- .cvsignore
- AbsToConDecl.agda
- AbsToConDecl.err
- Abstract.agda
- Abstract.err
- AbstractBlockInLet.agda
- AbstractBlockInLet.err
- AbsurdPatternRequiresNoRHS.agda
- AbsurdPatternRequiresNoRHS.err
- AgdalightTelescopeSyntax.agda
- AgdalightTelescopeSyntax.err
- AmbiguousModule.agda
- AmbiguousModule.err
- AmbiguousName.agda
- AmbiguousName.err
- AmbiguousParseForApplication.agda
- AmbiguousParseForApplication.err
- AmbiguousParseForLHS.agda
- AmbiguousParseForLHS.err
- AmbiguousTopLevelModuleName.agda
- AmbiguousTopLevelModuleName.err
- BadInductionRecursion1.agda
- BadInductionRecursion1.err
- BadInductionRecursion2.agda
- BadInductionRecursion2.err
- BadInductionRecursion3.agda
- BadInductionRecursion3.err
- BadTermination.agda
- BadTermination.err
- BoundedSizeNoMatch.agda
- BoundedSizeNoMatch.err
- BrokenInferenceDueToNonvariantPolarity.agda
- BrokenInferenceDueToNonvariantPolarity.err
- BuiltinConstructorsNeededForLiterals.agda
- BuiltinConstructorsNeededForLiterals.err
- BuiltinInParameterisedModule.agda
- BuiltinInParameterisedModule.err
- BuiltinMustBeConstructor.agda
- BuiltinMustBeConstructor.err
- CantOpenConstructorsFromRecordModule.agda
- CantOpenConstructorsFromRecordModule.err
- CheckSizeMetaBounds.agda
- CheckSizeMetaBounds.err
- ClashingDefinition.agda
- ClashingDefinition.err
- ClashingImport.agda
- ClashingImport.err
- ClashingModule.agda
- ClashingModule.err
- ClashingModuleImport.agda
- ClashingModuleImport.err
- Codata.agda
- Codata.err
- CoinductiveBuiltinList.agda
- CoinductiveBuiltinList.err
- CoinductiveBuiltinNatural.agda
- CoinductiveBuiltinNatural.err
- CoinductiveConstructorsAndLet.agda
- CoinductiveConstructorsAndLet.err
- CoinductiveUnitRecord.agda
- CoinductiveUnitRecord.err
- ColistMutual.agda
- ColistMutual.err
- CompiledMustBePostulate.agda
- CompiledMustBePostulate.err
- CompiledMustHaveHaskellType.agda
- CompiledMustHaveHaskellType.err
- ComplexIMPORT.agda
- ComplexIMPORT.err
- ConstructorHeadedDivergenceIn2-2-10.agda
- ConstructorHeadedDivergenceIn2-2-10.err
- CopatternCheckingNYI.agda
- CopatternCheckingNYI.err
- CopatternNonterminating.agda
- CopatternNonterminating.err
- CopatternWithoutFieldName.agda
- CopatternWithoutFieldName.err
- CorrectPrintingOfVariablesInSortCheckingForData.agda
- CorrectPrintingOfVariablesInSortCheckingForData.err
- Crash.agda
- Crash.err
- CyclicModuleDependency.agda
- CyclicModuleDependency.err
- DataParameterPolarity.agda
- DataParameterPolarity.err
- DataRecordCoinductive.agda
- DataRecordCoinductive.err
- DifferentArities.agda
- DifferentArities.err
- DoNotFireLiteralCatchAllForNeutrals.agda
- DoNotFireLiteralCatchAllForNeutrals.err
- DontPrune.agda
- DontPrune.err
- DuplicateBuiltinBinding.agda
- DuplicateBuiltinBinding.err
- DuplicateConstructors.agda
- DuplicateConstructors.err
- DuplicateFields.agda
- DuplicateFields.err
- EmptyInductiveRecord.agda
- EmptyInductiveRecord.err
- ExistentialsProjections.agda
- ExistentialsProjections.err
- FakeProjectionsDoNotPreserveGuardedness.agda
- FakeProjectionsDoNotPreserveGuardedness.err
- FileNotFound.agda
- FileNotFound.err
- FixityOutOfScopeInRecord.agda
- FixityOutOfScopeInRecord.err
- FrozenMVar.agda
- FrozenMVar.err
- FrozenMVar2.agda
- FrozenMVar2.err
- IllegalUseOfIrrelevantDeclaration.agda
- IllegalUseOfIrrelevantDeclaration.err
- IlltypedPattern.agda
- IlltypedPattern.err
- ImplicitRecordFields.agda
- ImplicitRecordFields.err
- ImportInMutual.agda
- ImportInMutual.err
- Impossible.agda
- Impossible.err
- IncompletePatternMatching.agda
- IncompletePatternMatching.err
- IndentedCheckingMessages.agda
- IndentedCheckingMessages.err
- IndentedCheckingMessages.flags
- InductiveAndCoinductiveConstructors.err
- InferRecordTypes-1.agda
- InferRecordTypes-1.err
- InferRecordTypes-2.agda
- InferRecordTypes-2.err
- InferRecordTypes-3.agda
- InferRecordTypes-3.err
- InferRecordTypes-4.agda
- InferRecordTypes-4.err
- Inference-of-implicit-function-space.agda
- Inference-of-implicit-function-space.err
- InjectiveTypeConstructors.agda
- InjectiveTypeConstructors.err
- InstanceArgumentsAmbiguous.agda
- InstanceArgumentsAmbiguous.err
- InstanceArgumentsBraceSpaces.agda
- InstanceArgumentsBraceSpaces.err
- InstanceArgumentsModNotParameterised.agda
- InstanceArgumentsModNotParameterised.err
- InstanceArgumentsNotFound.agda
- InstanceArgumentsNotFound.err
- Interaction-and-input-file.agda
- Interaction-and-input-file.err
- Interaction-and-input-file.flags
- IrrelevantData.agda
- IrrelevantData.err
- IrrelevantFamilyIndex.agda
- IrrelevantFamilyIndex.err
- IrrelevantFin.agda
- IrrelevantFin.err
- IrrelevantIndexNotInconsistent.agda
- IrrelevantIndexNotInconsistent.err
- IrrelevantLambda.agda
- IrrelevantLambda.err
- IrrelevantLevelHurkens.agda
- IrrelevantLevelHurkens.err
- IrrelevantLevelToSet.agda
- IrrelevantLevelToSet.err
- IrrelevantMatchRefl.agda
- IrrelevantMatchRefl.err
- IrrelevantModuleParameter.agda
- IrrelevantModuleParameter.err
- IrrelevantModuleParameter1.agda
- IrrelevantModuleParameter1.err
- IrrelevantProjections.agda
- IrrelevantProjections.err
- IrrelevantRecordField.agda
- IrrelevantRecordField.err
- IrrelevantRecordMatching.agda
- IrrelevantRecordMatching.err
- IrrelevantTelescope.agda
- IrrelevantTelescope.err
- IrrelevantTelescopeRecord.agda
- IrrelevantTelescopeRecord.err
- IrrelevantVar.agda
- IrrelevantVar.err
- Issue113.agda
- Issue113.err
- Issue118Comment9.agda
- Issue118Comment9.err
- Issue121.agda
- Issue121.err
- Issue127.agda
- Issue127.err
- Issue138.err
- Issue154.agda
- Issue154.err
- Issue160.agda
- Issue160.err
- Issue183.agda
- Issue183.err
- Issue202.agda
- Issue202.err
- Issue203.agda
- Issue203.err
- Issue203b.agda
- Issue203b.err
- Issue205.agda
- Issue205.err
- Issue206.agda
- Issue206.err
- Issue215.agda
- Issue215.err
- Issue216.agda
- Issue216.err
- Issue217.agda
- Issue217.err
- Issue228.agda
- Issue228.err
- Issue249-2.agda
- Issue249-2.err
- Issue249.agda
- Issue249.err
- Issue256.agda
- Issue256.err
- Issue260a.agda
- Issue260a.err
- Issue260b.agda
- Issue260b.err
- Issue260c.agda
- Issue260c.err
- Issue260d.agda
- Issue260d.err
- Issue274.agda
- Issue274.err
- Issue278.agda
- Issue278.err
- Issue279-2.agda
- Issue279-2.err
- Issue279.agda
- Issue279.err
- Issue280.agda
- Issue280.err
- Issue291a.agda
- Issue291a.err
- Issue291b.agda
- Issue291b.err
- Issue292.agda
- Issue292.err
- Issue292b.err
- Issue292c.agda
- Issue292c.err
- Issue292d.agda
- Issue292d.err
- Issue295.agda
- Issue295.err
- Issue308a.agda
- Issue308a.err
- Issue308b.agda
- Issue308b.err
- Issue309a.agda
- Issue309a.err
- Issue309b.agda
- Issue309b.err
- Issue318.agda
- Issue318.err
- Issue328.agda
- Issue328.err
- Issue329.agda
- Issue329.err
- Issue329b.agda
- Issue329b.err
- Issue329c.agda
- Issue329c.err
- Issue332.agda
- Issue332.err
- Issue334.agda
- Issue334.err
- Issue347.agda
- Issue347.err
- Issue351a.agda
- Issue351a.err
- Issue357.agda
- Issue357.err
- Issue380.agda
- Issue380.err
- Issue381.agda
- Issue381.err
- Issue390.agda
- Issue390.err
- Issue390.flags
- Issue392.agda
- Issue392.err
- Issue399.agda
- Issue399.err
- Issue402.agda
- Issue402.err
- Issue413.agda
- Issue413.err
- Issue418.agda
- Issue418.err
- Issue424.agda
- Issue424.err
- Issue427.agda
- Issue427.err
- Issue444.agda
- Issue444.err
- Issue452.agda
- Issue452.err
- Issue461.agda
- Issue461.err
- Issue464.agda
- Issue464.err
- Issue476a.agda
- Issue476a.err
- Issue476b.agda
- Issue476b.err
- Issue476c.agda
- Issue476c.err
- Issue476d.agda
- Issue476d.err
- Issue477.agda
- Issue477.err
- Issue477b.agda
- Issue477b.err
- Issue478.agda
- Issue478.err
- Issue478b.agda
- Issue478b.err
- Issue478c.agda
- Issue478c.err
- Issue481.agda
- Issue481.err
- Issue481InstantiatedImportOnly.agda
- Issue481InstantiatedImportOnly.err
- Issue481NonExistentModule.agda
- Issue481NonExistentModule.err
- Issue481a.agda
- Issue481a.err
- Issue483.agda
- Issue483.err
- Issue483a.agda
- Issue483a.err
- Issue483b.agda
- Issue483b.err
- Issue483c.agda
- Issue483c.err
- Issue484.agda
- Issue484.err
- Issue485.agda
- Issue485.err
- Issue503.agda
- Issue503.err
- Issue512.agda
- Issue512.err
- Issue526.agda
- Issue526.err
- Issue530.agda
- Issue530.err
- Issue543.agda
- Issue543.err
- Issue546.agda
- Issue546.err
- Issue549.agda
- Issue549.err
- Issue551.agda
- Issue551.err
- Issue551a.agda
- Issue551a.err
- Issue555.agda
- Issue555.err
- Issue555a.agda
- Issue555a.err
- Issue555b.agda
- Issue555b.err
- Issue555c.agda
- Issue555c.err
- Issue562.agda
- Issue562.err
- Issue580.agda
- Issue580.err
- Issue585-11.agda
- Issue585-11.err
- Issue585.agda
- Issue585.err
- Issue585t.agda
- Issue585t.err
- Issue586.agda
- Issue586.err
- Issue586.flags
- Issue610-4.agda
- Issue610-4.err
- Issue610.agda
- Issue610.err
- Issue62.agda
- Issue62.err
- Issue628.agda
- Issue628.err
- Issue631.agda
- Issue631.err
- Issue636.agda
- Issue636.err
- Issue644.agda
- Issue644.err
- Issue659.agda
- Issue659.err
- Issue676.agda
- Issue676.err
- Issue689.agda
- Issue689.err
- Issue690.agda
- Issue690.err
- Issue690a.agda
- Issue690a.err
- Issue691.agda
- Issue691.err
- Issue705.agda
- Issue705.err
- Issue719.agda
- Issue719.err
- Issue721a.agda
- Issue721a.err
- Issue721b.agda
- Issue721b.err
- Issue721c.agda
- Issue721c.err
- Issue723.agda
- Issue723.err
- Issue735.agda
- Issue735.err
- Issue738.agda
- Issue738.err
- Issue87.agda
- Issue87.err
- JasonReedPruning.agda
- JasonReedPruning.err
- LetPair.agda
- LetPair.err
- LevelLiterals.agda
- LevelLiterals.err
- LevelUnification.agda
- LevelUnification.err
- LocalVsImportedModuleClash.agda
- LocalVsImportedModuleClash.err
- LostTypeError.agda
- LostTypeError.err
- LostTypeError2.agda
- LostTypeError2.err
- MagicWith.agda
- MagicWith.err
- Makefile
- MalformedModuleNameInIMPORT.agda
- MalformedModuleNameInIMPORT.err
- MatchOnIrrelevantData1.agda
- MatchOnIrrelevantData1.err
- MetaAppUnderLambda.agda
- MetaAppUnderLambda.err
- MetaCannotDependOn.agda
- MetaCannotDependOn.err
- MetaOccursInItself.agda
- MetaOccursInItself.err
- MisformedTypeSignature.agda
- MisformedTypeSignature.err
- MissingDefinition.agda
- MissingDefinition.err
- MissingTypeSignature.agda
- MissingTypeSignature.err
- MissingTypeSignatureInMutual.agda
- MissingTypeSignatureInMutual.err
- MissingWithClauses.agda
- MissingWithClauses.err
- ModuleArityMismatch.agda
- ModuleArityMismatch.err
- ModuleDefinedInOtherFile.agda
- ModuleDefinedInOtherFile.err
- ModuleDoesntExport.agda
- ModuleDoesntExport.err
- ModuleInMutual.agda
- ModuleInMutual.err
- ModuleNameDoesntMatchFileName.agda
- ModuleNameDoesntMatchFileName.err
- MultipleFixityDecl.agda
- MultipleFixityDecl.err
- NaturalAndLevelDifferent.agda
- NaturalAndLevelDifferent.err
- NeedOptionCopatterns.agda
- NeedOptionCopatterns.err
- Negative1.agda
- Negative1.err
- Negative2.agda
- Negative2.err
- Negative3.agda
- Negative3.err
- Negative4.agda
- Negative4.err
- Negative5.agda
- Negative5.err
- NoBindingForBuiltin.agda
- NoBindingForBuiltin.err
- NoNoTerminationCheck.agda
- NoNoTerminationCheck.err
- NoPanic.agda
- NoPanic.err
- NoParseForApplication.agda
- NoParseForApplication.err
- NoParseForLHS.agda
- NoParseForLHS.err
- NoRHSRequiresAbsurdPattern.agda
- NoRHSRequiresAbsurdPattern.err
- NoSuchBuiltinName.agda
- NoSuchBuiltinName.err
- NoSuchModule.agda
- NoSuchModule.err
- NoSuchPrimitiveFunction.agda
- NoSuchPrimitiveFunction.err
- NoTerminationCheck1.agda
- NoTerminationCheck1.err
- NoTerminationCheck2.agda
- NoTerminationCheck2.err
- NoTerminationCheck3.agda
- NoTerminationCheck3.err
- NoTerminationCheck4.agda
- NoTerminationCheck4.err
- NonDependentConstructorType.agda
- NonDependentConstructorType.err
- NonLinearConstraint.agda
- NonLinearConstraint.err
- NotAModuleExpr.agda
- NotAModuleExpr.err
- NotAValidLetBinding.agda
- NotAValidLetBinding.err
- NotAnExpression.agda
- NotAnExpression.err
- NotApplyingInDontCareTriggersInternalError.agda
- NotApplyingInDontCareTriggersInternalError.err
- NotInScope.agda
- NotInScope.err
- NotLeqSort.agda
- NotLeqSort.err
- NotStrictlyPositive.agda
- NotStrictlyPositive.err
- NotStrictlyPositiveInMutual.agda
- NotStrictlyPositiveInMutual.err
- NotStronglyRigidOccurrence.agda
- NotStronglyRigidOccurrence.err
- NothingAppliedToHiddenArg.agda
- NothingAppliedToHiddenArg.err
- OccursCheck.agda
- OccursCheck.err
- OccursCheck1.agda
- OccursCheck1.err
- OpenInMutual.agda
- OpenInMutual.err
- OpenPublicPlusTypeError.agda
- OpenPublicPlusTypeError.err
- ParseError.agda
- ParseError.err
- ParseForallAbsurd.agda
- ParseForallAbsurd.err
- PatternMatchingOnCodata.agda
- PatternMatchingOnCodata.err
- PatternShadowsConstructor.agda
- PatternShadowsConstructor.err
- PatternShadowsConstructor2.agda
- PatternShadowsConstructor2.err
- PatternSynonymAmbiguousParse.agda
- PatternSynonymAmbiguousParse.err
- PatternSynonymMutualBlock.agda
- PatternSynonymMutualBlock.err
- PatternSynonymNoParse.agda
- PatternSynonymNoParse.err
- PatternSynonymOverapplied.agda
- PatternSynonymOverapplied.err
- PatternSynonymOverapplied2.agda
- PatternSynonymOverapplied2.err
- PatternSynonymOverloaded.agda
- PatternSynonymOverloaded.err
- PatternSynonymParameterisedModule.agda
- PatternSynonymParameterisedModule.err
- PatternSynonymUnderapplied.agda
- PatternSynonymUnderapplied.err
- PatternSynonymsErrorLocation.agda
- PatternSynonymsErrorLocation.err
- PositivityCheckNeedsLinearityCheck.agda
- PositivityCheckNeedsLinearityCheck.err
- PostulateInMutual.agda
- PostulateInMutual.err
- PragmaInMutual.agda
- PragmaInMutual.err
- PragmasApplyOnlyToCurrentModule.agda
- PragmasApplyOnlyToCurrentModule.err
- PrimitiveInMutual.agda
- PrimitiveInMutual.err
- Productivity.agda
- Productivity.err
- PropNoMore.agda
- PropNoMore.err
- PruningNonMillerPatternFail.agda
- PruningNonMillerPatternFail.err
- PublicWithoutOpen.agda
- PublicWithoutOpen.err
- PublicWithoutOpen2.agda
- PublicWithoutOpen2.err
- PureLambda.agda
- PureLambda.err
- RecordConstructorOutOfScope.agda
- RecordConstructorOutOfScope.err
- RecordConstructorsInErrorMessages.agda
- RecordConstructorsInErrorMessages.err
- RecordUpdatePreservesType.agda
- RecordUpdatePreservesType.err
- ReifyProjectionLike.agda
- ReifyProjectionLike.err
- RepeatedVariableInPattern.agda
- RepeatedVariableInPattern.err
- Rewrite.agda
- Rewrite.err
- SafeFlagNoTermination.agda
- SafeFlagNoTermination.err
- SafeFlagNoTermination.flags
- SafeFlagPostulate.agda
- SafeFlagPostulate.err
- SafeFlagPostulate.flags
- SafeFlagPragmas.agda
- SafeFlagPragmas.err
- SafeFlagPragmas.flags
- SafeFlagPrimTrustMe.agda
- SafeFlagPrimTrustMe.err
- SafeFlagPrimTrustMe.flags
- ScopeIrrelevantRecordField.agda
- ScopeIrrelevantRecordField.err
- SetOmega.agda
- SetOmega.err
- ShadowModule.agda
- ShadowModule.err
- ShadowModule2.agda
- ShadowModule2.err
- ShapeIrrelevantIndex.agda
- ShapeIrrelevantIndex.err
- ShapeIrrelevantIndexNoBecauseOfRecursion.agda
- ShapeIrrelevantIndexNoBecauseOfRecursion.err
- ShapeIrrelevantParameterNoBecauseOfRecursion.agda
- ShapeIrrelevantParameterNoBecauseOfRecursion.err
- ShouldBeASort.agda
- ShouldBeASort.err
- ShouldBeApplicationOf.agda
- ShouldBeApplicationOf.err
- ShouldBeAppliedToTheDatatypeParameters.agda
- ShouldBeAppliedToTheDatatypeParameters.err
- ShouldBeEmpty.agda
- ShouldBeEmpty.err
- ShouldBePi.agda
- ShouldBePi.err
- ShouldEndInApplicationOfTheDatatype.agda
- ShouldEndInApplicationOfTheDatatype.err
- SizeUnsolvedConstraintsInTypeSignature.agda
- SizeUnsolvedConstraintsInTypeSignature.err
- SizedTypesFunctionFromSuccSize.agda
- SizedTypesFunctionFromSuccSize.err
- SizedTypesRigidVarClash.agda
- SizedTypesRigidVarClash.err
- SizedTypesScopeExtrusion.agda
- SizedTypesScopeExtrusion.err
- SizedTypesVarSwap.agda
- SizedTypesVarSwap.err
- SkipParametersInConstructorReification.agda
- SkipParametersInConstructorReification.err
- SortDependingOnIndex.agda
- SortDependingOnIndex.err
- SplitOnIrrelevant.agda
- SplitOnIrrelevant.err
- StrangeRecursiveUnquote.agda
- StrangeRecursiveUnquote.err
- StronglyRigidOccurrence.agda
- StronglyRigidOccurrence.err
- SubjectReduction.agda
- SubjectReduction.err
- SyntaxForOperators.agda
- SyntaxForOperators.err
- Tabs.agda
- Tabs.err
- TabsInPragmas.agda
- TabsInPragmas.err
- TermSplicing1.agda
- TermSplicing1.err
- TermSplicingLooping.agda
- TermSplicingLooping.err
- TermSplicingOutOfScope.agda
- TermSplicingOutOfScope.err
- TerminationInfiniteRecord.agda
- TerminationInfiniteRecord.err
- TerminationLambda.agda
- TerminationLambda.err
- TerminationNoArgs.agda
- TerminationNoArgs.err
- TerminationOnIrrelevant.agda
- TerminationOnIrrelevant.err
- TerminationRecordPatternCoerce.agda
- TerminationRecordPatternCoerce.err
- TerminationRecordPatternLie.agda
- TerminationRecordPatternLie.err
- TerminationRecordPatternListAppend.agda
- TerminationRecordPatternListAppend.err
- TerminationWithInsufficientDepth.agda
- TerminationWithInsufficientDepth.err
- TerminationWithMerge.agda
- TerminationWithMerge.err
- TooManyArgumentsInLHS.agda
- TooManyArgumentsInLHS.err
- TooManyFields.agda
- TooManyFields.err
- TrustMe.agda
- TrustMe.err
- TwoCompilers.agda
- TwoCompilers.err
- TwoCompilers.flags
- TypeConstructorsWhichPreserveGuardedness1.agda
- TypeConstructorsWhichPreserveGuardedness1.err
- TypeConstructorsWhichPreserveGuardedness2.agda
- TypeConstructorsWhichPreserveGuardedness2.err
- TypeConstructorsWhichPreserveGuardedness3.agda
- TypeConstructorsWhichPreserveGuardedness3.err
- TypeConstructorsWhichPreserveGuardedness4.agda
- TypeConstructorsWhichPreserveGuardedness4.err
- UnequalHiding.agda
- UnequalHiding.err
- UnequalRelevance.agda
- UnequalRelevance.err
- UnequalSorts.agda
- UnequalSorts.err
- UnequalTerms.agda
- UnequalTerms.err
- UnificationUndecidedForNonStronglyRigidOccurrence.agda
- UnificationUndecidedForNonStronglyRigidOccurrence.err
- UnifyWithIrrelevantArgument.agda
- UnifyWithIrrelevantArgument.err
- UninstantiatedDotPattern.agda
- UninstantiatedDotPattern.err
- UnknownNameInFixityDecl.agda
- UnknownNameInFixityDecl.err
- UnquoteSetOmega.agda
- UnquoteSetOmega.err
- Unreachable.agda
- Unreachable.err
- UnsolvableLevelConstraintsInDataDef.agda
- UnsolvableLevelConstraintsInDataDef.err
- Unsolved-meta-in-module-application.agda
- Unsolved-meta-in-module-application.err
- Unsolved-meta-in-module-telescope.agda
- Unsolved-meta-in-module-telescope.err
- Unsolved-meta-in-postulate.agda
- Unsolved-meta-in-postulate.err
- UnsolvedMetas.agda
- UnsolvedMetas.err
- WhyWeNeedUntypedLambda.agda
- WhyWeNeedUntypedLambda.err
- WithScopeError.agda
- WithScopeError.err
- WithoutK1.agda
- WithoutK1.err
- WithoutK10.agda
- WithoutK10.err
- WithoutK2.agda
- WithoutK2.err
- WithoutK3.agda
- WithoutK3.err
- WithoutK4.agda
- WithoutK4.err
- WithoutK5.agda
- WithoutK5.err
- WithoutK6.agda
- WithoutK6.err
- WithoutK7.agda
- WithoutK7.err
- WithoutK8.agda
- WithoutK8.err
- WithoutK9.agda
- WithoutK9.err
- WrongDotPattern.agda
- WrongDotPattern.err
- WrongHidingInApplication.agda
- WrongHidingInApplication.err
- WrongHidingInLHS.agda
- WrongHidingInLHS.err
- WrongHidingInLambda.agda
- WrongHidingInLambda.err
- WrongMetaLeft.agda
- WrongMetaLeft.err
- WrongNumberOfConstructorArguments.agda
- WrongNumberOfConstructorArguments.err
- WrongPolarity.agda
- WrongPolarity.err
- WrongSizeAssignment.agda
- WrongSizeAssignment.err
- WrongSizeAssignment2.agda
- WrongSizeAssignment2.err
- A/
- Imports/
- customised/