Directory listing for MiniAgda-0.2025.7.23 candidate source tarball
MiniAgda-0.2025.7.23/test/
- GoldplateTests.hs
- fail.goldplate
- should-fail.goldplate
- should-succeed.goldplate
- succeed.goldplate
- bugs/
- fail/
- AccCoqTermination.err
- AccCoqTermination.ma
- AccImplicit.err
- AccImplicit.ma
- BadConstraint.err
- BadConstraint.ma
- BadConstraint1.err
- BadConstraint1.ma
- BadSizeLambda.err
- BadSizeLambda.ma
- BadSizeLambdaCoinductive.err
- BadSizeLambdaCoinductive.ma
- BadSizeLambdaInductive.err
- BadSizeLambdaInductive.ma
- BigDataInSet0.err
- BigDataInSet0.ma
- BoundedFake.err
- BoundedFake.ma
- BoundedQStrict.err
- BoundedQStrict.ma
- BoundedQWrong.err
- BoundedQWrong.ma
- BoxNeg.err
- BoxNeg.ma
- CheatSubtypingPos.err
- CheatSubtypingPos.ma
- CoNotLowerSemi.err
- CoNotLowerSemi.ma
- CoNotLowerSemi1.err
- CoNotLowerSemi1.ma
- ConorMcBrideCalco09inflationary.err
- D.err
- D.ma
- D1.err
- D1.ma
- DataAtSetInfty.err
- DataAtSetInfty.ma
- DeepForcedConstructors.err
- DeepForcedConstructors.ma
- DescendAscend.err
- DescendAscend.ma
- DescendAscend2.err
- DescendAscend2.ma
- DoNotEraseDataTeleForConTypes.err
- DoNotEraseDataTeleForConTypes.ma
- DottedConstructorsWrong.err
- DottedConstructorsWrong.ma
- EndsCoInEmpty.err
- EndsCoInEmpty.ma
- ExistsSPos.err
- ExistsSPos.ma
- Fib2.err
- Fib2.ma
- FinBranchMutualWrong.err
- FinBranchMutualWrong.ma
- FunctionExtensionality.err
- FunctionExtensionality.ma
- HOMatching.err
- HOMatching.ma
- HetIdFoolingEta.err
- HetIdFoolingEta.ma
- HungryEtaRecord.err
- HungryEtaRecord.ma
- IdFoolingEta.err
- IdFoolingEta.ma
- IllegalParameter.err
- IllegalParameter.ma
- InconsistentHypotheses.err
- InconsistentHypotheses.ma
- InjDataLoop.err
- InjDataLoop.ma
- InjDataLoop2.err
- InjDataLoop2.ma
- InvalidField.err
- InvalidField.ma
- InvalidSizeP.err
- InvalidSizeP.ma
- IrrHeterogeneousEta.err
- IrrHeterogeneousEta.ma
- IrrHeterogeneousFun.err
- IrrHeterogeneousFun.ma
- Makefile
- MeasureInTelescope.err
- MeasureInTelescope.ma
- MeasureInValue.err
- MeasureInValue.ma
- MeasuresTypo.err
- MeasuresTypo.ma
- MixedMeasureLength.err
- MixedMeasureLength.ma
- MixedMeasuredUnmeasured.err
- MixedMeasuredUnmeasured.ma
- MuOnlyPosNotSPos.err
- MuOnlyPosNotSPos.ma
- MustBeCofun.err
- MustBeCofun.ma
- MutualDataNotMon.err
- MutualDataNotMon.ma
- MutualNeg.err
- MutualNeg.ma
- MutualNeg2.err
- MutualNeg2.ma
- NatToSize.err
- NatToSize.ma
- NegPol.err
- NegPol.ma
- NonLinearParameter.err
- NonLinearParameter.ma
- NonLinearParameterPattern.err
- NonLinearParameterPattern.ma
- NonLinearPatterns.err
- NonLinearPatterns.ma
- NonPosBoundedData.err
- NonPosBoundedData.ma
- NotEnoughParameters.err
- NotEnoughParameters.ma
- NotForcedConstructors.err
- NotForcedConstructors.ma
- NumbersAsIds.err
- NumbersAsIds.ma
- OverlappingPatternIndFam-sound.err
- OverlappingPatternIndFam-sound.ma
- OverlappingPatternIndFam.err
- OverlappingPatternIndFam.ma
- PolarityWrongCast.err
- PolarityWrongCast.ma
- RecurseOnErased.err
- RecurseOnErased.ma
- ResurrectFromErasedPattern.err
- ResurrectFromErasedPattern.ma
- SPosNotPos.err
- SPosNotPos.ma
- ShadowBinding.err
- ShadowBinding.ma
- ShadowParameter.err
- ShadowParameter.ma
- ShadowPatternParameter.err
- ShadowPatternParameter.ma
- SizedDataWrongPol.err
- SizedDataWrongPol.ma
- StoreSize.err
- StoreSize.ma
- StreamDupl.err
- StreamDupl.ma
- StreamNotSemiCont.err
- StreamNotSemiCont.ma
- Tm.err
- Tm.ma
- TypeInTypeViaSetInfty.err
- TypeInTypeViaSetInfty.ma
- UlfsCounterexample.err
- UlfsCounterexample.ma
- UlfsCounterexample2.err
- UlfsCounterexample2.ma
- VectorPatternNotForced.err
- VectorPatternNotForced.ma
- VeiledParameter.err
- VeiledParameter.ma
- absurdPatUnit.err
- absurdPatUnit.ma
- bfSizePatternIncomplete.err
- bfSizePatternIncomplete.ma
- bfTypeNotAdmissible.err
- bfTypeNotAdmissible.ma
- bigData.err
- bigData.ma
- coSetOmega.err
- coSetOmega.ma
- coSizeInFun.err
- coSizeInFun.ma
- codataNotMonotone.err
- codataNotMonotone.ma
- codyPatternConditionExplicit.err
- codyPatternConditionExplicit.ma
- codyPatternConditionExplicit2.err
- codyPatternConditionExplicit2.ma
- cofunIntoBoolTimesStream.err
- cofunIntoBoolTimesStream.ma
- cofunIntoStreamPlusStream.err
- cofunIntoStreamPlusStream.ma
- countingBT.err
- countingBT.ma
- countingMerge.err
- countingMerge.ma
- dataNotMonotone.err
- dataNotMonotone.ma
- drop.err
- drop.ma
- erased1.err
- erased1.ma
- f_x_is_f_0.err
- f_x_is_f_0.ma
- fail1.err
- fail1.ma
- fibStream.err
- fibStream.ma
- hang.err
- hang.ma
- hang2.err
- hang2.ma
- huetHullotReverse.err
- huetHullotReverse.ma
- incompleteSizePattern1.err
- incompleteSizePattern1.ma
- incompleteSizePattern2.err
- incompleteSizePattern2.ma
- inconsistentAssumption.err
- inconsistentAssumption.ma
- inconsistentAssumption2.err
- inconsistentAssumption2.ma
- inductiveNotDotPattern.err
- inductiveNotDotPattern.ma
- lengthCoList.err
- lengthCoList.ma
- lengthCoList2.err
- lengthCoList2.ma
- loop.err
- loop.ma
- loopAdmStream-Nat.err
- loopAdmStream-Nat.ma
- loopAdmStream-simplified.err
- loopAdmStream-simplified.ma
- loopAdmStream.err
- loopAdmStream.ma
- loopBadTypesHidden.err
- loopBadTypesHidden.ma
- loopBounded.err
- loopBounded.ma
- loopOldNoSizePattern.err
- loopOldNoSizePattern.ma
- loopTypesHiddenInData.err
- loopTypesHiddenInData.ma
- mapStream2.err
- mapStream2.ma
- mapStream2sizeMatchDepth2.err
- mapStream2sizeMatchDepth2.ma
- matchOnNatSuccI.err
- matchOnNatSuccI.ma
- match_erased.err
- match_erased.ma
- match_on_set.err
- match_on_set.ma
- negativeFam.err
- negativeFam.ma
- notAdmMonotoneArg.err
- notAdmMonotoneArg.ma
- omegaInst.err
- omegaInst.ma
- omegaInst1.err
- omegaInst1.ma
- onesStreamUnguarded.err
- onesStreamUnguarded.ma
- partialFunction.err
- partialFunction.ma
- relevantArgErasedMagicVec.err
- relevantArgErasedMagicVec.ma
- scolist_not_lsc1.err
- scolist_not_lsc1.ma
- scolist_not_lsc2.err
- scolist_not_lsc2.ma
- shadowGlobal.err
- shadowGlobal.ma
- shouldBeDotPattern_snat.err
- shouldBeDotPattern_snat.ma
- singleton.err
- singleton.ma
- sizePatternSucc.err
- sizePatternSucc.ma
- stream.err
- stream.ma
- streamMisc.err
- streamMisc.ma
- stream_x_is_cons_x_tail_x.err
- stream_x_is_cons_x_tail_x.ma
- subtyping_erased.err
- subtyping_erased.ma
- subtyping_erased_wrongdir.err
- subtyping_erased_wrongdir.ma
- swapVariablesWithoutDecrease.err
- swapVariablesWithoutDecrease.ma
- tailBad.err
- tailBad.ma
- vec_eta.err
- vec_eta.ma
- vec_length.err
- vec_length.ma
- adm/
- should-fail/
- should-succeed/
- succeed/
- AbsurdMatchNonLin.golden
- AbsurdMatchNonLin.ma
- AccDestructorErasedIndex.golden
- AccDestructorErasedIndex.ma
- AgdaIssue1052.golden
- AgdaIssue1052.ma
- AgdaIssue1055.golden
- AgdaIssue1055.ma
- AppendAddSize.golden
- AppendAddSize.ma
- BelowLeInfty.golden
- BelowLeInfty.ma
- BigWrap.golden
- BigWrap.ma
- BoundedQ.golden
- BoundedQ.ma
- BuiltinSigma.golden
- BuiltinSigma.ma
- CoFunReturnsProduct.golden
- CoFunReturnsProduct.ma
- ConorMcBrideCalco09inflationary.golden
- ConorMcBrideCalco09inflationary.ma
- ConstructorTelescopes.golden
- ConstructorTelescopes.ma
- ConstructorVeiledTarget.golden
- ConstructorVeiledTarget.ma
- DataTypesNotFamilies.golden
- DataTypesNotFamilies.ma
- DeepMatch.golden
- DeepMatch.ma
- DescendAscendTerm.golden
- DescendAscendTerm.ma
- DotPatternNotLeftToRightBinding.golden
- DotPatternNotLeftToRightBinding.ma
- DottedConstructors.golden
- DottedConstructors.ma
- DottedPatSyn.golden
- DottedPatSyn.ma
- Empty.golden
- Empty.ma
- EvalBoveCaprettaNotSized.golden
- EvalBoveCaprettaNotSized.ma
- EvenOdd.golden
- EvenOdd.ma
- Evens.golden
- Evens.ma
- ExtractLets.golden
- ExtractLets.ma
- FakeMutual.golden
- FakeMutual.ma
- Fields.golden
- Fields.ma
- FinBranchMutual.golden
- FinBranchMutual.ma
- Fix.golden
- Fix.ma
- ForceInConType.golden
- ForceInConType.ma
- ForcedMatch.golden
- ForcedMatch.ma
- ForcedMatchIdType.golden
- ForcedMatchIdType.ma
- ForestRose.golden
- ForestRose.ma
- GADT.golden
- GADT.ma
- GoodConstraint.golden
- GoodConstraint.ma
- HEq.golden
- HEq.ma
- HVec.golden
- HVec.ma
- HungryEtaRecord.golden
- HungryEtaRecord.ma
- IdTypePos.golden
- IdTypePos.ma
- IrrHeterogeneousFun.golden
- IrrHeterogeneousFun.ma
- IrrHeterogeneousSingleton.golden
- IrrHeterogeneousSingleton.ma
- IrrHeterogeneousSize.golden
- IrrHeterogeneousSize.ma
- LargeElim.golden
- LargeElim.ma
- LetTele.golden
- LetTele.ma
- LowerSemiCont.golden
- LowerSemiCont.ma
- Makefile
- MeasureInFunTele.golden
- MeasureInFunTele.ma
- MeasuredHerSubst1.golden
- MeasuredHerSubst1.ma
- MeasuredRose.golden
- MeasuredRose.ma
- MergeWith.golden
- MergeWith.ma
- MockSig.golden
- MockSig.ma
- Mu.golden
- Mu.ma
- MultiSigma.golden
- MultiSigma.ma
- MutualBigDataKindInf.golden
- MutualBigDataKindInf.ma
- MutualRecordsNoEta.golden
- MutualRecordsNoEta.ma
- Nested.golden
- Nested.ma
- NewSyntaxTour.golden
- NewSyntaxTour.ma
- Nisse2012-02-17.golden
- Nisse2012-02-17.ma
- Nisse2012-03-06.golden
- Nisse2012-03-06.ma
- OverloadedConstructors.golden
- OverloadedConstructors.ma
- PTSRule.golden
- PTSRule.ma
- ParseMultBind.golden
- ParseMultBind.ma
- ParsePipeOperators.golden
- ParsePipeOperators.ma
- Pattern.golden
- Pattern.ma
- PatternParameters.golden
- PatternParameters.ma
- Polarities.golden
- Polarities.ma
- PredDepType.golden
- PredDepType.ma
- Prelude.golden
- Prelude.ma
- Prod.golden
- Prod.ma
- Projections.golden
- Projections.ma
- Rose.golden
- Rose.ma
- SP.golden
- SP.ma
- ScopeCheckFunDef.golden
- ScopeCheckFunDef.ma
- SgPredWrongMon.golden
- SgPredWrongMon.ma
- SolverBugStreamFixed.golden
- SolverBugStreamFixed.ma
- Squash.golden
- Squash.ma
- Stack.golden
- Stack.ma
- StreamDupl.golden
- StreamDupl.ma
- StrictBoundedQCoinductive.golden
- StrictBoundedQCoinductive.ma
- UPolyList.golden
- UPolyList.ma
- Universe.golden
- Universe.ma
- VecNotErased.golden
- VecNotErased.ma
- WrapAbsurd.golden
- WrapAbsurd.ma
- absurdPattern.golden
- absurdPattern.ma
- addWith.golden
- addWith.ma
- casePair.golden
- casePair.ma
- caseSList.golden
- caseSList.ma
- conat.golden
- conat.ma
- countConstructors.golden
- countConstructors.ma
- crazys.golden
- crazys.ma
- drop.golden
- drop.ma
- eta.golden
- eta.ma
- eta_unit.golden
- eta_unit.ma
- exists.golden
- exists.ma
- fib.golden
- fib.ma
- fibDeep.golden
- fibDeep.ma
- gcd-either.golden
- gcd-either.ma
- hamming.golden
- hamming.ma
- ho.golden
- ho.ma
- implicitSizeVarUsedExplicitely.golden
- implicitSizeVarUsedExplicitely.ma
- lengthCoList.golden
- lengthCoList.ma
- list.golden
- list.ma
- logic.golden
- logic.ma
- lossyIdentityOnStreams.golden
- lossyIdentityOnStreams.ma
- magicVecLookupProofIrr.golden
- magicVecLookupProofIrr.ma
- mapStream.golden
- mapStream.ma
- max.golden
- max.ma
- measures.golden
- measures.ma
- msort-implicit.golden
- msort-implicit.ma
- msort.golden
- msort.ma
- nat.golden
- nat.ma
- non-record.golden
- non-record.ma
- old_stream.golden
- old_stream.ma
- oldnat.golden
- oldnat.ma
- omegaInst1.golden
- omegaInst1.ma
- omegaInstTailInfty.golden
- omegaInstTailInfty.ma
- pred.golden
- pred.ma
- qsapp.golden
- qsapp.ma
- quicksort-filter-fragment.golden
- quicksort-filter-fragment.ma
- quicksort-filter.golden
- quicksort-filter.ma
- quicksort.golden
- quicksort.ma
- rank2SizeQuantStream.golden
- rank2SizeQuantStream.ma
- record.golden
- record.ma
- shadowDataParam.golden
- shadowDataParam.ma
- sigma.golden
- sigma.ma
- simple_nat.golden
- simple_nat.ma
- singleton.golden
- singleton.ma
- sizeFunctions.golden
- sizeFunctions.ma
- sizedFinitelyBranchingTrees.golden
- sizedFinitelyBranchingTrees.ma
- sizedMax.golden
- sizedMax.ma
- sizedMergeWith.golden
- sizedMergeWith.ma
- sizedOrd.golden
- sizedOrd.ma
- streamIdentityNatRecursive.golden
- streamIdentityNatRecursive.ma
- subset.golden
- subset.ma
- tailStream.golden
- tailStream.ma
- vec.golden
- vec.ma
- wkStream.golden
- wkStream.ma