instance MLIR.SimplyTyped.instSubstituteableTerminatorVarName : MLIR.UnTyped.SubstituteableTerminator MLIR.VarName

Equations

• MLIR.SimplyTyped.instSubstituteableTerminatorVarName = { substituteTerminator := fun (σ : MLIR.VarName → MLIR.VarName) => σ }

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

The type of Type-preserving substitutions. That is, substitutions σ such that for each variable v in the original context Γ we have that the result of applying σ to v is mapped to the same type in the target context Δ

Equations

• MLIR.SimplyTyped.Substitution Γ Δ = { σ : MLIR.UnTyped.Substitution // ∀ (v : MLIR.VarName) (t : Ty), Γ.hasType v t → Δ.hasType (σ.apply v) t }

theorem MLIR.SimplyTyped.Expr.WellTyped_of_substitute {Op : Type} {Ty : Type} [MLIR.SimplyTyped.OpSignature Op Ty] {Γ : MLIR.SimplyTyped.Context Ty} {Δ : MLIR.SimplyTyped.Context Ty} {σ : MLIR.SimplyTyped.Substitution Γ Δ} {ty : Ty} {e : MLIR.UnTyped.Expr Op MLIR.VarName} (h : MLIR.SimplyTyped.Expr.WellTyped Γ e ty) : MLIR.SimplyTyped.Expr.WellTyped Δ (MLIR.UnTyped.Expr.substitute (↑σ) e) ty