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