← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

« back to all changes in this revision

Viewing changes to src/Data/Fin/Substitution/Lemmas.agda

Committer: Package Import Robot
Author(s): Iain Lane
Date: 2011-11-29 17:00:35 UTC
mfrom: (2.1.4 sid)
Revision ID: package-import@ubuntu.com-20111129170035-be8cbok8ojft5tjl

Tags: 0.6~darcs20111129t1640-1

* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
+ Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

files added:
README/AVL.agda

README/Case.agda

README/Record.agda

debian/source

debian/source/format

ffi

ffi/Data

ffi/Data/FFI.hs

ffi/IO

ffi/IO/FFI.hs

ffi/Setup.hs

ffi/agda-lib-ffi.cabal

src/Data/Nat/Primality.agda

src/Data/Unit

src/Data/Unit/Core.agda

src/Function/Related

src/Function/Related.agda

src/Function/Related/TypeIsomorphisms.agda

src/Level

src/Record.agda

src/Relation/Binary/HeterogeneousEquality

src/Relation/Binary/HeterogeneousEquality/Core.agda

files removed:
src/Data/Context.agda

src/Function/Inverse

src/Function/Inverse/TypeIsomorphisms.agda

files modified:
Everything.agda

GNUmakefile

GenerateEverything.hs

Header

LICENCE

README.agda

README.txt

README/Nat.agda

debian/agda-stdlib.install *

debian/changelog

debian/control

lib.cabal

src/Algebra.agda

src/Algebra/FunctionProperties.agda

src/Algebra/FunctionProperties/Core.agda

src/Algebra/Morphism.agda

src/Algebra/Operations.agda

src/Algebra/Props/AbelianGroup.agda

src/Algebra/Props/BooleanAlgebra.agda

src/Algebra/Props/BooleanAlgebra/Expression.agda

src/Algebra/Props/DistributiveLattice.agda

src/Algebra/Props/Group.agda

src/Algebra/Props/Lattice.agda

src/Algebra/Props/Ring.agda

src/Algebra/RingSolver.agda

src/Algebra/RingSolver/AlmostCommutativeRing.agda

src/Algebra/RingSolver/Lemmas.agda

src/Algebra/RingSolver/Simple.agda

src/Algebra/Structures.agda

src/Category/Applicative.agda

src/Category/Applicative/Indexed.agda

src/Category/Functor.agda

src/Category/Monad.agda

src/Category/Monad/Continuation.agda

src/Category/Monad/Identity.agda

src/Category/Monad/Indexed.agda

src/Category/Monad/Partiality.agda

src/Category/Monad/State.agda

src/Coinduction.agda

src/Data/AVL.agda

src/Data/AVL/IndexedMap.agda

src/Data/AVL/Sets.agda

src/Data/Bin.agda

src/Data/Bool.agda

src/Data/Bool/Properties.agda

src/Data/Bool/Show.agda

src/Data/BoundedVec.agda

src/Data/BoundedVec/Inefficient.agda

src/Data/Char.agda

src/Data/Cofin.agda

src/Data/Colist.agda

src/Data/Conat.agda

src/Data/Container.agda

src/Data/Container/Any.agda

src/Data/Container/Combinator.agda

src/Data/Covec.agda

src/Data/DifferenceList.agda

src/Data/DifferenceNat.agda

src/Data/DifferenceVec.agda

src/Data/Digit.agda

src/Data/Empty.agda

src/Data/Fin.agda

src/Data/Fin/Dec.agda

src/Data/Fin/Props.agda

src/Data/Fin/Subset.agda

src/Data/Fin/Subset/Props.agda

src/Data/Fin/Substitution.agda

src/Data/Fin/Substitution/Example.agda

src/Data/Fin/Substitution/Lemmas.agda

src/Data/Fin/Substitution/List.agda

src/Data/Graph/Acyclic.agda

src/Data/Integer.agda

src/Data/Integer/Divisibility.agda

src/Data/Integer/Properties.agda

src/Data/List.agda

src/Data/List/All.agda

src/Data/List/All/Properties.agda

src/Data/List/Any.agda

src/Data/List/Any/BagAndSetEquality.agda

src/Data/List/Any/Membership.agda

src/Data/List/Any/Properties.agda

src/Data/List/Countdown.agda

src/Data/List/NonEmpty.agda

src/Data/List/NonEmpty/Properties.agda

src/Data/List/Properties.agda

src/Data/List/Reverse.agda

src/Data/Maybe.agda

src/Data/Maybe/Core.agda

