mk: lasto + init-o — last and not-last list relations
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 52s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 52s
lasto: x is the final element of l. Direct base case (l = (x)) plus recurse-on-cdr. init-o: init is l without its last element. Base case for singleton: (== init ()). Otherwise recurse, threading the head through to the init result via conso. Together with appendo, the round-trip init append (list last) = l holds, which is exercised by an end-to-end test. 8 new tests, 344/344 cumulative.
This commit is contained in:
@@ -156,3 +156,19 @@
|
||||
(conde
|
||||
((fresh (a d) (conso a d l) (rel a)))
|
||||
((fresh (a d) (conso a d l) (someo rel d))))))
|
||||
|
||||
(define
|
||||
lasto
|
||||
(fn
|
||||
(l x)
|
||||
(conde
|
||||
((conso x (list) l))
|
||||
((fresh (a d) (conso a d l) (lasto d x))))))
|
||||
|
||||
(define
|
||||
init-o
|
||||
(fn
|
||||
(l init)
|
||||
(conde
|
||||
((fresh (x) (conso x (list) l) (== init (list))))
|
||||
((fresh (a d d-init) (conso a d l) (conso a d-init init) (init-o d d-init))))))
|
||||
|
||||
Reference in New Issue
Block a user