Mercurial > cpdt > repo
comparison 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 |
comparison
equal
deleted
inserted
replaced
377:252ba054a1cd | 378:6413675f8e04 |
---|---|
1145 | 1145 |
1146 Variable values : hlist (fun x : Set => x) types'. | 1146 Variable values : hlist (fun x : Set => x) types'. |
1147 | 1147 |
1148 (** Now a bit of dependent pattern matching helps us rewrite [getNat] in a way that avoids any use of equality proofs. *) | 1148 (** Now a bit of dependent pattern matching helps us rewrite [getNat] in a way that avoids any use of equality proofs. *) |
1149 | 1149 |
1150 Fixpoint skipCopies (n : nat) | |
1151 : hlist (fun x : Set => x) (copies nat n ++ nat :: nil) -> nat := | |
1152 match n with | |
1153 | O => fun vs => hhd vs | |
1154 | S n' => fun vs => skipCopies n' (htl vs) | |
1155 end. | |
1156 | |
1150 Fixpoint getNat' (types'' : list Set) (natIndex : nat) | 1157 Fixpoint getNat' (types'' : list Set) (natIndex : nat) |
1151 : hlist (fun x : Set => x) (update types'' natIndex nat) -> nat := | 1158 : hlist (fun x : Set => x) (update types'' natIndex nat) -> nat := |
1152 match types'' with | 1159 match types'' with |
1153 | nil => fun vs => hhd vs | 1160 | nil => skipCopies natIndex |
1154 | t :: types0 => | 1161 | t :: types0 => |
1155 match natIndex return hlist (fun x : Set => x) | 1162 match natIndex return hlist (fun x : Set => x) |
1156 (update (t :: types0) natIndex nat) -> nat with | 1163 (update (t :: types0) natIndex nat) -> nat with |
1157 | O => fun vs => hhd vs | 1164 | O => fun vs => hhd vs |
1158 | S natIndex' => fun vs => getNat' types0 natIndex' (htl vs) | 1165 | S natIndex' => fun vs => getNat' types0 natIndex' (htl vs) |