Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] problem with dependant types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] problem with dependant types


chronological Thread 
  • From: Nicolas Magaud <nmagaud AT cse.unsw.edu.au>
  • To: casteran AT labri.fr
  • Cc: june andronick <jandronick AT axalto.com>, coq-club AT pauillac.inria.fr, conor AT cs.rhul.ac.uk
  • Subject: Re: [Coq-Club] problem with dependant types
  • Date: Mon, 15 Nov 2004 11:39:33 +1100
  • Comments: In-reply-to casteran AT labri.fr message dated "Fri, 12 Nov 2004 09:15:20 +0100."
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi folks,

You may be interested in the formalisation of square matrices I did a while 
ago:

http://www.cse.unsw.edu.au/~nmagaud/Coq/Matrices/

It deals with dependent types (vectors and matrices as vectors of vectors), 
their properties
and proofs of the very useful lemmas like vector_double_rec to make proofs 
easier.

Cheers,
Nicolas

--
Nicolas Magaud                            
mailto:nmagaud AT cse.unsw.edu.au
School of Computer Science & Eng.                   ph:  +61 2 9385 7369
The University of New South Wales                   fax: +61 2 9385 5995
Sydney NSW 2052, Australia           http://www.cse.unsw.edu.au/~nmagaud






Archive powered by MhonArc 2.6.16.

Top of Page