Mercurial > cpdt > repo
comparison src/Reflection.v @ 353:3322367e955d
Move GeneralRec one chapter slot later, since Subset should be a prereq
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 26 Oct 2011 17:14:28 -0400 |
| parents | ad315efc3b6b |
| children | e0d91bcf70ec |
comparison
equal
deleted
inserted
replaced
| 352:ab60b10890ed | 353:3322367e955d |
|---|---|
| 458 | 458 |
| 459 Hint Resolve allTrue_add allTrue_In. | 459 Hint Resolve allTrue_add allTrue_In. |
| 460 | 460 |
| 461 Local Open Scope partial_scope. | 461 Local Open Scope partial_scope. |
| 462 | 462 |
| 463 (** Now we can write a function [forward] which implements deconstruction of hypotheses. It has a dependent type, in the style of Chapter 7, guaranteeing correctness. The arguments to [forward] are a goal formula [f], a set [known] of atomic formulas that we may assume are true, a hypothesis formula [hyp], and a success continuation [cont] that we call when we have extended [known] to hold new truths implied by [hyp]. *) | 463 (** Now we can write a function [forward] which implements deconstruction of hypotheses. It has a dependent type, in the style of Chapter 6, guaranteeing correctness. The arguments to [forward] are a goal formula [f], a set [known] of atomic formulas that we may assume are true, a hypothesis formula [hyp], and a success continuation [cont] that we call when we have extended [known] to hold new truths implied by [hyp]. *) |
| 464 | 464 |
| 465 Definition forward : forall (f : formula) (known : set index) (hyp : formula) | 465 Definition forward : forall (f : formula) (known : set index) (hyp : formula) |
| 466 (cont : forall known', [allTrue known' -> formulaDenote atomics f]), | 466 (cont : forall known', [allTrue known' -> formulaDenote atomics f]), |
| 467 [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f]. | 467 [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f]. |
| 468 refine (fix F (f : formula) (known : set index) (hyp : formula) | 468 refine (fix F (f : formula) (known : set index) (hyp : formula) |