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

Directory listing for Agda-2.7.0 source tarball

Agda-2.7.0/

• Agda.cabal
• CHANGELOG.md
• LICENSE
• README.md
• Setup.hs
• stack-8.10.7.yaml
• stack-8.8.4.yaml
• stack-9.0.2.yaml
• stack-9.10.1.yaml
• stack-9.2.8.yaml
• stack-9.4.8.yaml
• stack-9.6.6.yaml
• stack-9.8.2.yaml
• doc/
  • release-notes/
    • 2.2.0.md
    • 2.2.10.md
    • 2.2.2.md
    • 2.2.4.md
    • 2.2.6.md
    • 2.2.8.md
    • 2.3.0.md
    • 2.3.2.1.md
    • 2.3.2.2.md
    • 2.3.2.md
    • 2.4.0.1.md
    • 2.4.0.2.md
    • 2.4.0.md
    • 2.4.2.1.md
    • 2.4.2.2.md
    • 2.4.2.3.md
    • 2.4.2.4.md
    • 2.4.2.5.md
    • 2.4.2.md
    • 2.5.1.1.md
    • 2.5.1.2.md
    • 2.5.1.md
    • 2.5.2.md
    • 2.5.3.md
    • 2.5.4.1.md
    • 2.5.4.2.md
    • 2.5.4.md
    • 2.6.0.1.md
    • 2.6.0.md
    • 2.6.1.1.md
    • 2.6.1.2.md
    • 2.6.1.3.md
    • 2.6.1.md
    • 2.6.2.1.md
    • 2.6.2.2.md
    • 2.6.2.md
    • 2.6.3.md
    • 2.6.4.1.md
    • 2.6.4.2.md
    • 2.6.4.3.md
    • 2.6.4.md
  • user-manual/
    • agda.svg
