API Reference shot_un v#0.1.9

Higher-order unification for the data structures and semantics of ShotDs.

Predicates that classify a unification problem into one of the decidable fragments handled by ShotUn.Pattern (Miller patterns) and ShotUn.Matching (Huet second-order matching), plus a helper for computing the order of a simple type.

Decidable higher-order matching for the second-order fragment.

Higher-order pattern unification (Miller 1991).

Decision-tree trace produced by ShotUn.unify/3, ShotUn.match/2 and ShotUn.pattern_unify/2 when invoked with vis: true. Each node records the rule applied, the resulting work-list, the accumulated substitutions and the deferred flex-flex pairs (pre-formatted as strings). Render the tree with ShotUn.Trace.Mermaid.render/2.

Renders a ShotUn.Trace as a Mermaid graph TD diagram.

A single node in a ShotUn.Trace decision tree.

Represents a single solution to a unification problem.