Directory listing for Agda-2.3.2.2 source tarball
Agda-2.3.2.2/test/
- .cvsignore
- Common/
- bugs/
- compiler/
- core/
- epic/
- 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/
- features/
- interaction/
- AutoMisc.agda
- AutoMisc.in
- AutoMisc.out
- Debug.agda
- Debug.in
- Debug.out
- Error-in-imported-module.agda
- Error-in-imported-module.in
- Error-in-imported-module.out
- ExtendedLambdaCase.agda
- ExtendedLambdaCase.in
- ExtendedLambdaCase.out
- GiveInSpiteOfUnsolvedIrr.agda
- GiveInSpiteOfUnsolvedIrr.in
- GiveInSpiteOfUnsolvedIrr.out
- GiveSize.agda
- GiveSize.in
- GiveSize.out
- Highlighting.agda
- Highlighting.in
- Highlighting.out
- Impossible.agda
- Impossible.in
- Impossible.out
- InferIrrelevant.agda
- InferIrrelevant.in
- InferIrrelevant.out
- IntroSharp.agda
- IntroSharp.in
- IntroSharp.out
- Issue208.agda
- Issue208.in
- Issue208.out
- Issue231.agda
- Issue231.in
- Issue231.out
- Issue254.agda
- Issue254.in
- Issue254.out
- Issue271.agda
- Issue271.in
- Issue271.out
- Issue277.agda
- Issue277.in
- Issue277.out
- Issue317.agda
- Issue317.in
- Issue317.out
- Issue358.agda
- Issue358.in
- Issue358.out
- Issue363.agda
- Issue363.in
- Issue363.out
- Issue373.agda
- Issue373.out
- Issue373.sh
- Issue378.agda
- Issue378.in
- Issue378.out
- Issue388.agda
- Issue388.in
- Issue388.out
- Issue417.agda
- Issue417.in
- Issue417.out
- Issue453.agda
- Issue453.in
- Issue453.out
- Issue499.agda
- Issue499.in
- Issue499.out
- Issue556.agda
- Issue556.in
- Issue556.out
- Issue564.agda
- Issue564.in
- Issue564.out
- Issue589.agda
- Issue589.in
- Issue589.out
- Issue591.agda
- Issue591.in
- Issue591.out
- Issue599.agda
- Issue599.in
- Issue599.out
- Issue604.agda
- Issue604.in
- Issue604.out
- Issue606.agda
- Issue606.in
- Issue606.out
- Issue620.agda
- Issue620.in
- Issue620.out
- Issue630.agda
- Issue630.in
- Issue630.out
- Issue637.agda
- Issue637.in
- Issue637.out
- Issue639.agda
- Issue639.in
- Issue639.out
- Issue641.agda
- Issue641.out
- Issue641.sh
- Issue642.agda
- Issue642.in
- Issue642.out
- Issue643.agda
- Issue643.in
- Issue643.out
- Issue670.agda
- Issue670.in
- Issue670.out
- Issue679a.agda
- Issue679a.in
- Issue679a.out
- Issue720.agda
- Issue720.out
- Issue720.sh
- Literate.in
- Literate.lagda
- Literate.out
- Long.agda
- Long.in
- Long.out
- Makefile
- Multisplit.agda
- Multisplit.in
- Multisplit.out
- NiceGoals.agda
- NiceGoals.in
- NiceGoals.out
- Positivity-once.agda
- Positivity-once.in
- Positivity-once.out
- PragmasRespected.agda
- PragmasRespected.in
- PragmasRespected.out
- README
- RecordPatternMatching.agda
- RecordPatternMatching.in
- RecordPatternMatching.out
- RecordUpdateSyntax.agda
- RecordUpdateSyntax.in
- RecordUpdateSyntax.out
- SetInf.agda
- SetInf.in
- SetInf.out
- With-flicker.agda
- With-flicker.in
- With-flicker.out
- Error-in-imported-module/
- Highlighting/
- Imports/
- Issue591/
- js/
- lib-succeed/
- succeed/
- .cvsignore
- Abstract.agda
- AbstractData.agda
- AbsurdIrrelevance.agda
- AbsurdLam.agda
- AbsurdPattern.agda
- Berry.agda
- Bush.agda
- CoPatStream.agda
- CoinductiveAfterEvaluation.agda
- Comments.agda
- CompareLevel.agda
- CompilingCoinduction.agda
- CompilingCoinduction.flags
- ComputedLevels.agda
- Const.agda
- Copatterns.agda
- CoverStrategy.agda
- DataPolarity.agda
- DataRecordInductive.agda
- DefinitionalEquality.agda
- DependentIrrelevance.agda
- DigitsInNames.agda
- Div.agda
- Div2.agda
- DoNotEtaExpandMVarsWhenComparingAgainstRecord.agda
- DontIgnoreIrrelevantVars.agda
- DotPatternTermination.agda
- EmptyInductiveRecord.agda
- Epic.agda
- Epic.flags
- EqTest.agda
- EtaAndMetas.agda
- EtaContractIrrelevant.agda
- EtaContractToMillerPattern.agda
- EtaContractionDefBody.agda
- Exist.agda
- ExplicitLambdaExperimentalIrrelevance.agda
- FancyRecordModule.agda
- Filter.agda
- FilterSub.agda
- FlexRemoval.agda
- ForallForParameters.agda
- FreezingTest.agda
- GuardednessPreservingTypeConstructors.agda
- HereditarilySingletonRecord.agda
- Hurkens.agda
- ImplicitRecordFields.agda
- ImplicitsAndWhere.agda
- IndexInference.agda
- IndexOnBuiltin.agda
- InductiveAndCoinductiveConstructors.agda
- InferRecordTypes.agda
- InferrableFields.agda
- InfixRecordFields.agda
- InjectiveTypeConstructors.agda
- Injectivity.agda
- InstanceArguments.agda
- InstanceArgumentsBraces.agda
- InstanceArgumentsConstraints.agda
- InstanceArgumentsDontDiscardCandidateUponUnsolvedConstraints.agda
- InstanceArgumentsHidden.agda
- InstanceArgumentsSections.agda
- InstanceGuessesMeta.agda
- InstanceGuessesMeta2.agda
- IrrelevanceCaseStudyPartialFunctions.agda
- IrrelevantApplication.agda
- IrrelevantDataParameter.agda
- IrrelevantDeclaration.agda
- IrrelevantLambda.agda
- IrrelevantLambdasDoNotNeedDotsAlways.agda
- IrrelevantLet.agda
- IrrelevantLevel.agda
- IrrelevantProjections.agda
- IrrelevantRecordFields.agda
- IrrelevantWith.agda
- Issue100.agda
- Issue106.agda
- Issue107.agda
- Issue117.agda
- Issue121.agda
- Issue124.agda
- Issue133.agda
- Issue137.agda
- Issue138.agda
- Issue148.agda
- Issue151.agda
- Issue152.agda
- Issue153.agda
- Issue154.agda
- Issue155.agda
- Issue162.agda
- Issue165.agda
- Issue166.agda
- Issue168-irrelevant.agda
- Issue168.agda
- Issue168b.agda
- Issue175.agda
- Issue175b.agda
- Issue180.agda
- Issue199.agda
- Issue202.agda
- Issue203.agda
- Issue204.agda
- Issue209.agda
- Issue211.agda
- Issue213.agda
- Issue222.agda
- Issue224.agda
- Issue227.agda
- Issue229.agda
- Issue232.agda
- Issue233.agda
- Issue234.agda
- Issue237.agda
- Issue242.agda
- Issue245.agda
- Issue246.agda
- Issue248.agda
- Issue251.agda
- Issue252.agda
- Issue253.agda
- Issue258.agda
- Issue259.agda
- Issue259b.agda
- Issue259c.agda
- Issue26.agda
- Issue261.agda
- Issue262.agda
- Issue263.agda
- Issue263b.agda
- Issue268.agda
- Issue274.agda
- Issue276.agda
- Issue279.agda
- Issue282.agda
- Issue286.agda
- Issue291.agda
- Issue292-14.agda
- Issue292-16.agda
- Issue292-16b.agda
- Issue292-17.agda
- Issue292-19.agda
- Issue292-23.agda
- Issue292-27.agda
- Issue292.agda
- Issue296.agda
- Issue296.flags
- Issue298.agda
- Issue298b.agda
- Issue300.agda
- Issue307.agda
- Issue31.agda
- Issue311.agda
- Issue312.agda
- Issue313.agda
- Issue314.agda
- Issue323.agda
- Issue326.agda
- Issue326.flags
- Issue327.agda
- Issue330.agda
- Issue331.agda
- Issue333.agda
- Issue334.agda
- Issue335.agda
- Issue337.agda
- Issue34.agda
- Issue348.agda
- Issue351-5.agda
- Issue351.agda
- Issue353.agda
- Issue354.agda
- Issue361.agda
- Issue365.agda
- Issue366.agda
- Issue376.agda
- Issue383.agda
- Issue383b.agda
- Issue384.agda
- Issue387.agda
- Issue392.agda
- Issue395.agda
- Issue396.agda
- Issue396b.agda
- Issue408.agda
- Issue411.agda
- Issue414.agda
- Issue420.agda
- Issue421.agda
- Issue422.agda
- Issue423.agda
- Issue425.agda
- Issue427.agda
- Issue435.agda
- Issue438.agda
- Issue439.agda
- Issue44.agda
- Issue441.agda
- Issue442.agda
- Issue443.agda
- Issue447.agda
- Issue448.agda
- Issue450.agda
- Issue451.agda
- Issue455.agda
- Issue458.agda
- Issue458b.agda
- Issue462.agda
- Issue468.agda
- Issue469.agda
- Issue472.agda
- Issue473.agda
- Issue474.agda
- Issue475.agda
- Issue479.agda
- Issue480.agda
- Issue481.agda
- Issue481PonderBase.agda
- Issue481PonderImportMe.agda
- Issue481PonderMaster.agda
- Issue481Record.agda
- Issue482.agda
- Issue483.agda
- Issue483c.agda
- Issue486.agda
- Issue49.agda
- Issue498.agda
- Issue498b.agda
- Issue501.agda
- Issue502.agda
- Issue505.agda
- Issue509.agda
- Issue533.agda
- Issue550.agda
- Issue551b.agda
- Issue552.agda
- Issue553a.agda
- Issue553b.agda
- Issue553c.agda
- Issue557.agda
- Issue558.agda
- Issue558b.agda
- Issue558c.agda
- Issue561.agda
- Issue561.flags
- Issue566.agda
- Issue574.agda
- Issue578.agda
- Issue585-17.agda
- Issue586.agda
- Issue586.flags
- Issue593.agda
- Issue596.agda
- Issue597.agda
- Issue602-2.agda
- Issue602.agda
- Issue611.agda
- Issue616.agda
- Issue629.agda
- Issue629a.agda
- Issue655.agda
- Issue658.agda
- Issue661.agda
- Issue670a.agda
- Issue671.agda
- Issue674.agda
- Issue675.agda
- Issue678.agda
- Issue679.agda
- Issue680-NeutralLevels.agda
- Issue700.agda
- Issue701-c.agda
- Issue709.agda
- Issue728.agda
- Issue728.flags
- Issue735.agda
- Issue739.agda
- Issue747.agda
- Issue754.agda
- Issue81.agda
- Issue89.agda
- Issue97.lagda
- Issue97b.lagda
- JMEq.agda
- LaTeX.flags
- LaTeX.lagda
- Lambda.agda
- LateExpansionOfRecordMeta.agda
- LetLHS.agda
- LetPair.agda
- LevelConstraints.agda
- LevelUnification.agda
- LevelWithBug.agda
- LinearTemporalLogic.agda
- ListsWithIrrelevantProofs.agda
- LitDistinct.agda
- Literate.lagda
- LocalOpenImplicit.agda
- MagicWith.agda
- Makefile
- MatchIrrelevant.agda
- MixfixBinders.agda
- ModuleInstInLet.agda
- MultipleIdentifiersOneSignature.agda
- NameFirstIfHidden.agda
- NamedImplicit.agda
- NamedWhere.agda
- Nat.agda
- NestedInj.agda
- NoBlockOnLevel.agda
- NoTerminationCheck.agda
- NoUniverseCheck.agda
- NonvariantPolarity.agda
- OpBind.agda
- OpenModule.agda
- OpenModuleShortHand.agda
- OpenPublicTermination.agda
- Operators.agda
- OverloadedConInParamModule.agda
- OverloadedConstructors.agda
- Parity.agda
- PartialityMonad.agda
- PartiallyAppliedConstructorInIndex.agda
- PatternMatchingLambda.agda
- PatternSynonymImports.agda
- PatternSynonymImports2.agda
- PatternSynonyms.agda
- PiInSet.agda
- Point.agda
- PosFunction.agda
- Positivity.agda
- PostponedTypeChecking.agda
- PostponedUnification.agda
- Printf.agda
- ProjectingRecordMeta.agda
- ProjectionLikeAndConstructorHeaded.agda
- ProjectionLikeAndMatching.agda
- ProjectionLikeFunctions.agda
- ProjectionLikeRecursive.agda
- ProjectionsPreserveGuardednessTrivialExample.agda
- PruneLHS.agda
- PruningNonMillerPattern.agda
- QualifiedConstructors.agda
- QuoteTerm.agda
- RawFunctor.agda
- RecordConstructorPatternMatching.agda
- RecordConstructors.agda
- RecordInMutual.agda
- RecordInParModule.agda
- RecordPatternMatching.agda
- RecordUpdateSyntax.agda
- RecordsAndModules.agda
- ReducingConstructorsInWith.agda
- Reflection.agda
- ReifyConstructorParametersForWith.agda
- RelevanceSubtyping.agda
- Rewrite-with-doubly-indexed-equality.agda
- Rewrite.agda
- RewriteAndUniversePolymorphism.agda
- RewriteAndWhere.agda
- Rose.agda
- SafeFlagSafePragmas.agda
- SafeFlagSafePragmas.flags
- SameMeta.agda
- Shadow.agda
- ShadowedLetBoundVar.agda
- ShapeIrrelevantIndex.agda
- SizeSucMonotone.agda
- SizedBTree.agda
- SizedCoinductiveRecords.agda
- SizedTypesLeqInfty.agda
- SizedTypesMergeSort.agda
- SolveNeutralApplication.agda
- SplitOnDotPattern.agda
- Squash.agda
- StreamProcEat.agda
- SubTermAndProjections.agda
- Subset.agda
- SubtermTermination.agda
- TermSplicing.agda
- TerminationArgumentSwapping.agda
- TerminationListInsertionNaive.agda
- TerminationMixingTupledCurried.agda
- TerminationOnIrrelevantArgument.agda
- TerminationSubExpression.agda
- TerminationTupledAckermann.agda
- TerminationWithTwoConstructors.agda
- TestQuote.agda
- TopLevelImport.agda
- TransColist.agda
- TrustMe-with-doubly-indexed-equality.agda
- TrustMe.agda
- TypeInTypeAndUnivPoly.agda
- UncurryMeta.agda
- UnderscoresAsDataParam.agda
- UnicodeSetIndex.agda
- UnifyWithIrrelevantArgument.agda
- UniversePolymorphicIO.agda
- UniversePolymorphicIO.flags
- UniversePolymorphicIO.hs
- UniversePolymorphism.agda
- UnusedArgsInPositivity.agda
- UnusedNamedImplicits.agda
- Using.agda
- WErrorOverride.agda
- WErrorOverride.flags
- Whitespace.agda
- WhyWeNeedTypedLambda.agda
- WhyWeNeedUntypedLambda.agda
- WithInParModule.agda
- WithInWhere.agda
- WithoutK.agda
- builtin.agda
- builtinInModule.agda
- checkOutput
- list.agda
- local.agda
- optionsPragma.agda
- para.agda
- qsort.agda
- simple.agda
- Issue204/
- LineEndings/