Up till date I have submitted two contributions for Coq:
- A serious one on linear algebra, LinAlg.tar.gz which extends Loic Pottier's algebra contribution
- And a slightly less serious one: Coqoban.tar.gz, which implements the game of Sokoban in Coq.

---

The following Coq files are included in the two contributions:
Coqoban/Coqoban_engine.v
Coqoban/Coqoban_levels.v


LinAlg/first_page.v

LinAlg/examples/antisymmetric_matrices.v
LinAlg/examples/infinite_sequences.v
LinAlg/examples/Matrices.v
LinAlg/examples/Matrix_multiplication.v
LinAlg/examples/symmetric_matrices.v
LinAlg/examples/trivial_spaces.v
LinAlg/examples/up_lo_triang_mat.v
LinAlg/examples/vecspace_Fn.v
LinAlg/examples/vecspace_functionspace.v
LinAlg/examples/vecspace_Mmn.v

LinAlg/extras/before_after.v
LinAlg/extras/Equality_structures.v
LinAlg/extras/finite_misc.v
LinAlg/extras/Inter_intersection.v
LinAlg/extras/matrix_algebra.v
LinAlg/extras/Matrix_related_defs.v
LinAlg/extras/restrict.v
LinAlg/extras/ring_module.v

LinAlg/LinAlg/algebraic_span_facts.v
LinAlg/LinAlg/alt_build_vecsp.v
LinAlg/LinAlg/bases.v
LinAlg/LinAlg/bases_finite_dim.v
LinAlg/LinAlg/bases_from_generating_sets.v
LinAlg/LinAlg/direct_sum.v
LinAlg/LinAlg/lin_comb_facts.v
LinAlg/LinAlg/lin_combinations.v
LinAlg/LinAlg/lin_dep_facts.v
LinAlg/LinAlg/lin_dependence.v
LinAlg/LinAlg/Lin_trafos.v
LinAlg/LinAlg/Linear_Algebra_by_Friedberg_Insel_Spence.v
LinAlg/LinAlg/maxlinindepsubsets.v
LinAlg/LinAlg/replacement_corollaries.v
LinAlg/LinAlg/replacement_theorem.v
LinAlg/LinAlg/spans.v
LinAlg/LinAlg/subspace_bases.v
LinAlg/LinAlg/subspace_dim.v
LinAlg/LinAlg/subspaces.v
LinAlg/LinAlg/vecspaces_verybasic.v

LinAlg/support/algebra_omissions.v
LinAlg/support/arb_intersections.v
LinAlg/support/cast_between_subsets.v
LinAlg/support/cast_seq_lengths.v
LinAlg/support/concat.v
LinAlg/support/concat_facts.v
LinAlg/support/conshdtl.v
LinAlg/support/const.v
LinAlg/support/counting_elements.v
LinAlg/support/distinct.v
LinAlg/support/distinct_facts.v
LinAlg/support/distribution_lemmas.v
LinAlg/support/empty.v
LinAlg/support/equal_syntax.v
LinAlg/support/finite.v
LinAlg/support/finite_subsets.v
LinAlg/support/has_n_elements.v
LinAlg/support/Map2.v
LinAlg/support/Map_embed.v
LinAlg/support/modify_seq.v
LinAlg/support/more_syntax.v
LinAlg/support/mult_by_scalars.v
LinAlg/support/omit.v
LinAlg/support/omit_facts.v
LinAlg/support/pointwise.v
LinAlg/support/random_facts.v
LinAlg/support/seq_equality.v
LinAlg/support/seq_equality_facts.v
LinAlg/support/seq_set.v
LinAlg/support/seq_set_facts.v
LinAlg/support/seq_set_seq.v
LinAlg/support/subseqs.v
LinAlg/support/sums.v
LinAlg/support/sums2.v


The linear algebra package comes with an installation script that also generates PostScript documentation if you have coqdoc installed. Otherwise, Linear_Algebra_by_Friedberg_Insel_Spence.v is your best place to begin.

This page was generated at the following date/time: Fri Sep 19 16:38:19 MEST 2003