package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct