Modules
This module collects the most important functions from the library. These include parsing functions as well as simple term construction.
Represents a type environment for parsing and type checking. Can also be
created by using the ~e sigil from ShotDs.Hol.Sigils.
Represents free and bound variables as well as constants.
A data structure to describe a (TPTP) proof problem.
Represents a substitution.
Represents a Hol term as directed acyclic graph (DAG).
Provides a data structure for Church's simple types.
Provides definitions for common HOL types, terms and constants.
Introduces a domain specific language (DSL) for constructing HOL terms.
Contains various macros for pattern matching on HOL terms.
Provides custom Elixir sigils for inline simple type, TH0 formula parsing, TPTP problem file parsing, context parsing and a wrapper for handling context.
Contains functionality to parse a formula in TH0 syntax with full type
inference. The algorithm is similar to Hindley-Milner type systems but for
simplicity reasons without the optimizations found in algorithms J or W.
Uses Robinson's first-order unification algorithm for type inference. A
context can be specified to clear up unknown types. If terms still have
unknown type after parsing, unifies their type with type o. The main entry
point is the parse/2 function.
An exception raised when parsing fails.
Church's encoding of Booleans in simple type theory (STT).
Encodes Church numerals in simple type theory.
Contains functionality of creating, memoizing and accessing terms using an ETS cache.
Contains utility to parse files from the TPTP problem library (https://tptp.org/TPTP/) as well as custom files in TPTP's TH0 syntax.
Contains functionality for formatting terms, variable names etc.
Contains a tokenize/1 function for tokenizing a string representing a
formula in TH0 syntax or a TPTP TH0 problem file using NimbleParsec. This
is mainly used as a preprocessing step for parsing. For information about the
returned structure, see https://hexdocs.pm/nimble_parsec/NimbleParsec.html.
Utilities for efficiently traversing and transforming Hol term DAGs.
An exception raised when type inference fails.