明示的な型を持たないCoq多型関数

Question

私はCoq用語言語で書かれた "列挙型"関数を持っています。この関数は、enumerate関数が使用されているときはいつも、明示的に指定する必要があるので、使用するのは面倒です（リスト内の要素の型はAです）。パラメータとしてAを明示的に渡す必要を避ける方法はありますか？

(* [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. 

は、私はいくつかの追加の構文は正確にAが何であるかを識別して、おそらく

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

ようなものを書くことができるようにしたいです。

Answer 1

引数を大括弧で囲み、デフォルトで暗黙的にする（see section 2.7.4 here）。また、おそらくこの関数を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)] *)