Mercurial > cpdt > repo

comparison src/Subset.v @ 475:1fd4109f7b31

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Batch of changes based on proofreader feedback
author Adam Chlipala <adam@chlipala.net>
date Mon, 22 Oct 2012 14:23:52 -0400
parents d9e1fb184672
children b7419a10e52e
comparison
equal deleted inserted replaced
474:d9e1fb184672 475:1fd4109f7b31
871 871
872 (* end thide *) 872 (* end thide *)
873 Definition typeCheck' : forall e : exp, {t : type | hasType e t} + {forall t, ~ hasType e t}. 873 Definition typeCheck' : forall e : exp, {t : type | hasType e t} + {forall t, ~ hasType e t}.
874 (* begin thide *) 874 (* begin thide *)
875 Hint Constructors hasType. 875 Hint Constructors hasType.
876
876 (** We register all of the typing rules as hints. *) 877 (** We register all of the typing rules as hints. *)
877 878
878 Hint Resolve hasType_det. 879 Hint Resolve hasType_det.
880
879 (** The lemma [hasType_det] will also be useful for proving proof obligations with contradictory contexts. Since its statement includes [forall]-bound variables that do not appear in its conclusion, only [eauto] will apply this hint. *) 881 (** The lemma [hasType_det] will also be useful for proving proof obligations with contradictory contexts. Since its statement includes [forall]-bound variables that do not appear in its conclusion, only [eauto] will apply this hint. *)
880 882
881 (** Finally, the implementation of [typeCheck] can be transcribed literally, simply switching notations as needed. *) 883 (** Finally, the implementation of [typeCheck] can be transcribed literally, simply switching notations as needed. *)
882 884
883 refine (fix F (e : exp) : {t : type | hasType e t} + {forall t, ~ hasType e t} := 885 refine (fix F (e : exp) : {t : type | hasType e t} + {forall t, ~ hasType e t} :=