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

Directory listing for Agda-2.6.3.20230805 candidate source tarball

Agda-2.6.3.20230805/src/full/

• Agda/
  • Benchmarking.hs
  • ImpossibleTest.hs
  • Main.hs
  • TheTypeChecker.hs
  • Version.hs
  • VersionCommit.hs
  • Auto/
    • Auto.hs
    • CaseSplit.hs
    • Convert.hs
    • NarrowingSearch.hs
    • Options.hs
    • SearchControl.hs
    • Syntax.hs
    • Typecheck.hs
  • Compiler/
    • Backend.hs
    • Backend.hs-boot
    • Builtin.hs
    • Builtin.hs-boot
    • CallCompiler.hs
    • Common.hs
    • ToTreeless.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
    • Response.hs
    • Response.hs-boot
    • 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
  • 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
    • TopLevelModuleName.hs-boot
    • Treeless.hs
    • Abstract/
      • Name.hs
      • Pattern.hs
      • PatternSynonyms.hs
      • Pretty.hs
      • UsedNames.hs
      • Views.hs
    • Common/
      • Aspect.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
      • Layout.hs
      • Layout.hs-boot
      • LexActions.hs
      • LexActions.hs-boot
      • Lexer.hs
      • Lexer.x
      • Literate.hs
      • LookAhead.hs
      • Monad.hs
      • Parser.y
      • StringLiterals.hs
      • Tokens.hs
    • Scope/
      • Base.hs
      • Flat.hs
      • Monad.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
    • DisplayForm.hs
    • DropArgs.hs
    • Empty.hs
    • Empty.hs-boot
    • Errors.hs
    • Errors.hs-boot
    • EtaContract.hs
    • EtaExpand.hs
    • Forcing.hs
    • Free.hs
    • Functions.hs
    • Generalize.hs
    • IApplyConfluence.hs
    • Implicit.hs
    • Injectivity.hs
    • Inlining.hs
    • InstanceArguments.hs
    • 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
    • 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
    • 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/
      • 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
    • 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