Mercurial > cpdt > repo
comparison src/Firstorder.v @ 250:76043a960a38
Proofreading pass over Firstorder
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Fri, 11 Dec 2009 16:18:29 -0500 |
| parents | 0f45421cae21 |
| children | 758778c0468c |
comparison
equal
deleted
inserted
replaced
| 249:0f45421cae21 | 250:76043a960a38 |
|---|---|
| 58 | 58 |
| 59 (** The definitions of our judgments will be prettier if we write them using mixfix syntax. To define a judgment for looking up the type of a variable in a context, we first %\textit{%#</i>#reserve#</i>#%}% a notation for the judgment. Reserved notations enable mutually-recursive definition of a judgment and its notation; in this sense, the reservation is like a forward declaration in C. *) | 59 (** The definitions of our judgments will be prettier if we write them using mixfix syntax. To define a judgment for looking up the type of a variable in a context, we first %\textit{%#</i>#reserve#</i>#%}% a notation for the judgment. Reserved notations enable mutually-recursive definition of a judgment and its notation; in this sense, the reservation is like a forward declaration in C. *) |
| 60 | 60 |
| 61 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level). | 61 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level). |
| 62 | 62 |
| 63 (** Now we define the judgment itself, using a [where] clause to associate a notation definition. *) | 63 (** Now we define the judgment itself, for variable typing, using a [where] clause to associate a notation definition. *) |
| 64 | 64 |
| 65 Inductive lookup : ctx -> var -> type -> Prop := | 65 Inductive lookup : ctx -> var -> type -> Prop := |
| 66 | First : forall x t G, | 66 | First : forall x t G, |
| 67 (x, t) :: G |-v x : t | 67 (x, t) :: G |-v x : t |
| 68 | Next : forall x t x' t' G, | 68 | Next : forall x t x' t' G, |