coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] small scripts of ssreflect?

From: Thery Laurent <thery AT ns.di.univaq.it>
To: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] small scripts of ssreflect?
Date: Fri, 25 Apr 2008 11:31:29 +0200 (CEST)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Could someone refer me to or kindly give me introductory,
i.e. not too complex or too large, scripts benefiting from ssreflect?

Personnally, I've learned ssreflect replaying the scripts of the
libraries (subdirectory theories).
The two files about arithmetic (ssrnat.v and div.v) are my favorites. The fact that most of these proofs are one-liners
show the conciseness you can achieve with ssreflect.

--
Laurent

[Coq-Club] small scripts of ssreflect?, Keiko Nakata
- Re: [Coq-Club] small scripts of ssreflect?, Thery Laurent
- Re: [Coq-Club] small scripts of ssreflect?, Thery Laurent