A given value provides a shape implementation for a concrete type.

export let intEq :=
  given Eq[Int] {
  let eq (left : Int, right : Int) : Bool := left = right;
};

Implement a shape

export let intEq := given Eq[Int] {
  let eq (left : Int, right : Int) : Bool := left = right;
};

The given value is evidence that Int can satisfy Eq.

Given value shape

A given value names the shape and the type argument: given Eq[Int]. The body provides the members that the shape requires.

For Eq[Int], the body provides eq. The implementation can use normal integer equality because both parameters are Int.

Put a given value near the type or near the shape module. Readers should not need to search the whole package to find how a type satisfies a shape.

If two modules disagree about equality, ordering, or formatting, keep that decision in the given value instead of hiding it in call sites.

Names like eqInt or ordPort make logs, errors, and docs easier to read.