J'ai vu une syntaxe très étrange: (nom: type1) type2 dans le type et [name: type] expr dans les expressions, ressemble à une syntaxe alternative pour Pi et Lambda, mais je n'ai rien trouvé dans la documentation après plusieurs heures cherchant, tout en vain.Quels sont les moyens (a: b) c et [a: b] c dans certaines théories Coq et où est-il défini?
Qu'est-ce que cela signifie et où est-il défini?
Vous avez lu une théorie écrite pour une ancienne version de Coq. La syntaxe a subi une refonte majeure avec V8.0. V8.0 livré avec un outil pour traduire les théories V7 en V8, qui a très bien fonctionné; l'outil a été supprimé des versions ultérieures.
Vous pouvez voir une revue des changements dans l'article Translation from Coq V7 to V8.
En particulier, (a:b) c est une quantification universelle, maintenant écrite forall a:b, c; est une abstraction lambda, maintenant écrit fun a:b => c. Une autre chose importante lors de la lecture des anciennes théories est que l'application de la fonction nécessite des parenthèses et a une faible priorité: jusqu'à V7, (f x = y) signifie (f (x=y)) et ([x:nat]y z) signifie (([x:nat]y) z).
oh! Merci beaucoup! J'ai déjà commencé à penser que c'était un cauchemar :) – Vag