Created
May 4, 2020 14:55
-
-
Save r-ryantm/165b0bfce12ca7ed21716a7c5346feb1 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| /nix/store/r3j0vp6gx16m3gahba54f8lq0gapj7nb-agda-stdlib-1.3 | |
| └── share | |
| └── agda | |
| ├── Algebra | |
| │ ├── Bundles.agda | |
| │ ├── Consequences | |
| │ │ ├── Base.agda | |
| │ │ ├── Propositional.agda | |
| │ │ └── Setoid.agda | |
| │ ├── Construct | |
| │ │ ├── LiftedChoice.agda | |
| │ │ └── NaturalChoice | |
| │ │ ├── Max.agda | |
| │ │ └── Min.agda | |
| │ ├── Core.agda | |
| │ ├── Definitions.agda | |
| │ ├── FunctionProperties | |
| │ │ ├── Consequences | |
| │ │ │ ├── Core.agda | |
| │ │ │ └── Propositional.agda | |
| │ │ ├── Consequences.agda | |
| │ │ └── Core.agda | |
| │ ├── FunctionProperties.agda | |
| │ ├── Module | |
| │ │ ├── Bundles.agda | |
| │ │ ├── Consequences.agda | |
| │ │ ├── Construct | |
| │ │ │ ├── TensorUnit.agda | |
| │ │ │ └── Zero.agda | |
| │ │ ├── Definitions | |
| │ │ │ ├── Bi.agda | |
| │ │ │ ├── Left.agda | |
| │ │ │ └── Right.agda | |
| │ │ ├── Definitions.agda | |
| │ │ ├── Structures | |
| │ │ │ └── Biased.agda | |
| │ │ └── Structures.agda | |
| │ ├── Morphism | |
| │ │ ├── Definitions.agda | |
| │ │ ├── GroupMonomorphism.agda | |
| │ │ ├── MagmaMonomorphism.agda | |
| │ │ ├── MonoidMonomorphism.agda | |
| │ │ ├── RingMonomorphism.agda | |
| │ │ └── Structures.agda | |
| │ ├── Morphism.agda | |
| │ ├── Operations | |
| │ │ ├── CommutativeMonoid.agda | |
| │ │ ├── Ring.agda | |
| │ │ └── Semiring.agda | |
| │ ├── Properties | |
| │ │ ├── AbelianGroup.agda | |
| │ │ ├── BooleanAlgebra | |
| │ │ │ └── Expression.agda | |
| │ │ ├── BooleanAlgebra.agda | |
| │ │ ├── CommutativeMonoid.agda | |
| │ │ ├── CommutativeSemigroup.agda | |
| │ │ ├── DistributiveLattice.agda | |
| │ │ ├── Group.agda | |
| │ │ ├── Lattice.agda | |
| │ │ ├── Ring.agda | |
| │ │ ├── Semigroup.agda | |
| │ │ └── Semilattice.agda | |
| │ ├── Solver | |
| │ │ ├── CommutativeMonoid | |
| │ │ │ └── Example.agda | |
| │ │ ├── CommutativeMonoid.agda | |
| │ │ ├── IdempotentCommutativeMonoid | |
| │ │ │ └── Example.agda | |
| │ │ ├── IdempotentCommutativeMonoid.agda | |
| │ │ ├── Monoid.agda | |
| │ │ ├── Ring | |
| │ │ │ ├── AlmostCommutativeRing.agda | |
| │ │ │ ├── Lemmas.agda | |
| │ │ │ ├── NaturalCoefficients | |
| │ │ │ │ └── Default.agda | |
| │ │ │ ├── NaturalCoefficients.agda | |
| │ │ │ └── Simple.agda | |
| │ │ └── Ring.agda | |
| │ ├── Structures | |
| │ │ └── Biased.agda | |
| │ └── Structures.agda | |
| ├── Algebra.agda | |
| ├── Axiom | |
| │ ├── DoubleNegationElimination.agda | |
| │ ├── ExcludedMiddle.agda | |
| │ ├── Extensionality | |
| │ │ ├── Heterogeneous.agda | |
| │ │ └── Propositional.agda | |
| │ ├── UniquenessOfIdentityProofs | |
| │ │ └── WithK.agda | |
| │ └── UniquenessOfIdentityProofs.agda | |
| ├── Category | |
| │ ├── Applicative | |
| │ │ ├── Indexed.agda | |
| │ │ └── Predicate.agda | |
| │ ├── Applicative.agda | |
| │ ├── Comonad.agda | |
| │ ├── Functor | |
| │ │ └── Predicate.agda | |
| │ ├── Functor.agda | |
| │ ├── Monad | |
| │ │ ├── Continuation.agda | |
| │ │ ├── Indexed.agda | |
| │ │ ├── Partiality | |
| │ │ │ └── All.agda | |
| │ │ ├── Partiality.agda | |
| │ │ ├── Predicate.agda | |
| │ │ ├── Reader.agda | |
| │ │ └── State.agda | |
| │ └── Monad.agda | |
| ├── Codata | |
| │ ├── Cofin | |
| │ │ └── Literals.agda | |
| │ ├── Cofin.agda | |
| │ ├── Colist | |
| │ │ ├── Bisimilarity.agda | |
| │ │ ├── Categorical.agda | |
| │ │ └── Properties.agda | |
| │ ├── Colist.agda | |
| │ ├── Conat | |
| │ │ ├── Bisimilarity.agda | |
| │ │ ├── Literals.agda | |
| │ │ └── Properties.agda | |
| │ ├── Conat.agda | |
| │ ├── Covec | |
| │ │ ├── Bisimilarity.agda | |
| │ │ ├── Categorical.agda | |
| │ │ └── Properties.agda | |
| │ ├── Covec.agda | |
| │ ├── Cowriter | |
| │ │ └── Bisimilarity.agda | |
| │ ├── Cowriter.agda | |
| │ ├── Delay | |
| │ │ ├── Bisimilarity.agda | |
| │ │ ├── Categorical.agda | |
| │ │ └── Properties.agda | |
| │ ├── Delay.agda | |
| │ ├── M | |
| │ │ ├── Bisimilarity.agda | |
| │ │ └── Properties.agda | |
| │ ├── M.agda | |
| │ ├── Musical | |
| │ │ ├── Cofin.agda | |
| │ │ ├── Colist | |
| │ │ │ └── Infinite-merge.agda | |
| │ │ ├── Colist.agda | |
| │ │ ├── Conat.agda | |
| │ │ ├── Costring.agda | |
| │ │ ├── Covec.agda | |
| │ │ ├── M | |
| │ │ │ └── Indexed.agda | |
| │ │ ├── M.agda | |
| │ │ ├── Notation.agda | |
| │ │ └── Stream.agda | |
| │ ├── Stream | |
| │ │ ├── Bisimilarity.agda | |
| │ │ ├── Categorical.agda | |
| │ │ └── Properties.agda | |
| │ ├── Stream.agda | |
| │ └── Thunk.agda | |
| ├── Data | |
| │ ├── AVL | |
| │ │ ├── Height.agda | |
| │ │ ├── Indexed | |
| │ │ │ └── WithK.agda | |
| │ │ ├── Indexed.agda | |
| │ │ ├── IndexedMap.agda | |
| │ │ ├── Key.agda | |
| │ │ ├── Map.agda | |
| │ │ ├── NonEmpty | |
| │ │ │ └── Propositional.agda | |
| │ │ ├── NonEmpty.agda | |
| │ │ ├── Sets.agda | |
| │ │ └── Value.agda | |
| │ ├── AVL.agda | |
| │ ├── Bin | |
| │ │ └── Properties.agda | |
| │ ├── Bin.agda | |
| │ ├── Bool | |
| │ │ ├── Base.agda | |
| │ │ ├── Properties.agda | |
| │ │ ├── Show.agda | |
| │ │ └── Solver.agda | |
| │ ├── Bool.agda | |
| │ ├── BoundedVec | |
| │ │ └── Inefficient.agda | |
| │ ├── BoundedVec.agda | |
| │ ├── Char | |
| │ │ ├── Base.agda | |
| │ │ └── Properties.agda | |
| │ ├── Char.agda | |
| │ ├── Container | |
| │ │ ├── Any.agda | |
| │ │ ├── Combinator | |
| │ │ │ └── Properties.agda | |
| │ │ ├── Combinator.agda | |
| │ │ ├── Core.agda | |
| │ │ ├── FreeMonad.agda | |
| │ │ ├── Indexed | |
| │ │ │ ├── Combinator.agda | |
| │ │ │ ├── Core.agda | |
| │ │ │ ├── FreeMonad.agda | |
| │ │ │ └── WithK.agda | |
| │ │ ├── Indexed.agda | |
| │ │ ├── Membership.agda | |
| │ │ ├── Morphism | |
| │ │ │ └── Properties.agda | |
| │ │ ├── Morphism.agda | |
| │ │ ├── Properties.agda | |
| │ │ ├── Related.agda | |
| │ │ └── Relation | |
| │ │ ├── Binary | |
| │ │ │ ├── Equality | |
| │ │ │ │ └── Setoid.agda | |
| │ │ │ ├── Pointwise | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ └── Pointwise.agda | |
| │ │ └── Unary | |
| │ │ ├── All.agda | |
| │ │ ├── Any | |
| │ │ │ └── Properties.agda | |
| │ │ └── Any.agda | |
| │ ├── Container.agda | |
| │ ├── DifferenceList.agda | |
| │ ├── DifferenceNat.agda | |
| │ ├── DifferenceVec.agda | |
| │ ├── Digit.agda | |
| │ ├── Empty | |
| │ │ ├── Irrelevant.agda | |
| │ │ └── Polymorphic.agda | |
| │ ├── Empty.agda | |
| │ ├── Erased.agda | |
| │ ├── Fin | |
| │ │ ├── Base.agda | |
| │ │ ├── Dec.agda | |
| │ │ ├── Induction.agda | |
| │ │ ├── Literals.agda | |
| │ │ ├── Patterns.agda | |
| │ │ ├── Permutation | |
| │ │ │ └── Components.agda | |
| │ │ ├── Permutation.agda | |
| │ │ ├── Properties.agda | |
| │ │ ├── Reflection.agda | |
| │ │ ├── Subset | |
| │ │ │ ├── Induction.agda | |
| │ │ │ └── Properties.agda | |
| │ │ ├── Subset.agda | |
| │ │ ├── Substitution | |
| │ │ │ ├── Example.agda | |
| │ │ │ ├── Lemmas.agda | |
| │ │ │ └── List.agda | |
| │ │ └── Substitution.agda | |
| │ ├── Fin.agda | |
| │ ├── Float | |
| │ │ ├── Base.agda | |
| │ │ └── Properties.agda | |
| │ ├── Float.agda | |
| │ ├── Graph | |
| │ │ └── Acyclic.agda | |
| │ ├── Integer | |
| │ │ ├── Base.agda | |
| │ │ ├── Coprimality.agda | |
| │ │ ├── Divisibility | |
| │ │ │ └── Signed.agda | |
| │ │ ├── Divisibility.agda | |
| │ │ ├── DivMod.agda | |
| │ │ ├── GCD.agda | |
| │ │ ├── LCM.agda | |
| │ │ ├── Literals.agda | |
| │ │ ├── Properties.agda | |
| │ │ ├── Solver.agda | |
| │ │ └── Tactic | |
| │ │ └── RingSolver.agda | |
| │ ├── Integer.agda | |
| │ ├── List | |
| │ │ ├── All | |
| │ │ │ └── Properties.agda | |
| │ │ ├── All.agda | |
| │ │ ├── Any | |
| │ │ │ └── Properties.agda | |
| │ │ ├── Any.agda | |
| │ │ ├── Base.agda | |
| │ │ ├── Categorical.agda | |
| │ │ ├── Countdown.agda | |
| │ │ ├── Extrema | |
| │ │ │ ├── Core.agda | |
| │ │ │ └── Nat.agda | |
| │ │ ├── Extrema.agda | |
| │ │ ├── Fresh | |
| │ │ │ ├── Membership | |
| │ │ │ │ ├── Setoid | |
| │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ └── Setoid.agda | |
| │ │ │ ├── Properties.agda | |
| │ │ │ └── Relation | |
| │ │ │ └── Unary | |
| │ │ │ ├── All | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ ├── All.agda | |
| │ │ │ ├── Any | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ └── Any.agda | |
| │ │ ├── Fresh.agda | |
| │ │ ├── Kleene | |
| │ │ │ ├── AsList.agda | |
| │ │ │ └── Base.agda | |
| │ │ ├── Kleene.agda | |
| │ │ ├── Literals.agda | |
| │ │ ├── Membership | |
| │ │ │ ├── DecPropositional.agda | |
| │ │ │ ├── DecSetoid.agda | |
| │ │ │ ├── Propositional | |
| │ │ │ │ ├── Properties | |
| │ │ │ │ │ ├── Core.agda | |
| │ │ │ │ │ └── WithK.agda | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ ├── Propositional.agda | |
| │ │ │ ├── Setoid | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ └── Setoid.agda | |
| │ │ ├── NonEmpty | |
| │ │ │ ├── Categorical.agda | |
| │ │ │ └── Properties.agda | |
| │ │ ├── NonEmpty.agda | |
| │ │ ├── Properties.agda | |
| │ │ ├── Relation | |
| │ │ │ ├── BagAndSetEquality.agda | |
| │ │ │ ├── Binary | |
| │ │ │ │ ├── BagAndSetEquality.agda | |
| │ │ │ │ ├── Disjoint | |
| │ │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ │ ├── Setoid | |
| │ │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ │ └── Setoid.agda | |
| │ │ │ │ ├── Equality | |
| │ │ │ │ │ ├── DecPropositional.agda | |
| │ │ │ │ │ ├── DecSetoid.agda | |
| │ │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ │ └── Setoid.agda | |
| │ │ │ │ ├── Lex | |
| │ │ │ │ │ ├── Core.agda | |
| │ │ │ │ │ ├── NonStrict.agda | |
| │ │ │ │ │ └── Strict.agda | |
| │ │ │ │ ├── Permutation | |
| │ │ │ │ │ ├── Homogeneous.agda | |
| │ │ │ │ │ ├── Inductive | |
| │ │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ │ ├── Inductive.agda | |
| │ │ │ │ │ ├── Propositional | |
| │ │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ │ ├── Setoid | |
| │ │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ │ └── Setoid.agda | |
| │ │ │ │ ├── Pointwise.agda | |
| │ │ │ │ ├── Prefix | |
| │ │ │ │ │ ├── Heterogeneous | |
| │ │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ │ └── Heterogeneous.agda | |
| │ │ │ │ ├── Sublist | |
| │ │ │ │ │ ├── DecPropositional | |
| │ │ │ │ │ │ └── Solver.agda | |
| │ │ │ │ │ ├── DecPropositional.agda | |
| │ │ │ │ │ ├── DecSetoid | |
| │ │ │ │ │ │ └── Solver.agda | |
| │ │ │ │ │ ├── DecSetoid.agda | |
| │ │ │ │ │ ├── Heterogeneous | |
| │ │ │ │ │ │ ├── Core.agda | |
| │ │ │ │ │ │ ├── Properties.agda | |
| │ │ │ │ │ │ └── Solver.agda | |
| │ │ │ │ │ ├── Heterogeneous.agda | |
| │ │ │ │ │ ├── Propositional | |
| │ │ │ │ │ │ ├── Disjoint.agda | |
| │ │ │ │ │ │ ├── Example | |
| │ │ │ │ │ │ │ └── UniqueBoundVariables.agda | |
| │ │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ │ ├── Setoid | |
| │ │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ │ └── Setoid.agda | |
| │ │ │ │ ├── Subset | |
| │ │ │ │ │ ├── Propositional | |
| │ │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ │ ├── Setoid | |
| │ │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ │ └── Setoid.agda | |
| │ │ │ │ └── Suffix | |
| │ │ │ │ ├── Heterogeneous | |
| │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ └── Heterogeneous.agda | |
| │ │ │ ├── Equality | |
| │ │ │ │ ├── DecPropositional.agda | |
| │ │ │ │ ├── DecSetoid.agda | |
| │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ └── Setoid.agda | |
| │ │ │ ├── Lex | |
| │ │ │ │ ├── Core.agda | |
| │ │ │ │ ├── NonStrict.agda | |
| │ │ │ │ └── Strict.agda | |
| │ │ │ ├── Permutation | |
| │ │ │ │ ├── Inductive | |
| │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ └── Inductive.agda | |
| │ │ │ ├── Pointwise.agda | |
| │ │ │ ├── Sublist | |
| │ │ │ │ ├── Propositional | |
| │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ └── Propositional.agda | |
| │ │ │ ├── Subset | |
| │ │ │ │ ├── Propositional | |
| │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ ├── Setoid | |
| │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ └── Setoid.agda | |
| │ │ │ ├── Ternary | |
| │ │ │ │ ├── Interleaving | |
| │ │ │ │ │ ├── Properties.agda | |
| │ │ │ │ │ ├── Propositional | |
| │ │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ │ ├── Setoid | |
| │ │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ │ └── Setoid.agda | |
| │ │ │ │ └── Interleaving.agda | |
| │ │ │ └── Unary | |
| │ │ │ ├── All | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ ├── All.agda | |
| │ │ │ ├── AllPairs | |
| │ │ │ │ ├── Core.agda | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ ├── AllPairs.agda | |
| │ │ │ ├── Any | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ ├── Any.agda | |
| │ │ │ ├── First | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ ├── First.agda | |
| │ │ │ ├── Grouped | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ ├── Grouped.agda | |
| │ │ │ ├── Linked | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ ├── Linked.agda | |
| │ │ │ └── Unique | |
| │ │ │ ├── Propositional | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ ├── Propositional.agda | |
| │ │ │ ├── Setoid | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ └── Setoid.agda | |
| │ │ ├── Reverse.agda | |
| │ │ ├── Solver.agda | |
| │ │ ├── Zipper | |
| │ │ │ └── Properties.agda | |
| │ │ └── Zipper.agda | |
| │ ├── List.agda | |
| │ ├── Maybe | |
| │ │ ├── Base.agda | |
| │ │ ├── Categorical.agda | |
| │ │ ├── Properties.agda | |
| │ │ └── Relation | |
| │ │ ├── Binary | |
| │ │ │ └── Pointwise.agda | |
| │ │ └── Unary | |
| │ │ ├── All | |
| │ │ │ └── Properties.agda | |
| │ │ ├── All.agda | |
| │ │ └── Any.agda | |
| │ ├── Maybe.agda | |
| │ ├── Nat | |
| │ │ ├── Base.agda | |
| │ │ ├── Binary | |
| │ │ │ ├── Base.agda | |
| │ │ │ ├── Induction.agda | |
| │ │ │ └── Properties.agda | |
| │ │ ├── Binary.agda | |
| │ │ ├── Coprimality.agda | |
| │ │ ├── Divisibility | |
| │ │ │ └── Core.agda | |
| │ │ ├── Divisibility.agda | |
| │ │ ├── DivMod | |
| │ │ │ ├── Core.agda | |
| │ │ │ └── WithK.agda | |
| │ │ ├── DivMod.agda | |
| │ │ ├── GCD | |
| │ │ │ └── Lemmas.agda | |
| │ │ ├── GCD.agda | |
| │ │ ├── GeneralisedArithmetic.agda | |
| │ │ ├── Induction.agda | |
| │ │ ├── InfinitelyOften.agda | |
| │ │ ├── LCM.agda | |
| │ │ ├── Literals.agda | |
| │ │ ├── Primality.agda | |
| │ │ ├── Properties.agda | |
| │ │ ├── Reflection.agda | |
| │ │ ├── Show.agda | |
| │ │ ├── Solver.agda | |
| │ │ ├── Tactic | |
| │ │ │ └── RingSolver.agda | |
| │ │ └── WithK.agda | |
| │ ├── Nat.agda | |
| │ ├── Plus.agda | |
| │ ├── Product | |
| │ │ ├── Categorical | |
| │ │ │ ├── Examples.agda | |
| │ │ │ ├── Left | |
| │ │ │ │ └── Base.agda | |
| │ │ │ ├── Left.agda | |
| │ │ │ ├── Right | |
| │ │ │ │ └── Base.agda | |
| │ │ │ └── Right.agda | |
| │ │ ├── Function | |
| │ │ │ ├── Dependent | |
| │ │ │ │ ├── Propositional | |
| │ │ │ │ │ └── WithK.agda | |
| │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ ├── Setoid | |
| │ │ │ │ │ └── WithK.agda | |
| │ │ │ │ └── Setoid.agda | |
| │ │ │ └── NonDependent | |
| │ │ │ ├── Propositional.agda | |
| │ │ │ └── Setoid.agda | |
| │ │ ├── N-ary | |
| │ │ │ ├── Categorical.agda | |
| │ │ │ └── Properties.agda | |
| │ │ ├── Nary | |
| │ │ │ └── NonDependent.agda | |
| │ │ ├── N-ary.agda | |
| │ │ ├── Properties | |
| │ │ │ └── WithK.agda | |
| │ │ ├── Properties.agda | |
| │ │ └── Relation | |
| │ │ ├── Binary | |
| │ │ │ ├── Lex | |
| │ │ │ │ ├── NonStrict.agda | |
| │ │ │ │ └── Strict.agda | |
| │ │ │ └── Pointwise | |
| │ │ │ ├── Dependent | |
| │ │ │ │ └── WithK.agda | |
| │ │ │ ├── Dependent.agda | |
| │ │ │ └── NonDependent.agda | |
| │ │ ├── Lex | |
| │ │ │ ├── NonStrict.agda | |
| │ │ │ └── Strict.agda | |
| │ │ ├── Pointwise | |
| │ │ │ ├── Dependent.agda | |
| │ │ │ └── NonDependent.agda | |
| │ │ └── Unary | |
| │ │ └── All.agda | |
| │ ├── Product.agda | |
| │ ├── Rational | |
| │ │ ├── Base.agda | |
| │ │ ├── Literals.agda | |
| │ │ ├── Properties.agda | |
| │ │ ├── Unnormalised | |
| │ │ │ └── Properties.agda | |
| │ │ └── Unnormalised.agda | |
| │ ├── Rational.agda | |
| │ ├── Record.agda | |
| │ ├── Refinement | |
| │ │ └── Relation | |
| │ │ └── Unary | |
| │ │ └── All.agda | |
| │ ├── Refinement.agda | |
| │ ├── ReflexiveClosure.agda | |
| │ ├── Sign | |
| │ │ ├── Base.agda | |
| │ │ └── Properties.agda | |
| │ ├── Sign.agda | |
| │ ├── Star | |
| │ │ ├── BoundedVec.agda | |
| │ │ ├── Decoration.agda | |
| │ │ ├── Environment.agda | |
| │ │ ├── Fin.agda | |
| │ │ ├── List.agda | |
| │ │ ├── Nat.agda | |
| │ │ ├── Pointer.agda | |
| │ │ ├── Properties.agda | |
| │ │ └── Vec.agda | |
| │ ├── Star.agda | |
| │ ├── String | |
| │ │ ├── Base.agda | |
| │ │ ├── Literals.agda | |
| │ │ ├── Properties.agda | |
| │ │ └── Unsafe.agda | |
| │ ├── String.agda | |
| │ ├── Sum | |
| │ │ ├── Base.agda | |
| │ │ ├── Categorical | |
| │ │ │ ├── Examples.agda | |
| │ │ │ ├── Left.agda | |
| │ │ │ └── Right.agda | |
| │ │ ├── Function | |
| │ │ │ ├── Propositional.agda | |
| │ │ │ └── Setoid.agda | |
| │ │ ├── Properties.agda | |
| │ │ └── Relation | |
| │ │ ├── Binary | |
| │ │ │ ├── LeftOrder.agda | |
| │ │ │ └── Pointwise.agda | |
| │ │ ├── LeftOrder.agda | |
| │ │ └── Pointwise.agda | |
| │ ├── Sum.agda | |
| │ ├── Table | |
| │ │ ├── Base.agda | |
| │ │ ├── Properties.agda | |
| │ │ └── Relation | |
| │ │ ├── Binary | |
| │ │ │ └── Equality.agda | |
| │ │ └── Equality.agda | |
| │ ├── Table.agda | |
| │ ├── These | |
| │ │ ├── Base.agda | |
| │ │ ├── Categorical | |
| │ │ │ ├── Left | |
| │ │ │ │ └── Base.agda | |
| │ │ │ ├── Left.agda | |
| │ │ │ ├── Right | |
| │ │ │ │ └── Base.agda | |
| │ │ │ └── Right.agda | |
| │ │ └── Properties.agda | |
| │ ├── These.agda | |
| │ ├── Tree | |
| │ │ ├── Binary | |
| │ │ │ ├── Properties.agda | |
| │ │ │ └── Relation | |
| │ │ │ └── Unary | |
| │ │ │ ├── All | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ └── All.agda | |
| │ │ ├── Binary.agda | |
| │ │ ├── Rose | |
| │ │ │ └── Properties.agda | |
| │ │ └── Rose.agda | |
| │ ├── Trie | |
| │ │ └── NonEmpty.agda | |
| │ ├── Trie.agda | |
| │ ├── Unit | |
| │ │ ├── Base.agda | |
| │ │ ├── NonEta.agda | |
| │ │ ├── Polymorphic | |
| │ │ │ ├── Base.agda | |
| │ │ │ └── Properties.agda | |
| │ │ ├── Polymorphic.agda | |
| │ │ └── Properties.agda | |
| │ ├── Unit.agda | |
| │ ├── Universe | |
| │ │ └── Indexed.agda | |
| │ ├── Universe.agda | |
| │ ├── Vec | |
| │ │ ├── All | |
| │ │ │ └── Properties.agda | |
| │ │ ├── All.agda | |
| │ │ ├── Any.agda | |
| │ │ ├── Base.agda | |
| │ │ ├── Bounded | |
| │ │ │ └── Base.agda | |
| │ │ ├── Bounded.agda | |
| │ │ ├── Categorical.agda | |
| │ │ ├── Functional | |
| │ │ │ └── Relation | |
| │ │ │ ├── Binary | |
| │ │ │ │ ├── Pointwise | |
| │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ └── Pointwise.agda | |
| │ │ │ └── Unary | |
| │ │ │ ├── All | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ ├── All.agda | |
| │ │ │ └── Any.agda | |
| │ │ ├── Functional.agda | |
| │ │ ├── Membership | |
| │ │ │ ├── DecPropositional.agda | |
| │ │ │ ├── DecSetoid.agda | |
| │ │ │ ├── Propositional | |
| │ │ │ │ └── Properties.agda | |
| │ │ │ ├── Propositional.agda | |
| │ │ │ └── Setoid.agda | |
| │ │ ├── N-ary.agda | |
| │ │ ├── Properties | |
| │ │ │ └── WithK.agda | |
| │ │ ├── Properties.agda | |
| │ │ ├── Recursive | |
| │ │ │ ├── Categorical.agda | |
| │ │ │ └── Properties.agda | |
| │ │ ├── Recursive.agda | |
| │ │ └── Relation | |
| │ │ ├── Binary | |
| │ │ │ ├── Equality | |
| │ │ │ │ ├── DecPropositional.agda | |
| │ │ │ │ ├── DecSetoid.agda | |
| │ │ │ │ ├── Propositional | |
| │ │ │ │ │ └── WithK.agda | |
| │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ └── Setoid.agda | |
| │ │ │ └── Pointwise | |
| │ │ │ ├── Extensional.agda | |
| │ │ │ └── Inductive.agda | |
| │ │ ├── Equality | |
| │ │ │ ├── DecPropositional.agda | |
| │ │ │ ├── DecSetoid.agda | |
| │ │ │ ├── Propositional.agda | |
| │ │ │ └── Setoid.agda | |
| │ │ ├── Pointwise | |
| │ │ │ ├── Extensional.agda | |
| │ │ │ └── Inductive.agda | |
| │ │ └── Unary | |
| │ │ ├── All | |
| │ │ │ └── Properties.agda | |
| │ │ ├── All.agda | |
| │ │ ├── Any | |
| │ │ │ └── Properties.agda | |
| │ │ └── Any.agda | |
| │ ├── Vec.agda | |
| │ ├── W | |
| │ │ ├── Indexed.agda | |
| │ │ └── WithK.agda | |
| │ ├── W.agda | |
| │ ├── Word | |
| │ │ ├── Base.agda | |
| │ │ └── Properties.agda | |
| │ └── Word.agda | |
| ├── Debug | |
| │ └── Trace.agda | |
| ├── Foreign | |
| │ ├── Haskell | |
| │ │ ├── Coerce.agda | |
| │ │ ├── Either.agda | |
| │ │ ├── Maybe.agda | |
| │ │ └── Pair.agda | |
| │ └── Haskell.agda | |
| ├── Function | |
| │ ├── Base.agda | |
| │ ├── Bijection.agda | |
| │ ├── Bundles.agda | |
| │ ├── Construct | |
| │ │ ├── Composition.agda | |
| │ │ └── Identity.agda | |
| │ ├── Core.agda | |
| │ ├── Definitions | |
| │ │ ├── Core1.agda | |
| │ │ └── Core2.agda | |
| │ ├── Definitions.agda | |
| │ ├── Endomorphism | |
| │ │ ├── Propositional.agda | |
| │ │ └── Setoid.agda | |
| │ ├── Equality.agda | |
| │ ├── Equivalence.agda | |
| │ ├── HalfAdjointEquivalence.agda | |
| │ ├── Identity | |
| │ │ └── Categorical.agda | |
| │ ├── Injection.agda | |
| │ ├── Inverse.agda | |
| │ ├── LeftInverse.agda | |
| │ ├── Nary | |
| │ │ ├── NonDependent | |
| │ │ │ └── Base.agda | |
| │ │ └── NonDependent.agda | |
| │ ├── Reasoning.agda | |
| │ ├── Related | |
| │ │ ├── TypeIsomorphisms | |
| │ │ │ └── Solver.agda | |
| │ │ └── TypeIsomorphisms.agda | |
| │ ├── Related.agda | |
| │ ├── Structures.agda | |
| │ └── Surjection.agda | |
| ├── Function.agda | |
| ├── Induction | |
| │ ├── Lexicographic.agda | |
| │ ├── Nat.agda | |
| │ └── WellFounded.agda | |
| ├── Induction.agda | |
| ├── IO | |
| │ └── Primitive.agda | |
| ├── IO.agda | |
| ├── Level | |
| │ └── Literals.agda | |
| ├── Level.agda | |
| ├── Record.agda | |
| ├── Reflection | |
| │ ├── Abstraction.agda | |
| │ ├── Argument | |
| │ │ ├── Information.agda | |
| │ │ ├── Relevance.agda | |
| │ │ └── Visibility.agda | |
| │ ├── Argument.agda | |
| │ ├── Definition.agda | |
| │ ├── Literal.agda | |
| │ ├── Meta.agda | |
| │ ├── Name.agda | |
| │ ├── Pattern.agda | |
| │ ├── Show.agda | |
| │ ├── Term.agda | |
| │ └── TypeChecking | |
| │ └── MonadSyntax.agda | |
| ├── Reflection.agda | |
| ├── Relation | |
| │ ├── Binary | |
| │ │ ├── Bundles.agda | |
| │ │ ├── Consequences.agda | |
| │ │ ├── Construct | |
| │ │ │ ├── Add | |
| │ │ │ │ ├── Extrema | |
| │ │ │ │ │ ├── Equality.agda | |
| │ │ │ │ │ ├── NonStrict.agda | |
| │ │ │ │ │ └── Strict.agda | |
| │ │ │ │ ├── Infimum | |
| │ │ │ │ │ ├── Equality.agda | |
| │ │ │ │ │ ├── NonStrict.agda | |
| │ │ │ │ │ └── Strict.agda | |
| │ │ │ │ ├── Point | |
| │ │ │ │ │ └── Equality.agda | |
| │ │ │ │ └── Supremum | |
| │ │ │ │ ├── Equality.agda | |
| │ │ │ │ ├── NonStrict.agda | |
| │ │ │ │ └── Strict.agda | |
| │ │ │ ├── Always.agda | |
| │ │ │ ├── Closure | |
| │ │ │ │ ├── Equivalence | |
| │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ ├── Equivalence.agda | |
| │ │ │ │ ├── Reflexive | |
| │ │ │ │ │ ├── Properties | |
| │ │ │ │ │ │ └── WithK.agda | |
| │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ ├── Reflexive.agda | |
| │ │ │ │ ├── ReflexiveTransitive | |
| │ │ │ │ │ ├── Properties | |
| │ │ │ │ │ │ └── WithK.agda | |
| │ │ │ │ │ └── Properties.agda | |
| │ │ │ │ ├── ReflexiveTransitive.agda | |
| │ │ │ │ ├── Symmetric.agda | |
| │ │ │ │ ├── Transitive | |
| │ │ │ │ │ └── WithK.agda | |
| │ │ │ │ └── Transitive.agda | |
| │ │ │ ├── Constant.agda | |
| │ │ │ ├── Converse.agda | |
| │ │ │ ├── Flip.agda | |
| │ │ │ ├── FromPred.agda | |
| │ │ │ ├── FromRel.agda | |
| │ │ │ ├── Intersection.agda | |
| │ │ │ ├── NaturalOrder | |
| │ │ │ │ ├── Left.agda | |
| │ │ │ │ └── Right.agda | |
| │ │ │ ├── Never.agda | |
| │ │ │ ├── NonStrictToStrict.agda | |
| │ │ │ ├── On.agda | |
| │ │ │ ├── StrictToNonStrict.agda | |
| │ │ │ └── Union.agda | |
| │ │ ├── Core.agda | |
| │ │ ├── Definitions.agda | |
| │ │ ├── EqReasoning.agda | |
| │ │ ├── EquivalenceClosure.agda | |
| │ │ ├── HeterogeneousEquality | |
| │ │ │ ├── Core.agda | |
| │ │ │ ├── Quotients | |
| │ │ │ │ └── Examples.agda | |
| │ │ │ └── Quotients.agda | |
| │ │ ├── HeterogeneousEquality.agda | |
| │ │ ├── Indexed | |
| │ │ │ ├── Heterogeneous | |
| │ │ │ │ ├── Bundles.agda | |
| │ │ │ │ ├── Construct | |
| │ │ │ │ │ ├── At.agda | |
| │ │ │ │ │ └── Trivial.agda | |
| │ │ │ │ ├── Core.agda | |
| │ │ │ │ ├── Definitions.agda | |
| │ │ │ │ └── Structures.agda | |
| │ │ │ ├── Heterogeneous.agda | |
| │ │ │ ├── Homogeneous | |
| │ │ │ │ ├── Bundles.agda | |
| │ │ │ │ ├── Core.agda | |
| │ │ │ │ ├── Definitions.agda | |
| │ │ │ │ └── Structures.agda | |
| │ │ │ └── Homogeneous.agda | |
| │ │ ├── Lattice.agda | |
| │ │ ├── Morphism | |
| │ │ │ ├── Definitions.agda | |
| │ │ │ ├── OrderMonomorphism.agda | |
| │ │ │ ├── RelMonomorphism.agda | |
| │ │ │ └── Structures.agda | |
| │ │ ├── Morphism.agda | |
| │ │ ├── OrderMorphism.agda | |
| │ │ ├── PartialOrderReasoning.agda | |
| │ │ ├── PreorderReasoning.agda | |
| │ │ ├── Properties | |
| │ │ │ ├── BoundedJoinSemilattice.agda | |
| │ │ │ ├── BoundedLattice.agda | |
| │ │ │ ├── BoundedMeetSemilattice.agda | |
| │ │ │ ├── DecTotalOrder.agda | |
| │ │ │ ├── DistributiveLattice.agda | |
| │ │ │ ├── HeytingAlgebra.agda | |
| │ │ │ ├── JoinSemilattice.agda | |
| │ │ │ ├── Lattice.agda | |
| │ │ │ ├── MeetSemilattice.agda | |
| │ │ │ ├── Poset.agda | |
| │ │ │ ├── Preorder.agda | |
| │ │ │ ├── Setoid.agda | |
| │ │ │ ├── StrictPartialOrder.agda | |
| │ │ │ ├── StrictTotalOrder.agda | |
| │ │ │ └── TotalOrder.agda | |
| │ │ ├── PropositionalEquality | |
| │ │ │ ├── Core.agda | |
| │ │ │ ├── TrustMe.agda | |
| │ │ │ └── WithK.agda | |
| │ │ ├── PropositionalEquality.agda | |
| │ │ ├── Reasoning | |
| │ │ │ ├── Base | |
| │ │ │ │ ├── Double.agda | |
| │ │ │ │ ├── Partial.agda | |
| │ │ │ │ ├── Single.agda | |
| │ │ │ │ └── Triple.agda | |
| │ │ │ ├── MultiSetoid.agda | |
| │ │ │ ├── PartialOrder.agda | |
| │ │ │ ├── PartialSetoid.agda | |
| │ │ │ ├── Preorder.agda | |
| │ │ │ ├── Setoid.agda | |
| │ │ │ └── StrictPartialOrder.agda | |
| │ │ ├── Reflection.agda | |
| │ │ ├── Rewriting.agda | |
| │ │ ├── SetoidReasoning.agda | |
| │ │ ├── StrictPartialOrderReasoning.agda | |
| │ │ ├── Structures.agda | |
| │ │ └── SymmetricClosure.agda | |
| │ ├── Binary.agda | |
| │ ├── Nary.agda | |
| │ ├── Nullary | |
| │ │ ├── Construct | |
| │ │ │ └── Add | |
| │ │ │ ├── Extrema.agda | |
| │ │ │ ├── Infimum.agda | |
| │ │ │ ├── Point.agda | |
| │ │ │ └── Supremum.agda | |
| │ │ ├── Decidable | |
| │ │ │ └── Core.agda | |
| │ │ ├── Decidable.agda | |
| │ │ ├── Implication.agda | |
| │ │ ├── Negation.agda | |
| │ │ ├── Product.agda | |
| │ │ ├── Reflects.agda | |
| │ │ ├── Sum.agda | |
| │ │ └── Universe.agda | |
| │ ├── Nullary.agda | |
| │ ├── Unary | |
| │ │ ├── Closure | |
| │ │ │ ├── Base.agda | |
| │ │ │ ├── Preorder.agda | |
| │ │ │ └── StrictPartialOrder.agda | |
| │ │ ├── Consequences.agda | |
| │ │ ├── Indexed.agda | |
| │ │ ├── PredicateTransformer.agda | |
| │ │ └── Properties.agda | |
| │ └── Unary.agda | |
| ├── Size.agda | |
| ├── Strict.agda | |
| ├── Tactic | |
| │ ├── MonoidSolver.agda | |
| │ ├── RingSolver | |
| │ │ ├── Core | |
| │ │ │ ├── AlmostCommutativeRing.agda | |
| │ │ │ ├── Expression.agda | |
| │ │ │ ├── NatSet.agda | |
| │ │ │ ├── Polynomial | |
| │ │ │ │ ├── Base.agda | |
| │ │ │ │ ├── Homomorphism | |
| │ │ │ │ │ ├── Addition.agda | |
| │ │ │ │ │ ├── Constants.agda | |
| │ │ │ │ │ ├── Exponentiation.agda | |
| │ │ │ │ │ ├── Lemmas.agda | |
| │ │ │ │ │ ├── Multiplication.agda | |
| │ │ │ │ │ ├── Negation.agda | |
| │ │ │ │ │ └── Variables.agda | |
| │ │ │ │ ├── Homomorphism.agda | |
| │ │ │ │ ├── Parameters.agda | |
| │ │ │ │ ├── Reasoning.agda | |
| │ │ │ │ └── Semantics.agda | |
| │ │ │ └── ReflectionHelp.agda | |
| │ │ └── NonReflective.agda | |
| │ └── RingSolver.agda | |
| ├── Text | |
| │ ├── Format.agda | |
| │ ├── Pretty | |
| │ │ └── Core.agda | |
| │ ├── Pretty.agda | |
| │ ├── Printf.agda | |
| │ ├── Tabular | |
| │ │ ├── Base.agda | |
| │ │ ├── List.agda | |
| │ │ └── Vec.agda | |
| │ └── Tree | |
| │ └── Linear.agda | |
| └── Universe.agda | |
| 281 directories, 713 files |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment