Égalité dans Dedukti Le code ci-dessous est la définition de l'égalité qu'on a proposée dans la section 5.1.2. On y démontre la symétrie et la transitivité de cette opération à l ,
Dedukti : a logical framework based on the ??-calculus modulo theory ,
Term Rewriting and All That, 1998. ,
The Why3 Platform, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00822856
The formulae-as-types notions of construction, Essays on Combinatory Logic, Lambda-Calculus, and Formalism, pp.479-490, 1980. ,