diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-02 20:27:45 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-02 20:27:45 +0000 |
commit | 465eb43ae41bae4c4ee9d5a6e7b5fe95768fb92e (patch) | |
tree | 7cd84f89f63eaff3d1aec9bf4fa5b05b6925ee3c /theories/Strings | |
parent | 64f0c19dc57a4cba968115a9f8e9ffd128580fad (diff) |
Initial implementation of a new command to define (dependent) functions by
equations.
It is essentially an implementation of the "Eliminating Dependent
Pattern-Matching" paper by Goguen, McBride and McKinna, relying on the
new dependent eliminations tactics. The bulk is in
contrib/subtac/equations.ml4. It implements a tree splitting on a set of
clauses and the generation of a corresponding proof term along with some
obligations at each splitting node. The obligations are solved by
driving the dependent elimination tactic and you get a complete proof
term at the end with the code given by the equations at the right spots,
the rest of the cases being pruned automatically.
Does not support recursion yet, a file with examples is in the
test-suite. With recursion, it would be similar to Agda 2's pattern
matching, except it won't reduce in Coq due to JMeq's/K.
Incidentally, the simplification tactics after dependent elimination
have been improved, resulting in a clearer and more space efficient
implementation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11352 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Strings')
0 files changed, 0 insertions, 0 deletions