logtk

Core types and algorithms for logic
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library logtk
type t = defined_cst
val ty : t -> Type.t
val rules : t -> rule_set
val rules_seq : t -> rule Iter.t
val rules_term_seq : t -> Term.rule Iter.t
val rules_lit_seq : t -> Lit.rule Iter.t
val defined_positions : t -> Defined_pos.Arr.t
val level : t -> int
val declare : ?level:int -> ID.t -> rule_set -> t

declare id rules makes id a defined constant with the given (initial) set of rules

  • raises Invalid_argument

    if the ID is already a skolem or a constructor, or if the list of rules is empty

val declare_or_add : ID.t -> rule -> unit

declare_or_add id rule defines id if it's not already a defined constant, and add rule to it

val declare_proj : proof:Proof.t -> Ind_ty.projector -> unit

Declare an inductive projector

val declare_cstor : proof:Proof.t -> Ind_ty.constructor -> unit

Add a rewrite rule cstor (proj1 x)…(projn x) --> x

val add_term_rule : t -> Term.rule -> unit
val add_term_rule_l : t -> Term.rule list -> unit
val add_lit_rule : t -> Lit.rule -> unit
val add_lit_rule_l : t -> Lit.rule list -> unit
val add_eq_rule : Lit.rule -> unit

Add a rule on (dis)equality

val add_eq_rule_l : Lit.rule list -> unit
include Interfaces.PRINT with type t := t
val to_string : t -> string