Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] math-comp examples, import warning

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] math-comp examples, import warning


Chronological Thread 
  • From: Enrico Tassi <>
  • To:
  • Subject: Re: [ssreflect] math-comp examples, import warning
  • Date: Thu, 19 May 2016 13:50:56 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=None ; spf=None
  • Ironport-phdr: 9a23:v/iP/BwtIY49rlHXCy+O+j09IxM/srCxBDY+r6Qd0e4eIJqq85mqBkHD//Il1AaPBtWKrakewLaM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt+U1J78i7r60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884motVbS6j0e6kzUZRdFy5jMmYv5cSttB/ZTALJ6GFPfH8Rl09lBRLE5xayYp7qqSqy4ud7wiiROovqRKsvWByj6b1qQVnmknFUZHYC7GjLh5ko3+pgqxW7qkknzg==
On Thu, May 19, 2016 at 09:06:50AM +0000, Georges Gonthier wrote:
> Hello and welcome!
>
> For initial material, you may want to look into the Advanced Coq
> Winter
> School<https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016/>
> course material; lesson 7 covers the matrix library (but you’ll need
> much of the earlier material as well).

For convenience, a short tutorial (cited in lesson 7) is available here:
http://ssr.msr-inria.inria.fr/doc/tutorial-itp13/
and a quite embarrassing video (I hate my accent) of the tutorial is here:

http://videos.rennes.inria.fr/Conference-ITP/indexAssiaMahboubiEnricoTassi.html
The demo (about matrix) starts at minute 25.

Best,
--
Enrico Tassi

Archive powered by MHonArc 2.6.18.

Top of Page