相关疑难解决方法(0)

我们可以枚举列表的元素,如下所示:

-- enumerate-? = zip [0..]
enumerate-? : ? {?} {A : Set ?} -> List A -> List (? × A)
enumerate-? = go 0 where
  go : ? {?} {A : Set ?} -> ? -> List A -> List (? × A)
  go n  []      = []
  go n (x ? xs) = (n , x) ? go (?.suc n) xs

Eg enumerate-? (1 ? 3 ? 2 ? 5 ? [])等于(0 , 1) ? …