scoped_belongs_two.agda

¬[_] : ∀ {a b : Name} → Dec (a ≡ b) → Set
¬[ (yes x₁) ] = ⊥
¬[ (no x₁) ] = ⊤

data _,_∈x_ (n : Name) (p : Pointer) : Env → Set where
  zero : ∀ {xs}            → n , p ∈x ((n , p) ∷ xs)
  suc  : ∀ {n' : Name}  { p' : Pointer} {xs} {pr : ¬[  n == n'  ]}
    → n , p ∈x xs → n , p ∈x ((n' , p') ∷ xs)
    
private
  env : Env
  env = (y , 5) ∷ (x , 1) ∷ (z , 0) ∷(x , 0 ) ∷ []

  p₁' : x , 1 ∈x env
  p₁' = suc zero

  -- type checker complains! :D
  -- p₂' : x , 0 ∈x env
  -- p₂' = suc (suc (suc zero))