bounded_extend_function.chr

:- module(bounded_extend_function, [result/1]).
:- use_module(library(prelude)).

:- chr_constraint result(int).

:- class (gt(int, int) -> bool), (gt(float, float) -> bool).
gt(X, Y) -> X > Y.

% Bounded open function with one initial equation.
:- open_function pick(T, T) -> T requiring gt(T, T) -> bool.
pick(X, _) | gt(X, X) -> X.

% Extension: a new equation for the bounded open function. Allowed
% because :- extend_function is permitted on bounded open functions;
% the new equation type-checks under the same ambient bound.
:- extend_function pick(_, Y) -> Y.

result(R) <=> R is pick(3, 5).