def MLIR.SimplyTyped.Context (Ty : Type) : Type

Equations

• MLIR.SimplyTyped.Context Ty = List (MLIR.VarName × Ty)

def MLIR.SimplyTyped.Context.hasType {Ty : Type} (Γ : MLIR.SimplyTyped.Context Ty) (v : MLIR.VarName) (ty : Ty) : Prop

Γ.hasType v ty holds if Γ maps variable v to type ty

Equations

• Γ.hasType v ty = (List.lookup v Γ = some ty)

instance MLIR.SimplyTyped.Context.instDecidableHasTypeOfDecidableEq {Ty : Type} {Γ : MLIR.SimplyTyped.Context Ty} [DecidableEq Ty] {v : MLIR.VarName} {ty : Ty} : Decidable (Γ.hasType v ty)

Γ.hasType v ty is decidable when our type universe has decidable equality

Equations

• MLIR.SimplyTyped.Context.instDecidableHasTypeOfDecidableEq = id inferInstance

def MLIR.SimplyTyped.Context.push {Ty : Type} (Γ : MLIR.SimplyTyped.Context Ty) (v : MLIR.VarName) (ty : Ty) : MLIR.SimplyTyped.Context Ty

Γ.push v ty returns a context which maps v to ty, and works like Γ on all other variables

Equations

• Γ.push v ty = (v, ty) :: Γ

@[simp]

theorem MLIR.SimplyTyped.Context.hasType_push {Ty : Type} {v : MLIR.VarName} {ty : Ty} {Γ : MLIR.SimplyTyped.Context Ty} : (Γ.push v ty).hasType v ty

@[simp]

theorem MLIR.SimplyTyped.Context.hasType_push_of_neq {Ty : Type} {w : MLIR.VarName} {v : MLIR.VarName} {ty : Ty} {ty' : Ty} {Γ : MLIR.SimplyTyped.Context Ty} (h : w ≠ v) : (Γ.push v ty).hasType w ty' ↔ Γ.hasType w ty'

ExtEq

def MLIR.SimplyTyped.Context.ExtEq {Ty : Type} (Γ : MLIR.SimplyTyped.Context Ty) (Δ : MLIR.SimplyTyped.Context Ty) : Prop

Two contexts are extensionally equal if they map each variable to the same type

Equations

• Γ.ExtEq Δ = ∀ (v : MLIR.VarName), List.lookup v Γ = List.lookup v Δ

@[simp]

theorem MLIR.SimplyTyped.Context.ExtEq.rfl {Ty : Type} {Γ : MLIR.SimplyTyped.Context Ty} : Γ.ExtEq Γ

theorem MLIR.SimplyTyped.Context.ExtEq.trans {Ty : Type} {Γ : MLIR.SimplyTyped.Context Ty} {Δ : MLIR.SimplyTyped.Context Ty} {Ξ : MLIR.SimplyTyped.Context Ty} : Γ.ExtEq Δ → Δ.ExtEq Ξ → Γ.ExtEq Ξ

instance MLIR.SimplyTyped.Context.instTransExtEq {Op : Type} : Trans MLIR.SimplyTyped.Context.ExtEq MLIR.SimplyTyped.Context.ExtEq MLIR.SimplyTyped.Context.ExtEq

Equations

• MLIR.SimplyTyped.Context.instTransExtEq = { trans := ⋯ }

theorem MLIR.SimplyTyped.Context.ExtEq.symm {Ty : Type} {Γ : MLIR.SimplyTyped.Context Ty} {Δ : MLIR.SimplyTyped.Context Ty} : Γ.ExtEq Δ → Δ.ExtEq Γ

theorem MLIR.SimplyTyped.Context.hasType_of_extEq {Ty : Type} {v : MLIR.VarName} {t : Ty} {Γ : MLIR.SimplyTyped.Context Ty} {Δ : MLIR.SimplyTyped.Context Ty} (h_eq : Γ.ExtEq Δ) (h : Δ.hasType v t) : Γ.hasType v t