package lambdapi

  1. Overview
  2. Docs
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type

This module provides a function to translate a signature to the HRS format used in the confluence competition.

print_sym ppf s outputs the fully qualified name of s to ppf. The name is prefixed by "c_", and modules are separated with "_", not ".".

val print_term : bool -> Core.Term.term Lplib.Base.pp

print_patt ppf p outputs TPDB format corresponding to the pattern p, to ppf.

val print_rule : Format.formatter -> Core.Term.term -> Core.Term.term -> unit

print_rule ppf lhs rhs outputs the rule declaration lhs->rhs to ppf

val print_sym_rule : Format.formatter -> Core.Term.sym -> Core.Term.rule -> unit

print_sym_rule ppf s r outputs the rule declaration corresponding r (on the symbol s), to ppf.

val to_HRS : Format.formatter -> Core.Sign.t -> unit

to_HRS ppf sign outputs a TPDB representation of the rewriting system of the signature sign to ppf.