equal
deleted
inserted
replaced
610 | calc "Groups.minus_class.minus" (n1, n2) = n1-n2 |
610 | calc "Groups.minus_class.minus" (n1, n2) = n1-n2 |
611 | calc "Groups.times_class.times" (n1, n2) = n1*n2 |
611 | calc "Groups.times_class.times" (n1, n2) = n1*n2 |
612 | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2 |
612 | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2 |
613 | calc "Atools.pow"(n1, n2) = power n1 n2 |
613 | calc "Atools.pow"(n1, n2) = power n1 n2 |
614 | calc op_ _ = error ("calc: operator = "^op_^" not defined");-----*) |
614 | calc op_ _ = error ("calc: operator = "^op_^" not defined");-----*) |
615 fun calc_equ "op <" (n1, n2) = n1 < n2 |
615 fun calc_equ "Orderings.ord_class.less" (n1, n2) = n1 < n2 |
616 | calc_equ "op <=" (n1, n2) = n1 <= n2 |
616 | calc_equ "Orderings.ord_class.less_eq" (n1, n2) = n1 <= n2 |
617 | calc_equ op_ _ = |
617 | calc_equ op_ _ = |
618 error ("calc_equ: operator = "^op_^" not defined"); |
618 error ("calc_equ: operator = "^op_^" not defined"); |
619 fun sqrt (n:int) = if n < 0 then 0 |
619 fun sqrt (n:int) = if n < 0 then 0 |
620 (*FIXME ~~~*) else (trunc o Math.sqrt o Real.fromInt) n; |
620 (*FIXME ~~~*) else (trunc o Math.sqrt o Real.fromInt) n; |
621 |
621 |