cabal-version: 2.4 name: Agda version: 2.6.20240731 build-type: Custom license: MIT license-file: LICENSE copyright: (c) 2005-2024 The Agda Team. author: The Agda Team, see https://agda.readthedocs.io/en/latest/team.html maintainer: The Agda Team homepage: https://wiki.portal.chalmers.se/agda/ bug-reports: https://github.com/agda/agda/issues category: Dependent types synopsis: A dependently typed functional programming language and proof assistant description: Agda is a dependently typed functional programming language: It has inductive families, which are similar to Haskell's GADTs, but they can be indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist in the development of your code). . Agda is also a proof assistant: It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Idris, Lean and NuPRL. . This package includes both a command-line program (agda) and an Emacs mode. If you want to use the Emacs mode you can set it up by running @agda-mode setup@ (see the README). . Note that the Agda package does not follow the package versioning policy, because it is not intended to be used by third-party packages. tested-with: GHC == 9.10.1 GHC == 9.8.2 GHC == 9.6.6 GHC == 9.4.8 GHC == 9.2.8 GHC == 9.0.2 GHC == 8.10.7 GHC == 8.8.4 GHC == 8.6.5 extra-doc-files: CHANGELOG.md README.md doc/user-manual/agda.svg doc/release-notes/2.6.4.3.md doc/release-notes/2.6.4.2.md doc/release-notes/2.6.4.1.md doc/release-notes/2.6.4.md doc/release-notes/2.6.3.md doc/release-notes/2.6.2.2.md doc/release-notes/2.6.2.1.md doc/release-notes/2.6.2.md doc/release-notes/2.6.1.3.md doc/release-notes/2.6.1.2.md doc/release-notes/2.6.1.1.md doc/release-notes/2.6.1.md doc/release-notes/2.6.0.1.md doc/release-notes/2.6.0.md doc/release-notes/2.5.4.2.md doc/release-notes/2.5.4.1.md doc/release-notes/2.5.4.md doc/release-notes/2.5.3.md doc/release-notes/2.5.2.md doc/release-notes/2.5.1.2.md doc/release-notes/2.5.1.1.md doc/release-notes/2.5.1.md doc/release-notes/2.4.2.5.md doc/release-notes/2.4.2.4.md doc/release-notes/2.4.2.3.md doc/release-notes/2.4.2.2.md doc/release-notes/2.4.2.1.md doc/release-notes/2.4.2.md doc/release-notes/2.4.0.2.md doc/release-notes/2.4.0.1.md doc/release-notes/2.4.0.md doc/release-notes/2.3.2.2.md doc/release-notes/2.3.2.1.md doc/release-notes/2.3.2.md doc/release-notes/2.3.0.md doc/release-notes/2.2.10.md doc/release-notes/2.2.8.md doc/release-notes/2.2.6.md doc/release-notes/2.2.2.md doc/release-notes/2.2.4.md doc/release-notes/2.2.0.md extra-source-files: stack-9.10.1.yaml stack-9.8.2.yaml stack-9.6.6.yaml stack-9.4.8.yaml stack-9.2.8.yaml stack-9.0.2.yaml stack-8.10.7.yaml stack-8.8.4.yaml data-dir: src/data data-files: emacs-mode/*.el html/Agda.css html/highlight-hover.js JS/agda-rts.js JS/agda-rts.amd.js latex/agda.sty latex/postprocess-latex.pl lib/prim/agda-builtins.agda-lib lib/prim/Agda/Builtin/Bool.agda lib/prim/Agda/Builtin/Char.agda lib/prim/Agda/Builtin/Char/Properties.agda lib/prim/Agda/Builtin/Coinduction.agda lib/prim/Agda/Builtin/Cubical/Path.agda lib/prim/Agda/Builtin/Cubical/Id.agda lib/prim/Agda/Builtin/Cubical/Sub.agda lib/prim/Agda/Builtin/Cubical/Glue.agda lib/prim/Agda/Builtin/Cubical/Equiv.agda lib/prim/Agda/Builtin/Cubical/HCompU.agda lib/prim/Agda/Builtin/Equality.agda lib/prim/Agda/Builtin/Equality/Erase.agda lib/prim/Agda/Builtin/Equality/Rewrite.agda lib/prim/Agda/Builtin/Float.agda lib/prim/Agda/Builtin/Float/Properties.agda lib/prim/Agda/Builtin/FromNat.agda lib/prim/Agda/Builtin/FromNeg.agda lib/prim/Agda/Builtin/FromString.agda lib/prim/Agda/Builtin/IO.agda lib/prim/Agda/Builtin/Int.agda lib/prim/Agda/Builtin/List.agda lib/prim/Agda/Builtin/Maybe.agda lib/prim/Agda/Builtin/Nat.agda lib/prim/Agda/Builtin/Reflection.agda lib/prim/Agda/Builtin/Reflection/External.agda lib/prim/Agda/Builtin/Reflection/Properties.agda lib/prim/Agda/Builtin/Sigma.agda lib/prim/Agda/Builtin/Size.agda lib/prim/Agda/Builtin/Strict.agda lib/prim/Agda/Builtin/String.agda lib/prim/Agda/Builtin/String/Properties.agda lib/prim/Agda/Builtin/TrustMe.agda lib/prim/Agda/Builtin/Unit.agda lib/prim/Agda/Builtin/Word.agda lib/prim/Agda/Builtin/Word/Properties.agda lib/prim/Agda/Primitive.agda lib/prim/Agda/Primitive/Cubical.agda MAlonzo/src/MAlonzo/*.hs MAlonzo/src/MAlonzo/RTE/*.hs source-repository head type: git location: https://github.com/agda/agda.git source-repository this type: git location: https://github.com/agda/agda.git tag: v2.6.20240731 -- Build flags --------------------------------------------------------------------------- flag debug default: False manual: True description: Enable debug printing. This makes Agda slightly slower, and building Agda slower as well. The --verbose=N option only has an effect when Agda was built with this flag. flag debug-serialisation default: False manual: True description: Enable debug mode in serialisation. This makes serialisation slower. flag debug-parsing default: False manual: True description: Enable debug mode in parsing. This makes parsing slower. flag enable-cluster-counting default: False manual: True description: Enable the --count-clusters flag. (If enable-cluster-counting is False, then the --count-clusters flag triggers an error message.) flag optimise-heavily default: False manual: True description: Enable some expensive optimisations when compiling Agda. -- Setup --------------------------------------------------------------------------- custom-setup setup-depends: , base >= 4.12.0.0 && < 4.21 , Cabal >= 2.4.0.1 && < 3.13 , directory >= 1.3.3.0 && < 1.4 , filepath >= 1.4.2.1 && < 1.6 , process >= 1.6.3.0 && < 1.7 -- Common stanzas --------------------------------------------------------------------------- common language if flag(optimise-heavily) cpp-options: -DOPTIMISE_HEAVILY ghc-options: -fexpose-all-unfoldings -fspecialise-aggressively ghc-options: -- ASR (2022-05-31). Workaround to Issue #5932. -Wwarn -Wwarn=cpp-undef -Wwarn=deprecated-flags -Wwarn=deriving-typeable -Wwarn=dodgy-exports -Wwarn=dodgy-foreign-imports -Wwarn=dodgy-imports -Wwarn=duplicate-exports -Wwarn=empty-enumerations -Wwarn=identities -Wwarn=inaccessible-code -Wwarn=inline-rule-shadowing -Wwarn=missing-fields -Wwarn=missing-home-modules -Wwarn=missing-methods -Wwarn=missing-pattern-synonym-signatures -Wwarn=missing-signatures -Wwarn=noncanonical-monad-instances -Wwarn=noncanonical-monoid-instances -Wwarn=overflowed-literals -Wwarn=overlapping-patterns -- -Wwarn=redundant-constraints -Wwarn=simplifiable-class-constraints -Wwarn=star-binder -Wwarn=star-is-type -Wwarn=tabs -Wwarn=typed-holes -Wwarn=unbanged-strict-patterns -Wwarn=unrecognised-pragmas -Wwarn=unrecognised-warning-flags -Wwarn=unticked-promoted-constructors -Wwarn=unused-do-bind -Wwarn=unused-foralls -Wwarn=warnings-deprecations -Wwarn=wrong-do-bind -- The following warning is an error in GHC >= 8.10. if impl(ghc < 8.10) ghc-options: -Wwarn=implicit-kind-vars -- #6623: Turn off this (nameless) warning: -- "Pattern match checker exceeded (2000000) iterations in a case alternative." -- See: https://gitlab.haskell.org/ghc/ghc/-/issues/13464 -Wno-incomplete-patterns -Wno-overlapping-patterns if impl(ghc < 9.10) ghc-options: -Wwarn=semigroup -- The semigroup warning is deprecated in GHC 9.10 if impl(ghc >= 8.8) ghc-options: -Wwarn=missed-extra-shared-lib if impl(ghc >= 8.10) ghc-options: -Wwarn=compat-unqualified-imports -Wwarn=deriving-defaults -Wwarn=redundant-record-wildcards -Wwarn=unused-packages -Wwarn=unused-record-wildcards if impl(ghc >= 9.0) ghc-options: -Wwarn=invalid-haddock -- #6137: coverage checker works only sufficiently well from GHC 9.0 -Wwarn=incomplete-patterns -Wwarn=incomplete-record-updates -Wwarn=overlapping-patterns -- ASR (2022-04-27). This warning was added in GHC 9.0.2, removed -- from 9.2.1 and added back in 9.2.2. if impl(ghc == 9.0.2 || >= 9.2.2) ghc-options: -Wwarn=unicode-bidirectional-format-characters if impl(ghc >= 9.2) ghc-options: -Wwarn=operator-whitespace -Wwarn=redundant-bang-patterns if impl(ghc >= 9.4) ghc-options: -Wwarn=type-equality-out-of-scope if impl(ghc >= 9.4 && < 9.10) ghc-options: -Wwarn=forall-identifier -- The forall-identifier warning is deprecated in GHC 9.10 default-language: Haskell2010 -- NOTE: If adding or removing default extensions, also change: -- .hlint.yaml default-extensions: BangPatterns BlockArguments ConstraintKinds --L-T Chen (2019-07-15): -- Enabling DataKinds only locally makes the compile time -- slightly shorter, see PR #3920. -- DataKinds DefaultSignatures DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies ExistentialQuantification FlexibleContexts FlexibleInstances FunctionalDependencies GADTs GeneralizedNewtypeDeriving InstanceSigs LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns OverloadedStrings PatternSynonyms RankNTypes RecordWildCards ScopedTypeVariables StandaloneDeriving TupleSections TypeFamilies TypeOperators TypeSynonymInstances ViewPatterns other-extensions: CPP DeriveAnyClass PartialTypeSignatures -- Agda library --------------------------------------------------------------------------- library import: language hs-source-dirs: src/full -- Andreas, 2021-03-10: -- All packages we depend upon should be mentioned in an unconditional -- build-depends field, but additional restrictions on their -- version for specific GHCs may be placed in conditionals. -- -- The goal is to be able to make (e.g. when a new GHC comes out) -- revisions on hackage, e.g. relaxing upper bounds. This process -- currently does not support revising conditionals. -- -- An exceptions are packages that are only needed for certain configurations, -- like for flags, Windows, etc. if flag(debug) cpp-options: -DDEBUG if flag(debug-serialisation) cpp-options: -DDEBUG_SERIALISATION if flag(debug-parsing) cpp-options: -DDEBUG_PARSING if flag(enable-cluster-counting) cpp-options: -DCOUNT_CLUSTERS build-depends: text-icu >= 0.7.1.0 if os(windows) build-depends: Win32 >= 2.6.1.0 && < 2.15 -- Agda cannot be built with GHC 8.6.1 due to a compiler bug, see -- Agda Issue #3344. if impl(ghc == 8.6.1) buildable: False -- Agda cannot be built with Windows and GHC 8.6.3 due to a compiler -- bug, see Agda Issue #3657. if os(windows) && impl(ghc == 8.6.3) buildable: False -- For libraries that come with GHC, we take the shipped version as default lower bound. build-depends: -- Please keep in alphabetical order! , aeson >= 1.1.2.0 && < 2.3 , ansi-terminal >= 0.9 && < 1.2 , array >= 0.5.2.0 && < 0.6 , async >= 2.2 && < 2.3 , base >= 4.12.0.0 && < 4.21 , binary >= 0.8.6.0 && < 0.9 , blaze-html >= 0.8 && < 0.10 , boxes >= 0.1.3 && < 0.2 , bytestring >= 0.10.8.2 && < 0.13 , case-insensitive >= 1.2.0.4 && < 1.3 , containers >= 0.6.0.1 && < 0.8 , data-hash >= 0.2.0.0 && < 0.3 , deepseq >= 1.4.4.0 && < 1.6 , directory >= 1.3.3.0 && < 1.4 , dlist >= 0.8 && < 1.1 , edit-distance >= 0.2.1.2 && < 0.3 , equivalence >= 0.3.2 && < 0.5 -- exceptions-0.8 instead of 0.10 because of stack , exceptions >= 0.8 && < 0.11 , filepath >= 1.4.2.1 && < 1.6 , ghc-compact == 0.1.* , gitrev >= 1.3.1 && < 2 -- hashable 1.2.0.10 makes library-test 10x -- slower. The issue was fixed in hashable 1.2.1.0. -- https://github.com/tibbe/hashable/issues/57. , hashable >= 1.2.1.0 && < 1.5 , haskeline >= 0.7.4.3 && < 0.9 -- monad-control-1.0.1.0 is the first to contain liftThrough , monad-control >= 1.0.1.0 && < 1.1 , mtl >= 2.2.2 && < 2.4 , murmur-hash >= 0.1 && < 0.2 , parallel >= 3.2.2.0 && < 3.3 , peano >= 0.1.0.1 && < 0.2 , pqueue >= 1.4.1.2 && < 1.6 , pretty >= 1.1.3.3 && < 1.2 , process >= 1.6.3.0 && < 1.7 , regex-tdfa >= 1.3.1.0 && < 1.4 , split >= 0.2.0.0 && < 0.3 , stm >= 2.4.4 && < 2.6 , STMonadTrans >= 0.4.3 && < 0.5 , strict >= 0.4.0.1 && < 0.6 , text >= 1.2.3.1 && < 2.2 , time >= 1.9.2 && < 1.15 , transformers >= 0.5.5.0 && < 0.7 , unordered-containers >= 0.2.9.0 && < 0.3 -- unordered-containers < 0.2.9 need base < 4.11 , uri-encode >= 1.5.0.4 && < 1.6 , vector >= 0.12 && < 0.14 , vector-hashtables >= 0.1.1.1 && < 0.2 , zlib >= 0.6 && < 0.8 -- We don't write upper bounds for Alex nor Happy because the -- `build-tool-depends` field can not be modified in Hackage. build-tool-depends: , alex:alex >= 3.2.3 -- alex-3.2.3 is packaged with Ubuntu 18.04 , happy:happy >= 1.19.8 -- happy-1.19.8 is packaged with Ubuntu 18.04 exposed-modules: Agda.Benchmarking Agda.Compiler.Backend Agda.Compiler.Backend.Base Agda.Compiler.Builtin Agda.Compiler.CallCompiler Agda.Compiler.Common Agda.Compiler.JS.Compiler Agda.Compiler.JS.Syntax Agda.Compiler.JS.Substitution Agda.Compiler.JS.Pretty Agda.Compiler.MAlonzo.Coerce Agda.Compiler.MAlonzo.Compiler Agda.Compiler.MAlonzo.Encode Agda.Compiler.MAlonzo.HaskellTypes Agda.Compiler.MAlonzo.Misc Agda.Compiler.MAlonzo.Pragmas Agda.Compiler.MAlonzo.Pretty Agda.Compiler.MAlonzo.Primitives Agda.Compiler.MAlonzo.Strict Agda.Compiler.ToTreeless Agda.Compiler.Treeless.AsPatterns Agda.Compiler.Treeless.Builtin Agda.Compiler.Treeless.Compare Agda.Compiler.Treeless.EliminateDefaults Agda.Compiler.Treeless.EliminateLiteralPatterns Agda.Compiler.Treeless.Erase Agda.Compiler.Treeless.GuardsToPrims Agda.Compiler.Treeless.Identity Agda.Compiler.Treeless.NormalizeNames Agda.Compiler.Treeless.Pretty Agda.Compiler.Treeless.Simplify Agda.Compiler.Treeless.Subst Agda.Compiler.Treeless.Uncase Agda.Compiler.Treeless.Unused Agda.ImpossibleTest Agda.Interaction.AgdaTop Agda.Interaction.Base Agda.Interaction.BasicOps Agda.Interaction.SearchAbout Agda.Interaction.CommandLine Agda.Interaction.EmacsCommand Agda.Interaction.EmacsTop Agda.Interaction.ExitCode Agda.Interaction.JSONTop Agda.Interaction.JSON Agda.Interaction.FindFile Agda.Interaction.Highlighting.Common Agda.Interaction.Highlighting.Dot Agda.Interaction.Highlighting.Emacs Agda.Interaction.Highlighting.FromAbstract Agda.Interaction.Highlighting.Generate Agda.Interaction.Highlighting.HTML Agda.Interaction.Highlighting.JSON Agda.Interaction.Highlighting.Precise Agda.Interaction.Highlighting.Range Agda.Interaction.Highlighting.Vim Agda.Interaction.Highlighting.LaTeX Agda.Interaction.Imports Agda.Interaction.InteractionTop Agda.Interaction.Output Agda.Interaction.Response Agda.Interaction.Response.Base Agda.Interaction.MakeCase Agda.Interaction.Monad Agda.Interaction.Library Agda.Interaction.Library.Base Agda.Interaction.Library.Parse Agda.Interaction.Options Agda.Interaction.Options.Help Agda.Interaction.Options.Lenses Agda.Interaction.Options.Warnings Agda.Main Agda.Mimer.Mimer Agda.Mimer.Options Agda.Syntax.Abstract.Name Agda.Syntax.Abstract.Pattern Agda.Syntax.Abstract.PatternSynonyms Agda.Syntax.Abstract.Pretty Agda.Syntax.Abstract.UsedNames Agda.Syntax.Abstract.Views Agda.Syntax.Abstract Agda.Syntax.Builtin Agda.Syntax.Common Agda.Syntax.Common.Aspect Agda.Syntax.Common.KeywordRange Agda.Syntax.Common.Pretty Agda.Syntax.Common.Pretty.ANSI Agda.Syntax.Concrete.Attribute Agda.Syntax.Concrete.Definitions Agda.Syntax.Concrete.Definitions.Errors Agda.Syntax.Concrete.Definitions.Monad Agda.Syntax.Concrete.Definitions.Types Agda.Syntax.Concrete.Fixity Agda.Syntax.Concrete.Generic Agda.Syntax.Concrete.Glyph Agda.Syntax.Concrete.Name Agda.Syntax.Concrete.Operators.Parser Agda.Syntax.Concrete.Operators.Parser.Monad Agda.Syntax.Concrete.Operators Agda.Syntax.Concrete.Pattern Agda.Syntax.Concrete.Pretty Agda.Syntax.Concrete Agda.Syntax.DoNotation Agda.Syntax.Fixity Agda.Syntax.IdiomBrackets Agda.Syntax.Info Agda.Syntax.Internal Agda.Syntax.Internal.Blockers Agda.Syntax.Internal.Defs Agda.Syntax.Internal.Elim Agda.Syntax.Internal.Generic Agda.Syntax.Internal.MetaVars Agda.Syntax.Internal.Names Agda.Syntax.Internal.Pattern Agda.Syntax.Internal.SanityCheck Agda.Syntax.Internal.Univ Agda.Syntax.Literal Agda.Syntax.Notation Agda.Syntax.Parser.Alex Agda.Syntax.Parser.Comments Agda.Syntax.Parser.Helpers Agda.Syntax.Parser.Layout Agda.Syntax.Parser.LexActions Agda.Syntax.Parser.Lexer Agda.Syntax.Parser.Literate Agda.Syntax.Parser.LookAhead Agda.Syntax.Parser.Monad Agda.Syntax.Parser.Parser Agda.Syntax.Parser.StringLiterals Agda.Syntax.Parser.Tokens Agda.Syntax.Parser Agda.Syntax.Position Agda.Syntax.Reflected Agda.Syntax.Scope.Base Agda.Syntax.Scope.Flat Agda.Syntax.Scope.Monad Agda.Syntax.TopLevelModuleName Agda.Syntax.TopLevelModuleName.Boot Agda.Syntax.Translation.AbstractToConcrete Agda.Syntax.Translation.ConcreteToAbstract Agda.Syntax.Translation.InternalToAbstract Agda.Syntax.Translation.ReflectedToAbstract Agda.Syntax.Treeless Agda.Termination.CallGraph Agda.Termination.CallMatrix Agda.Termination.CutOff Agda.Termination.Monad Agda.Termination.Order Agda.Termination.RecCheck Agda.Termination.SparseMatrix Agda.Termination.Semiring Agda.Termination.TermCheck Agda.Termination.Termination Agda.TheTypeChecker Agda.TypeChecking.Abstract Agda.TypeChecking.CheckInternal Agda.TypeChecking.CompiledClause Agda.TypeChecking.CompiledClause.Compile Agda.TypeChecking.CompiledClause.Match Agda.TypeChecking.Constraints Agda.TypeChecking.Conversion Agda.TypeChecking.Conversion.Pure Agda.TypeChecking.Coverage Agda.TypeChecking.Coverage.Match Agda.TypeChecking.Coverage.SplitTree Agda.TypeChecking.Coverage.SplitClause Agda.TypeChecking.Coverage.Cubical Agda.TypeChecking.Datatypes Agda.TypeChecking.DeadCode Agda.TypeChecking.DisplayForm Agda.TypeChecking.DropArgs Agda.TypeChecking.DiscrimTree Agda.TypeChecking.DiscrimTree.Types Agda.TypeChecking.Empty Agda.TypeChecking.EtaContract Agda.TypeChecking.Errors Agda.TypeChecking.Free Agda.TypeChecking.Free.Lazy Agda.TypeChecking.Free.Precompute Agda.TypeChecking.Free.Reduce Agda.TypeChecking.Forcing Agda.TypeChecking.Functions Agda.TypeChecking.Generalize Agda.TypeChecking.IApplyConfluence Agda.TypeChecking.Implicit Agda.TypeChecking.Injectivity Agda.TypeChecking.Inlining Agda.TypeChecking.InstanceArguments Agda.TypeChecking.Irrelevance Agda.TypeChecking.Level Agda.TypeChecking.LevelConstraints Agda.TypeChecking.Lock Agda.TypeChecking.Level.Solve Agda.TypeChecking.MetaVars Agda.TypeChecking.MetaVars.Mention Agda.TypeChecking.MetaVars.Occurs Agda.TypeChecking.Modalities Agda.TypeChecking.Monad.Base Agda.TypeChecking.Monad.Base.Types Agda.TypeChecking.Monad.Base.Warning Agda.TypeChecking.Monad.Benchmark Agda.TypeChecking.Monad.Builtin Agda.TypeChecking.Monad.Caching Agda.TypeChecking.Monad.Closure Agda.TypeChecking.Monad.Constraints Agda.TypeChecking.Monad.Context Agda.TypeChecking.Monad.Debug Agda.TypeChecking.Monad.Env Agda.TypeChecking.Monad.Imports Agda.TypeChecking.Monad.MetaVars Agda.TypeChecking.Monad.Modality Agda.TypeChecking.Monad.Mutual Agda.TypeChecking.Monad.Open Agda.TypeChecking.Monad.Options Agda.TypeChecking.Monad.Pure Agda.TypeChecking.Monad.Signature Agda.TypeChecking.Monad.SizedTypes Agda.TypeChecking.Monad.State Agda.TypeChecking.Monad.Statistics Agda.TypeChecking.Monad.Trace Agda.TypeChecking.Monad Agda.TypeChecking.Names Agda.TypeChecking.Opacity Agda.TypeChecking.Patterns.Abstract Agda.TypeChecking.Patterns.Internal Agda.TypeChecking.Patterns.Match Agda.TypeChecking.Polarity Agda.TypeChecking.Positivity Agda.TypeChecking.Positivity.Occurrence Agda.TypeChecking.Pretty Agda.TypeChecking.Pretty.Call Agda.TypeChecking.Pretty.Constraint Agda.TypeChecking.Pretty.Warning Agda.TypeChecking.Primitive Agda.TypeChecking.Primitive.Base Agda.TypeChecking.Primitive.Cubical Agda.TypeChecking.Primitive.Cubical.Id Agda.TypeChecking.Primitive.Cubical.Glue Agda.TypeChecking.Primitive.Cubical.Base Agda.TypeChecking.Primitive.Cubical.HCompU Agda.TypeChecking.ProjectionLike Agda.TypeChecking.Quote Agda.TypeChecking.ReconstructParameters Agda.TypeChecking.RecordPatterns Agda.TypeChecking.Records Agda.TypeChecking.Reduce Agda.TypeChecking.Reduce.Fast Agda.TypeChecking.Reduce.Monad Agda.TypeChecking.Rewriting Agda.TypeChecking.Rewriting.Clause Agda.TypeChecking.Rewriting.Confluence Agda.TypeChecking.Rewriting.NonLinMatch Agda.TypeChecking.Rewriting.NonLinPattern Agda.TypeChecking.Rules.Application Agda.TypeChecking.Rules.Builtin Agda.TypeChecking.Rules.Builtin.Coinduction Agda.TypeChecking.Rules.Data Agda.TypeChecking.Rules.Decl Agda.TypeChecking.Rules.Def Agda.TypeChecking.Rules.Display Agda.TypeChecking.Rules.LHS Agda.TypeChecking.Rules.LHS.Implicit Agda.TypeChecking.Rules.LHS.Problem Agda.TypeChecking.Rules.LHS.ProblemRest Agda.TypeChecking.Rules.LHS.Unify Agda.TypeChecking.Rules.LHS.Unify.Types Agda.TypeChecking.Rules.LHS.Unify.LeftInverse Agda.TypeChecking.Rules.Record Agda.TypeChecking.Rules.Term Agda.TypeChecking.Serialise Agda.TypeChecking.Serialise.Base Agda.TypeChecking.Serialise.Instances Agda.TypeChecking.Serialise.Instances.Abstract Agda.TypeChecking.Serialise.Instances.Common Agda.TypeChecking.Serialise.Instances.Compilers Agda.TypeChecking.Serialise.Instances.Highlighting Agda.TypeChecking.Serialise.Instances.Internal Agda.TypeChecking.Serialise.Instances.Errors Agda.TypeChecking.SizedTypes Agda.TypeChecking.SizedTypes.Pretty Agda.TypeChecking.SizedTypes.Solve Agda.TypeChecking.SizedTypes.Syntax Agda.TypeChecking.SizedTypes.Utils Agda.TypeChecking.SizedTypes.WarshallSolver Agda.TypeChecking.Sort Agda.TypeChecking.Substitute Agda.TypeChecking.Substitute.Class Agda.TypeChecking.Substitute.DeBruijn Agda.TypeChecking.SyntacticEquality Agda.TypeChecking.Telescope Agda.TypeChecking.Telescope.Path Agda.TypeChecking.Unquote Agda.TypeChecking.Warnings Agda.TypeChecking.With Agda.Utils.AffineHole Agda.Utils.Applicative Agda.Utils.AssocList Agda.Utils.Bag Agda.Utils.Benchmark Agda.Utils.BiMap Agda.Utils.Boolean Agda.Utils.BoolSet Agda.Utils.CallStack Agda.Utils.Char Agda.Utils.Cluster Agda.Utils.Empty Agda.Utils.Environment Agda.Utils.Either Agda.Utils.Fail Agda.Utils.Favorites Agda.Utils.FileName Agda.Utils.Float Agda.Utils.Functor Agda.Utils.Function Agda.Utils.Graph.AdjacencyMap.Unidirectional Agda.Utils.Graph.TopSort Agda.Utils.Hash Agda.Utils.HashTable Agda.Utils.Haskell.Syntax Agda.Utils.IArray Agda.Utils.Impossible Agda.Utils.IndexedList Agda.Utils.IntSet.Infinite Agda.Utils.IO Agda.Utils.IO.Binary Agda.Utils.IO.Directory Agda.Utils.IO.TempFile Agda.Utils.IO.UTF8 Agda.Utils.IORef Agda.Utils.Lens Agda.Utils.Lens.Examples Agda.Utils.List Agda.Utils.List1 Agda.Utils.List2 Agda.Utils.ListT Agda.Utils.Map Agda.Utils.Maybe Agda.Utils.Maybe.Strict Agda.Utils.Memo Agda.Utils.Monad Agda.Utils.Monoid Agda.Utils.Null Agda.Utils.Parser.MemoisedCPS Agda.Utils.PartialOrd Agda.Utils.Permutation Agda.Utils.Pointer Agda.Utils.POMonoid Agda.Utils.ProfileOptions Agda.Utils.RangeMap Agda.Utils.SemiRing Agda.Utils.Semigroup Agda.Utils.Singleton Agda.Utils.Size Agda.Utils.SmallSet Agda.Utils.String Agda.Utils.Suffix Agda.Utils.Three Agda.Utils.Time Agda.Utils.Trie Agda.Utils.Tuple Agda.Utils.TypeLevel Agda.Utils.TypeLits Agda.Utils.Unsafe Agda.Utils.Update Agda.Utils.VarSet Agda.Utils.Warshall Agda.Utils.WithDefault Agda.Utils.Zipper Agda.Version Agda.VersionCommit autogen-modules: Paths_Agda other-modules: Paths_Agda -- Need not export submodules if parent module reexports them. Agda.Interaction.Highlighting.Dot.Backend Agda.Interaction.Highlighting.Dot.Base Agda.Interaction.Highlighting.HTML.Backend Agda.Interaction.Highlighting.HTML.Base Agda.Interaction.Highlighting.LaTeX.Backend Agda.Interaction.Highlighting.LaTeX.Base Agda.Interaction.Options.Base Agda.Interaction.Options.HasOptions Agda.Utils.CallStack.Base Agda.Utils.CallStack.Pretty -- Agda binary --------------------------------------------------------------------------- executable agda hs-source-dirs: src/main main-is: Main.hs build-depends: , Agda -- Nothing is used from the following package, -- except for the Prelude. , base default-language: Haskell2010 -- If someone installs Agda with the setuid bit set, then the -- presence of +RTS may be a security problem (see GHC bug #3910). -- However, we sometimes recommend people to use +RTS to control -- Agda's memory usage, so we want this functionality enabled by -- default. -- The threaded RTS by default starts a major GC after a program has -- been idle for 0.3 s. This feature turned out to be annoying, so -- the idle GC is now by default turned off (-I0). ghc-options: -threaded -rtsopts -with-rtsopts=-I0 -- agda-mode executable --------------------------------------------------------------------------- executable agda-mode hs-source-dirs: src/agda-mode main-is: Main.hs autogen-modules: Paths_Agda other-modules: Paths_Agda build-depends: , base >= 4.12.0.0 && < 4.21 , directory >= 1.3.3.0 && < 1.4 , filepath >= 1.4.2.1 && < 1.6 , process >= 1.6.3.0 && < 1.7 default-language: Haskell2010