Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-10-06 04:17:14 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #53 from Kindelia/revert-52-hole-fix

Browse Source 
Revert "Fix hole equality" (temporarily)
This commit is contained in:
Victor Taelin 2022-08-23 14:41:45 -03:00 committed by GitHub
commit f7447ced16
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/checker.hvm
View File

@ -809,17 +809,11 @@ Line = (String.cons 10 String.nil)
(Equal a (Hlp b.orig)) =
(Checker.done True)
// Hole equality #0
(Equal (Hol a.orig a.numb) (Hol b.orig b.numb)) =
(U60.if (== a.numb b.numb)
(Checker.done True)
(Equal.hol a.orig a.numb (Hol b.orig b.numb)))
// Hol equality #1
// Hol equality #0
(Equal (Hol a.orig a.numb) b) =
(Equal.hol a.orig a.numb b)
// Hol equality #2
// Hol equality #1
(Equal a (Hol b.orig b.numb)) =
(Equal.hol b.orig b.numb a)