src/Data/Nat.agda

src/Data/Nat/Coprimality.agda

src/Data/Nat/DivMod.agda

src/Data/Nat/Divisibility.agda

src/Data/Nat/GCD.agda

src/Data/Nat/GCD/Lemmas.agda

src/Data/Nat/InfinitelyOften.agda

src/Data/Nat/LCM.agda

src/Data/Nat/Properties.agda

src/Data/Nat/Show.agda

src/Data/Plus.agda

src/Data/Product.agda

src/Data/Product/N-ary.agda

src/Data/Rational.agda

src/Data/ReflexiveClosure.agda

src/Data/Sign.agda

src/Data/Sign/Properties.agda

src/Data/Star.agda

src/Data/Star/BoundedVec.agda

src/Data/Star/Decoration.agda

src/Data/Star/Environment.agda

src/Data/Star/Fin.agda

src/Data/Star/List.agda

src/Data/Star/Nat.agda

src/Data/Star/Pointer.agda

src/Data/Star/Properties.agda

src/Data/Star/Vec.agda

src/Data/Stream.agda

src/Data/String.agda

src/Data/Sum.agda

src/Data/Unit.agda

src/Data/Vec.agda

src/Data/Vec/Equality.agda

src/Data/Vec/N-ary.agda

src/Data/Vec/Properties.agda

src/Data/W.agda

src/Foreign/Haskell.agda

src/Function.agda

src/Function/Bijection.agda

src/Function/Equality.agda

src/Function/Equivalence.agda

src/Function/Injection.agda

src/Function/Inverse.agda

src/Function/LeftInverse.agda

src/Function/Surjection.agda

src/IO.agda

src/IO/Primitive.agda

src/Induction.agda

src/Induction/Lexicographic.agda

src/Induction/Nat.agda

src/Induction/WellFounded.agda

src/Level.agda

src/Reflection.agda

src/Relation/Binary.agda

src/Relation/Binary/Consequences.agda

src/Relation/Binary/Consequences/Core.agda

src/Relation/Binary/Core.agda

src/Relation/Binary/EqReasoning.agda

src/Relation/Binary/Flip.agda

src/Relation/Binary/HeterogeneousEquality.agda

src/Relation/Binary/Indexed.agda

src/Relation/Binary/Indexed/Core.agda

src/Relation/Binary/InducedPreorders.agda

src/Relation/Binary/List/NonStrictLex.agda

src/Relation/Binary/List/Pointwise.agda

src/Relation/Binary/List/StrictLex.agda

src/Relation/Binary/NonStrictToStrict.agda

src/Relation/Binary/On.agda

src/Relation/Binary/OrderMorphism.agda

src/Relation/Binary/PartialOrderReasoning.agda

src/Relation/Binary/PreorderReasoning.agda

src/Relation/Binary/Product/NonStrictLex.agda

src/Relation/Binary/Product/Pointwise.agda

src/Relation/Binary/Product/StrictLex.agda

src/Relation/Binary/PropositionalEquality.agda

src/Relation/Binary/PropositionalEquality/Core.agda

src/Relation/Binary/PropositionalEquality/TrustMe.agda

src/Relation/Binary/Props/DecTotalOrder.agda

src/Relation/Binary/Props/Poset.agda

src/Relation/Binary/Props/Preorder.agda

src/Relation/Binary/Props/StrictPartialOrder.agda

src/Relation/Binary/Props/StrictTotalOrder.agda

src/Relation/Binary/Props/TotalOrder.agda

src/Relation/Binary/Reflection.agda

src/Relation/Binary/Sigma/Pointwise.agda

src/Relation/Binary/Simple.agda

src/Relation/Binary/StrictPartialOrderReasoning.agda

src/Relation/Binary/StrictToNonStrict.agda

src/Relation/Binary/Sum.agda

src/Relation/Binary/Vec/Pointwise.agda

src/Relation/Nullary.agda

src/Relation/Nullary/Core.agda

src/Relation/Nullary/Decidable.agda

src/Relation/Nullary/Negation.agda

src/Relation/Nullary/Product.agda

src/Relation/Nullary/Sum.agda

src/Relation/Nullary/Universe.agda

src/Relation/Unary.agda

src/Size.agda

src/Universe.agda

Show diffs side-by-side

added added

removed removed

src/Data/Fin/Substitution/Lemmas.agda

1

1

------------------------------------------------------------------------

2

-- The Agda standard library

3

--

2

4

-- Substitution lemmas

3

5

------------------------------------------------------------------------

4

6

Older »