[clean-list] Sparkle manual

[Maarten de Mol]

Hello Dmitry,

> Hi, All!
> 
> Is there any manual on using Sparkle besides "Theorem proving for
> functional programmers" paper avaliable? What is the syntax used for
> entering new thorems?

Unfortunately, there is no manual for Sparkle available. The only
other very limited source of information is the website at
http:\\www.cs.kun.nl\Sparkle.

The syntax for entering new theorems is as follows:
-----------------------------------------------------
EQUALITY:                  "E = E"
NEGATION:                  "~P"
CONJUNCTION:               "P /\ Q"
DISJUNCTION:               "P \/ Q"
IMPLICATION:               "P -> Q" or "P => Q"
EQUIVALENCE:               "P <-> Q" or "P <=> Q"
UNIVERSAL QUANTIFICATION:  "[x::T] P"
EXISTENTIAL QUANTIFICATION:"{x::T} P"
-----------------------------------------------------
Notes:
  * The types in the quantifications may be omitted. (Sparkle
    tries to derive types for variables automatically, but this
    might fail in some case, such as overloading).
  * Universal quantifications may be omitted completed. (Sparkle
    automatically adds universal quantifications for all free
    variables it finds)
 
> BTW What is current status of Sparkle? Is there any ongoing development?
> Last 0.0.3a from Jan 2002 seems a bit outdated.

Development on Sparkle has effectively been frozen since January 2002, when
I started tackling remaining theoretical issues and started writing my
PhD-thesis. Hopefully, when funding can be arranged, work on Sparkle can
be continued this summer.

> Best regards,
> Dmitry Malenko.

Greetings,
Maarten de Mol