Qcert.Basic.Operators.ROpsEq

Section ROpsEq.



  Context {fdata:foreign_data}.
  Context {fuop:foreign_unary_op}.
  Context {fbop:foreign_binary_op}.


  Definition unaryop_eq (uop1 uop2:unaryOp) : Prop :=
    ∀ (h:list (string×string)),
    ∀ (x:data),
      data_normalized h x →
      (fun_of_unaryop h uop1) x = (fun_of_unaryop h uop2) x.

  Global Instance unaryop_equiv : Equivalence unaryop_eq.

  Definition binop_eq (bop1 bop2:binOp) : Prop :=
    ∀ (h:list (string×string)),
    ∀ (x:data),
      data_normalized h x →
      ∀ (y:data),
        data_normalized h x →
        (fun_of_binop h bop1) x y = (fun_of_binop h bop2) x y.

  Global Instance binop_equiv : Equivalence binop_eq.

End ROpsEq.