Directory listing for MiniAgda-0.2019.3.29 candidate source tarball
MiniAgda-0.2019.3.29/test/
- 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/
 
 - succeed/
- AbsurdMatchNonLin.ma
 - AccDestructorErasedIndex.ma
 - AgdaIssue1052.ma
 - AgdaIssue1055.ma
 - AppendAddSize.ma
 - BelowLeInfty.ma
 - BigWrap.ma
 - BoundedQ.ma
 - BuiltinSigma.ma
 - CoFunReturnsProduct.ma
 - ConorMcBrideCalco09inflationary.ma
 - ConstructorTelescopes.ma
 - ConstructorVeiledTarget.ma
 - DataTypesNotFamilies.ma
 - DeepMatch.ma
 - DescendAscendTerm.ma
 - DotPatternNotLeftToRightBinding.ma
 - DottedConstructors.ma
 - DottedPatSyn.ma
 - Empty.ma
 - EvalBoveCaprettaNotSized.ma
 - EvenOdd.ma
 - Evens.ma
 - ExtractLets.ma
 - FakeMutual.ma
 - Fields.ma
 - FinBranchMutual.ma
 - Fix.ma
 - ForceInConType.ma
 - ForcedMatch.ma
 - ForcedMatchIdType.ma
 - ForestRose.ma
 - GADT.ma
 - GoodConstraint.ma
 - HEq.ma
 - HVec.ma
 - HungryEtaRecord.ma
 - IdTypePos.ma
 - IrrHeterogeneousFun.ma
 - IrrHeterogeneousSingleton.ma
 - IrrHeterogeneousSize.ma
 - LargeElim.ma
 - LetTele.ma
 - LowerSemiCont.ma
 - Makefile
 - MeasureInFunTele.ma
 - MeasuredHerSubst1.ma
 - MeasuredRose.ma
 - MergeWith.ma
 - MockSig.ma
 - Mu.ma
 - MultiSigma.ma
 - MutualBigDataKindInf.ma
 - MutualRecordsNoEta.ma
 - Nested.ma
 - NewSyntaxTour.ma
 - Nisse2012-02-17.ma
 - Nisse2012-03-06.ma
 - OverloadedConstructors.ma
 - PTSRule.ma
 - ParseMultBind.ma
 - ParsePipeOperators.ma
 - Pattern.ma
 - PatternParameters.ma
 - Polarities.ma
 - PredDepType.ma
 - Prelude.ma
 - Prod.ma
 - Projections.ma
 - Rose.ma
 - SP.ma
 - ScopeCheckFunDef.ma
 - SgPredWrongMon.ma
 - SolverBugStreamFixed.ma
 - Squash.ma
 - Stack.ma
 - StreamDupl.ma
 - StrictBoundedQCoinductive.ma
 - UPolyList.ma
 - Universe.ma
 - VecNotErased.ma
 - WrapAbsurd.ma
 - absurdPattern.ma
 - addWith.ma
 - casePair.ma
 - caseSList.ma
 - conat.ma
 - countConstructors.ma
 - crazys.ma
 - drop.ma
 - eta.ma
 - eta_unit.ma
 - exists.ma
 - fib.ma
 - fibDeep.ma
 - gcd-either.ma
 - hamming.ma
 - ho.ma
 - implicitSizeVarUsedExplicitely.ma
 - lengthCoList.ma
 - list.ma
 - logic.ma
 - lossyIdentityOnStreams.ma
 - magicVecLookupProofIrr.ma
 - mapStream.ma
 - max.ma
 - measures.ma
 - msort-implicit.ma
 - msort.ma
 - nat.ma
 - non-record.ma
 - old_stream.ma
 - oldnat.ma
 - omegaInst1.ma
 - omegaInstTailInfty.ma
 - pred.ma
 - qsapp.ma
 - quicksort-filter-fragment.ma
 - quicksort-filter.ma
 - quicksort.ma
 - rank2SizeQuantStream.ma
 - record.ma
 - shadowDataParam.ma
 - sigma.ma
 - simple_nat.ma
 - singleton.ma
 - sizeFunctions.ma
 - sizedFinitelyBranchingTrees.ma
 - sizedMax.ma
 - sizedMergeWith.ma
 - sizedOrd.ma
 - streamIdentityNatRecursive.ma
 - subset.ma
 - tailStream.ma
 - vec.ma
 - wkStream.ma