module finite_function.

kind finite_fun		type -> type -> type.

type empty_f_fun 	(finite_fun Domain Range).
type f_fun_extend	Domain -> Range -> (finite_fun Domain Range)
				-> (finite_fun Domain Range).
type f_fun_apply	(finite_fun Domain Range) -> Domain -> Range -> o.
type f_fun_in_domain	(finite_fun Domain Range) -> Domain -> o.


f_fun_apply (f_fun_extend DomainElem Res FF) DomainElem Res :- !.
f_fun_apply (f_fun_extend DomainElem Res FF) X Y :-
	f_fun_apply FF X Y.

f_fun_in_domain (f_fun_extend DomainElem Res FF) DomainElem :- !.
f_fun_in_domain (f_fun_extend DomainElem Res FF) X :-
	f_fun_in_domain FF X.