mk: prefixo + suffixo — appendo-derived sublist relations
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 40s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 40s
Two-line definitions over appendo: (prefixo p l) ≡ ∃rest. (appendo p rest l) (suffixo s l) ≡ ∃front. (appendo front s l) Both enumerate all prefixes/suffixes when called with a fresh first arg, and serve as decision relations when called with both grounded. 9 new tests, 398/398 cumulative.
This commit is contained in:
@@ -68,6 +68,11 @@
|
||||
|
||||
(define palindromeo (fn (l) (fresh (rev) (reverseo l rev) (== l rev))))
|
||||
|
||||
(define prefixo (fn (p l) (fresh (rest) (appendo p rest l))))
|
||||
|
||||
(define suffixo (fn (s l) (fresh (front) (appendo front s l))))
|
||||
|
||||
|
||||
(define
|
||||
lengtho
|
||||
(fn
|
||||
@@ -84,7 +89,6 @@
|
||||
((conso a l p))
|
||||
((fresh (h t pt) (conso h t l) (conso h pt p) (inserto a t pt))))))
|
||||
|
||||
|
||||
(define
|
||||
permuteo
|
||||
(fn
|
||||
|
||||
Reference in New Issue
Block a user