Télescopes généralisés en Coq.
Loic Pottier, janvier 1999
Définition
des télescopes et de leurs éléments, fonctions de
manipulation.
Inclusion
de télescopes, coercions entre leurs éléments.
Exemples,
où comment récupérer avec les télescopes ce
que l'on peut faire en Coq avec les Records et les coercions.
Amalgames
de télescopes avec une définition plus faible de l'inclusion.
Tout ça est expérimental...
