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 /Makefile.common | |
| 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 'Makefile.common')
| -rw-r--r-- | Makefile.common | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index e323e2d9b..08ae6f835 100644 --- a/Makefile.common +++ b/Makefile.common @@ -309,8 +309,8 @@ SUBTACCMO:=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \ contrib/subtac/subtac_obligations.cmo contrib/subtac/subtac_cases.cmo \ contrib/subtac/subtac_pretyping_F.cmo contrib/subtac/subtac_pretyping.cmo \ contrib/subtac/subtac_command.cmo contrib/subtac/subtac_classes.cmo \ - contrib/subtac/subtac.cmo \ - contrib/subtac/g_subtac.cmo + contrib/subtac/subtac.cmo contrib/subtac/g_subtac.cmo \ + contrib/subtac/equations.cmo RTAUTOCMO:=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \ contrib/rtauto/g_rtauto.cmo |