Library for partial functions

[Andreas Abel]

Has anyone developed a library for partial functions in the style of

   parfun A B := Sigma P : A -> Prop. {x : A | P x} -> B

Stuff like currying, uncurrying, dependent partial functions, theorems  
about partial functions...

Cheers,
Andreas

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: [phone]



--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club