Skip to content
This repository


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

Sean Wilson's rippling plugin.

branch: trunk

Fetching latest commit…


Cannot retrieve the latest commit at this time

Octocat-spinner-32 LICENSE
Octocat-spinner-32 Make
Octocat-spinner-32 README
Octocat-spinner-32 Rippling.v
Octocat-spinner-32 demo.v
Octocat-spinner-32 discover.v
Octocat-spinner-32 general_tactics.v
Octocat-spinner-32 rippling_plugin.ml4
Octocat-spinner-32 tools.v
Inductive proof automation for Coq
by Sean Wilson

This package contains an inductive proof automation plugin for Coq. This automation
includes a rippling tactic, generalisation heuristics and a counterexample finder tool.
This file explains how to compile the code and run the demo file (see theory/demo.v),
which includes many examples of theorems that can be automated. See here for documentation
about how the automation works:

These tactics are still in development. The code and the installation process should
hopefully be simplified in the future.

Note that this code has only been tested under Linux so far.

Something went wrong with that request. Please try again.