/usr/share/axiom-20170501/src/algebra/FRETRCT.spad is in axiom-source 20170501-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 | )abbrev category FRETRCT FullyRetractableTo
++ Author: Manuel Bronstein
++ Date Created: March 1990
++ Date Last Updated: 9 April 1991
++ Description:
++ A is fully retractable to B means that A is retractable to B and
++ if B is retractable to the integers or rational numbers then so is A.
++ In particular, what we are asserting is that there are no integers
++ (rationals) in A which don't retract into B.
FullyRetractableTo(S) : Category == SIG where
S : Type
SIG ==> RetractableTo(S) with
if (S has RetractableTo Integer) then RetractableTo Integer
if (S has RetractableTo Fraction Integer) then
RetractableTo Fraction Integer
add
if not(S is Integer) then
if (S has RetractableTo Integer) then -- induction
coerce(n:Integer):% == n::S::%
retract(r:%):Integer == retract(retract(r)@S)
retractIfCan(r:%):Union(Integer, "failed") ==
(u:= retractIfCan(r)@Union(S,"failed")) case "failed"=> "failed"
retractIfCan(u::S)
if not(S is Fraction Integer) then
if (S has RetractableTo Fraction Integer) then -- induction
coerce(n:Fraction Integer):% == n::S::%
retract(r:%):Fraction(Integer) == retract(retract(r)@S)
retractIfCan(r:%):Union(Fraction Integer, "failed") ==
(u:=retractIfCan(r)@Union(S,"failed")) case "failed"=>"failed"
retractIfCan(u::S)
|