class LO.Rhd (F : Type u_1) : Type u_1

• rhd : F → F → F

def LO.«term_▷_» : Lean.TrailingParserDescr

Equations

• LO.«term_▷_» = Lean.ParserDescr.trailingNode `LO.«term_▷_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ▷ ") (Lean.ParserDescr.cat `term 71))

class LO.InterpretabilityLogicalConnective (F : Type u_1) extends LO.BasicModalLogicalConnective F, LO.Rhd F : Type u_1

• top : F
• bot : F
• tilde : F → F
• arrow : F → F → F
• wedge : F → F → F
• vee : F → F → F
• box : F → F
• box_injective : Function.Injective box
• dia : F → F
• dia_injective : Function.Injective dia
• rhd : F → F → F