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

Directory listing for Agda-2.9.0 documentation

Agda-2.9.0-docs/src/

• Agda.Benchmarking.html
• Agda.Compiler.Backend.Base.html
• Agda.Compiler.Backend.html
• Agda.Compiler.Builtin.html
• Agda.Compiler.CallCompiler.html
• Agda.Compiler.Common.html
• Agda.Compiler.JS.Compiler.html
• Agda.Compiler.JS.Pretty.html
• Agda.Compiler.JS.Substitution.html
• Agda.Compiler.JS.Syntax.html
• Agda.Compiler.MAlonzo.Coerce.html
• Agda.Compiler.MAlonzo.Compiler.html
• Agda.Compiler.MAlonzo.Encode.html
• Agda.Compiler.MAlonzo.HaskellTypes.html
• Agda.Compiler.MAlonzo.Misc.html
• Agda.Compiler.MAlonzo.Pragmas.html
• Agda.Compiler.MAlonzo.Pretty.html
• Agda.Compiler.MAlonzo.Primitives.html
• Agda.Compiler.MAlonzo.Strict.html
• Agda.Compiler.ToTreeless.html
• Agda.Compiler.Treeless.AsPatterns.html
• Agda.Compiler.Treeless.Builtin.html
• Agda.Compiler.Treeless.Compare.html
• Agda.Compiler.Treeless.EliminateDefaults.html
• Agda.Compiler.Treeless.EliminateLiteralPatterns.html
• Agda.Compiler.Treeless.Erase.html
• Agda.Compiler.Treeless.GuardsToPrims.html
• Agda.Compiler.Treeless.Identity.html
• Agda.Compiler.Treeless.NormalizeNames.html
• Agda.Compiler.Treeless.Pretty.html
• Agda.Compiler.Treeless.Simplify.html
• Agda.Compiler.Treeless.Subst.html
• Agda.Compiler.Treeless.Uncase.html
• Agda.Compiler.Treeless.Unused.html
• Agda.ImpossibleTest.html
• Agda.Interaction.AgdaTop.html
• Agda.Interaction.Base.html
• Agda.Interaction.BasicOps.html
• Agda.Interaction.BuildLibrary.html
• Agda.Interaction.Command.html
• Agda.Interaction.CommandLine.html
• Agda.Interaction.Emacs.Lisp.html
• Agda.Interaction.EmacsCommand.html
• Agda.Interaction.EmacsTop.html
• Agda.Interaction.ExitCode.html
• Agda.Interaction.FindFile.html
• Agda.Interaction.Highlighting.Common.html
• Agda.Interaction.Highlighting.Dot.Backend.html
• Agda.Interaction.Highlighting.Dot.Base.html
• Agda.Interaction.Highlighting.Dot.html
• Agda.Interaction.Highlighting.Emacs.html
• Agda.Interaction.Highlighting.FromAbstract.html
• Agda.Interaction.Highlighting.Generate.html
• Agda.Interaction.Highlighting.HTML.Backend.html
• Agda.Interaction.Highlighting.HTML.Base.html
• Agda.Interaction.Highlighting.HTML.Forester.html
• Agda.Interaction.Highlighting.HTML.html
• Agda.Interaction.Highlighting.JSON.html
• Agda.Interaction.Highlighting.LaTeX.Backend.html
• Agda.Interaction.Highlighting.LaTeX.Base.html
• Agda.Interaction.Highlighting.LaTeX.html
• Agda.Interaction.Highlighting.Precise.html
• Agda.Interaction.Highlighting.Range.html
• Agda.Interaction.Highlighting.Vim.html
• Agda.Interaction.Imports.html
• Agda.Interaction.InteractionTop.html
• Agda.Interaction.JSON.html
• Agda.Interaction.JSONTop.html
• Agda.Interaction.Library.Base.html
• Agda.Interaction.Library.Parse.html
• Agda.Interaction.Library.html
• Agda.Interaction.MakeCase.html
• Agda.Interaction.Monad.html
• Agda.Interaction.Options.Arguments.html
• Agda.Interaction.Options.Base.html
• Agda.Interaction.Options.BashCompletion.html
• Agda.Interaction.Options.Default.html
• Agda.Interaction.Options.Errors.html
• Agda.Interaction.Options.HasOptions.html
• Agda.Interaction.Options.Help.html
• Agda.Interaction.Options.Lenses.html
• Agda.Interaction.Options.ProfileOptions.html
• Agda.Interaction.Options.Types.html
• Agda.Interaction.Options.Warnings.html
• Agda.Interaction.Options.html
• Agda.Interaction.Output.html
• Agda.Interaction.Response.Base.html
• Agda.Interaction.Response.html
• Agda.Interaction.SearchAbout.html
• Agda.Main.html
• Agda.Mimer.Mimer.html
• Agda.Mimer.Monad.html
• Agda.Mimer.Options.html
• Agda.Mimer.Types.html
• Agda.Setup.DataFiles.html
• Agda.Setup.EmacsMode.html
• Agda.Setup.LockFile.html
• Agda.Setup.html
• Agda.Syntax.Abstract.Name.html
• Agda.Syntax.Abstract.Pattern.html
• Agda.Syntax.Abstract.PatternSynonyms.html
• Agda.Syntax.Abstract.Pretty.html
• Agda.Syntax.Abstract.UsedNames.html
• Agda.Syntax.Abstract.Views.html
• Agda.Syntax.Abstract.html
• Agda.Syntax.Builtin.html
• Agda.Syntax.Common.Aspect.html
• Agda.Syntax.Common.KeywordRange.html
• Agda.Syntax.Common.Pretty.ANSI.html
• Agda.Syntax.Common.Pretty.html
• Agda.Syntax.Common.html
• Agda.Syntax.Concrete.Attribute.html
• Agda.Syntax.Concrete.Definitions.Errors.html
• Agda.Syntax.Concrete.Definitions.Monad.html
• Agda.Syntax.Concrete.Definitions.Types.html
• Agda.Syntax.Concrete.Definitions.html
• Agda.Syntax.Concrete.Fixity.html
• Agda.Syntax.Concrete.Generic.html
• Agda.Syntax.Concrete.Glyph.html
• Agda.Syntax.Concrete.Name.html
• Agda.Syntax.Concrete.Operators.Parser.Monad.html
• Agda.Syntax.Concrete.Operators.Parser.html
• Agda.Syntax.Concrete.Operators.html
• Agda.Syntax.Concrete.Pattern.html
• Agda.Syntax.Concrete.Pretty.html
• Agda.Syntax.Concrete.html
• Agda.Syntax.DoNotation.html
• Agda.Syntax.Fixity.html
• Agda.Syntax.IdiomBrackets.html
• Agda.Syntax.Info.html
• Agda.Syntax.Internal.Blockers.html
• Agda.Syntax.Internal.Defs.html
• Agda.Syntax.Internal.Elim.html
• Agda.Syntax.Internal.Generic.html
• Agda.Syntax.Internal.MetaVars.html
• Agda.Syntax.Internal.Names.html
• Agda.Syntax.Internal.Pattern.html
• Agda.Syntax.Internal.SanityCheck.html
• Agda.Syntax.Internal.Univ.html
• Agda.Syntax.Internal.html
• Agda.Syntax.Literal.html
• Agda.Syntax.Notation.html
• Agda.Syntax.Parser.Alex.html
• Agda.Syntax.Parser.Comments.html
• Agda.Syntax.Parser.Helpers.html
• Agda.Syntax.Parser.Layout.html
• Agda.Syntax.Parser.LexActions.html
• Agda.Syntax.Parser.Lexer.html
• Agda.Syntax.Parser.Literate.html
• Agda.Syntax.Parser.LookAhead.html
• Agda.Syntax.Parser.Monad.html
• Agda.Syntax.Parser.Parser.html
• Agda.Syntax.Parser.StringLiterals.html
• Agda.Syntax.Parser.Tokens.html
• Agda.Syntax.Parser.html
• Agda.Syntax.Position.html
• Agda.Syntax.Reflected.html
• Agda.Syntax.Scope.Base.html
• Agda.Syntax.Scope.Monad.html
• Agda.Syntax.Scope.Operator.html
• Agda.Syntax.Scope.State.html
• Agda.Syntax.Scope.UnusedImports.html
• Agda.Syntax.TopLevelModuleName.Boot.html
• Agda.Syntax.TopLevelModuleName.html
• Agda.Syntax.Translation.AbstractToConcrete.html
• Agda.Syntax.Translation.ConcreteToAbstract.html
• Agda.Syntax.Translation.InternalToAbstract.html
• Agda.Syntax.Translation.ReflectedToAbstract.html
• Agda.Syntax.Treeless.html
• Agda.Termination.CallGraph.html
• Agda.Termination.CallMatrix.html
• Agda.Termination.CutOff.html
• Agda.Termination.Monad.html
• Agda.Termination.Order.html
• Agda.Termination.RecCheck.html
• Agda.Termination.Semiring.html
• Agda.Termination.SparseMatrix.html
• Agda.Termination.TermCheck.html
• Agda.Termination.Termination.html
• Agda.TheTypeChecker.html
• Agda.TypeChecking.Abstract.html
• Agda.TypeChecking.CheckInternal.html
• Agda.TypeChecking.CompiledClause.Compile.html
• Agda.TypeChecking.CompiledClause.Match.html
• Agda.TypeChecking.CompiledClause.html
• Agda.TypeChecking.Constraints.html
• Agda.TypeChecking.Conversion.Errors.html
• Agda.TypeChecking.Conversion.Pure.html
• Agda.TypeChecking.Conversion.html
• Agda.TypeChecking.Coverage.Cubical.html
• Agda.TypeChecking.Coverage.Match.html
• Agda.TypeChecking.Coverage.SplitClause.html
• Agda.TypeChecking.Coverage.SplitPattern.html
• Agda.TypeChecking.Coverage.SplitTree.html
• Agda.TypeChecking.Coverage.html
• Agda.TypeChecking.Datatypes.html
• Agda.TypeChecking.DeadCode.html
• Agda.TypeChecking.DiscrimTree.Types.html
• Agda.TypeChecking.DiscrimTree.html
• Agda.TypeChecking.DisplayForm.html
• Agda.TypeChecking.DropArgs.html
• Agda.TypeChecking.Empty.html
• Agda.TypeChecking.Errors.Names.html
• Agda.TypeChecking.Errors.html
• Agda.TypeChecking.EtaContract.html
• Agda.TypeChecking.Forcing.html
• Agda.TypeChecking.Free.Base.html
• Agda.TypeChecking.Free.Generic.html
• Agda.TypeChecking.Free.Precompute.html
• Agda.TypeChecking.Free.Reduce.html
• Agda.TypeChecking.Free.html
• Agda.TypeChecking.Functions.html
• Agda.TypeChecking.Generalize.html
• Agda.TypeChecking.IApplyConfluence.html
• Agda.TypeChecking.Implicit.html
• Agda.TypeChecking.Injectivity.html
• Agda.TypeChecking.Inlining.html
• Agda.TypeChecking.InstanceArguments.html
• Agda.TypeChecking.Irrelevance.html
• Agda.TypeChecking.Level.Solve.html
• Agda.TypeChecking.Level.html
• Agda.TypeChecking.LevelConstraints.html
• Agda.TypeChecking.Lock.html
• Agda.TypeChecking.MetaVars.Mention.html
• Agda.TypeChecking.MetaVars.Occurs.html
• Agda.TypeChecking.MetaVars.html
• Agda.TypeChecking.Modalities.html
• Agda.TypeChecking.Monad.Base.Types.html
• Agda.TypeChecking.Monad.Base.Warning.html
• Agda.TypeChecking.Monad.Base.html
• Agda.TypeChecking.Monad.Benchmark.html
• Agda.TypeChecking.Monad.Builtin.html
• Agda.TypeChecking.Monad.Caching.html
• Agda.TypeChecking.Monad.Closure.html
• Agda.TypeChecking.Monad.Constraints.html
• Agda.TypeChecking.Monad.Context.html
• Agda.TypeChecking.Monad.Debug.html
• Agda.TypeChecking.Monad.Env.html
• Agda.TypeChecking.Monad.Imports.html
• Agda.TypeChecking.Monad.MetaVars.html
• Agda.TypeChecking.Monad.Modality.html
• Agda.TypeChecking.Monad.Mutual.html
• Agda.TypeChecking.Monad.Open.html
• Agda.TypeChecking.Monad.Options.html
• Agda.TypeChecking.Monad.Pure.html
• Agda.TypeChecking.Monad.Signature.html
• Agda.TypeChecking.Monad.SizedTypes.html
• Agda.TypeChecking.Monad.State.html
• Agda.TypeChecking.Monad.Statistics.html
• Agda.TypeChecking.Monad.Trace.html
• Agda.TypeChecking.Monad.html
• Agda.TypeChecking.Names.html
• Agda.TypeChecking.Opacity.html
• Agda.TypeChecking.Patterns.Abstract.html
• Agda.TypeChecking.Patterns.Internal.html
• Agda.TypeChecking.Patterns.Match.html
• Agda.TypeChecking.Polarity.html
• Agda.TypeChecking.Positivity.Occurrence.html
• Agda.TypeChecking.Positivity.OccurrenceAnalysis.html
• Agda.TypeChecking.Positivity.Warnings.html
• Agda.TypeChecking.Positivity.html
• Agda.TypeChecking.Pretty.Call.html
• Agda.TypeChecking.Pretty.Constraint.html
• Agda.TypeChecking.Pretty.Warning.html
• Agda.TypeChecking.Pretty.html
• Agda.TypeChecking.Primitive.Base.html
• Agda.TypeChecking.Primitive.Cubical.Base.html
• Agda.TypeChecking.Primitive.Cubical.Glue.html
• Agda.TypeChecking.Primitive.Cubical.HCompU.html
• Agda.TypeChecking.Primitive.Cubical.html
• Agda.TypeChecking.Primitive.html
• Agda.TypeChecking.ProjectionLike.html
• Agda.TypeChecking.Quote.html
• Agda.TypeChecking.ReconstructParameters.html
• Agda.TypeChecking.RecordPatterns.html
• Agda.TypeChecking.Records.html
• Agda.TypeChecking.Reduce.Fast.html
• Agda.TypeChecking.Reduce.Monad.html
• Agda.TypeChecking.Reduce.html
• Agda.TypeChecking.Rewriting.Clause.html
• Agda.TypeChecking.Rewriting.Confluence.html
• Agda.TypeChecking.Rewriting.NonLinMatch.html
• Agda.TypeChecking.Rewriting.NonLinPattern.html
• Agda.TypeChecking.Rewriting.html
• Agda.TypeChecking.Rules.Application.html
• Agda.TypeChecking.Rules.Builtin.Coinduction.html
• Agda.TypeChecking.Rules.Builtin.html
• Agda.TypeChecking.Rules.Data.html
• Agda.TypeChecking.Rules.Decl.html
• Agda.TypeChecking.Rules.Def.html
• Agda.TypeChecking.Rules.Display.html
• Agda.TypeChecking.Rules.LHS.Implicit.html
• Agda.TypeChecking.Rules.LHS.Problem.html
• Agda.TypeChecking.Rules.LHS.ProblemRest.html
• Agda.TypeChecking.Rules.LHS.Unify.LeftInverse.html
• Agda.TypeChecking.Rules.LHS.Unify.Types.html
• Agda.TypeChecking.Rules.LHS.Unify.html
• Agda.TypeChecking.Rules.LHS.html
• Agda.TypeChecking.Rules.Record.Cubical.html
• Agda.TypeChecking.Rules.Record.html
• Agda.TypeChecking.Rules.Term.html
• Agda.TypeChecking.Serialise.Base.html
• Agda.TypeChecking.Serialise.Instances.Abstract.html
• Agda.TypeChecking.Serialise.Instances.Common.html
• Agda.TypeChecking.Serialise.Instances.Compilers.html
• Agda.TypeChecking.Serialise.Instances.Errors.html
• Agda.TypeChecking.Serialise.Instances.General.html
• Agda.TypeChecking.Serialise.Instances.Highlighting.html
• Agda.TypeChecking.Serialise.Instances.Internal.html
• Agda.TypeChecking.Serialise.Instances.html
• Agda.TypeChecking.Serialise.Node.html
• Agda.TypeChecking.Serialise.html
• Agda.TypeChecking.SizedTypes.Pretty.html
• Agda.TypeChecking.SizedTypes.Solve.html
• Agda.TypeChecking.SizedTypes.Syntax.html
• Agda.TypeChecking.SizedTypes.Utils.html
• Agda.TypeChecking.SizedTypes.WarshallSolver.html
• Agda.TypeChecking.SizedTypes.html
• Agda.TypeChecking.Sort.html
• Agda.TypeChecking.Substitute.Class.html
• Agda.TypeChecking.Substitute.DeBruijn.html
• Agda.TypeChecking.Substitute.html
• Agda.TypeChecking.SyntacticEquality.html
• Agda.TypeChecking.Telescope.Path.html
• Agda.TypeChecking.Telescope.html
• Agda.TypeChecking.Unquote.html
• Agda.TypeChecking.Warnings.html
• Agda.TypeChecking.With.html
• Agda.Utils.AffineHole.html
• Agda.Utils.Applicative.html
• Agda.Utils.AssocList.html
• Agda.Utils.Atomic.html
• Agda.Utils.Bag.html
• Agda.Utils.Benchmark.html
• Agda.Utils.BiMap.html
• Agda.Utils.BinTree.html
• Agda.Utils.BinTree1.html
• Agda.Utils.BoolSet.html
• Agda.Utils.Boolean.html
• Agda.Utils.ByteArray.html
• Agda.Utils.CallStack.Base.html
• Agda.Utils.CallStack.Pretty.html
• Agda.Utils.CallStack.html
• Agda.Utils.Char.html
• Agda.Utils.Cluster.html
• Agda.Utils.CompactRegion.html
• Agda.Utils.CompressedTrie.html
• Agda.Utils.DocTree.html
• Agda.Utils.Either.html
• Agda.Utils.Empty.html
• Agda.Utils.Environment.html
• Agda.Utils.ExpandCase.html
• Agda.Utils.Fail.html
• Agda.Utils.Favorites.html
• Agda.Utils.FileId.html
• Agda.Utils.FileName.html
• Agda.Utils.Float.html
• Agda.Utils.Function.html
• Agda.Utils.Functor.html
• Agda.Utils.GetOpt.html
• Agda.Utils.Graph.AdjacencyMap.Unidirectional.html
• Agda.Utils.Graph.TopSort.html
• Agda.Utils.Hash.html
• Agda.Utils.HashTable.html
• Agda.Utils.Haskell.Syntax.html
• Agda.Utils.IArray.html
• Agda.Utils.IO.Binary.html
• Agda.Utils.IO.Directory.html
• Agda.Utils.IO.TempFile.html
• Agda.Utils.IO.Terminal.html
• Agda.Utils.IO.UTF8.html
• Agda.Utils.IO.html
• Agda.Utils.IORef.Strict.html
• Agda.Utils.IORef.html
• Agda.Utils.Impossible.html
• Agda.Utils.IndexMap.html
• Agda.Utils.IndexedList.html
• Agda.Utils.IntMap.html
• Agda.Utils.IntSet.Infinite.html
• Agda.Utils.Lens.Examples.html
• Agda.Utils.Lens.html
• Agda.Utils.List.html
• Agda.Utils.List1.html
• Agda.Utils.List2.html
• Agda.Utils.ListInf.html
• Agda.Utils.ListT.html
• Agda.Utils.Map.html
• Agda.Utils.Map1.html
• Agda.Utils.Maybe.Strict.html
• Agda.Utils.Maybe.Unboxable.html
• Agda.Utils.Maybe.html
• Agda.Utils.Memo.html
• Agda.Utils.MinimalArray.Lifted.html
• Agda.Utils.MinimalArray.MutableLifted.html
• Agda.Utils.MinimalArray.MutablePrim.html
• Agda.Utils.MinimalArray.Prim.html
• Agda.Utils.Monad.html
• Agda.Utils.Monoid.html
• Agda.Utils.Null.html
• Agda.Utils.POMonoid.html
• Agda.Utils.Parser.MemoisedCPS.html
• Agda.Utils.PartialOrd.html
• Agda.Utils.Permutation.html
• Agda.Utils.Range.html
• Agda.Utils.RangeMap.html
• Agda.Utils.SemiRing.html
• Agda.Utils.Semigroup.html
• Agda.Utils.Serialize.html
• Agda.Utils.Set.html
• Agda.Utils.Set1.html
• Agda.Utils.Singleton.html
• Agda.Utils.Size.html
• Agda.Utils.SmallSet.html
• Agda.Utils.StrictEndo.html
• Agda.Utils.StrictFlipEndo.html
• Agda.Utils.StrictReader.html
• Agda.Utils.StrictState.html
• Agda.Utils.StrictState2.html
• Agda.Utils.StrictWriter.html
• Agda.Utils.String.html
• Agda.Utils.Suffix.html
• Agda.Utils.Three.html
• Agda.Utils.Time.html
• Agda.Utils.Trie.html
• Agda.Utils.Tuple.Strict.html
• Agda.Utils.Tuple.html
• Agda.Utils.TypeLevel.html
• Agda.Utils.TypeLits.html
• Agda.Utils.Unsafe.html
• Agda.Utils.Update.html
• Agda.Utils.VarSet.html
• Agda.Utils.WithDefault.html
• Agda.Utils.Word.html
• Agda.Utils.Zip.html
• Agda.Utils.Zipper.html
• Agda.Version.html
• Agda.VersionCommit.html
• Paths_Agda.html
• highlight.js
• style.css