X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FBool%2FBvector.mma;h=c50415feca2653e25dc697251418bda17eb4e0fb;hb=4dc282b8b71479d45704b414d1a10a27e71752f1;hp=0894e8eea9392d7e5806a4fdfcc7ff00d2a2bfe7;hpb=29714797b01e0ac8c22e4df2827b1785a759f482;p=helm.git

diff --git a/helm/software/matita/contribs/procedural/Coq/Bool/Bvector.mma b/helm/software/matita/contribs/procedural/Coq/Bool/Bvector.mma
index 0894e8eea..c50415fec 100644
--- a/helm/software/matita/contribs/procedural/Coq/Bool/Bvector.mma
+++ b/helm/software/matita/contribs/procedural/Coq/Bool/Bvector.mma
@@ -46,17 +46,17 @@ Open Local Scope nat_scope.
 
 (*  
 On s'inspire de PolyList pour fabriquer les vecteurs de bits.
-La dimension du vecteur est un paramètre trop important pour
+La dimension du vecteur est un param\232\tre trop important pour
 se contenter de la fonction "length".
-La première idée est de faire un record avec la liste et la longueur.
+La premi\232\re id\233\e est de faire un record avec la liste et la longueur.
 Malheureusement, cette verification a posteriori amene a faire
 de nombreux lemmes pour gerer les longueurs.
-La seconde idée est de faire un type dépendant dans lequel la
-longueur est un paramètre de construction. Cela complique un
-peu les inductions structurelles, la solution qui a ma préférence
-est alors d'utiliser un terme de preuve comme définition.
+La seconde id\233\e est de faire un type d\233\pendant dans lequel la
+longueur est un param\232\tre de construction. Cela complique un
+peu les inductions structurelles, la solution qui a ma pr\233\f\233\rence
+est alors d'utiliser un terme de preuve comme d\233\finition.
 
-(En effet une définition comme :
+(En effet une d\233\finition comme :
 Fixpoint Vunaire [n:nat; v:(vector n)]: (vector n) :=
 Cases v of
 	| Vnil => Vnil
@@ -97,16 +97,16 @@ Section VECTORS
 *)
 
 (* 
-Un vecteur est une liste de taille n d'éléments d'un ensemble A.
-Si la taille est non nulle, on peut extraire la première composante et 
-le reste du vecteur, la dernière composante ou rajouter ou enlever 
-une composante (carry) ou repeter la dernière composante en fin de vecteur.
-On peut aussi tronquer le vecteur de ses p dernières composantes ou
-au contraire l'étendre (concaténer) d'un vecteur de longueur p.
-Une fonction unaire sur A génère une fonction des vecteurs de taille n
-dans les vecteurs de taille n en appliquant f terme à terme.
-Une fonction binaire sur A génère une fonction des couple de vecteurs 
-de taille n dans les vecteurs de taille n en appliquant f terme à terme.
+Un vecteur est une liste de taille n d'\233\l\233\ments d'un ensemble A.
+Si la taille est non nulle, on peut extraire la premi\232\re composante et 
+le reste du vecteur, la derni\232\re composante ou rajouter ou enlever 
+une composante (carry) ou repeter la derni\232\re composante en fin de vecteur.
+On peut aussi tronquer le vecteur de ses p derni\232\res composantes ou
+au contraire l'\233\tendre (concat\233\ner) d'un vecteur de longueur p.
+Une fonction unaire sur A g\233\n\232\re une fonction des vecteurs de taille n
+dans les vecteurs de taille n en appliquant f terme \224\ terme.
+Une fonction binaire sur A g\233\n\232\re une fonction des couple de vecteurs 
+de taille n dans les vecteurs de taille n en appliquant f terme \224\ terme.
 *)
 
 (* UNEXPORTED
@@ -166,14 +166,14 @@ Section BOOLEAN_VECTORS
 *)
 
 (* 
-Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. 
-ATTENTION : le stockage s'effectue poids FAIBLE en tête.
+Un vecteur de bits est un vecteur sur l'ensemble des bool\233\ens de longueur fixe. 
+ATTENTION : le stockage s'effectue poids FAIBLE en t\234\te.
 On en extrait le bit  de poids faible (head) et la fin du vecteur (tail).
-On calcule la négation d'un vecteur, le et, le ou et le xor bit à bit de 2 vecteurs.
-On calcule les décalages d'une position vers la gauche (vers les poids forts, on
+On calcule la n\233\gation d'un vecteur, le et, le ou et le xor bit \224\ bit de 2 vecteurs.
+On calcule les d\233\calages d'une position vers la gauche (vers les poids forts, on
 utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en 
-insérant un bit 'carry' (logique) ou en répétant le bit de poids fort (arithmétique).
-ATTENTION : Tous les décalages prennent la taille moins un comme paramètre
+ins\233\rant un bit 'carry' (logique) ou en r\233\p\233\tant le bit de poids fort (arithm\233\tique).
+ATTENTION : Tous les d\233\calages prennent la taille moins un comme param\232\tre
 (ils ne travaillent que sur des vecteurs au moins de longueur un).
 *)