HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-10-03 18:27:13 +03:00
Code Issues Packages Projects Releases Wiki Activity

Add unification polishments to kind2.hvm2

Browse Source
This commit is contained in:
LunaAmora 2024-03-18 17:20:39 -03:00
parent 3c89c73d2f
commit 5008491fe9
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/kind2.hvm2
View File

@ -465,12 +465,12 @@ termIdenticalGo a (Ann chk bVal bTyp) dep =
(termIdentical a bVal dep)
// termIdenticalGo (Met aUid aSpn) (Met bUid bSpn) dep =
// envPure (eq aUid bUid)
termIdenticalGo (Met aUid aSpn) b dep =
// traceShow (stringJoin ["unify: ", (u60Show aUid), " x=", (termShow (Met aUid aSpn) dep), " t=", (termShow b dep)])
(termUnify aUid aSpn b dep)
termIdenticalGo a (Met bUid bSpn) dep =
// traceShow (stringJoin ["unify: ", (u60Show bUid), " x=", (termShow (Met bUid bSpn) dep), " t=", (termShow a dep)])
(termUnify bUid bSpn a dep)
termIdenticalGo (Met aUid aSpn) b dep =
// traceShow (stringJoin ["unify: ", (u60Show aUid), " x=", (termShow (Met aUid aSpn) dep), " t=", (termShow b dep)])
(termUnify aUid aSpn b dep)
termIdenticalGo (Hol aNam aCtx) b dep =
(envPure True)
termIdenticalGo a (Hol bNam bCtx) dep =