Names with offsets

Names.agda

open import Data.String.Base
open import Data.Nat.Base
open import Data.List.Base
open import Relation.Binary.PropositionalEquality

infix 5 _at_
record Variable : Set where
  constructor _at_
  field name   : String
        offset : ℕ
open Variable public

infix 3 _∈_
data _∈_ : Variable → List String → Set where
  here : ∀ {s xs} → s at 0 ∈ s ∷ xs
  next : ∀ {s t xs} → s ∈ xs → name s ≢ t → s ∈ t ∷ xs
  skip : ∀ {s n xs} → s at n ∈ xs → s at suc n ∈ s ∷ xs