Mercurial > cpdt > repo
diff src/Reflection.v @ 297:b441010125d4
Everything compiles in Coq 8.3pl1
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 14 Jan 2011 14:39:12 -0500 |
parents | 4662b6f099b0 |
children | 7b38729be069 |
line wrap: on
line diff
--- a/src/Reflection.v Thu Dec 09 14:39:49 2010 -0500 +++ b/src/Reflection.v Fri Jan 14 14:39:12 2011 -0500 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2010, Adam Chlipala +(* Copyright (c) 2008-2011, Adam Chlipala * * This work is licensed under a * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 @@ -68,7 +68,7 @@ (** We bring into scope some notations for the [partial] type. These overlap with some of the notations we have seen previously for specification types, so they were placed in a separate scope that needs separate opening. *) (* begin thide *) -Definition check_even (n : nat) : [isEven n]. +Definition check_even : forall n : nat, [isEven n]. Hint Constructors isEven. refine (fix F (n : nat) : [isEven n] := @@ -462,9 +462,9 @@ (** 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]. *) - Definition forward (f : formula) (known : set index) (hyp : formula) - (cont : forall known', [allTrue known' -> formulaDenote atomics f]) - : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f]. + Definition forward : forall (f : formula) (known : set index) (hyp : formula) + (cont : forall known', [allTrue known' -> formulaDenote atomics f]), + [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f]. refine (fix F (f : formula) (known : set index) (hyp : formula) (cont : forall known', [allTrue known' -> formulaDenote atomics f]) : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] := @@ -482,8 +482,8 @@ (** A [backward] function implements analysis of the final goal. It calls [forward] to handle implications. *) - Definition backward (known : set index) (f : formula) - : [allTrue known -> formulaDenote atomics f]. + Definition backward : forall (known : set index) (f : formula), + [allTrue known -> formulaDenote atomics f]. refine (fix F (known : set index) (f : formula) : [allTrue known -> formulaDenote atomics f] := match f with @@ -498,7 +498,7 @@ (** A simple wrapper around [backward] gives us the usual type of a partial decision procedure. *) - Definition my_tauto (f : formula) : [formulaDenote atomics f]. + Definition my_tauto : forall f : formula, [formulaDenote atomics f]. intro; refine (Reduce (backward nil f)); crush. Defined. End my_tauto.