package logtk

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

Module TypedSTerm.SubstSource

Sourceval empty : t
Sourceval mem : t -> term Var.t -> bool
Sourceval add : t -> term Var.t -> term -> t

Add new binding to substitution Fails if the variable is bound already

Sourceval find : t -> term Var.t -> term option
Sourceval find_exn : t -> term Var.t -> term
  • raises Not_found

    if the variable is not present

Sourceval rename_var : rename_binders:bool -> t -> term Var.t -> t * term Var.t
Sourceval merge : t -> t -> t
Sourceval eval : ?rename_binders:bool -> t -> term -> term
Sourceval eval_nonrec : t -> term -> term

Evaluate under substitution, but consider the substitution as not idempotent

include Interfaces.PRINT with type t := t
Sourceval to_string : t -> string