Created
December 16, 2018 19:14
-
-
Save ryantm/514ce005d5774e59cdccb148ce55dcc3 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/hhj006v7r40c048brb8x5yfb71i5wchb-agda-stdlib-0.17 | |
| └── share | |
| └── agda | |
| ├── Algebra | |
| │ ├── FunctionProperties | |
| │ │ ├── Consequences.agda | |
| │ │ ├── Consequences.agdai | |
| │ │ ├── Core.agda | |
| │ │ └── Core.agdai | |
| │ ├── FunctionProperties.agda | |
| │ ├── FunctionProperties.agdai | |
| │ ├── Morphism.agda | |
| │ ├── Morphism.agdai | |
| │ ├── Operations | |
| │ │ ├── CommutativeMonoid.agda | |
| │ │ ├── CommutativeMonoid.agdai | |
| │ │ ├── Semiring.agda | |
| │ │ └── Semiring.agdai | |
| │ ├── Properties | |
| │ │ ├── AbelianGroup.agda | |
| │ │ ├── AbelianGroup.agdai | |
| │ │ ├── BooleanAlgebra | |
| │ │ │ ├── Expression.agda | |
| │ │ │ └── Expression.agdai | |
| │ │ ├── BooleanAlgebra.agda | |
| │ │ ├── BooleanAlgebra.agdai | |
| │ │ ├── CommutativeMonoid.agda | |
| │ │ ├── CommutativeMonoid.agdai | |
| │ │ ├── DistributiveLattice.agda | |
| │ │ ├── DistributiveLattice.agdai | |
| │ │ ├── Group.agda | |
| │ │ ├── Group.agdai | |
| │ │ ├── Lattice.agda | |
| │ │ ├── Lattice.agdai | |
| │ │ ├── Ring.agda | |
| │ │ └── Ring.agdai | |
| │ ├── Solver | |
| │ │ ├── CommutativeMonoid | |
| │ │ │ ├── Example.agda | |
| │ │ │ └── Example.agdai | |
| │ │ ├── CommutativeMonoid.agda | |
| │ │ ├── CommutativeMonoid.agdai | |
| │ │ ├── IdempotentCommutativeMonoid | |
| │ │ │ ├── Example.agda | |
| │ │ │ └── Example.agdai | |
| │ │ ├── IdempotentCommutativeMonoid.agda | |
| │ │ ├── IdempotentCommutativeMonoid.agdai | |
| │ │ ├── Monoid.agda | |
| │ │ ├── Monoid.agdai | |
| │ │ ├── Ring | |
| │ │ │ ├── AlmostCommutativeRing.agda | |
| │ │ │ ├── AlmostCommutativeRing.agdai | |
| │ │ │ ├── Lemmas.agda | |
| │ │ │ ├── Lemmas.agdai | |
| │ │ │ ├── NaturalCoefficients.agda | |
| │ │ │ ├── NaturalCoefficients.agdai | |
| │ │ │ ├── Simple.agda | |
| │ │ │ └── Simple.agdai | |
| │ │ ├── Ring.agda | |
| │ │ └── Ring.agdai | |
| │ ├── Structures.agda | |
| │ └── Structures.agdai | |
| ├── Algebra.agda | |
| ├── Algebra.agdai | |
| ├── Category | |
| │ ├── Applicative | |
| │ │ ├── Indexed.agda | |
| │ │ ├── Indexed.agdai | |
| │ │ ├── Predicate.agda | |
| │ │ └── Predicate.agdai | |
| │ ├── Applicative.agda | |
| │ ├── Applicative.agdai | |
| │ ├── Comonad.agda | |
| │ ├── Comonad.agdai | |
| │ ├── Functor | |
| │ │ ├── Predicate.agda | |
| │ │ └── Predicate.agdai | |
| │ ├── Functor.agda | |
| │ ├── Functor.agdai | |
| │ ├── Monad | |
| │ │ ├── Continuation.agda | |
| │ │ ├── Continuation.agdai | |
| │ │ ├── Indexed.agda | |
| │ │ ├── Indexed.agdai | |
| │ │ ├── Partiality | |
| │ │ │ ├── All.agda | |
| │ │ │ └── All.agdai | |
| │ │ ├── Partiality.agda | |
| │ │ ├── Partiality.agdai | |
| │ │ ├── Predicate.agda | |
| │ │ ├── Predicate.agdai | |
| │ │ ├── State.agda | |
| │ │ └── State.agdai | |
| │ ├── Monad.agda | |
| │ └── Monad.agdai | |
| ├── Codata | |
| │ ├── Cofin | |
| │ │ ├── Literals.agda | |
| │ │ └── Literals.agdai | |
| │ ├── Cofin.agda | |
| │ ├── Cofin.agdai | |
| │ ├── Colist | |
| │ │ ├── Bisimilarity.agda | |
| │ │ ├── Bisimilarity.agdai | |
| │ │ ├── Categorical.agda | |
| │ │ ├── Categorical.agdai | |
| │ │ ├── Properties.agda | |
| │ │ └── Properties.agdai | |
| │ ├── Colist.agda | |
| │ ├── Colist.agdai | |
| │ ├── Conat | |
| │ │ ├── Bisimilarity.agda | |
| │ │ ├── Bisimilarity.agdai | |
| │ │ ├── Literals.agda | |
| │ │ ├── Literals.agdai | |
| │ │ ├── Properties.agda | |
| │ │ └── Properties.agdai | |
| │ ├── Conat.agda | |
| │ ├── Conat.agdai | |
| │ ├── Covec | |
| │ │ ├── Bisimilarity.agda | |
| │ │ ├── Bisimilarity.agdai | |
| │ │ ├── Categorical.agda | |
| │ │ ├── Categorical.agdai | |
| │ │ ├── Properties.agda | |
| │ │ └── Properties.agdai | |
| │ ├── Covec.agda | |
| │ ├── Covec.agdai | |
| │ ├── Delay | |
| │ │ ├── Bisimilarity.agda | |
| │ │ ├── Bisimilarity.agdai | |
| │ │ ├── Categorical.agda | |
| │ │ ├── Categorical.agdai | |
| │ │ ├── Properties.agda | |
| │ │ └── Properties.agdai | |
| │ ├── Delay.agda | |
| │ ├── Delay.agdai | |
| │ ├── M.agda | |
| │ ├── M.agdai | |
| │ ├── Musical | |
| │ │ ├── Cofin.agda | |
| │ │ ├── Cofin.agdai | |
| │ │ ├── Colist | |
| │ │ │ ├── Infinite-merge.agda | |
| │ │ │ └── Infinite-merge.agdai | |
| │ │ ├── Colist.agda | |
| │ │ ├── Colist.agdai | |
| │ │ ├── Conat.agda | |
| │ │ ├── Conat.agdai | |
| │ │ ├── Costring.agda | |
| │ │ ├── Costring.agdai | |
| │ │ ├── Covec.agda | |
| │ │ ├── Covec.agdai | |
| │ │ ├── M | |
| │ │ │ ├── Indexed.agda | |
| │ │ │ └── Indexed.agdai | |
| │ │ ├── M.agda | |
| │ │ ├── M.agdai | |
| │ │ ├── Notation.agda | |
| │ │ ├── Notation.agdai | |
| │ │ ├── Stream.agda | |
| │ │ └── Stream.agdai | |
| │ ├── Stream | |
| │ │ ├── Bisimilarity.agda | |
| │ │ ├── Bisimilarity.agdai | |
| │ │ ├── Categorical.agda | |
| │ │ ├── Categorical.agdai | |
| │ │ ├── Properties.agda | |
| │ │ └── Properties.agdai | |
| │ ├── Stream.agda | |
| │ ├── Stream.agdai | |
| │ ├── Thunk.agda | |
| │ └── Thunk.agdai | |
| ├── Data | |
| │ ├── AVL | |
| │ │ ├── Height.agda | |
| │ │ ├── Height.agdai | |
| │ │ ├── Indexed.agda | |
| │ │ ├── Indexed.agdai | |
| │ │ ├── IndexedMap.agda | |
| │ │ ├── IndexedMap.agdai | |
| │ │ ├── Key.agda | |
| │ │ ├── Key.agdai | |
| │ │ ├── Sets.agda | |
| │ │ └── Sets.agdai | |
| │ ├── AVL.agda | |
| │ ├── AVL.agdai | |
| │ ├── Bin | |
| │ │ ├── Properties.agda | |
| │ │ └── Properties.agdai | |
| │ ├── Bin.agda | |
| │ ├── Bin.agdai | |
| │ ├── Bool | |
| │ │ ├── Base.agda | |
| │ │ ├── Base.agdai | |
| │ │ ├── Properties.agda | |
| │ │ ├── Properties.agdai | |
| │ │ ├── Show.agda | |
| │ │ ├── Show.agdai | |
| │ │ ├── Solver.agda | |
| │ │ └── Solver.agdai | |
| │ ├── Bool.agda | |
| │ ├── Bool.agdai | |
| │ ├── BoundedVec | |
| │ │ ├── Inefficient.agda | |
| │ │ └── Inefficient.agdai | |
| │ ├── BoundedVec.agda | |
| │ ├── BoundedVec.agdai | |
| │ ├── Char | |
| │ │ ├── Base.agda | |
| │ │ ├── Base.agdai | |
| │ │ ├── Unsafe.agda | |
| │ │ └── Unsafe.agdai | |
| │ ├── Char.agda | |
| │ ├── Char.agdai | |
| │ ├── Container | |
| │ │ ├── Any.agda | |
| │ │ ├── Any.agdai | |
| │ │ ├── Combinator.agda | |
| │ │ ├── Combinator.agdai | |
| │ │ ├── Core.agda | |
| │ │ ├── Core.agdai | |
| │ │ ├── FreeMonad.agda | |
| │ │ ├── FreeMonad.agdai | |
| │ │ ├── Indexed | |
| │ │ │ ├── Combinator.agda | |
| │ │ │ ├── Combinator.agdai | |
| │ │ │ ├── Core.agda | |
| │ │ │ ├── Core.agdai | |
| │ │ │ ├── FreeMonad.agda | |
| │ │ │ └── FreeMonad.agdai | |
| │ │ ├── Indexed.agda | |
| │ │ └── Indexed.agdai | |
| │ ├── Container.agda | |
| │ ├── Container.agdai | |
| │ ├── DifferenceList.agda | |
| │ ├── DifferenceList.agdai | |
| │ ├── DifferenceNat.agda | |
| │ ├── DifferenceNat.agdai | |
| │ ├── DifferenceVec.agda | |
| │ ├── DifferenceVec.agdai | |
| │ ├── Digit.agda | |
| │ ├── Digit.agdai | |
| │ ├── Empty | |
| │ │ ├── Irrelevant.agda | |
| │ │ └── Irrelevant.agdai | |
| │ ├── Empty.agda | |
| │ ├── Empty.agdai | |
| │ ├── Fin | |
| │ │ ├── Base.agda | |
| │ │ ├── Base.agdai | |
| │ │ ├── Dec.agda | |
| │ │ ├── Dec.agdai | |
| │ │ ├── Literals.agda | |
| │ │ ├── Literals.agdai | |
| │ │ ├── Permutation | |
| │ │ │ ├── Components.agda | |
| │ │ │ └── Components.agdai | |
| │ │ ├── Permutation.agda | |
| │ │ ├── Permutation.agdai | |
| │ │ ├── Properties.agda | |
| │ │ ├── Properties.agdai | |
| │ │ ├── Subset | |
| │ │ │ ├── Properties.agda | |
| │ │ │ └── Properties.agdai | |
| │ │ ├── Subset.agda | |
| │ │ ├── Subset.agdai | |
| │ │ ├── Substitution | |
| │ │ │ ├── Example.agda | |
| │ │ │ ├── Example.agdai | |
| │ │ │ ├── Lemmas.agda | |
| │ │ │ ├── Lemmas.agdai | |
| │ │ │ ├── List.agda | |
| │ │ │ └── List.agdai | |
| │ │ ├── Substitution.agda | |
| │ │ └── Substitution.agdai | |
| │ ├── Fin.agda | |
| │ ├── Fin.agdai | |
| │ ├── Float | |
| │ │ ├── Unsafe.agda | |
| │ │ └── Unsafe.agdai | |
| │ ├── Float.agda | |
| │ ├── Float.agdai | |
| │ ├── Graph | |
| │ │ ├── Acyclic.agda | |
| │ │ └── Acyclic.agdai | |
| │ ├── Integer | |
| │ │ ├── Addition | |
| │ │ │ ├── Properties.agda | |
| │ │ │ └── Properties.agdai | |
| │ │ ├── Base.agda | |
| │ │ ├── Base.agdai | |
| │ │ ├── Divisibility.agda | |
| │ │ ├── Divisibility.agdai | |
| │ │ ├── Literals.agda | |
| │ │ ├── Literals.agdai | |
| │ │ ├── Multiplication | |
| │ │ │ ├── Properties.agda | |
| │ │ │ └── Properties.agdai | |
| │ │ ├── Properties.agda | |
| │ │ ├── Properties.agdai | |
| │ │ ├── Solver.agda | |
| │ │ └── Solver.agdai | |
| │ ├── Integer.agda | |
| │ ├── Integer.agdai | |
| │ ├── List | |
| │ │ ├── All | |
| │ │ │ ├── Properties.agda | |
| │ │ │ └── Properties.agdai | |
| │ │ ├── All.agda | |
| │ │ ├── All.agdai | |
| │ │ ├── Any | |
| │ │ │ ├── Properties.agda | |
| │ │ │ └── Properties.agdai | |
| │ │ ├── Any.agda | |
| │ │ ├── Any.agdai | |
| │ │ ├── Base.agda | |
| │ │ ├── Base.agdai | |
| │ │ ├── Categorical.agda | |
| │ │ ├── Categorical.agdai | |
| │ │ ├── Countdown.agda | |
| │ │ ├── Countdown.agdai | |
| │ │ ├── Literals.agda | |
| │ │ ├── Literals.agdai | |
| │ │ ├── Membership | |
| │ │ │ ├── DecPropositional.agda | |
| │ │ │ ├── DecPropositional.agdai | |
| │ │ │ ├── DecSetoid.agda | |
| │ │ │ ├── DecSetoid.agdai | |
| │ │ │ ├── Propositional | |
| │ │ │ │ ├── Properties | |
| │ │ │ │ │ ├── Core.agda | |
| │ │ │ │ │ └── Core.agdai | |
| │ │ │ │ ├── Properties.agda | |
| │ │ │ │ └── Properties.agdai | |
| │ │ │ ├── Propositional.agda | |
| │ │ │ ├── Propositional.agdai | |
| │ │ │ ├── Setoid | |
| │ │ │ │ ├── Properties.agda | |
| │ │ │ │ └── Properties.agdai | |
| │ │ │ ├── Setoid.agda | |
| │ │ │ └── Setoid.agdai | |
| │ │ ├── NonEmpty | |
| │ │ │ ├── Categorical.agda | |
| │ │ │ ├── Categorical.agdai | |
| │ │ │ ├── Properties.agda | |
| │ │ │ └── Properties.agdai | |
| │ │ ├── NonEmpty.agda | |
| │ │ ├── NonEmpty.agdai | |
| │ │ ├── Properties.agda | |
| │ │ ├── Properties.agdai | |
| │ │ ├── Relation | |
| │ │ │ ├── BagAndSetEquality.agda | |
| │ │ │ ├── BagAndSetEquality.agdai | |
| │ │ │ ├── Equality | |
| │ │ │ │ ├── DecPropositional.agda | |
| │ │ │ │ ├── DecPropositional.agdai | |
| │ │ │ │ ├── DecSetoid.agda | |
| │ │ │ │ ├── DecSetoid.agdai | |
| │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ ├── Propositional.agdai | |
| │ │ │ │ ├── Setoid.agda | |
| │ │ │ │ └── Setoid.agdai | |
| │ │ │ ├── Lex | |
| │ │ │ │ ├── Core.agda | |
| │ │ │ │ ├── Core.agdai | |
| │ │ │ │ ├── NonStrict.agda | |
| │ │ │ │ ├── NonStrict.agdai | |
| │ │ │ │ ├── Strict.agda | |
| │ │ │ │ └── Strict.agdai | |
| │ │ │ ├── Permutation | |
| │ │ │ │ ├── Inductive | |
| │ │ │ │ │ ├── Properties.agda | |
| │ │ │ │ │ └── Properties.agdai | |
| │ │ │ │ ├── Inductive.agda | |
| │ │ │ │ └── Inductive.agdai | |
| │ │ │ ├── Pointwise.agda | |
| │ │ │ ├── Pointwise.agdai | |
| │ │ │ ├── Sublist | |
| │ │ │ │ ├── Propositional | |
| │ │ │ │ │ ├── Properties.agda | |
| │ │ │ │ │ ├── Properties.agdai | |
| │ │ │ │ │ ├── Solver.agda | |
| │ │ │ │ │ └── Solver.agdai | |
| │ │ │ │ ├── Propositional.agda | |
| │ │ │ │ └── Propositional.agdai | |
| │ │ │ └── Subset | |
| │ │ │ ├── Propositional | |
| │ │ │ │ ├── Properties.agda | |
| │ │ │ │ └── Properties.agdai | |
| │ │ │ ├── Propositional.agda | |
| │ │ │ ├── Propositional.agdai | |
| │ │ │ ├── Setoid | |
| │ │ │ │ ├── Properties.agda | |
| │ │ │ │ └── Properties.agdai | |
| │ │ │ ├── Setoid.agda | |
| │ │ │ └── Setoid.agdai | |
| │ │ ├── Reverse.agda | |
| │ │ ├── Reverse.agdai | |
| │ │ ├── Solver.agda | |
| │ │ ├── Solver.agdai | |
| │ │ ├── Zipper | |
| │ │ │ ├── Properties.agda | |
| │ │ │ └── Properties.agdai | |
| │ │ ├── Zipper.agda | |
| │ │ └── Zipper.agdai | |
| │ ├── List.agda | |
| │ ├── List.agdai | |
| │ ├── Maybe | |
| │ │ ├── Base.agda | |
| │ │ ├── Base.agdai | |
| │ │ ├── Categorical.agda | |
| │ │ └── Categorical.agdai | |
| │ ├── Maybe.agda | |
| │ ├── Maybe.agdai | |
| │ ├── Nat | |
| │ │ ├── Base.agda | |
| │ │ ├── Base.agdai | |
| │ │ ├── Coprimality.agda | |
| │ │ ├── Coprimality.agdai | |
| │ │ ├── Divisibility.agda | |
| │ │ ├── Divisibility.agdai | |
| │ │ ├── DivMod | |
| │ │ │ ├── Core.agda | |
| │ │ │ ├── Core.agdai | |
| │ │ │ ├── Unsafe.agda | |
| │ │ │ └── Unsafe.agdai | |
| │ │ ├── DivMod.agda | |
| │ │ ├── DivMod.agdai | |
| │ │ ├── GCD | |
| │ │ │ ├── Lemmas.agda | |
| │ │ │ └── Lemmas.agdai | |
| │ │ ├── GCD.agda | |
| │ │ ├── GCD.agdai | |
| │ │ ├── GeneralisedArithmetic.agda | |
| │ │ ├── GeneralisedArithmetic.agdai | |
| │ │ ├── InfinitelyOften.agda | |
| │ │ ├── InfinitelyOften.agdai | |
| │ │ ├── LCM.agda | |
| │ │ ├── LCM.agdai | |
| │ │ ├── Literals.agda | |
| │ │ ├── Literals.agdai | |
| │ │ ├── Primality.agda | |
| │ │ ├── Primality.agdai | |
| │ │ ├── Properties | |
| │ │ │ ├── Simple.agda | |
| │ │ │ └── Simple.agdai | |
| │ │ ├── Properties.agda | |
| │ │ ├── Properties.agdai | |
| │ │ ├── Show.agda | |
| │ │ ├── Show.agdai | |
| │ │ ├── Solver.agda | |
| │ │ ├── Solver.agdai | |
| │ │ ├── Unsafe.agda | |
| │ │ └── Unsafe.agdai | |
| │ ├── Nat.agda | |
| │ ├── Nat.agdai | |
| │ ├── Plus.agda | |
| │ ├── Plus.agdai | |
| │ ├── Product | |
| │ │ ├── Categorical | |
| │ │ │ ├── Examples.agda | |
| │ │ │ ├── Examples.agdai | |
| │ │ │ ├── Left | |
| │ │ │ │ ├── Base.agda | |
| │ │ │ │ └── Base.agdai | |
| │ │ │ ├── Left.agda | |
| │ │ │ ├── Left.agdai | |
| │ │ │ ├── Right | |
| │ │ │ │ ├── Base.agda | |
| │ │ │ │ └── Base.agdai | |
| │ │ │ ├── Right.agda | |
| │ │ │ └── Right.agdai | |
| │ │ ├── N-ary | |
| │ │ │ ├── Categorical.agda | |
| │ │ │ ├── Categorical.agdai | |
| │ │ │ ├── Properties.agda | |
| │ │ │ └── Properties.agdai | |
| │ │ ├── N-ary.agda | |
| │ │ ├── N-ary.agdai | |
| │ │ ├── Properties.agda | |
| │ │ ├── Properties.agdai | |
| │ │ └── Relation | |
| │ │ ├── Lex | |
| │ │ │ ├── NonStrict.agda | |
| │ │ │ ├── NonStrict.agdai | |
| │ │ │ ├── Strict.agda | |
| │ │ │ └── Strict.agdai | |
| │ │ └── Pointwise | |
| │ │ ├── Dependent.agda | |
| │ │ ├── Dependent.agdai | |
| │ │ ├── NonDependent.agda | |
| │ │ └── NonDependent.agdai | |
| │ ├── Product.agda | |
| │ ├── Product.agdai | |
| │ ├── Rational | |
| │ │ ├── Literals.agda | |
| │ │ ├── Literals.agdai | |
| │ │ ├── Properties.agda | |
| │ │ └── Properties.agdai | |
| │ ├── Rational.agda | |
| │ ├── Rational.agdai | |
| │ ├── ReflexiveClosure.agda | |
| │ ├── ReflexiveClosure.agdai | |
| │ ├── Sign | |
| │ │ ├── Properties.agda | |
| │ │ └── Properties.agdai | |
| │ ├── Sign.agda | |
| │ ├── Sign.agdai | |
| │ ├── Star | |
| │ │ ├── BoundedVec.agda | |
| │ │ ├── BoundedVec.agdai | |
| │ │ ├── Decoration.agda | |
| │ │ ├── Decoration.agdai | |
| │ │ ├── Environment.agda | |
| │ │ ├── Environment.agdai | |
| │ │ ├── Fin.agda | |
| │ │ ├── Fin.agdai | |
| │ │ ├── List.agda | |
| │ │ ├── List.agdai | |
| │ │ ├── Nat.agda | |
| │ │ ├── Nat.agdai | |
| │ │ ├── Pointer.agda | |
| │ │ ├── Pointer.agdai | |
| │ │ ├── Properties.agda | |
| │ │ ├── Properties.agdai | |
| │ │ ├── Vec.agda | |
| │ │ └── Vec.agdai | |
| │ ├── Star.agda | |
| │ ├── Star.agdai | |
| │ ├── String | |
| │ │ ├── Base.agda | |
| │ │ ├── Base.agdai | |
| │ │ ├── Literals.agda | |
| │ │ ├── Literals.agdai | |
| │ │ ├── Unsafe.agda | |
| │ │ └── Unsafe.agdai | |
| │ ├── String.agda | |
| │ ├── String.agdai | |
| │ ├── Sum | |
| │ │ ├── Base.agda | |
| │ │ ├── Base.agdai | |
| │ │ ├── Categorical | |
| │ │ │ ├── Examples.agda | |
| │ │ │ ├── Examples.agdai | |
| │ │ │ ├── Left.agda | |
| │ │ │ ├── Left.agdai | |
| │ │ │ ├── Right.agda | |
| │ │ │ └── Right.agdai | |
| │ │ ├── Properties.agda | |
| │ │ ├── Properties.agdai | |
| │ │ └── Relation | |
| │ │ ├── Core.agda | |
| │ │ ├── Core.agdai | |
| │ │ ├── LeftOrder.agda | |
| │ │ ├── LeftOrder.agdai | |
| │ │ ├── Pointwise.agda | |
| │ │ └── Pointwise.agdai | |
| │ ├── Sum.agda | |
| │ ├── Sum.agdai | |
| │ ├── Table | |
| │ │ ├── Base.agda | |
| │ │ ├── Base.agdai | |
| │ │ ├── Properties.agda | |
| │ │ ├── Properties.agdai | |
| │ │ └── Relation | |
| │ │ ├── Equality.agda | |
| │ │ └── Equality.agdai | |
| │ ├── Table.agda | |
| │ ├── Table.agdai | |
| │ ├── These | |
| │ │ └── Categorical | |
| │ │ ├── Left | |
| │ │ │ ├── Base.agda | |
| │ │ │ └── Base.agdai | |
| │ │ ├── Left.agda | |
| │ │ ├── Left.agdai | |
| │ │ ├── Right | |
| │ │ │ ├── Base.agda | |
| │ │ │ └── Base.agdai | |
| │ │ ├── Right.agda | |
| │ │ └── Right.agdai | |
| │ ├── These.agda | |
| │ ├── These.agdai | |
| │ ├── Unit | |
| │ │ ├── Base.agda | |
| │ │ ├── Base.agdai | |
| │ │ ├── NonEta.agda | |
| │ │ └── NonEta.agdai | |
| │ ├── Unit.agda | |
| │ ├── Unit.agdai | |
| │ ├── Vec | |
| │ │ ├── All | |
| │ │ │ ├── Properties.agda | |
| │ │ │ └── Properties.agdai | |
| │ │ ├── All.agda | |
| │ │ ├── All.agdai | |
| │ │ ├── Any.agda | |
| │ │ ├── Any.agdai | |
| │ │ ├── Categorical.agda | |
| │ │ ├── Categorical.agdai | |
| │ │ ├── Membership | |
| │ │ │ ├── Propositional | |
| │ │ │ │ ├── Properties.agda | |
| │ │ │ │ └── Properties.agdai | |
| │ │ │ ├── Propositional.agda | |
| │ │ │ └── Propositional.agdai | |
| │ │ ├── N-ary.agda | |
| │ │ ├── N-ary.agdai | |
| │ │ ├── Properties.agda | |
| │ │ ├── Properties.agdai | |
| │ │ └── Relation | |
| │ │ ├── Equality | |
| │ │ │ ├── DecPropositional.agda | |
| │ │ │ ├── DecPropositional.agdai | |
| │ │ │ ├── DecSetoid.agda | |
| │ │ │ ├── DecSetoid.agdai | |
| │ │ │ ├── Propositional.agda | |
| │ │ │ ├── Propositional.agdai | |
| │ │ │ ├── Setoid.agda | |
| │ │ │ └── Setoid.agdai | |
| │ │ └── Pointwise | |
| │ │ ├── Extensional.agda | |
| │ │ ├── Extensional.agdai | |
| │ │ ├── Inductive.agda | |
| │ │ └── Inductive.agdai | |
| │ ├── Vec.agda | |
| │ ├── Vec.agdai | |
| │ ├── W | |
| │ │ ├── Indexed.agda | |
| │ │ └── Indexed.agdai | |
| │ ├── W.agda | |
| │ ├── W.agdai | |
| │ ├── Word | |
| │ │ ├── Unsafe.agda | |
| │ │ └── Unsafe.agdai | |
| │ ├── Word.agda | |
| │ └── Word.agdai | |
| ├── Foreign | |
| │ ├── Haskell.agda | |
| │ └── Haskell.agdai | |
| ├── Function | |
| │ ├── Bijection.agda | |
| │ ├── Bijection.agdai | |
| │ ├── Equality.agda | |
| │ ├── Equality.agdai | |
| │ ├── Equivalence.agda | |
| │ ├── Equivalence.agdai | |
| │ ├── Identity | |
| │ │ ├── Categorical.agda | |
| │ │ └── Categorical.agdai | |
| │ ├── Injection.agda | |
| │ ├── Injection.agdai | |
| │ ├── Inverse.agda | |
| │ ├── Inverse.agdai | |
| │ ├── LeftInverse.agda | |
| │ ├── LeftInverse.agdai | |
| │ ├── Reasoning.agda | |
| │ ├── Reasoning.agdai | |
| │ ├── Related | |
| │ │ ├── TypeIsomorphisms | |
| │ │ │ ├── Solver.agda | |
| │ │ │ └── Solver.agdai | |
| │ │ ├── TypeIsomorphisms.agda | |
| │ │ └── TypeIsomorphisms.agdai | |
| │ ├── Related.agda | |
| │ ├── Related.agdai | |
| │ ├── Surjection.agda | |
| │ └── Surjection.agdai | |
| ├── Function.agda | |
| ├── Function.agdai | |
| ├── Induction | |
| │ ├── Lexicographic.agda | |
| │ ├── Lexicographic.agdai | |
| │ ├── Nat.agda | |
| │ ├── Nat.agdai | |
| │ ├── WellFounded.agda | |
| │ └── WellFounded.agdai | |
| ├── Induction.agda | |
| ├── Induction.agdai | |
| ├── IO | |
| │ ├── Primitive.agda | |
| │ └── Primitive.agdai | |
| ├── IO.agda | |
| ├── IO.agdai | |
| ├── Level | |
| │ ├── Literals.agda | |
| │ └── Literals.agdai | |
| ├── Level.agda | |
| ├── Level.agdai | |
| ├── Record.agda | |
| ├── Record.agdai | |
| ├── Reflection.agda | |
| ├── Reflection.agdai | |
| ├── Relation | |
| │ ├── Binary | |
| │ │ ├── Consequences.agda | |
| │ │ ├── Consequences.agdai | |
| │ │ ├── Construct | |
| │ │ │ ├── Always.agda | |
| │ │ │ ├── Always.agdai | |
| │ │ │ ├── Closure | |
| │ │ │ │ ├── Equivalence.agda | |
| │ │ │ │ ├── Equivalence.agdai | |
| │ │ │ │ ├── Reflexive.agda | |
| │ │ │ │ ├── Reflexive.agdai | |
| │ │ │ │ ├── ReflexiveTransitive | |
| │ │ │ │ │ ├── Properties.agda | |
| │ │ │ │ │ └── Properties.agdai | |
| │ │ │ │ ├── ReflexiveTransitive.agda | |
| │ │ │ │ ├── ReflexiveTransitive.agdai | |
| │ │ │ │ ├── Symmetric.agda | |
| │ │ │ │ ├── Symmetric.agdai | |
| │ │ │ │ ├── Transitive.agda | |
| │ │ │ │ └── Transitive.agdai | |
| │ │ │ ├── Constant.agda | |
| │ │ │ ├── Constant.agdai | |
| │ │ │ ├── Converse.agda | |
| │ │ │ ├── Converse.agdai | |
| │ │ │ ├── Flip.agda | |
| │ │ │ ├── Flip.agdai | |
| │ │ │ ├── FromPred.agda | |
| │ │ │ ├── FromPred.agdai | |
| │ │ │ ├── FromRel.agda | |
| │ │ │ ├── FromRel.agdai | |
| │ │ │ ├── Never.agda | |
| │ │ │ ├── Never.agdai | |
| │ │ │ ├── NonStrictToStrict.agda | |
| │ │ │ ├── NonStrictToStrict.agdai | |
| │ │ │ ├── On.agda | |
| │ │ │ ├── On.agdai | |
| │ │ │ ├── StrictToNonStrict.agda | |
| │ │ │ └── StrictToNonStrict.agdai | |
| │ │ ├── Core.agda | |
| │ │ ├── Core.agdai | |
| │ │ ├── EqReasoning.agda | |
| │ │ ├── EqReasoning.agdai | |
| │ │ ├── EquivalenceClosure.agda | |
| │ │ ├── EquivalenceClosure.agdai | |
| │ │ ├── HeterogeneousEquality | |
| │ │ │ ├── Core.agda | |
| │ │ │ ├── Core.agdai | |
| │ │ │ ├── Quotients | |
| │ │ │ │ ├── Examples.agda | |
| │ │ │ │ └── Examples.agdai | |
| │ │ │ ├── Quotients.agda | |
| │ │ │ └── Quotients.agdai | |
| │ │ ├── HeterogeneousEquality.agda | |
| │ │ ├── HeterogeneousEquality.agdai | |
| │ │ ├── Indexed | |
| │ │ │ ├── Heterogeneous | |
| │ │ │ │ ├── Construct | |
| │ │ │ │ │ ├── At.agda | |
| │ │ │ │ │ ├── At.agdai | |
| │ │ │ │ │ ├── Trivial.agda | |
| │ │ │ │ │ └── Trivial.agdai | |
| │ │ │ │ ├── Core.agda | |
| │ │ │ │ └── Core.agdai | |
| │ │ │ ├── Heterogeneous.agda | |
| │ │ │ ├── Heterogeneous.agdai | |
| │ │ │ ├── Homogeneous | |
| │ │ │ │ ├── Core.agda | |
| │ │ │ │ └── Core.agdai | |
| │ │ │ ├── Homogeneous.agda | |
| │ │ │ └── Homogeneous.agdai | |
| │ │ ├── Lattice.agda | |
| │ │ ├── Lattice.agdai | |
| │ │ ├── List | |
| │ │ │ ├── NonStrictLex.agda | |
| │ │ │ ├── NonStrictLex.agdai | |
| │ │ │ ├── Pointwise.agda | |
| │ │ │ ├── Pointwise.agdai | |
| │ │ │ ├── StrictLex.agda | |
| │ │ │ └── StrictLex.agdai | |
| │ │ ├── OrderMorphism.agda | |
| │ │ ├── OrderMorphism.agdai | |
| │ │ ├── PartialOrderReasoning.agda | |
| │ │ ├── PartialOrderReasoning.agdai | |
| │ │ ├── PreorderReasoning.agda | |
| │ │ ├── PreorderReasoning.agdai | |
| │ │ ├── Product | |
| │ │ │ ├── NonStrictLex.agda | |
| │ │ │ ├── NonStrictLex.agdai | |
| │ │ │ ├── Pointwise.agda | |
| │ │ │ ├── Pointwise.agdai | |
| │ │ │ ├── StrictLex.agda | |
| │ │ │ └── StrictLex.agdai | |
| │ │ ├── Properties | |
| │ │ │ ├── BoundedJoinSemilattice.agda | |
| │ │ │ ├── BoundedJoinSemilattice.agdai | |
| │ │ │ ├── BoundedMeetSemilattice.agda | |
| │ │ │ ├── BoundedMeetSemilattice.agdai | |
| │ │ │ ├── DecTotalOrder.agda | |
| │ │ │ ├── DecTotalOrder.agdai | |
| │ │ │ ├── DistributiveLattice.agda | |
| │ │ │ ├── DistributiveLattice.agdai | |
| │ │ │ ├── HeytingAlgebra.agda | |
| │ │ │ ├── HeytingAlgebra.agdai | |
| │ │ │ ├── JoinSemilattice.agda | |
| │ │ │ ├── JoinSemilattice.agdai | |
| │ │ │ ├── Lattice.agda | |
| │ │ │ ├── Lattice.agdai | |
| │ │ │ ├── MeetSemilattice.agda | |
| │ │ │ ├── MeetSemilattice.agdai | |
| │ │ │ ├── Poset.agda | |
| │ │ │ ├── Poset.agdai | |
| │ │ │ ├── Preorder.agda | |
| │ │ │ ├── Preorder.agdai | |
| │ │ │ ├── StrictPartialOrder.agda | |
| │ │ │ ├── StrictPartialOrder.agdai | |
| │ │ │ ├── StrictTotalOrder.agda | |
| │ │ │ ├── StrictTotalOrder.agdai | |
| │ │ │ ├── TotalOrder.agda | |
| │ │ │ └── TotalOrder.agdai | |
| │ │ ├── PropositionalEquality | |
| │ │ │ ├── Core.agda | |
| │ │ │ ├── Core.agdai | |
| │ │ │ ├── TrustMe.agda | |
| │ │ │ └── TrustMe.agdai | |
| │ │ ├── PropositionalEquality.agda | |
| │ │ ├── PropositionalEquality.agdai | |
| │ │ ├── Reflection.agda | |
| │ │ ├── Reflection.agdai | |
| │ │ ├── SetoidReasoning.agda | |
| │ │ ├── SetoidReasoning.agdai | |
| │ │ ├── Sigma | |
| │ │ │ ├── Pointwise.agda | |
| │ │ │ └── Pointwise.agdai | |
| │ │ ├── StrictPartialOrderReasoning.agda | |
| │ │ ├── StrictPartialOrderReasoning.agdai | |
| │ │ ├── Sum.agda | |
| │ │ ├── Sum.agdai | |
| │ │ ├── SymmetricClosure.agda | |
| │ │ ├── SymmetricClosure.agdai | |
| │ │ └── Vec | |
| │ │ ├── Pointwise.agda | |
| │ │ └── Pointwise.agdai | |
| │ ├── Binary.agda | |
| │ ├── Binary.agdai | |
| │ ├── Nullary | |
| │ │ ├── Decidable.agda | |
| │ │ ├── Decidable.agdai | |
| │ │ ├── Implication.agda | |
| │ │ ├── Implication.agdai | |
| │ │ ├── Negation.agda | |
| │ │ ├── Negation.agdai | |
| │ │ ├── Product.agda | |
| │ │ ├── Product.agdai | |
| │ │ ├── Sum.agda | |
| │ │ ├── Sum.agdai | |
| │ │ ├── Universe.agda | |
| │ │ └── Universe.agdai | |
| │ ├── Nullary.agda | |
| │ ├── Nullary.agdai | |
| │ ├── Unary | |
| │ │ ├── Closure | |
| │ │ │ ├── Base.agda | |
| │ │ │ ├── Base.agdai | |
| │ │ │ ├── Preorder.agda | |
| │ │ │ ├── Preorder.agdai | |
| │ │ │ ├── StrictPartialOrder.agda | |
| │ │ │ └── StrictPartialOrder.agdai | |
| │ │ ├── Indexed.agda | |
| │ │ ├── Indexed.agdai | |
| │ │ ├── PredicateTransformer.agda | |
| │ │ ├── PredicateTransformer.agdai | |
| │ │ ├── Properties.agda | |
| │ │ └── Properties.agdai | |
| │ ├── Unary.agda | |
| │ └── Unary.agdai | |
| ├── Size.agda | |
| ├── Size.agdai | |
| ├── Strict.agda | |
| ├── Strict.agdai | |
| ├── Universe.agda | |
| └── Universe.agdai | |
| 127 directories, 748 files |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment