module Stdlib.Trait.Eq;

import Stdlib.Data.Bool.Base open;
import Stdlib.Data.Fixity open;

--- A trait defining equality
trait
type Eq A := mkEq@{eq : A -> A -> Bool};

syntax operator == comparison;
syntax operator /= comparison;

{-# inline: always, isabelle-operator: {name: "=", prec: 50, assoc: none} #-}
== {A} {{Eq A}} : A -> A -> Bool := Eq.eq;

--- Test for inequality.
{-# inline: always, isabelle-operator: {name: "\\<noteq>", prec: 50, assoc: none} #-}
/= {A} {{Eq A}} (x y : A) : Bool := not (x == y);