package logtk

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

Module Rewrite.RuleSource

Sourcetype t = rule
Sourceval of_term : Term.Rule.t -> t
Sourceval of_lit : Lit.Rule.t -> t
Sourceval proof : t -> proof
Sourceval as_proof : t -> Proof.t
Sourceval lit_as_proof_parent_subst : Subst.Renaming.t -> Subst.t -> Lit.Rule.t Scoped.t -> Proof.parent

Helper for clause rewriting

Sourceval set_as_proof_parents : Term.Rule_inst_set.t -> Proof.parent list

Proof parents from a set of rules instances

Sourceval make_lit : proof:Proof.t -> Literal.t -> Literal.t list list -> t

Make a literal rule

OCaml

Innovation. Community. Security.