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

Directory listing for Agda-2.4.2.3 source tarball

Agda-2.4.2.3/

• Agda.cabal
• CHANGELOG
• LICENSE
• README.md
• Setup.hs
• dist/
  • build/
    • Agda/
      • Syntax/
        • Parser/
          • Lexer.hs
          • Parser.hs
• src/
  • agda-mode/
    • Main.hs
  • data/
    • Agda.css
    • agda.sty
    • postprocess-latex.pl
    • emacs-mode/
      • agda-input.el
      • agda2-abbrevs.el
      • agda2-highlight.el
      • agda2-mode.el
      • agda2-queue.el
      • agda2.el
      • annotation.el
      • eri.el
    • lib/
      • prim/
        • Agda/
          • Primitive.agda
  • full/
    • undefined.h
    • Agda/
      • ImpossibleTest.hs
      • Main.hs
      • Tests.hs
      • TheTypeChecker.hs
      • Version.hs
      • Auto/
        • Auto.hs
        • CaseSplit.hs
        • Convert.hs
        • NarrowingSearch.hs
        • SearchControl.hs
        • Syntax.hs
        • Typecheck.hs
      • Compiler/
        • CallCompiler.hs
        • HaskellTypes.hs
        • Epic/
          • AuxAST.hs
          • CaseOpts.hs
          • CompileState.hs
          • Compiler.hs
          • Epic.hs
          • Erasure.hs
          • ForceConstrs.hs
          • Forcing.hs
          • FromAgda.hs
          • Injection.hs
          • Interface.hs
          • NatDetection.hs
          • Primitive.hs
          • Smashing.hs
          • Static.hs
        • JS/
          • Case.hs
          • Compiler.hs
          • Parser.hs
          • Pretty.hs
          • Substitution.hs
          • Syntax.hs
        • MAlonzo/
          • Compiler.hs
          • Compiler.hs-boot
          • Encode.hs
          • Misc.hs
          • Pretty.hs
          • Primitives.hs
      • Interaction/
        • BasicOps.hs
        • CommandLine.hs
        • EmacsCommand.hs
        • EmacsTop.hs
        • Exceptions.hs
        • FindFile.hs
        • FindFile.hs-boot
        • Imports.hs
        • Imports.hs-boot
        • InteractionTop.hs
        • InteractionTop.hs-boot
        • MakeCase.hs
        • Monad.hs
        • Options.hs
        • Response.hs
        • Response.hs-boot
        • Highlighting/
          • Dot.hs
          • Emacs.hs
          • Generate.hs
          • Generate.hs-boot
          • HTML.hs
          • LaTeX.hs
          • Precise.hs
          • Range.hs
          • Vim.hs
        • Options/
          • Lenses.hs
      • Syntax/
        • Abstract.hs
        • Common.hs
        • Concrete.hs
        • Fixity.hs
        • Fixity.hs-boot
        • Info.hs
        • Internal.hs
        • Literal.hs
        • Notation.hs
        • Parser.hs
        • Position.hs
        • Abstract/
          • Copatterns.hs
          • Name.hs
          • Name.hs-boot
          • Pretty.hs
          • Views.hs
        • Concrete/
          • Definitions.hs
          • Generic.hs
          • Name.hs
          • Operators.hs
          • Pretty.hs
          • Operators/
            • Parser.hs
        • Internal/
          • Defs.hs
          • Generic.hs
          • Pattern.hs
        • Parser/
          • Alex.hs
          • Comments.hs
          • Layout.hs
          • Layout.hs-boot
          • LexActions.hs
          • LexActions.hs-boot
          • Lexer.x
          • LookAhead.hs
          • Monad.hs
          • Parser.y
          • StringLiterals.hs
          • Tokens.hs
        • Scope/
          • Base.hs
          • Monad.hs
        • Translation/
          • AbstractToConcrete.hs
          • ConcreteToAbstract.hs
          • InternalToAbstract.hs
      • Termination/
        • CallGraph.hs
        • CallMatrix.hs
        • CutOff.hs
        • Inlining.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
        • DisplayForm.hs
        • DropArgs.hs
        • Empty.hs
        • Empty.hs-boot
        • Errors.hs
        • Errors.hs-boot
        • EtaContract.hs
        • Forcing.hs
        • Free.hs
        • Implicit.hs
        • Injectivity.hs
        • InstanceArguments.hs
        • InstanceArguments.hs-boot
        • Irrelevance.hs
        • Level.hs
        • Level.hs-boot
        • LevelConstraints.hs
        • MetaVars.hs
        • MetaVars.hs-boot
        • Monad.hs
        • Polarity.hs
        • Polarity.hs-boot
        • Positivity.hs
        • Pretty.hs
        • Pretty.hs-boot
        • Primitive.hs
        • ProjectionLike.hs
        • ProjectionLike.hs-boot
        • Quote.hs
        • RecordPatterns.hs
        • Records.hs
        • Records.hs-boot
        • Reduce.hs
        • Rewriting.hs
        • Rewriting.hs-boot
        • Serialise.hs
        • SizedTypes.hs
        • Substitute.hs
        • SyntacticEquality.hs
        • Telescope.hs
        • Tests.hs
        • Unquote.hs
        • With.hs
        • CompiledClause/
          • Compile.hs
          • Compile.hs-boot
          • Match.hs
          • Match.hs-boot
        • Coverage/
          • Match.hs
          • SplitTree.hs
        • MetaVars/
          • Mention.hs
          • Occurs.hs
        • Monad/
          • Base.hs
          • Base.hs-boot
          • Benchmark.hs
          • Builtin.hs
          • Closure.hs
          • Constraints.hs
          • Context.hs
          • Context.hs-boot
          • Debug.hs
          • Env.hs
          • Exception.hs
          • Imports.hs
          • MetaVars.hs
          • Mutual.hs
          • Open.hs
          • Options.hs
          • Options.hs-boot
          • Sharing.hs
          • Signature.hs
          • SizedTypes.hs
          • State.hs
          • Statistics.hs
          • Trace.hs
          • Base/
            • Benchmark.hs
            • KillRange.hs
        • Patterns/
          • Abstract.hs
          • Match.hs
          • Match.hs-boot
        • Reduce/
          • Monad.hs
        • Rewriting/
          • NonLinMatch.hs
        • Rules/
          • Builtin.hs
          • Data.hs
          • Decl.hs
          • Decl.hs-boot
          • Def.hs
          • Def.hs-boot
          • LHS.hs
          • Record.hs
          • Term.hs
          • Term.hs-boot
          • Builtin/
            • Coinduction.hs
            • Coinduction.hs-boot
          • LHS/
            • Implicit.hs
            • Instantiate.hs
            • Problem.hs
            • ProblemRest.hs
            • Split.hs
            • Unify.hs
        • SizedTypes/
          • Solve.hs
          • Syntax.hs
          • Tests.hs
          • Utils.hs
          • WarshallSolver.hs
        • Test/
          • Generators.hs
      • Utils/
        • AssocList.hs
        • Bag.hs
        • BiMap.hs
        • Char.hs
        • Cluster.hs
        • Either.hs
        • Empty.hs
        • Except.hs
        • Favorites.hs
        • FileName.hs
        • Function.hs
        • Functor.hs
        • Geniplate.hs
        • Hash.hs
        • HashMap.hs
        • IORef.hs
        • Impossible.hs
        • Lens.hs
        • List.hs
        • ListT.hs
        • Map.hs
        • Maybe.hs
        • Monad.hs
        • Null.hs
        • PartialOrd.hs
        • Permutation.hs
        • Pointer.hs
        • Pretty.hs
        • QuickCheck.hs
        • ReadP.hs
        • SemiRing.hs
        • Singleton.hs
        • Size.hs
        • String.hs
        • Suffix.hs
        • TestHelpers.hs
        • Time.hs
        • Trie.hs
        • Tuple.hs
        • Update.hs
        • VarSet.hs
        • Warshall.hs
        • Graph/
          • AdjacencyMap.hs
          • AdjacencyMap/
            • Unidirectional.hs
        • IO/
          • Binary.hs
          • UTF8.hs
        • Lens/
          • Examples.hs
        • ListT/
          • Tests.hs
        • Map/
          • Compat.hs
        • Maybe/
          • Strict.hs
        • Permutation/
          • Tests.hs
  • main/
    • Main.hs