export {
    /* Platform Specific Types */
    type machine.Float16 = IEEE-754.half ~ <machine.Bits 16>;
    type machine.Float32 = IEEE-754.single ~ <machine.Bits 32>;
    type machine.Float64 = IEEE-754.double ~ <machine.Bits 64>;

    overload + = λ{
        a:ℝ ~ machine.Float16 ;
        b:ℝ ~ machine.Float16 ;
    } -> ℝ ~ machine.Float16 ↦ {
        machine.Float16.add a b;
    };

    overload * = λ{
        a:ℝ ~ machine.Float16 ;
        b:ℝ ~ machine.Float16 ;
    } -> ℝ ~ machine.Float16 ↦ {
        machine.Float16.mul a b;
    };

    let Sign = enum { Positive; Negative; };
    let Sign.Positive : <machine.Bits 1> = 0;
    let Sign.Negative : <machine.Bits 1> = 1;

    let softfloat16-mul = λ{
        {
		    a.sign: Sign
                  ~ <machine.Bits 1>
                  ;
            a.exponent: ℤ_[-14,15]
                      ~ <BiasedInt -14>
                      ~ ℤ_32
                      ~ <PosInt 2 BigEndian>
                      ~ <Seq <Digit 2>~Bit >
                      ~ <machine.Bits 5>
                      ;
            a.significand: ℤ_2048
                         ~ <PosInt 2 BigEndian>
                         ~ <Seq <Digit2> ~ Bit>
                         ~ <machine.Bits 11>
                         ;
		} : ℝ
          ~ IEEE-754.Half
          ~ <machine.Bits 16>
		  ;
		{
            b.sign: <machine.Bits 1>;
		} : ℝ ~ IEEE-754.Half ~ <machine.Bits 16> ;
    } -> result: ℝ ~ IEEE~754.Half ~ <machine.Bits 16> ↦ {

		/* 1. unify  */

		/* 2. add exponent */
		+ a.exponent b.exponent;

		/* 3. normaize */
		
		result.sign = bit-xor a.sign b.sign ;
	}
}