@[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

def «term_⊑_» : Lean.TrailingParserDescr

Equations

• «term_⊑_» = Lean.ParserDescr.trailingNode `«term_⊑_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 90))