package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = rule
val lhs : t -> term
val rhs : t -> term
val vars : t -> Term.VarSet.t
val vars_l : t -> Type.t HVar.t list
val head_id : t -> ID.t
val args : t -> term list
val arity : t -> int
val proof : t -> proof
val as_lit : t -> Literal.t
val make_const : proof:Proof.t -> ID.t -> Type.t -> term -> t

make_const id ty rhs is the same as T.const id ty --> rhs

val make : proof:Proof.t -> ID.t -> Type.t -> term list -> term -> t

make id ty args rhs is the same as T.app (T.const id ty) args --> rhs

include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
val compare : t -> t -> int
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