| 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 |