Toggle navigation
?
users online
Logout
Open hangout
Open chat for current file
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % (SWI-Prolog) :- module(peano_ari, [ nat/1, nat_zero/1, nat_lte/2, nat_succ/2, nat_add/3 ]). :- use_module(library(error)). error:has_type(nat_part, N) :- is_nat_part_(N). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% nat(N) :- must_be(nat_part, N), nat_(N). nat_zero(N) :- must_be(nat_part, N), nat_zero_(N). nat_lte(N0, N) :- must_be(nat_part, N0), must_be(nat_part, N), nat_lte_(N0, N). nat_succ(N0, N) :- must_be(nat_part, N0), must_be(nat_part, N), nat_succ_(N0, N). nat_add(N1, N2, N) :- must_be(nat_part, N1), must_be(nat_part, N2), must_be(nat_part, N), nat_add_(N1, N2, N). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% is_nat_part_(N) :- \+ \+ nat__(N). nat_(N) :- ( nat_ground__(N) ), !, once(nat__(N)). nat_(N) :- nat__(N). nat_zero_(N) :- nat_zero__(N). nat_lte_(N0, N) :- ( nat_ground__(N0), nat_ground__(N) ), !, once(nat_lte__(N0, N)). nat_lte_(N0, N) :- nat_lte__(N0, N). nat_succ_(N0, N) :- ( nat_ground__(N0) ; nat_ground__(N) ), !, once(nat_succ__(N0, N)). nat_succ_(N0, N) :- nat_succ__(N0, N). nat_add_(N1, N2, N) :- ( nat_ground__(N1), nat_ground__(N2) ; nat_ground__(N2), nat_ground__(N) ; nat_ground__(N), nat_ground__(N1) ), !, once(nat_add__(N1, N2, N)). nat_add_(N1, N2, N) :- nat_add__(N1, N2, N). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% nat__(Z) :- nat_zero__(Z). nat__(N) :- nat_next__(N0, N), nat__(N0). nat_lte__(Z, N) :- nat_zero__(Z), nat__(N). nat_lte__(N1, N3) :- nat_next__(N0, N1), nat_next__(N2, N3), nat_lte__(N0, N2). nat_succ__(N0, N) :- nat_next__(N0, N), nat__(N). nat_add__(Z, N, N) :- nat_zero__(Z), nat__(N). nat_add__(N1, N2, N) :- nat_next__(N0, N1), nat_next__(N2, N3), nat_add__(N0, N3, N). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% nat_zero__([]). nat_next__(N0, [N0]). nat_ground__(N) :- ground(N). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%