• Home
• Search 
• Browse
• What's new
• Upload
• User accounts

Directory listing for MiniAgda-0.2018.11.4 candidate source tarball

MiniAgda-0.2018.11.4/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/
    • adm1.err
    • adm1.ma
    • adm2.err
    • adm2.ma
    • adm3.err
    • adm3.ma
• 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