logtk

Core types and algorithms for logic
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library logtk
Module Logtk . Literal . View

Specific views

val as_eqn : t -> (term * term * bool) option
val get_eqn : t -> Position.t -> (term * term * bool) option

View of a Prop or Equation literal, oriented by the position. If the position selects its left term, return l, r, otherwise r, l. for propositions it will always be p, true.

  • returns

    None for other literals

  • raises Invalid_argument

    if the position doesn't match the literal.

val get_lhs : t -> term option
val get_rhs : t -> term option