Mercurial > cpdt > repo

comparison src/Reflection.v @ 350:ad315efc3b6b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Stub out new chapter
author Adam Chlipala <adam@chlipala.net>
date Wed, 26 Oct 2011 11:19:52 -0400
parents d5787b70cf48
children 3322367e955d
comparison
equal deleted inserted replaced
349:de7db21a016c 350:ad315efc3b6b
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 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]. *) 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]. *)
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)