mk: even-i / odd-i — host-arithmetic parity goals
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 27s

Two-line definitions over project + host even?/odd?. Ground-only — no
relational behaviour, but they pair cleanly with membero for filtered
enumeration:
  (fresh (x) (membero x (list 1 2 3 4 5 6)) (even-i x) (== q x))
    -> (2 4 6)

5 new tests, 416/416 cumulative.
This commit is contained in:
2026-05-08 11:49:47 +00:00
parent 4d861575df
commit d992788a03
3 changed files with 23 additions and 0 deletions

View File

@@ -60,3 +60,11 @@
(define stringo (fn (x) (project (x) (if (string? x) succeed fail))))
(define symbolo (fn (x) (project (x) (if (symbol? x) succeed fail))))
(define
even-i
(fn (n) (project (n) (if (and (number? n) (even? n)) succeed fail))))
(define
odd-i
(fn (n) (project (n) (if (and (number? n) (odd? n)) succeed fail))))

View File

@@ -86,4 +86,18 @@
(== q x)))
(list 1 2))
(mk-test "even-i-pos" (run* q (even-i 4)) (list (make-symbol "_.0")))
(mk-test "even-i-neg" (run* q (even-i 5)) (list))
(mk-test "odd-i-pos" (run* q (odd-i 7)) (list (make-symbol "_.0")))
(mk-test "odd-i-neg" (run* q (odd-i 4)) (list))
(mk-test
"even-i-filter"
(run* q (fresh (x) (membero x (list 1 2 3 4 5 6)) (even-i x) (== q x)))
(list 2 4 6))
(mk-tests-run!)