Mercurial > cpdt > repo
diff src/Reflection.v @ 205:f05514cc6c0d
'make doc' works with 8.2
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 06 Nov 2009 12:15:05 -0500 |
parents | e71904f61e69 |
children | 54e8ecb5ec88 |
line wrap: on
line diff
--- a/src/Reflection.v Fri Nov 06 10:52:43 2009 -0500 +++ b/src/Reflection.v Fri Nov 06 12:15:05 2009 -0500 @@ -118,6 +118,8 @@ prove_even_reflective. + ]] + [[ User error: No matching clauses for match goal @@ -129,6 +131,8 @@ exact (partialOut (check_even 255)). + ]] + [[ Error: The term "partialOut (check_even 255)" has type @@ -633,12 +637,19 @@ Theorem t2 : forall x y z, (2 # 1) * (x - (3 # 2) * y) == 15 # 1 -> z + (8 # 1) * x == 20 # 1 -> (-6 # 2) * y + (10 # 1) * x + z == 35 # 1. + + ]] + [[ intros; reflectContext; assumption. + + ]] [[ Qed. +]] + Your solution can work in any way that involves reflecting syntax and doing most calculation with a Gallina function. These hints outline a particular possible solution. Throughout, the [ring] tactic will be helpful for proving many simple facts about rationals, and tactics like [rewrite] are correctly overloaded to work with rational equality [==]. %\begin{enumerate}%#<ol># @@ -680,6 +691,8 @@ end ] end. +]] + #</ol>#%\end{enumerate}% #</li>#