Directory listing for Agda-2.3.2.2 source tarball
Agda-2.3.2.2/test/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/