tidues/heterogenous-list-in-coq

heterogenous-list-in-coq's Issues

Returns None on last element of hlist.

A correct solution

Require Import List.
Set Implicit Arguments.

Inductive hlist : list Set -> Type :=
| hnil : hlist nil
| hcons {X : Set} {Xs : list Set} (x : X) :
  hlist Xs -> hlist (X :: Xs).

Notation "[;;]" := (hnil).
Notation "h ;; t" := (hcons h t)
  (at level 30, right associativity).

Fixpoint hget 
  {Xs : list Set} 
  (hls : hlist Xs)
  (n : nat) 
: option (nth n Xs Empty_set) :=
  match n with
  | O =>
    match hls with
    | hnil => None 
    | hcons x _ => Some x
    end
  | S n =>
    match hls with
    | hnil => None
    | @hcons _ Xs _ hls => @hget Xs hls n
    end
  end.