package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Rewrite.Defined_cstSource

Sourceval ty : t -> Type.t
Sourceval rules : t -> rule_set
Sourceval rules_seq : t -> rule Iter.t
Sourceval rules_term_seq : t -> Term.rule Iter.t
Sourceval rules_lit_seq : t -> Lit.rule Iter.t
Sourceval defined_positions : t -> Defined_pos.Arr.t
Sourceval level : t -> int
Sourceval 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

Sourceval 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

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

Declare an inductive projector

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

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

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

Add a rule on (dis)equality

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