OCaml logo

logtk

Core types and algorithms for logic
Overview Documentation
IN THIS PACKAGE
Module Logtk . Builtin . ArithOp
exception TypeMismatch of string

This exception is raised when Arith functions are called on non-numeric values

type arith_view = [
| `Int of Z.t
| `Rat of Q.t
| `Other of t
]
val view : t -> arith_view

Arith centered view of symbols

val parse_num : string -> t
val sign : t -> int
val one_i : t
val zero_i : t
val one_rat : t
val zero_rat : t
val zero_of_ty : [< `Int | `Rat ] -> t
val one_of_ty : [< `Int | `Rat ] -> t
val is_zero : t -> bool
val is_one : t -> bool
val is_minus_one : t -> bool
val floor : t -> t
val ceiling : t -> t
val truncate : t -> t
val round : t -> t
val prec : t -> t
val succ : t -> t
val sum : t -> t -> t
val difference : t -> t -> t
val uminus : t -> t
val product : t -> t -> t
val quotient : t -> t -> t
val quotient_e : t -> t -> t
val quotient_t : t -> t -> t
val quotient_f : t -> t -> t
val remainder_e : t -> t -> t
val remainder_t : t -> t -> t
val remainder_f : t -> t -> t
val to_int : t -> t
val to_rat : t -> t
val abs : t -> t
val divides : t -> t -> bool
val gcd : t -> t -> t
val lcm : t -> t -> t
val less : t -> t -> bool
val lesseq : t -> t -> bool
val greater : t -> t -> bool
val greatereq : t -> t -> bool
val divisors : Z.t -> Z.t list

List of non-trivial strict divisors of the int.

  • returns

    if int <= 1, the list of divisors otherwise. Empty list for prime numbers, obviously.