Mercurial > cpdt > repo
diff src/Universes.v @ 378:6413675f8e04
Recursing under binders in reification
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 29 Mar 2012 17:13:23 -0400 |
parents | 252ba054a1cd |
children | 057a29f9c773 |
line wrap: on
line diff
--- a/src/Universes.v Wed Mar 28 13:20:50 2012 -0400 +++ b/src/Universes.v Thu Mar 29 17:13:23 2012 -0400 @@ -1147,10 +1147,17 @@ (** Now a bit of dependent pattern matching helps us rewrite [getNat] in a way that avoids any use of equality proofs. *) + Fixpoint skipCopies (n : nat) + : hlist (fun x : Set => x) (copies nat n ++ nat :: nil) -> nat := + match n with + | O => fun vs => hhd vs + | S n' => fun vs => skipCopies n' (htl vs) + end. + Fixpoint getNat' (types'' : list Set) (natIndex : nat) : hlist (fun x : Set => x) (update types'' natIndex nat) -> nat := match types'' with - | nil => fun vs => hhd vs + | nil => skipCopies natIndex | t :: types0 => match natIndex return hlist (fun x : Set => x) (update (t :: types0) natIndex nat) -> nat with