Coq fonction polymorphique sans type explicite

Question

J'ai une fonction "enumerate" écrite dans le langage de terme Coq (comment s'appelle-t-elle?). Cette fonction est un peu ennuyante à utiliser car elle nécessite que A (le type d'un élément de la liste l) soit explicitement fourni chaque fois que la fonction enumerate est utilisée. Y at-il un moyen d'éviter de devoir passer explicitement A en tant que paramètre?

(* [a, b] -> [(0,a), (1,b)] *) 
Fixpoint enumerate (A : Type) (l : list A) : list (nat * A) := 
    let empty : (list (nat * A)) := nil in 
    let incr_pair xy := match xy with 
    | (x, y) => ((S x), y) 
    end in 
    match l with 
    | nil => empty 
    | (x :: xs) => (O, x) :: (map incr_pair (enumerate A xs)) 
    end. 

Je veux être capable d'écrire quelque chose comme

Fixpoint enumerate (l : list A) : list (nat * A) := ... 

Peut-être avec une syntaxe d'identifier ce A exactement supplémentaire est.

Answer 1

Mettez les arguments entre parenthèses pour les rendre implicites par défaut (voir section 2.7.4 here). De plus, vous devriez probablement écrire cette fonction de manière non quadratique avec un accumulateur nat.

Require Import Lists.List. 
Import ListNotations. 

Fixpoint enumerate_from {A : Type} (n : nat) (l : list A) : list (nat * A) := 
    match l with 
    | [] => [] 
    | x :: xs => (n, x) :: enumerate_from (S n) xs 
    end. 

Definition enumerate {A} l : list (nat * A) := enumerate_from 0 l. 

Compute (enumerate [3; 4; 5]). (* prints [(0, 3); (1, 4); (2, 5)] *)