Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

REAL_INT_RAT_CONV : conv

SYNOPSIS

Convert basic rational constant of real type to canonical form.

DESCRIPTION

When applied to a term that is a rational constant of type :real, REAL_INT_RAT_CONV converts it to an explicit ratio &p / &q or -- &p / &q; q is always there, even if it is 1.

FAILURE CONDITIONS

Never fails; simply has no effect if it is not applied to a suitable constant.

EXAMPLE

  # REAL_INT_RAT_CONV `&22 / &7`;;
  val it : thm = |- &22 / &7 = &22 / &7

  # REAL_INT_RAT_CONV `&42`;;
  val it : thm = |- &42 = &42 / &1

  # REAL_INT_RAT_CONV `#3.1415926`;;
  val it : thm = |- #3.1415926 = &31415926 / &10000000

USES

Mainly for internal use as a preprocessing step in rational-number calculations.

SEE ALSO

REAL_RAT_REDUCE_CONV.