Agda vs. Coq

indexed_list.agda

(* Indexed list indexing in Agda *)

data IList {a} (A : Set a) : Nat → Set a where
  Nil : IList A 0
  Cons : {n : Nat} -> A -> IList A n -> IList A (S n)

data Fin : Nat -> Set where
  Z : {n : Nat} -> Fin (S n)
  S : {n : Nat} -> Fin n -> Fin (S n)

get : ∀{a}{A : Set a} {n} -> IList A n -> Fin n -> A
get (Cons x l) Z = x
get (Cons x l) (S n) = get l n

indexed_list.v

(* Indexed list indexing in Coq, from http://adam.chlipala.net/cpdt/html/DataStruct.html *)

Section ilist.
  Variable A : Set.

  Inductive ilist : nat -> Set :=
  | Nil : ilist O
  | Cons : forall n, A -> ilist n -> ilist (S n).

  Inductive fin : nat -> Set :=
  | First : forall n, fin (S n)
  | Next : forall n, fin n -> fin (S n).

  (* So far so good, but then: *)
  Fixpoint get n (ls : ilist n) : fin n -> A :=
    match ls with
      | Nil => fun idx =>
        match idx in fin n' return (match n' with
                                        | O => A
                                        | S _ => unit
                                      end) with
          | First _ => tt
          | Next _ _ => tt
        end
      | Cons _ x ls' => fun idx =>
        match idx in fin n' return (fin (pred n') -> A) -> A with
          | First _ => fun _ => x
          | Next _ idx' => fun get_ls' => get_ls' idx'
        end (get ls')
    end.
  
   (* asdf. *)

End ilist.