# shot_un v0.2.1 - Table of Contents

> Higher-order pre-unification, Miller pattern unification, and second-order matching for ShotDs terms.

## Pages

- [ShotUn](readme.md)
- [Demo of the ShotUn Package](demo.md)

## Modules

- [ShotUn](ShotUn.md): Higher-order unification for the data structures and semantics of
[ShotDs](https://hexdocs.pm/shot_ds/readme.html).
- [ShotUn.Fragment](ShotUn.Fragment.md): 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.

- [ShotUn.Matching](ShotUn.Matching.md): Decidable higher-order matching for the second-order fragment.
- [ShotUn.Pattern](ShotUn.Pattern.md): Higher-order pattern unification (Miller 1991).
- [ShotUn.Trace](ShotUn.Trace.md): 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`.
- [ShotUn.Trace.Mermaid](ShotUn.Trace.Mermaid.md): Renders a `ShotUn.Trace` as a Mermaid `graph TD` diagram.
- [ShotUn.Trace.Node](ShotUn.Trace.Node.md): A single node in a `ShotUn.Trace` decision tree.
- [ShotUn.UnifSolution](ShotUn.UnifSolution.md): Represents a single solution to a unification problem.