λ-calculus

Contexts as pairs of free variables and types.

@[reducible, inline]

abbrev Cslib.LambdaCalculus.LocallyNameless.Context (α : Type u) (β : Type v) : Type (max v u)

A typing context is a list of free variables and corresponding types.

Equations

• Cslib.LambdaCalculus.LocallyNameless.Context α β = List ((_ : α) × β)

def Cslib.LambdaCalculus.LocallyNameless.Context.dom {α : Type u} {β : Type v} [DecidableEq α] (Γ : Context α β) : Finset α

The domain of a context is the finite set of free variables it uses.

Equations

• Γ.dom = (List.keys Γ).toFinset

instance Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed {α : Type u} {β : Type v} : HasWellFormed (Context α β)

Equations

• Cslib.LambdaCalculus.LocallyNameless.Context.instHasWellFormed = { wf := List.NodupKeys }

theorem Cslib.LambdaCalculus.LocallyNameless.Context.haswellformed_def {α : Type u} {β : Type v} (Γ : Context α β) : Γ✓ = List.NodupKeys Γ

def Cslib.LambdaCalculus.LocallyNameless.Context.map_val {α : Type u} {β : Type v} (f : β → β) (Γ : Context α β) : Context α β

A mapping of values within a context.

Equations

• Cslib.LambdaCalculus.LocallyNameless.Context.map_val f Γ = List.map (fun (x : (_ : α) × β) => match x with | ⟨var, ty⟩ => ⟨var, f ty⟩) Γ

theorem Cslib.LambdaCalculus.LocallyNameless.Context.map_val_keys {α : Type u} {β : Type v} {Γ : Context α β} (f : β → β) : List.keys Γ = List.keys (map_val f Γ)

A mapping of values preserves keys.

theorem Cslib.LambdaCalculus.LocallyNameless.Context.map_val_mem {α : Type u} {β : Type v} [DecidableEq α] {Γ : Context α β} {x : α} {σ : β} (mem : σ ∈ List.dlookup x Γ) (f : β → β) : f σ ∈ List.dlookup x (map_val f Γ)

A mapping of values maps lookups.