32 lines
767 B
Text
32 lines
767 B
Text
(forall (car' cdr) (car (cons car' cdr)) car')
|
|
(forall (car cdr') (cdr (cons car cdr')) cdr')
|
|
|
|
(forall (a as bs) (++ (cons a as) bs) (cons a (++ as bs)))
|
|
(forall (bs) (++ () bs) bs)
|
|
|
|
(forall (f acc) (foldr f acc ()) acc)
|
|
(forall (f acc x xs) (foldr f acc (cons x xs)) (foldr f (app f acc x) xs))
|
|
|
|
(forall (x xs) (snoc x xs) (++ xs (cons x ())))
|
|
|
|
(def (reverse ()) ())
|
|
(forall (x xs) (reverse (cons x xs)) (snoc x (reverse xs)))
|
|
|
|
(forall (bindings body) (@ bindings body) (lambda-like lambda bindings body))
|
|
(forall (var body arg) ((lambda var body) arg) (let var arg body))
|
|
|
|
(forall (lam bindings body)
|
|
(lambda-like' lam bindings body)
|
|
(unquote
|
|
(foldr
|
|
(@ (acc' x')
|
|
(quote (lam x' acc'))
|
|
)
|
|
body
|
|
(reverse (quote bindings))
|
|
)
|
|
)
|
|
)
|
|
|
|
(lambda-like' -> (a b c) d)
|