(*
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
*)
(*
-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
*)
(*
-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).
*)
projects / helm.git / blobdiff