• src/
  • agda-mode/
    • Main.hs
  • data/
    • JS/
      • agda-rts.amd.js
      • agda-rts.js
    • MAlonzo/
      • src/
        • MAlonzo/
          • RTE.hs
          • RTE/
            • Float.hs
    • emacs-mode/
      • agda-input.el
      • agda2-abbrevs.el
      • agda2-highlight.el
      • agda2-mode-pkg.el
      • agda2-mode.el
      • agda2-queue.el
      • agda2.el
      • annotation.el
      • eri.el
    • html/
      • Agda.css
      • highlight-hover.js
    • latex/
      • agda.sty
      • postprocess-latex.pl
    • lib/
      • prim/
        • agda-builtins.agda-lib
        • Agda/
          • Primitive.agda
          • Builtin/
            • Bool.agda
            • Char.agda
            • Coinduction.agda
            • Equality.agda
            • Float.agda
            • FromNat.agda
            • FromNeg.agda
            • FromString.agda
            • IO.agda
            • Int.agda
            • List.agda
            • Maybe.agda
            • Nat.agda
            • Reflection.agda
            • Sigma.agda
            • Size.agda
            • Strict.agda
            • String.agda
            • TrustMe.agda
            • Unit.agda
            • Word.agda
            • Char/
              • Properties.agda
            • Cubical/
              • Equiv.agda
              • Glue.agda
              • HCompU.agda
              • Id.agda
              • Path.agda
              • Sub.agda
            • Equality/
              • Erase.agda
              • Rewrite.agda
            • Float/
              • Properties.agda
            • Reflection/
              • External.agda
              • Properties.agda
            • String/
              • Properties.agda
            • Word/
              • Properties.agda
          • Primitive/
            • Cubical.agda
  • full/
    • Agda/
      • Benchmarking.hs
      • ImpossibleTest.hs
      • Main.hs
      • TheTypeChecker.hs
      • Version.hs
      • VersionCommit.hs
      • Compiler/
        • Backend.hs
        • Backend.hs-boot
        • Builtin.hs
        • Builtin.hs-boot
        • CallCompiler.hs
        • Common.hs
        • ToTreeless.hs
        • Backend/
          • Base.hs
        • JS/
          • Compiler.hs
          • Pretty.hs
          • Substitution.hs
          • Syntax.hs
        • MAlonzo/
          • Coerce.hs
          • Compiler.hs
          • Encode.hs
          • HaskellTypes.hs
          • Misc.hs
          • Pragmas.hs
          • Pretty.hs
          • Primitives.hs
          • Strict.hs
        • Treeless/
          • AsPatterns.hs
          • Builtin.hs
          • Compare.hs
          • EliminateDefaults.hs
          • EliminateLiteralPatterns.hs
          • Erase.hs
          • Erase.hs-boot
          • GuardsToPrims.hs
          • Identity.hs
          • NormalizeNames.hs
          • Pretty.hs
          • Pretty.hs-boot
          • Simplify.hs
          • Subst.hs
          • Uncase.hs
          • Unused.hs
      • Interaction/
        • AgdaTop.hs
        • Base.hs
        • BasicOps.hs
        • CommandLine.hs
        • EmacsCommand.hs
        • EmacsTop.hs
        • ExitCode.hs
        • FindFile.hs
        • Imports.hs
        • Imports.hs-boot
        • InteractionTop.hs
        • JSON.hs
        • JSONTop.hs
        • Library.hs
        • MakeCase.hs
        • Monad.hs
        • Options.hs
        • Output.hs
        • Response.hs
        • SearchAbout.hs
        • Highlighting/
          • Common.hs
          • Dot.hs
          • Emacs.hs
          • FromAbstract.hs
          • Generate.hs
          • Generate.hs-boot
          • HTML.hs
          • JSON.hs
          • LaTeX.hs
          • Precise.hs
          • Range.hs
          • Vim.hs
          • Dot/
            • Backend.hs
            • Base.hs
          • HTML/
            • Backend.hs
            • Base.hs
          • LaTeX/
            • Backend.hs
            • Base.hs
        • Library/
          • Base.hs
          • Parse.hs
        • Options/
          • Base.hs
          • HasOptions.hs
          • Help.hs
          • Lenses.hs
          • Warnings.hs
        • Response/
          • Base.hs
      • Mimer/
        • Mimer.hs
        • Options.hs
      • Syntax/
        • Abstract.hs
        • Builtin.hs
        • Common.hs
        • Concrete.hs
        • DoNotation.hs
        • Fixity.hs
        • IdiomBrackets.hs
        • Info.hs
        • Internal.hs
        • Literal.hs
        • Notation.hs
        • Parser.hs
        • Position.hs
        • Position.hs-boot
        • Reflected.hs
        • TopLevelModuleName.hs
        • Treeless.hs
        • Abstract/
          • Name.hs
          • Pattern.hs
          • PatternSynonyms.hs
          • Pretty.hs
          • UsedNames.hs
          • Views.hs
        • Common/
          • Aspect.hs
          • KeywordRange.hs
          • Pretty.hs
          • Pretty/
            • ANSI.hs
        • Concrete/
          • Attribute.hs
          • Definitions.hs
          • Fixity.hs
          • Generic.hs
          • Glyph.hs
          • Name.hs
          • Operators.hs
          • Pattern.hs
          • Pretty.hs
          • Definitions/
            • Errors.hs
            • Monad.hs
            • Types.hs
          • Operators/
            • Parser.hs
            • Parser/
              • Monad.hs
        • Internal/
          • Blockers.hs
          • Defs.hs
          • Elim.hs
          • Generic.hs
          • MetaVars.hs
          • Names.hs
          • Pattern.hs
          • SanityCheck.hs
          • Univ.hs
        • Parser/
          • Alex.hs
          • Comments.hs
          • Helpers.hs
          • Layout.hs
          • Layout.hs-boot
          • LexActions.hs
          • LexActions.hs-boot
          • Lexer.x
          • Literate.hs
          • LookAhead.hs
          • Monad.hs
          • Parser.y
          • StringLiterals.hs
          • Tokens.hs
        • Scope/
          • Base.hs
          • Flat.hs
          • Monad.hs
        • TopLevelModuleName/
          • Boot.hs
        • Translation/
          • AbstractToConcrete.hs
          • ConcreteToAbstract.hs
          • InternalToAbstract.hs
          • ReflectedToAbstract.hs
      • Termination/
        • CallGraph.hs
        • CallMatrix.hs
        • CutOff.hs
        • Monad.hs
        • Order.hs
        • RecCheck.hs
        • Semiring.hs
        • SparseMatrix.hs
        • TermCheck.hs
        • Termination.hs
      • TypeChecking/
        • Abstract.hs
        • CheckInternal.hs
        • CheckInternal.hs-boot
        • CompiledClause.hs
        • Constraints.hs
        • Constraints.hs-boot
        • Conversion.hs
        • Conversion.hs-boot
        • Coverage.hs
        • Datatypes.hs
        • Datatypes.hs-boot
        • DeadCode.hs
        • DiscrimTree.hs
        • DisplayForm.hs
        • DropArgs.hs
        • Empty.hs
        • Empty.hs-boot
        • Errors.hs
        • Errors.hs-boot
        • EtaContract.hs
        • Forcing.hs
        • Free.hs
        • Functions.hs
        • Generalize.hs
        • IApplyConfluence.hs
        • Implicit.hs
        • Injectivity.hs
        • Inlining.hs
        • InstanceArguments.hs
        • InstanceArguments.hs-boot
        • Irrelevance.hs
        • Irrelevance.hs-boot
        • Level.hs
        • Level.hs-boot
        • LevelConstraints.hs
        • Lock.hs
        • Lock.hs-boot
        • MetaVars.hs
        • MetaVars.hs-boot
        • Modalities.hs
        • Monad.hs
        • Names.hs
        • Opacity.hs
        • Opacity.hs-boot
        • Polarity.hs
        • Polarity.hs-boot
        • Positivity.hs
        • Pretty.hs
        • Pretty.hs-boot
        • Primitive.hs
        • Primitive.hs-boot
        • ProjectionLike.hs
        • ProjectionLike.hs-boot
        • Quote.hs
        • ReconstructParameters.hs
        • RecordPatterns.hs
        • Records.hs
        • Records.hs-boot
        • Reduce.hs
        • Reduce.hs-boot
        • Rewriting.hs
        • Rewriting.hs-boot
        • Serialise.hs
        • SizedTypes.hs
        • Sort.hs
        • Substitute.hs
        • SyntacticEquality.hs
        • Telescope.hs
        • Telescope.hs-boot
        • Unquote.hs
        • Warnings.hs
        • With.hs
        • CompiledClause/
          • Compile.hs
          • Compile.hs-boot
          • Match.hs
          • Match.hs-boot
        • Conversion/
          • Pure.hs
        • Coverage/
          • Cubical.hs
          • Match.hs
          • SplitClause.hs
          • SplitTree.hs
        • DiscrimTree/
          • Types.hs
        • Free/
          • Lazy.hs
          • Precompute.hs
          • Reduce.hs
        • Level/
          • Solve.hs
        • MetaVars/
          • Mention.hs
          • Occurs.hs
        • Monad/
          • Base.hs
          • Base.hs-boot
          • Benchmark.hs
          • Builtin.hs
          • Builtin.hs-boot
          • Caching.hs
          • Closure.hs
          • Constraints.hs
          • Context.hs
          • Context.hs-boot
          • Debug.hs
          • Debug.hs-boot
          • Env.hs
          • Imports.hs
          • MetaVars.hs
          • MetaVars.hs-boot
          • Modality.hs
          • Mutual.hs
          • Open.hs
          • Options.hs
          • Options.hs-boot
          • Pure.hs
          • Pure.hs-boot
          • Signature.hs
          • Signature.hs-boot
          • SizedTypes.hs
          • State.hs
          • Statistics.hs
          • Trace.hs
          • Base/
            • Types.hs
            • Warning.hs
        • Patterns/
          • Abstract.hs
          • Internal.hs
          • Match.hs
          • Match.hs-boot
        • Positivity/
          • Occurrence.hs
        • Pretty/
          • Call.hs
          • Call.hs-boot
          • Constraint.hs
          • Constraint.hs-boot
          • Warning.hs
          • Warning.hs-boot
        • Primitive/
          • Base.hs
          • Cubical.hs
          • Cubical/
            • Base.hs
            • Base.hs-boot
            • Glue.hs
            • HCompU.hs
            • Id.hs
        • Reduce/
          • Fast.hs
          • Fast.hs-boot
          • Monad.hs
        • Rewriting/
          • Clause.hs
          • Confluence.hs
          • NonLinMatch.hs
          • NonLinPattern.hs
        • Rules/
          • Application.hs
          • Application.hs-boot
          • Builtin.hs
          • Data.hs
          • Data.hs-boot
          • Decl.hs
          • Decl.hs-boot
          • Def.hs
          • Def.hs-boot
          • Display.hs
          • LHS.hs
          • Record.hs
          • Term.hs
          • Term.hs-boot
          • Builtin/
            • Coinduction.hs
            • Coinduction.hs-boot
          • LHS/
            • Implicit.hs
            • Problem.hs
            • ProblemRest.hs
            • Unify.hs
            • Unify/
              • LeftInverse.hs
              • Types.hs
        • Serialise/
          • Base.hs
          • Instances.hs
          • Instances/
            • Abstract.hs
            • Common.hs
            • Compilers.hs
            • Errors.hs
            • Highlighting.hs
            • Internal.hs
        • SizedTypes/
          • Pretty.hs
          • Solve.hs
          • Syntax.hs
          • Utils.hs
          • WarshallSolver.hs
        • Substitute/
          • Class.hs
          • DeBruijn.hs
        • Telescope/
          • Path.hs
      • Utils/
        • AffineHole.hs
        • Applicative.hs
        • AssocList.hs
        • Bag.hs
        • Benchmark.hs
        • BiMap.hs
        • BoolSet.hs
        • Boolean.hs
        • CallStack.hs
        • Char.hs
        • Cluster.hs
        • Either.hs
        • Empty.hs
        • Environment.hs
        • Fail.hs
        • Favorites.hs
        • FileName.hs
        • Float.hs
        • Function.hs
        • Functor.hs
        • Hash.hs
        • HashTable.hs
        • IArray.hs
        • IO.hs
        • IORef.hs
        • Impossible.hs
        • IndexedList.hs
        • Lens.hs
        • List.hs
        • List1.hs
        • List1.hs-boot
        • List2.hs
        • ListT.hs
        • Map.hs
        • Maybe.hs
        • Memo.hs
        • Monad.hs
        • Monoid.hs
        • Null.hs
        • POMonoid.hs
        • PartialOrd.hs
        • Permutation.hs
        • Pointer.hs
        • ProfileOptions.hs
        • RangeMap.hs
        • SemiRing.hs
        • Semigroup.hs
        • Singleton.hs
        • Size.hs
        • SmallSet.hs
        • String.hs
        • Suffix.hs
        • Three.hs
        • Time.hs
        • Trie.hs
        • Tuple.hs
        • TypeLevel.hs
        • TypeLits.hs
        • Unsafe.hs
        • Update.hs
        • VarSet.hs
        • Warshall.hs
        • WithDefault.hs
        • Zipper.hs
        • CallStack/
          • Base.hs
          • Pretty.hs
        • Graph/
          • TopSort.hs
          • AdjacencyMap/
            • Unidirectional.hs
        • Haskell/
          • Syntax.hs
        • IO/
          • Binary.hs
          • Directory.hs
          • TempFile.hs
          • UTF8.hs
        • IntSet/
          • Infinite.hs
        • Lens/
          • Examples.hs
        • Maybe/
          • Strict.hs
        • Parser/
          • MemoisedCPS.hs
  • main/
    • Main.hs