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

Directory listing for MiniAgda-0.2022.3.11 source tarball

MiniAgda-0.2022.3.11/

• CHANGELOG
• LICENSE
• Makefile
• MiniAgda.cabal
• README.md
• lib/
  • base.ma
  • bintree.ma
  • colist.ma
  • list.ma
  • nat.ma
  • stl.ma
• src/
  • Abstract.hs
  • Abstract.hs-boot
  • Collection.hs
  • Concrete.hs
  • Eval.hs
  • Eval.hs-boot
  • Extract.hs
  • HsSyntax.hs
  • Lexer.hs
  • Lexer.x
  • Main.hs
  • Makefile
  • Parser.hs
  • Parser.y
  • Polarity.hs
  • PrettyTCM.hs
  • ScopeChecker.hs
  • Semiring.hs
  • SparseMatrix.hs
  • TCM.hs
  • TCM.hs-boot
  • Termination.hs
  • ToHaskell.hs
  • Tokens.hs
  • TraceError.hs
  • TreeShapedOrder.hs
  • TypeChecker.hs
  • Util.hs
  • Value.hs
  • Value.hs-boot
  • Warshall.hs
• test/
  • GoldplateTests.hs
  • fail.goldplate
  • should-fail.goldplate
  • should-succeed.goldplate
  • succeed.goldplate
  • bugs/
    • AgdaIssue1052.ma
    • AgdaIssue1458.ma
  • 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
  • should-fail/
    • AgdaIssue1015.golden
    • AgdaIssue1015.ma
    • AgdaIssue1015NonMutual.golden
    • AgdaIssue1015NonMutual.ma
    • StrictInfty.golden
    • StrictInfty.ma
  • should-succeed/
    • Umlaut.err
    • Umlaut.ma
  • 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