CurryInfo: binint-3.1.0 / Data.BinInt.-^
definition: 
|
(-^) :: Nat -> Nat -> BinInt IHi -^ y = inc (Neg y) -- 1-n = 1+(-n) x@(O _) -^ IHi = Pos (pred x) -- (O x) -^ (O y) = mult2 (x -^ y) (O x) -^ (I y) = dec (mult2 (x -^ y)) (I x) -^ IHi = Pos (O x) (I x) -^ (O y) = inc (mult2 (x -^ y)) -- 2*n+1 - 2*m = 1+2*(n-m) (I x) -^ (I y) = mult2 (x -^ y) -- 2*n+1 - (2*m+1) = 2*(n-m) |
|
demand:
|
argument 1 |
|
deterministic:
|
deterministic operation |
|
documentation:
|
Subtraction |
|
failfree:
|
(_, _) |
|
indeterministic:
|
referentially transparent operation |
|
infix:
|
no fixity defined |
|
iotype:
|
{({IHi},_) |-> {Neg,Pos,Zero} || ({O},{IHi}) |-> {Pos} || ({O},{O}) |-> {Neg,Pos,Zero} || ({O},{I}) |-> {Neg,Pos,Zero} || ({I},{IHi}) |-> {Pos} || ({I},{O}) |-> {Neg,Pos,Zero} || ({I},{I}) |-> {Neg,Pos,Zero}}
|
|
name:
|
-^ |
|
precedence:
|
no precedence defined |
|
result-values:
|
{Neg,Pos,Zero}
|
|
signature:
|
Nat -> Nat -> BinInt |
|
solution-complete:
|
operation might suspend on free variables |
|
terminating:
|
yes |
|
totally-defined:
|
possibly non-reducible on same data term |