Index of

---

Agda.Builtin.Bool.html

Agda.Builtin.Equality.html

Agda.Builtin.List.html

Agda.Builtin.Nat.html

Agda.Builtin.TrustMe.html

Agda.Builtin.Unit.html

Agda.css

Agda.Primitive.html

Algebra.FunctionProperties.Core.html

Algebra.FunctionProperties.html

Algebra.html

Algebra.Monoid-solver.html

Algebra.Morphism.html

Algebra.Operations.html

Algebra.Properties.AbelianGroup.html

Algebra.Properties.BooleanAlgebra.Expression.html

Algebra.Properties.BooleanAlgebra.html

Algebra.Properties.DistributiveLattice.html

Algebra.Properties.Group.html

Algebra.Properties.Lattice.html

Algebra.Properties.Ring.html

Algebra.RingSolver.AlmostCommutativeRing.html

Algebra.RingSolver.html

Algebra.RingSolver.Lemmas.html

Algebra.RingSolver.Natural-coefficients.html

Algebra.RingSolver.Simple.html

Algebra.Structures.html

Alpha.html

Atom.html

auto-index.sh

Beta.html

Category.Applicative.html

Category.Applicative.Indexed.html

Category.Functor.html

Category.Monad.html

Category.Monad.Identity.html

Category.Monad.Indexed.html

Chi.html

Context.html

Data.Bool.Base.html

Data.Bool.html

Data.Bool.Properties.html

Data.Empty.html

Data.Fin.Dec.html

Data.Fin.html

Data.Fin.Properties.html

Data.Fin.Subset.html

Data.Fin.Subset.Properties.html

Data.List.All.html

Data.List.Any.html

Data.List.Any.Membership.html

Data.List.Any.Properties.html

Data.List.Base.html

Data.List.html

Data.List.Properties.html

Data.Maybe.Base.html

Data.Maybe.Core.html

Data.Maybe.html

Data.Nat.Base.html

Data.Nat.html

Data.Nat.Properties.html

Data.Nat.Properties.Simple.html

Data.Plus.html

Data.Product.html

Data.Sum.html

Data.Unit.Base.html

Data.Unit.Core.html

Data.Unit.html

Data.Unit.NonEta.html

Data.Vec.Equality.html

Data.Vec.html

Data.Vec.N-ary.html

Data.Vec.Properties.html

Diamond.html

Equivariant.html

FreeVariables.html

Function.Bijection.html

Function.Equality.html

Function.Equivalence.html

Function.html

Function.Injection.html

Function.Inverse.html

Function.LeftInverse.html

Function.Related.html

Function.Related.TypeIsomorphisms.html

Function.Surjection.html

index.html

Induction.html

Induction.Nat.html

Induction.WellFounded.html

Level.html

ListProperties.html

NaturalProperties.html

Parallel.html

Permutation.html

Relation.Binary.Consequences.Core.html

Relation.Binary.Consequences.html

Relation.Binary.Core.html

Relation.Binary.EqReasoning.html

Relation.Binary.HeterogeneousEquality.Core.html

Relation.Binary.HeterogeneousEquality.html

Relation.Binary.html

Relation.Binary.Indexed.Core.html

Relation.Binary.Indexed.html

Relation.Binary.InducedPreorders.html

Relation.Binary.Lattice.html

Relation.Binary.List.Pointwise.html

Relation.Binary.NonStrictToStrict.html

Relation.Binary.PartialOrderReasoning.html

Relation.Binary.PreorderReasoning.html

Relation.Binary.Product.Pointwise.html

Relation.Binary.Properties.DecTotalOrder.html

Relation.Binary.PropositionalEquality.Core.html

Relation.Binary.PropositionalEquality.html

Relation.Binary.PropositionalEquality.TrustMe.html

Relation.Binary.Reflection.html

Relation.Binary.Sigma.Pointwise.html

Relation.Binary.Sum.html

Relation.Binary.Vec.Pointwise.html

Relation.html

Relation.Nullary.Core.html

Relation.Nullary.Decidable.html

Relation.Nullary.html

Relation.Nullary.Negation.html

Relation.Nullary.Product.html

Relation.Unary.html

Substitution.html

TermAcc.html

Term.html

TermInduction.html

TermRecursion.html

Types.html

WeakNormalization.html