coq-club AT inria.fr

Subject: The Coq mailing list

List archive

delta-reduction and Cases elimination

From: Boite Olivier <boite AT cnam.fr>
To: coq-club AT pauillac.inria.fr
Subject: delta-reduction and Cases elimination
Date: Mon, 02 Jul 2001 12:11:22 +0200

hello,

In the following example,

A : Set
B : Set
a : A
f : A->B
============================
   f
    =([a':A]
       Cases (eq_A_dec a a') of
         (left _) => (f a)
       | (right _) => (f a')
       end)

where eq_A_dec is (x,y:A){x=y}+{~x=y},

I'd like to perform a delta-reduction, but a'
would be free in the context.
How to eliminate the Cases in the abstraction ?

Best regards

-- 
Olivier Boite                             | (33)1 69 36 73 23
CNAM  Departement d'informatique          | boite AT cnam.fr
CEDRIC-IIE, 18 allee J.Rostand 91025 EVRY |

delta-reduction and Cases elimination, Boite Olivier