package logtk

  1. Overview
  2. Docs
On This Page
  1. Specific views
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

val get_arith : t -> Int_lit.t option

Extract an arithmetic literal

val focus_arith : t -> Position.t -> Int_lit.Focus.t option

Focus on a specific term in an arithmetic literal. The focused term is removed from its monome, and its coefficient is returned.

val unfocus_arith : Int_lit.Focus.t -> t
val get_rat : t -> Rat_lit.t option

Extract an arithmetic literal

val focus_rat : t -> Position.t -> Rat_lit.Focus.t option

Focus on a specific term in an arithmetic literal. The focused term is removed from its monome, and its coefficient is returned.

val unfocus_rat : Rat_lit.Focus.t -> t