Module Rewrite.Defined_cst

type t = defined_cst
val ty : t -> Type.t
val rules : t -> rule_set
val rules_seq : t -> rule Sequence.t
val rules_term_seq : t -> Term.rule Sequence.t
val rules_lit_seq : t -> Lit.rule Sequence.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
type t
val pp : t CCFormat.printer
val to_string : t -> string