Mercurial > cpdt > repo

comparison src/Universes.v @ 378:6413675f8e04

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)