mrs-unify 0.1.8

First-order unification and matching algorithms
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

# mrs-unify

First-order term unification and one-way matching.

## Key API

```rust
// Most-general unifier (Robinson's algorithm, with occurs check)
unify(s: &Term, t: &Term) -> Result<Substitution, UnifyError>

// One-way matching (pattern variables only)
match_term(pattern: &Term, target: &Term) -> Result<Substitution, UnifyError>

// Failure reasons
enum UnifyError { SymbolClash, ArityMismatch, OccursCheck }
```

## Dependencies

`mrs-core`