Structure Arbrat

Source File Identifier index Theory binding index 
signature Arbrat =
sig

  eqtype rat

  type num = Arbnum.num
  type aint = Arbint.int

  val zero       : rat
  val one        : rat
  val two        : rat
  val numerator  : rat -> aint
  val denominator: rat -> num

  val toString   : rat -> string
  val fromString : string -> rat  (* only integral forms *)

  val fromInt    : Int.int -> rat
  val fromAInt   : aint -> rat
  val fromNat    : num -> rat

  val toAInt     : rat -> aint
  val toInt      : rat -> Int.int
  val toNat      : rat -> num

  val +          : (rat * rat) -> rat
  val -          : (rat * rat) -> rat
  val *          : (rat * rat) -> rat
  val /          : (rat * rat) -> rat
  val inv        : rat -> rat
  val negate     : rat -> rat
  val ~          : rat -> rat
  val abs        : rat -> rat

  val <          : rat * rat -> bool
  val <=         : rat * rat -> bool
  val >          : rat * rat -> bool
  val >=         : rat * rat -> bool

  val compare    : rat * rat -> order
  val min        : rat * rat -> rat
  val max        : rat * rat -> rat

  val floor      : rat -> aint
  val ceil       : rat -> aint

  val pp_rat     : rat -> HOLPP.pretty

end
Source File Identifier index Theory binding index

HOL 4, Kananaskis-13