Bosatsu/Num/BinNat

public dependencies: Bosatsu/Num/Nat

Index

Types

BinNat

a natural number with three variants: Zero = 0 Odd(n) = 2n + 1 Even(n) = 2(n + 1) e.g: Zero, Odd(Zero), Even(Zero), Odd(Odd(Zero)), Even(Odd(Zero))

type BinNat

Constructors

  • Even(half1: BinNat)
  • Odd(half: BinNat)
  • Zero

Values

add_BinNat

def add_BinNat(left: BinNat, right: BinNat) -> BinNat

cmp_BinNat

def cmp_BinNat(a: BinNat, b: BinNat) -> Comparison

div2

def div2(b: BinNat) -> BinNat

divmod

def divmod(numerator: BinNat, divisor: BinNat) -> (BinNat, BinNat)

eq_BinNat

this is more efficient potentially than cmp_BinNat because at the first difference we can stop. In the worst case of equality, the cost is the same.

def eq_BinNat(a: BinNat, b: BinNat) -> Bool

exp

def exp(base: BinNat, power: BinNat) -> BinNat

is_even

def is_even(b: BinNat) -> Bool

mul2

multiply by 2

def mul2(b: BinNat) -> BinNat

next

Return the next number

def next(b: BinNat) -> BinNat

prev

Return the previous number if the number is > 0, else return 0

def prev(b: BinNat) -> BinNat

sub_BinNat

def sub_BinNat(left: BinNat, right: BinNat) -> BinNat

sub_Option

def sub_Option(left: BinNat, right: BinNat) -> Option[BinNat]

times_BinNat

multiply two BinNat together

def times_BinNat(left: BinNat, right: BinNat) -> BinNat

to_BinNat

Convert a built in integer to a BinNat. <= 0 is converted to 0

def to_BinNat(n: Int) -> BinNat

to_Int

Convert a BinNat into the equivalent Int this is O(log(b)) operation

def to_Int(b: BinNat) -> Int

to_Nat

This is an O(b) operation

def to_Nat(b: BinNat) -> Bosatsu/Num/Nat::Nat
The source code for this page can be found here.