Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Equations command in trunk

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Equations command in trunk


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page