Changes
2 changed files (+13/-26)
-
-
@@ -6,3 +6,8 @@ How to install Lurk:3. `cargo install --path . --locked` Lurk docs: https://docs.argument.xyz/ Lurk gotchas: Q: Difference between `(cons 1 2)` and `(list 1 2)`? A: `(cons 1 2)` reduces to `(1 . 2)` and `(list 1 2)` reduces to `(1 2)` which is equivalent to `(1 . (2))`. Basically, `(cdr '(1 . 2))` returns `2` while `cdr '(1 2)` returns `(2)`.
-
-
-
@@ -9,37 +9,19 @@; Boolean and !(def and (lambda (x y) (if x (if y t nil) nil))) !(def check (lambda (env typ term) ; NEED defrec instead of def for recursive functions !(defrec check (lambda (env typ term) (if (eq (car term) "var") (eq typ (eval (cdr term) (env))) (eq typ (eval (cdr term) env)) (if (and (eq (car typ) "fn") (eq (car term) "lam")) (and (eq (arg2 typ) (arg21 term)) (eval '(let (( (arg1 typ))) (check env (arg2 typ) (arg22 term)))) (env)) (and (eq (arg2 typ) (arg21 term)) (check (eval (list 'let (list (list (arg1 term) (list 'quote (arg1 typ)))) '(current-env)) env) (arg21 term) (arg22 term))) nil)))) ; Autogenerated by Main.lean !(def a_imp_a (cons (list "fn" (cons "new" "A") (cons "new" "A")) (list "lam" 'a (cons (cons "new" "A") (cons "var" 'a))))) !(def typ (car a_imp_a)) (check (empty-env) (car a_imp_a) (cdr a_imp_a)) !(def term (cdr a_imp_a)) (check empty-env (car a_imp_a) (cdr a_imp_a)) ; 123 ; (+ 1 1) ; !(def square (lambda (x) (* x x))) ; (square 8) ; !(def make-adder ; (lambda (n) ; (lambda (x) ; (+ x n)))) ; !(def five-plus ; (make-adder 5)) ; (five-plus 3) ; !(def env (empty-env)) ; !(def typ (car a_imp_a)) ; !(def term (cdr a_imp_a))
-