Some examples of reflection in Coq. Propositional logic (prop) and Primitive Recursive Arithmetic (pra). This is very old, but might still be of interest.
|
dec.v |
|
|
pra_example.v |
|
|
pra.v |
|
|
prop_example.v |
|
|
prop.v |