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

Directory listing for Agda-2.8.0 candidate source tarball

Agda-2.8.0/src/

• agda-mode/
  • Main.hs
• data/
  • JS/
    • agda-rts.amd.js
    • agda-rts.js
    • agda-rts.mjs
  • 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
            • 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
    • Compiler/
      • Backend.hs
      • Builtin.hs
      • 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
      • BuildLibrary.hs
      • Command.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
        • Errors.hs
        • HasOptions.hs
        • Help.hs
        • Lenses.hs
        • Types.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
      • Errors/
        • Names.hs
      • Free/
        • Lazy.hs
        • Precompute.hs
        • Reduce.hs
      • Level/
        • Solve.hs
      • MetaVars/
        • Mention.hs
        • Occurs.hs
      • Monad/
        • Base.hs
        • 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
      • 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
      • FileId.hs
      • FileName.hs
      • Float.hs
      • Function.hs
      • Functor.hs
      • GetOpt.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
      • Map1.hs
      • Maybe.hs
      • Memo.hs
      • Monad.hs
      • Monoid.hs
      • Null.hs
      • POMonoid.hs
      • PartialOrd.hs
      • Permutation.hs
      • ProfileOptions.hs
      • RangeMap.hs
      • SemiRing.hs
      • Semigroup.hs
      • Set1.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
      • 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
• setup/
  • Agda/
    • Setup.hs
    • Version.hs
    • VersionCommit.hs
    • Setup/
      • DataFiles.hs
      • EmacsMode.hs