12 lines
172 B
Text
12 lines
172 B
Text
pattern:
|
|
@eq.{?l_3876} ?m_3879 ?m_3882 ?m_3885
|
|
term to unify:
|
|
@eq.{1} nat a b
|
|
unification results using whnf:
|
|
nat
|
|
a
|
|
b
|
|
unification results using get_assignment:
|
|
nat
|
|
a
|
|
b
|