Lazi

Extension fonctions

Objet

Étude

L'extension doit-elle ajouter une règle pour traduire la notation en sa forme "distribute" ?
C'est le cas actuellement dans l'extension définie 06-function.ext-nota.lazi .
Mais que devient cette traduction avec setF ?

Extension du type des formules

Nouvelles règles de déduction

Règle "application d'un l'argument à une fonction"

Si

f ne contient pas de setL u libre
alors
($F u → f) a = {f où la variable u libre est remplacée par a}

Règle "lecture partielle de la variable"

($F u → u x) a

@todo

Règle ""

Si ($F u → x) a = ($F u → x) a

Traduction des preuves

Validité de l'extension