28 lines
911 B
Text
28 lines
911 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))
|
||
|
|
|
||
|
|
; could be sugared much better
|
||
|
|
; also this is just map? ugh this is just map
|
||
|
|
; defeats the whoel point KLFJkljfksdljf 1:24 brain
|
||
|
|
(forall (var body) (for var () body) ())
|
||
|
|
(forall (var x xs body) (for var (cons x xs) body) (cons (let var x body) (for var xs body)))
|
||
|
|
(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 binding)
|
||
|
|
(quote (lam binding acc)))
|
||
|
|
body
|
||
|
|
(quote bindings))))
|
||
|
|
|
||
|
|
(lambda-like' -> (a b c) d)
|