Études-Mathématique/Type des formules et paramètres

From Lazi wiki
Jump to: navigation, search

Question

Certaines formules utilisent des variables (dans les règles de déduction simples). Plus tard, dans la notation de fonction, on pourra avoir aussi des formules à variable.

Comment intégrer ce paramètre de liste de variables acceptées au type ?

Étude

Les types dans Top ne peuvent dépendre d'un autre argument que Top.

Solution par liste de variables en instance

Le type "lazi0VarFormulaT" a pour instance une liste de variables. Son objet est l'objet des formules avec ces variables. Mais comme le type des formules est récurssif (apply a besoin du type des formules), il faut passer en contexte non par Top, mais le type des formules.

Mais comment faire pour que le type des formules puisse être changé pour y ajouter les variables ?

On peut modifier topT pour le rendre configurable: on ajoute une entrées pour le dictionnaire des types et une entrée de données quelconques. Ainsi les types peuvent utiliser ces données ou modifier les types de Top juste en changeant l'entrée "types".

Réponse

Voir la seule solution de l'étude.