Mercurial > cpdt > repo
comparison src/Intro.v @ 227:d8c54a25c81f
Update DataStruct with a new reason to use reflexive types; start Universes
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 18 Nov 2009 15:38:01 -0500 |
parents | dbac52f5bce1 |
children | 52b9e43be069 |
comparison
equal
deleted
inserted
replaced
226:9d0b9577f8b1 | 227:d8c54a25c81f |
---|---|
199 \hline | 199 \hline |
200 Reasoning About Equality Proofs & \texttt{Equality.v} \\ | 200 Reasoning About Equality Proofs & \texttt{Equality.v} \\ |
201 \hline | 201 \hline |
202 Generic Programming & \texttt{Generic.v} \\ | 202 Generic Programming & \texttt{Generic.v} \\ |
203 \hline | 203 \hline |
204 Universes and Axioms & \texttt{Universes.v} \\ | |
205 \hline | |
204 Proof Search in Ltac & \texttt{Match.v} \\ | 206 Proof Search in Ltac & \texttt{Match.v} \\ |
205 \hline | 207 \hline |
206 Proof by Reflection & \texttt{Reflection.v} \\ | 208 Proof by Reflection & \texttt{Reflection.v} \\ |
207 \hline | 209 \hline |
208 First-Order Abstract Syntax & \texttt{Firstorder.v} \\ | 210 First-Order Abstract Syntax & \texttt{Firstorder.v} \\ |