Initial commit

Changes

2 changed files (+104/-0)

• Main.lean (new)
  • @@ -0,0 +1,48 @@
    + import Std.Data.HashMap + + inductive Typ + | var : String → Typ + | fn : Typ → Typ → Typ + | prod : Typ → Typ → Typ + | sum : Typ → Typ → Typ + deriving BEq + + inductive Term + | var : Typ → String → Term + | fn : Typ → String → Term → Term + | app : Typ → Term → Term → Term + | prod : Typ → Term → Term → Term + | sum : Typ → Term → Term → Term + + def Term.getTyp : Term → Typ + | .var τ _ => τ + | .fn τ _ _ => τ + | .app τ _ _ => τ + | .prod τ _ _ => τ + | .sum τ _ _ => τ + + def check (env : Std.HashMap String Typ) : Term → Bool + | .var τ x => + (· == τ) <$> env[x]? |>.getD false + | .fn τ x b => + match τ with + | .fn α β => b.getTyp == β && check (env.insert x α) b + | _ => false + | .app τ f x => + match f.getTyp with + | .fn α β => x.getTyp == α && β == τ && check env f && check env x + | _ => false + | .prod τ x y => + match τ with + | .prod α β => + x.getTyp == α && y.getTyp == β && check env x && check env y + | _ => false + | .sum τ x y => + match τ with + | .sum α β => + x.getTyp == α && y.getTyp == β && check env x && check env y + | _ => false + + def ab_imp_ba := Term.fn (.fn (.var "A") (.fn (.var "B") (.prod (.var "B") (.var "A")))) "a" (.fn (.fn (.var "B") (.prod (.var "B") (.var "A"))) "b" (.prod (.prod (.var "B") (.var "A")) (.var (.var "B") "b") (.var (.var "A") "a"))) + + #eval check (.ofList []) ab_imp_ba
• main.lurk (new)
  • @@ -0,0 +1,56 @@
    + !(def typ (lambda (x) (car (cdr x)))) + + !(def funtl (lambda (x) (car (cdr (typ x))))) + + !(def funtr (lambda (x) (car (cdr (cdr (typ x)))))) + + !(def funv (lambda (x) (car (cdr (cdr x))))) + + !(def funb (lambda (x) (car (cdr (cdr (cdr x)))))) + + !(def check (lambda (x) + (if (eq (car x) "fun") + (if (eq (car (typ x)) "fun") + (if (eq (car ())) + + + let ((car (cdr (cdr x))) (car (cdr (car (cdr x))))) + (check )) + nil + + + ) + + + ) (if (eq (car x) "app") ( + ) + + (if (eq (car x) "prod")) ( + ) + (if (eq (car x) "sum")) ()) + nil)))) + + + + (check + (list "fun" (list "fun" "A" (list "fun" "B" (list "prod" "B" "A"))) "a" + (list "fun" (list "fun" "B" (cons "B" "A")) "b" + (list "prod" (list "list" "B" "A") "b" "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)