coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <sozeau AT lri.fr>
- To: Robin Green <greenrd AT greenrd.org>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Equations command in trunk
- Date: Tue, 7 Oct 2008 21:34:35 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Le 7 oct. 08 à 13:42, Robin Green a écrit :
Can anyone tell me what the apparently undocumented Equations command is
for, in the trunk version? It seems like it might be useful for my
development.
Hi,
this is a very experimental, proof of concept, unfinished piece of work by me, that
would maybe better live in another branch. Let's spoil it though: it's a primitive
implementation of a dependent pattern matching compiler (from equations to
Coq case-expressions, plus K when needed). IT DOES NOT WORK yet except for simple examples, but it will get properly documented when it does.
-- Matthieu
- [Coq-Club] Equations command in trunk, Robin Green
- Re: [Coq-Club] Equations command in trunk, Matthieu Sozeau
Archive powered by MhonArc 2.6.16.