déduction de calcul
Contexte
Pour une mathématique lazi, on veut définir un type particulier : une déduction prenant en argument une formule x (dans le domaine des formules pouvant être calculées par cette déduction) et déduit une égalité où x est le membre de gauche.
Définition de "type (ou règle) de déduction de calcul"
Soit M une mathématique lazi et td un type de déduction de M. On dit que td est un type de déduction de calcul si td prend en argument une formule x et si la vérité déduite est de la forme x = y.
Définition de "déduction de calcul"
On dit que d est une déduction de calcul si son type est un type de déduction de calcul.