@[reducible, inline]

abbrev Com.Refinement {Γ : Ctxt InstCombine.LLVM.Ty} {t : InstCombine.LLVM.Ty} {α : Type} (src : Com InstCombine.LLVM Γ EffectKind.pure t) (tgt : Com InstCombine.LLVM Γ EffectKind.pure t) (h : autoParam (⟦t⟧ = Option α) _auto✝) : Prop

Equations

• (src ⊑ tgt) h = ∀ (Γv : Γ.Valuation), h ▸ src.denote Γv ⊑ h ▸ tgt.denote Γv