chained_op.lean

section
universe u
parameters (α β : Type u) (op : α → β → Prop)

structure chained_op_val :=
(left : α)
(right : β)
(val : Prop)

instance coe_chained_op_val : has_coe chained_op_val Prop :=
⟨chained_op_val.val⟩
end

instance coe_to_chained_op_val (α : Type) : has_coe α (chained_op_val α α) :=
⟨λ a, ⟨a, a, true⟩⟩

--def mk_chained_op {α β : Type} (op : α → β → Prop) {l r : Type} :
--  chained_op_val l α → chained_op_val β r → chained_op_val l r :=
--λ l r, ⟨l.left, r.right, l.val ∧ op l.right r.left ∧ r.val⟩
def mk_chained_op {α : Type} (op : α → α → Prop) :
  chained_op_val α α → chained_op_val α α → chained_op_val α α :=
λ l r, ⟨l.left, r.right, l.val ∧ op l.right r.left ∧ r.val⟩

constant cls : Type
constant inh_nonvirt : cls → cls → Prop
constant inh_virt : cls → cls → Prop
constant rtrancl_inh : cls → cls → Prop

infix ` <^* `:20 := mk_chained_op inh_nonvirt
infix ` <ᵥ `:20 := mk_chained_op inh_virt

#check λ a b c : cls, (a <^* b <ᵥ c : Prop)