CurryInfo: binint-3.0.0 / Data.BinInt.+^

 
(+^) :: Nat -> Nat -> Nat
IHi +^ y   = succ y           -- 1  +  n   = n + 1
O x +^ IHi = I x              -- 2*n + 1   = 2*n + 1
O x +^ O y = O (x +^ y)       -- 2*m + 2*n = 2*(m+n)
O x +^ I y = I (x +^ y)
I x +^ IHi = O (succ x)
I x +^ O y = I (x +^ y)
I x +^ I y = O (succ x +^ y)

 arguments 1 2

 deterministic operation

 
Addition, O(max (m, n))

 (_, _)

 referentially transparent operation

 no fixity defined

 {({IHi},_) |-> {I,O} || ({O},{IHi}) |-> {I} || ({O},{O}) |-> {O} || ({O},{I}) |-> {I} || ({I},{IHi}) |-> {O} || ({I},{O}) |-> {I} || ({I},{I}) |-> {O}}

 +^

 no precedence defined

 {I,O}

 Nat -> Nat -> Nat

 operationally complete operation

 yes

 reducible on all ground data terms