The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Constants are considered in the Const rule (same rule as Var but with E instead of gamma).

On Tue, Oct 28, 2014 at 10:34 PM, Matej Kosik<5764c029b688c1c0d24a2e97cd764f AT gmail.com>wrote:

Hello,

In the Reference Manual (Section 4.2 : Typed Terms)
there is this rule:


      𝓦𝓕(E)[Γ]    (x:T) ∈ Γ or (x:=t:T) ∈ Γ for some t
  Var ─────────────────────────────────────────────────
                         E[Γ] ⊢ x:T


Isn't that rule, as it is stated, too weak?
Shouldn't the rule read:

      𝓦𝓕(E)[Γ]    (x:T) ∈ E∪Γ or (x:=t:T) ∈ E∪Γ for some t
  Var ─────────────────────────────────────────────────────
                         E[Γ] ⊢ x:T

?

Otherwise, how would one be able to prove that x:T
if  (x,T) ∈ E
but (x,T) ∉ Γ
?