Sparkle

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Sparkle is a proof tool specially constructed for Clean. The tool knows the Clean syntax and semantics. It comes with a rich set of proof tactics and a powerful hint mechanism to aid the user in proving properties of Clean programs.