diff --git a/.gitignore b/.gitignore
index 7ecfa581fb..e83a23ac8c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,6 +12,7 @@
 .sbt
 .npm
 .node-gyp
+.elan
 */experiments
 node_modules
 */notes
diff --git a/IMPLS.yml b/IMPLS.yml
index 02a8056ce8..c6c8c3382b 100644
--- a/IMPLS.yml
+++ b/IMPLS.yml
@@ -49,6 +49,7 @@ IMPL:
   - {IMPL: julia}
   - {IMPL: kotlin}
   - {IMPL: latex3, NO_PERF: 1, NO_SELF_HOST: 1, SLOW: 1}
+  - {IMPL: lean}
   - {IMPL: livescript}
   - {IMPL: logo}
   - {IMPL: lua}
diff --git a/Makefile.impls b/Makefile.impls
index 32fe439ca6..ee9699e560 100644
--- a/Makefile.impls
+++ b/Makefile.impls
@@ -36,7 +36,7 @@ wasm_MODE = wasmtime
 
 IMPLS = ada ada.2 awk bash basic bbc-basic c c.2 chuck clojure coffee common-lisp cpp crystal cs d dart \
 	elisp elixir elm erlang es6 factor fantom fennel forth fsharp go groovy gnu-smalltalk \
-	guile haskell haxe hy io janet java java-truffle js jq julia kotlin latex3 livescript logo lua make mal \
+	guile haskell haxe hy io janet java java-truffle js jq julia kotlin latex3 lean livescript logo lua make mal \
 	matlab miniMAL nasm nim objc objpascal ocaml perl perl6 php picolisp pike plpgsql \
 	plsql powershell prolog ps purs python python.2 r racket rexx rpython ruby ruby.2 rust scala scheme skew sml \
 	swift swift3 swift4 swift5 tcl ts vala vb vbs vhdl vimscript wasm wren yorick xslt zig
@@ -149,6 +149,7 @@ jq_STEP_PROG =               impls/jq/$($(1)).jq
 julia_STEP_TO_PROG =         impls/julia/$($(1)).jl
 kotlin_STEP_TO_PROG =        impls/kotlin/$($(1)).jar
 latex3_STEP_TO_PROG =        impls/latex3/$($(1)).tex
+lean_STEP_TO_PROG =          impls/lean/$($(1))
 livescript_STEP_TO_PROG =    impls/livescript/$($(1)).js
 logo_STEP_TO_PROG =          impls/logo/$($(1)).lg
 lua_STEP_TO_PROG =           impls/lua/$($(1)).lua
diff --git a/impls/lean/.gitignore b/impls/lean/.gitignore
new file mode 100644
index 0000000000..bfb30ec8c7
--- /dev/null
+++ b/impls/lean/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/impls/lean/Dockerfile b/impls/lean/Dockerfile
new file mode 100644
index 0000000000..ff368bcbb6
--- /dev/null
+++ b/impls/lean/Dockerfile
@@ -0,0 +1,35 @@
+FROM ubuntu:24.04
+LABEL org.opencontainers.image.source=https://github.com/kanaka/mal
+LABEL org.opencontainers.image.description="mal test container: lean"
+
+##########################################################
+# General requirements for testing or common across many
+# implementations
+##########################################################
+
+RUN apt-get -y update
+
+# Required for running tests
+RUN apt-get -y install make python3
+RUN ln -fs /usr/bin/python3 /usr/local/bin/python
+
+RUN mkdir -p /mal
+
+WORKDIR /mal
+
+##########################################################
+# Specific implementation requirements
+##########################################################
+
+RUN apt-get -y install curl git-core
+
+# install lean toolchain manager
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y -v
+
+RUN /root/.elan/bin/elan default leanprover/lean4:stable
+
+# non-root users must have access
+RUN mv /root/.elan/bin/lake /usr/local/bin/
+
+# lake needs to create $HOME/.elan
+ENV HOME=/mal
diff --git a/impls/lean/LeanMal.lean b/impls/lean/LeanMal.lean
new file mode 100644
index 0000000000..d8cccf1d66
--- /dev/null
+++ b/impls/lean/LeanMal.lean
@@ -0,0 +1,2 @@
+-- This module serves as the root of the `Mal` library.
+-- Import modules here that should be built as part of the library.
diff --git a/impls/lean/LeanMal/core.lean b/impls/lean/LeanMal/core.lean
new file mode 100644
index 0000000000..8c6c4b23f4
--- /dev/null
+++ b/impls/lean/LeanMal/core.lean
@@ -0,0 +1,621 @@
+import Lean
+import LeanMal.types
+import LeanMal.reader
+
+universe u
+
+def sum (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x + y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x + y))
+  | _                                    => throw (IO.userError "+ operator not supported")
+
+def sub (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x - y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x - y))
+  | _                                    => throw (IO.userError "- operator not supported")
+
+def mul (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x * y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x * y))
+  | _                                    => throw (IO.userError "* operator not supported")
+
+def div (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x / y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x / y))
+  | _                                    => throw (IO.userError "/ operator not supported")
+
+def ltInternal (first: Types) (second: Types) (orEq: Bool) : Bool :=
+  match first, second with
+  | Types.intVal n, Types.intVal v => n < v || (if orEq then n == v else false)
+  | Types.intVal n, Types.floatVal v => (Float.ofInt n) < v || (if orEq then (Float.ofInt n) == v else false)
+  | Types.floatVal n, Types.floatVal v => n < v || (if orEq then n == v else false)
+  | Types.floatVal n, Types.intVal v => n < (Float.ofInt v) || (if orEq then n == (Float.ofInt v) else false)
+  | Types.strVal n, Types.strVal v => n < v || (if orEq then n == v else false)
+  | _, _ => false
+
+def lt (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "eq: 2 arguments required")
+  else
+    let first := lst[0]!
+    let second := lst[1]!
+    let res := ltInternal first second false
+    return (env, Types.boolVal res)
+
+def lte (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "eq: 2 arguments required")
+  else
+    let first := lst[0]!
+    let second := lst[1]!
+    let res := ltInternal first second true
+    return (env, Types.boolVal res)
+
+def gtInternal (first: Types) (second: Types) (orEq: Bool) : Bool :=
+  match first, second with
+  | Types.intVal n, Types.intVal v => n > v || (if orEq then n == v else false)
+  | Types.intVal n, Types.floatVal v => (Float.ofInt n) > v || (if orEq then (Float.ofInt n) == v else false)
+  | Types.floatVal n, Types.floatVal v => n > v || (if orEq then n == v else false)
+  | Types.floatVal n, Types.intVal v => n > (Float.ofInt v) || (if orEq then n == (Float.ofInt v) else false)
+  | Types.strVal n, Types.strVal v => n > v || (if orEq then n == v else false)
+  | _, _ => false
+
+def gt (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "eq: 2 arguments required")
+  else
+    let first := lst[0]!
+    let second := lst[1]!
+    let res := gtInternal first second false
+    return (env, Types.boolVal res)
+
+def gte (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "eq: 2 arguments required")
+  else
+    let first := lst[0]!
+    let second := lst[1]!
+    let res := gtInternal first second true
+    return (env, Types.boolVal res)
+
+mutual
+  partial def eqList (n: List Types) (v: List Types) (strict: Bool) : Bool :=
+    match n, v with
+    | [], [] => true
+    | [], _ => false
+    | _, [] => false
+    | a :: nrest, b :: vrest =>
+      if !(eqInternal a b strict) then false
+      else eqList nrest vrest strict
+
+  -- partial def eqDictKeys (k1: List KeyType) (k2: List KeyType) : Bool :=
+  --   match k1, k2 with
+  --   | KeyType.strKey x,
+
+  partial def eqDict (n: Dict) (v: Dict) (strict: Bool) : Bool :=
+    match n, v with
+    | Dict.empty, Dict.empty => true
+    | d1, d2 =>
+      let keys1 := d1.keys
+      let keys2 := d2.keys
+      if keys1.length != keys2.length then false
+      else
+        keys1.all (fun k =>
+          match (d1.get k, d2.get k) with
+          | (some (_, v1), some (_, v2)) => eqInternal v1 v2 strict
+          | _ => false)
+
+  partial def eqInternal (first: Types) (second: Types) (strict: Bool) : Bool :=
+    match first, second with
+    | Types.intVal n, Types.intVal v => n == v
+    | Types.intVal n, Types.floatVal v => if strict then false else (Float.ofInt n) == v
+    | Types.floatVal n, Types.floatVal v => n == v
+    | Types.floatVal n, Types.intVal v => if strict then false else n == (Float.ofInt v)
+    | Types.strVal n, Types.strVal v => n == v
+    | Types.boolVal n, Types.boolVal v => n == v
+    | Types.symbolVal n, Types.symbolVal v => n == v
+    | Types.keywordVal n, Types.keywordVal v => n == v
+    | Types.Nil, Types.Nil => true
+    | Types.listVal n, Types.listVal v =>
+      if n.length != v.length then false
+      else eqList n v strict
+    | Types.vecVal nvec, Types.vecVal vvec =>
+      let n := toList nvec
+      let v := toList vvec
+      if n.length != v.length then false
+      else eqList n v strict
+    | Types.dictVal n, Types.dictVal v => eqDict n v strict
+    | Types.listVal n, Types.vecVal vvec => if strict then false else
+      let v := toList vvec
+      if n.length != v.length then false
+      else eqList n v strict
+    | Types.vecVal nvec, Types.listVal v => if strict then false else
+      let n := toList nvec
+      if n.length != v.length then false
+      else eqList n v strict
+    | _, _ => false
+
+end
+
+def eq (env : Env) (lst: List Types) (strict: Bool) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "eq: 2 arguments required")
+  else
+    let first := lst[0]!
+    let second := lst[1]!
+    let res := eqInternal first second strict
+    return (env, Types.boolVal res)
+
+def makeAtom (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "keyword: 1 argument required")
+  else
+    let first := lst[0]!
+    return (env, Types.atomVal (Atom.v first))
+
+def derefAtom (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "deref: 1 argument required")
+  else
+    let first := lst[0]!
+    match first with
+    | Types.atomVal x => match x with
+      | Atom.v v => return (env, v)
+      | Atom.withmeta v _ => return (env, v)
+    | x => throw (IO.userError s!"deref: unexpected symbol: {x.toString true}, expected: atom")
+
+def resetAtom (env : Env) (lst: List Types) (args: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "reset!: 2 argument required")
+  else
+    let first := lst[0]!
+    let second := lst[1]!
+    let atomSymbol := args[0]!
+    match atomSymbol with
+    | Types.symbolVal sym =>
+      match env.get (KeyType.strKey sym) with
+      | none => throw (IO.userError s!"{sym} not found")
+      | some (level, _) => match first with
+        | Types.atomVal x => match x with
+          | Atom.v _ =>
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.v second))
+              return (newEnv, second)
+          | Atom.withmeta _ meta =>
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.withmeta second meta))
+              return (newEnv, second)
+        | x => throw (IO.userError s!"reset!: unexpected symbol: {x.toString true}, expected: atom")
+    | x => throw (IO.userError s!"reset!: unexpected token: {x.toString true}, expected: symbol")
+
+def prStrInternal (lst: List Types) (printReadably: Bool) (sep: String) : String :=
+  let elems := lst.map (fun x => x.toString printReadably)
+  String.intercalate sep elems
+
+def KEY_DEBUG_EVAL := "DEBUG-EVAL"
+
+def getDebugEval (env : Env): Bool :=
+  match env.get (KeyType.strKey KEY_DEBUG_EVAL) with
+    | some (_, v) => match v with
+      | Types.boolVal v => v
+      | Types.Nil => false
+      | _ => false
+    | _ => false
+
+def prStrFunc (env : Env) (lst: List Types) : IO (Env × Types) := do
+  let str := prStrInternal lst true " "
+  return (env, Types.strVal str)
+
+def prnFunc (env : Env) (lst: List Types) : IO (Env × Types) := do
+  let str := prStrInternal lst true " "
+  IO.println str
+  return (env, Types.Nil)
+
+def printlnFunc (env : Env) (lst: List Types) : IO (Env × Types) := do
+  let str := prStrInternal lst false " "
+  IO.println str
+  return (env, Types.Nil)
+
+def strFunc (env : Env) (lst: List Types) : IO (Env × Types) := do
+  let str := prStrInternal lst false ""
+  return (env, Types.strVal str)
+
+def countFunc(env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "count: 1 argument required")
+  else
+    let x := lst[0]!
+    match x with
+      | Types.listVal v => return (env, Types.intVal v.length)
+      | Types.vecVal v => return (env, Types.intVal (toList v).length)
+      | Types.Nil => return (env, Types.intVal 0)
+      | _ => throw (IO.userError "count called on non-sequence")
+
+def readString (lst: List Types) (_: Env) : IO Types := do
+  if lst.length < 1 then throw (IO.userError "read-string: 1 arguments required")
+  else
+    let first := lst[0]!
+    match first with
+    | Types.strVal v => match read_types_with_env v with -- Dict.empty
+      | Except.error e => throw (IO.userError e)
+      | Except.ok res => return res
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: string")
+
+def cons (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "cons: >= 2 arguments required")
+  else
+    let elem := lst[0]!
+    let seq := lst[1]!
+    match seq with
+    | Types.listVal v => return (env, (Types.listVal (elem :: v)))
+    | Types.vecVal v => return (env, (Types.listVal (elem :: (toList v))))
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: list or vector")
+
+def concat (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then return (env, Types.listVal [])
+  else
+    let v ← lst.foldlM (fun (acc: List Types) x =>
+      match x with
+        | Types.listVal v => return acc ++ v
+        | Types.vecVal v => return acc ++ (toList v)
+        | x => return acc ++ [x]
+    ) []
+    return (env, Types.listVal v)
+
+
+def makeVec (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "vec: 1 arguments required")
+  else
+    let first := lst[0]!
+    match first with
+    | Types.vecVal v => return (env, Types.vecVal v)
+    | Types.listVal v => return (env, Types.vecVal (listToVec v))
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: list or vector")
+
+def nthSeq (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "nth: >= 2 arguments required")
+  else
+    let first := lst[0]!
+    let indx := lst[1]!
+    match indx with
+    | Types.intVal i =>
+      match first with
+      | Types.vecVal v =>
+        let lv := toList v
+        match lv.get? i.toNat with
+          | some v => return (env, v)
+          | none => throw (IO.userError "nth: index out of range")
+      | Types.listVal lv =>
+        if lv.length <= i then throw (IO.userError s!"nth: index out of range: {i}")
+        else
+          match lv.get? i.toNat with
+          | some v => return (env, v)
+          | none => throw (IO.userError "nth: index out of range")
+      | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: list or vector")
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: number")
+
+def firstSeq (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "first: 1 arguments required")
+  else
+    let first := lst[0]!
+    match first with
+    | Types.Nil => return (env, Types.Nil)
+    | Types.vecVal v =>
+      let lv := toList v
+      if lv.length == 0 then return (env, Types.Nil)
+      else
+        let elem := lv[0]!
+        return (env, elem)
+    | Types.listVal lv =>
+      if lv.length == 0 then return (env, Types.Nil)
+      else
+        let elem := lv[0]!
+        return (env, elem)
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: list or vector")
+
+def restSeq (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "rest: 1 arguments required")
+  else
+    let first := lst[0]!
+    match first with
+    | Types.Nil => return (env, Types.listVal [])
+    | Types.vecVal v =>
+      let lv := toList v
+      if lv.length < 1 then return (env, Types.listVal [])
+      else
+        return (env, Types.listVal (lv.drop 1))
+    | Types.listVal lv =>
+      if lv.length < 1 then return (env, Types.listVal [])
+      else
+        return (env, Types.listVal (lv.drop 1))
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: list or vector")
+
+def makeVector (env : Env) (lst: List Types) : IO (Env × Types) := do
+  return (env, Types.vecVal (listToVec lst))
+
+def makeDictInternal (initialDict : Dict) (lst: List Types) : IO (Dict) := do
+  let rec loop (lst : List Types) (acckeys: List String) (acc : Dict) : IO (Dict × List String) :=
+    match lst with
+    | [] => return (acc, acckeys)
+    | (Types.strVal k) :: v :: rest =>
+      if acckeys.contains k then return (acc, acckeys)
+      else loop rest (acckeys ++ [k]) (Dict.insert (KeyType.strKey k) 0 v acc)
+    | (Types.keywordVal k) :: v :: rest =>
+      if acckeys.contains k then return (acc, acckeys)
+      else loop rest (acckeys ++ [k]) (Dict.insert (KeyType.keywordKey k) 0 v acc)
+    | _ => throw (IO.userError "Invalid list format: Expected alternating string/keyword and value")
+  let (v, _) ← loop lst [] initialDict
+  return v
+
+def makeDict (env : Env) (lst: List Types) : IO (Env × Types) := do
+  let newDict ← makeDictInternal Dict.empty lst
+  return (env, Types.dictVal newDict)
+
+def assocDict (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "assoc: >= 1 arguments required")
+  else
+    let first := lst[0]!
+    let rest := lst.drop 1
+    match first with
+    | Types.dictVal v =>
+      let newDict ← makeDictInternal v rest
+      return (env, Types.dictVal newDict)
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: hash-map")
+
+def dissoc (dict : Dict) (keys : List Types) : IO Dict :=
+  let rec loop (keys : List Types) (acc : Dict) : IO Dict :=
+    match keys with
+    | [] => return acc
+    | key :: rest =>
+      match key with
+      | Types.strVal v =>
+        let newDict := acc.remove (KeyType.strKey v)
+        loop rest newDict
+      | Types.keywordVal v =>
+        let newDict := acc.remove (KeyType.strKey v)
+        loop rest newDict
+      | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: keyword or string")
+  loop keys dict
+
+def dissocDict (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "dissoc: >= 1 arguments required")
+  else
+    let first := lst[0]!
+    let rest := lst.drop 1
+    match first with
+    | Types.dictVal v =>
+      let newDict ← dissoc v rest
+      return (env, Types.dictVal newDict)
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: hash-map")
+
+def getDict (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "get: >= 1 arguments required")
+  else
+    let first := lst[0]!
+    let rest := lst.drop 1
+    match first with
+    | Types.dictVal v =>
+      match rest with
+      | [] => return (env, Types.Nil)
+      | _ =>
+        match (rest[0]!) with
+        | Types.strVal k =>
+          match v.get (KeyType.strKey k) with
+          | some (_, val) => return (env, val)
+          | none => return (env, Types.Nil)
+        | Types.keywordVal k =>
+          match v.get (KeyType.keywordKey k) with
+          | some (_, val) => return (env, val)
+          | none => return (env, Types.Nil)
+        | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: keyword or string")
+    | Types.Nil => return (env, Types.Nil)
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: hash-map")
+
+def containsDict (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "contains?: >= 1 arguments required")
+  else
+    let first := lst[0]!
+    let rest := lst.drop 1
+    match first with
+    | Types.dictVal v =>
+      match rest with
+        | [] => return (env, Types.boolVal false)
+        | _ =>
+          match (rest[0]!) with
+          | Types.strVal k =>
+            match v.get (KeyType.strKey k) with
+            | some _ => return (env, Types.boolVal true)
+            | none => return (env, Types.boolVal false)
+          | Types.keywordVal k =>
+            match v.get  (KeyType.strKey k) with
+            | some _ => return (env, Types.boolVal true)
+            | none => return (env, Types.boolVal false)
+          | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: keyword or string")
+    | Types.Nil => return (env, Types.boolVal false)
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: hash-map")
+
+def getKeysDict (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "keys: 1 arguments required")
+  else
+    let first := lst[0]!
+    match first with
+    | Types.dictVal v =>
+      let keys := v.keys
+      let result := keys.map (fun k =>
+        match k with
+        | KeyType.strKey v => (Types.strVal v)
+        | KeyType.keywordKey v => (Types.keywordVal v)
+      )
+      return (env, (Types.listVal result))
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: hash-map")
+
+def getValuesDict (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "get: 1 arguments required")
+  else
+    let first := lst[0]!
+    match first with
+    | Types.dictVal v =>
+      let values := v.values
+      return (env, (Types.listVal values))
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: hash-map")
+
+def makeSymbol (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "symbol: 1 argument required")
+  else
+    let first := lst[0]!
+    match first with
+    | Types.symbolVal v => return (env, Types.symbolVal v)
+    | Types.strVal v => return (env, Types.symbolVal v)
+    | x => throw (IO.userError s!"symbol: unexpected symbol: {x.toString true}, expected: string")
+
+def makeKeyword (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "keyword: 1 argument required")
+  else
+    let first := lst[0]!
+    match first with
+    | Types.keywordVal v => return (env, Types.keywordVal v)
+    | Types.strVal v => return (env, Types.keywordVal v)
+    | x => throw (IO.userError s!"keyword: unexpected symbol: {x.toString true}, expected: string")
+
+def conj (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "conj: >= 1 arguments required")
+  else
+    let first := lst[0]!
+    let rest := lst.drop 1
+    match first with
+    | Types.listVal v => return (env, Types.listVal ( rest.reverse ++ v))
+    | Types.vecVal v => return (env, Types.vecVal (listToVec ((toList v) ++ rest)))
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: list or vector")
+
+def seq (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then throw (IO.userError "conj: 1 arguments required")
+  else
+    let first := lst[0]!
+    match first with
+    | Types.Nil => return (env, Types.Nil)
+    | Types.listVal v => if v.length == 0 then return (env, Types.Nil) else return (env, Types.listVal v)
+    | Types.vecVal vv =>
+      let v := toList vv
+      if v.length == 0 then return (env, Types.Nil) else return (env, Types.listVal v)
+    | Types.strVal v =>
+      if v.length == 0 then return (env, Types.Nil)
+      else
+        let lv := v.toList.map (fun x => Types.strVal (String.singleton x))
+        return (env, Types.listVal lv)
+    | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: list, vector or string")
+
+partial def throwFn (_ : Env) (lst : List Types) : IO (Env × Types) := do
+    if lst.length < 1 then throw (IO.userError "panic")
+    else
+      let a := lst[0]!
+      match a with
+      | Types.strVal v => throw (IO.userError v)
+      | x => throw (IO.userError (x.toString true))
+
+def readFileContent (filePath : String) : IO String := do
+  IO.FS.readFile filePath
+
+def slurp (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then
+    throw (IO.userError "slurp: 1 argument required")
+  else
+    match lst[0]! with
+    | Types.strVal filename => do
+      let result ← try
+        let content ← readFileContent filename
+        return (env, Types.strVal content)
+      catch e =>
+        throw (IO.userError s!"slurp: failed to read file: {e.toString}")
+    | _ => throw (IO.userError "slurp: filename must be a string")
+
+def isEOF (stdin : IO.FS.Stream) : IO Bool := do
+  let input ← stdin.read 1 -- Try to read one more character
+  if input.isEmpty then
+    pure true -- EOF detected
+  else
+    pure false -- Some input available
+
+def prompt (msg: String) : IO (Option String) := do
+  IO.print msg
+  let stdin ← IO.getStdin
+  let input ← stdin.getLine
+  if input.isEmpty then
+    let eof ← isEOF stdin
+    if eof then
+      return none -- Indicates EOF (Ctrl+D)
+    else
+      return some ""
+  else
+    let value := input.trim
+    if value = "exit" then
+      return some ""
+    else
+      return some value
+
+def readline (env : Env) (lst: List Types) : IO (Env × Types) := do
+  if lst.length < 1 then
+    throw (IO.userError "readline: 1 arguments required")
+  else
+     match lst[0]! with
+    | Types.strVal msg => do
+      let ret := ← prompt msg
+      match ret with
+      | none => return (env, Types.Nil)
+      | some v => return (env, Types.strVal v)
+    | _ => throw (IO.userError "readline: argument must be a string")
+
+def loadFnNative (env : Env) (name: String) : Env :=
+  env.add (KeyType.strKey name) 0 (Types.funcVal (Fun.builtin name))
+
+def loadFnNativeFold (env : Env) (fnNames : List String) : Env :=
+  fnNames.foldl loadFnNative env
+
+def coreFnSymbols: List String := [
+  "+", "-", "*", "/",
+  "<", "<=", ">", ">=", "=",
+  "number?",
+  "list", "list?", "empty?", "count",
+  "concat", "cons",
+  "vec", "nth", "first", "rest", "vector", "vector?",
+  "map", "apply",
+  "conj", "seq", "sequential?",
+  "hash-map", "assoc", "dissoc", "get", "contains?", "keys", "vals", "map?",
+  "string?",
+  "throw",
+  "symbol", "keyword", "symbol?", "keyword?",
+  "nil?", "true?", "false?", "fn?", "macro?",
+  "prn", "pr-str", "str", "println",
+  "read-string", "slurp",
+  "atom", "atom?", "deref", "reset!", "swap!",
+  "eval",
+  "readline",
+  "time-ms", "meta", "with-meta"
+]
+
+def loadFnNativeAll (env : Env) : Env :=
+  (
+    loadFnNativeFold env coreFnSymbols
+  ).add (KeyType.strKey KEY_DEBUG_EVAL) 0 (Types.boolVal false)
+
+def setSymbol (env : Env) (name: String) (value: Types): Env :=
+  env.add (KeyType.strKey name) 0 value
+
+-- forwards mutated variables defined in outer scopes
+-- outer scopes always have a lower level index
+-- used to forward mutated atoms and variables defined by `eval` in the root scope
+def forwardOuterScopeDefs (envSource: Env) (envOuter: Env): Env :=
+  envSource.getDict.fold envOuter (fun key l v acc =>
+    if l > acc.getLevel then acc
+    else if l < acc.getLevel then acc.add key l v
+    else
+      match acc.get key with
+        | none => acc.add key l v
+        | some (lOuter, _) =>
+          if l != lOuter then acc
+          else acc.add key l v
+  )
diff --git a/impls/lean/LeanMal/printer.lean b/impls/lean/LeanMal/printer.lean
new file mode 100644
index 0000000000..8593e43fb6
--- /dev/null
+++ b/impls/lean/LeanMal/printer.lean
@@ -0,0 +1,6 @@
+import LeanMal.types
+
+universe u
+
+def pr_str (readably: Bool) (input : Types)  : String :=
+  input.toString readably
diff --git a/impls/lean/LeanMal/reader.lean b/impls/lean/LeanMal/reader.lean
new file mode 100644
index 0000000000..54146d890a
--- /dev/null
+++ b/impls/lean/LeanMal/reader.lean
@@ -0,0 +1,266 @@
+import Lean
+import LeanMal.types
+
+open Lean Lean.Parsec
+
+universe u
+
+-- parser for optional whitespace
+def wspace : Parsec Unit :=
+  many (pchar ' ' <|> pchar '\t' <|> pchar '\n' <|> pchar '\r') *> pure ()
+
+def wspace_or_comma_strict : Parsec Unit :=
+  many1 (pchar ' ' <|> pchar ',' <|> pchar '\t' <|> pchar '\n' <|> pchar '\r') *> pure ()
+
+-- custom `sep_by` combinator
+partial def sep_by {α β : Type} (p : Parsec α) (sep : Parsec β) : Parsec (Array α) := do
+  let mut res := #[]
+  let first ← optional p
+  match first with
+  | none => pure res
+  | some x =>
+    res := res.push x
+    while true do
+      let next ← optional (sep *> p)
+      match next with
+      | none => break
+      | some y => res := res.push y
+    pure res
+
+
+def int_to_float (n : Int) : Float :=
+  if n >= 0 then
+    Float.ofNat n.toNat
+  else
+    -Float.ofNat (-n).toNat
+
+def read_float (intPart fracPart expPart : String) (sign : Option Char) : Option Float :=
+  let fullnum := (intPart ++ fracPart).toNat!
+  let plc := fracPart.length
+  let exponent := expPart.toInt!
+  let floatVal := Float.ofScientific fullnum true plc
+  let adjustedFloat := floatVal * Float.pow 10.0 (int_to_float exponent)
+  match sign with
+  | some '-' => some (-adjustedFloat)
+  | _        => some adjustedFloat
+
+def read_str_val : Parsec Types := do
+  let _ ← pchar '"'
+  let str ← manyChars (do
+    let c ← satisfy (λ c => c ≠ '"')
+    if c = '\\' then
+      let nextChar ← anyChar
+      match nextChar with
+      | '"' => pure '"'
+      | '\\' => pure '\\'
+      | 'n' => pure '\n'
+      | 't' => pure '\t'
+      | _ => fail s!"Invalid escape sequence: \\{nextChar}"
+    else
+      pure c
+  )
+  let _ ← pchar '"'
+  return Types.strVal str
+
+def is_symbol_char (c: Char): Bool :=
+  c.isAlphanum || c == '+' || c == '-' || c == '*' || c == '/' || c == '=' || c == '<' || c == '>' || c == ':' || c == '_' || c == '!' || c == '?' || c == '&'
+
+def read_symbol_val : Parsec Types := do
+  ws
+    let sym ← many1Chars (satisfy (λ c => is_symbol_char c))
+  ws
+  return Types.symbolVal sym
+
+def read_bool_val : Parsec Types := do
+  ws
+  let b ← (pstring "true" <|> pstring "false")
+  let boolVal := Types.boolVal (b == "true")
+  let nextChar ← peek?
+  match nextChar with
+  | none => return boolVal
+  | some v =>
+    if is_symbol_char v then
+      let rest ← read_symbol_val
+      match rest with
+      | Types.symbolVal x => return Types.symbolVal (b ++ x)
+      | _ => return boolVal
+    else
+      return boolVal
+
+def read_nil_val : Parsec Types := do
+  ws
+  let _ ← pstring "nil"
+  let nextChar ← peek?
+  match nextChar with
+  | none => return Types.Nil
+  | some v =>
+    if is_symbol_char v then
+      let rest ← read_symbol_val
+      match rest with
+      | Types.symbolVal x => return Types.symbolVal ("nil" ++ x)
+      | _ => return Types.Nil
+    else
+      return Types.Nil
+
+def read_keyword : Parsec Types := do
+  let _ ← pstring ":"
+  let rest ← read_symbol_val
+  match rest with
+  | Types.symbolVal x => return Types.keywordVal x
+  | _ => fail "not keyword"
+
+def read_float_or_int_internal (sign: Option Char) : Parsec Types := do
+  let intPart ← many1Chars digit
+  optional (pchar '.') >>= fun
+  | some _ => do
+    let fracPart ← many1Chars digit
+    optional (pchar 'e' <|> pchar 'E') >>= fun
+    | some _ => do
+      let expPart ← manyChars (pchar '+' <|> pchar '-' <|> digit)
+      let floatStr := intPart ++ "." ++ fracPart ++ "e" ++ expPart
+      match read_float intPart fracPart expPart sign with
+      | some f => return Types.floatVal f
+      | none   => fail s!"Invalid float: {floatStr}"
+    | none => do
+      let floatStr := intPart ++ "." ++ fracPart
+      match read_float intPart fracPart "0" sign with
+      | some f => return Types.floatVal f
+      | none   => fail s!"Invalid float: {floatStr}"
+  | none => do
+    let intVal := intPart.toInt!
+    return Types.intVal (match sign with | some '-' => -intVal | _ => intVal)
+
+def read_float_or_int : Parsec Types := do
+  let sign ← optional (pchar '+' <|> pchar '-')
+  read_float_or_int_internal sign
+
+def read_operator_or_number : Parsec Types := do
+  let sign ← (pchar '+' <|> pchar '-')
+  let nextChar ← peek?
+  match nextChar with
+  | some c =>
+    if c.isWhitespace then return Types.symbolVal (String.singleton sign)
+    else if c.isDigit then read_float_or_int_internal sign
+    else if is_symbol_char c then
+      let rest ← read_symbol_val
+      match rest with
+      | Types.symbolVal x => return Types.symbolVal (String.singleton sign ++ x)
+      | _ => return Types.symbolVal (String.singleton sign)
+    else return Types.symbolVal (String.singleton sign)
+  | none => return Types.symbolVal (String.singleton sign)
+
+-- Define a parser for inline comments starting with ";" or ";;"
+def read_comment : Parsec Unit := do
+  skipString ";"
+
+  let nextCh ← peek?
+  match nextCh with
+  | none => pure ()
+  | some _ =>
+    let _ ← optional (many (satisfy (λ c => c ≠ '\n' && c ≠ '\r')))
+    _ ← optional (satisfy (λ c => c = '\n' || c = '\r'))
+    let _ ← optional  wspace
+    pure ()
+
+mutual
+  partial def read_list : Parsec Types := do
+    -- ws
+    let _ ← optional  wspace_or_comma_strict
+    let _ ← pstring "("
+    let _ ← optional  wspace_or_comma_strict
+    let els ← many (do
+      let e ← read_types
+      let _ ← optional  wspace_or_comma_strict
+      -- let _ ← optional (pchar ',')
+      return e)
+    -- ws
+    let _ ← optional  wspace_or_comma_strict
+    let _ ← pchar ')'
+    let _ ← optional  wspace_or_comma_strict
+    return Types.listVal (els.toList)
+
+    partial def read_vector : Parsec Types := do
+    let _ ← optional  wspace_or_comma_strict
+    let _ ← pchar '['
+    let _ ← optional  wspace_or_comma_strict
+    let els ← many (do
+      let e ← read_types
+      let _ ← optional  wspace_or_comma_strict
+      -- let _ ← optional (pchar ',')
+      return e)
+    let _ ← optional  wspace_or_comma_strict
+    let _ ← pchar ']'
+    let _ ← optional  wspace_or_comma_strict
+    let vecLst := els.toList
+    let vec  := listToVec vecLst
+    return Types.vecVal vec
+
+  partial def read_hash_map : Parsec Types := do
+    let _ ← optional  wspace_or_comma_strict
+    let _ ← pchar '{'
+    let _ ← optional  wspace_or_comma_strict
+    let els ← sep_by read_hash_map_pair (wspace *> optional (pchar ',') *> wspace)
+    let _ ← optional  wspace_or_comma_strict
+    let _ ← pchar '}'
+    let _ ← optional  wspace_or_comma_strict
+    let dict := Array.foldl (fun m (k, v) =>
+
+      m.insert k 0 v
+    ) (Dict.empty) els
+    return Types.dictVal dict
+
+  -- A parser for key-value pairs (String, Int in this case)
+  partial def read_hash_map_pair : Parsec (KeyType × Types) := do
+    let _ ← optional  wspace_or_comma_strict
+    let key ← read_keyword <|> read_str_val
+    let _ ← optional  wspace_or_comma_strict
+    let value ← read_types
+    let _ ← optional  wspace_or_comma_strict
+
+    match key with
+      | Types.keywordVal v => return (KeyType.keywordKey v, value)
+      | Types.strVal v => return (KeyType.strKey v, value)
+      | _ => default
+
+  partial def read_symbol (chars: String) (name: String) : Parsec Types := do
+    let _ ← optional  wspace_or_comma_strict
+    let _ ← pstring chars
+    let elem ← read_types
+    let _ ← optional  wspace_or_comma_strict
+
+    let vecLst := [(Types.symbolVal name), elem]
+    return Types.listVal vecLst
+
+  partial def read_with_meta : Parsec Types := do
+    ws
+    let _ ← pstring "^"
+
+    let els ← many (do
+      let e ← read_types
+      ws
+      let _ ← optional (pchar ',')
+      return e)
+
+    let elsVec := els.toList
+    let vecLst := (Types.symbolVal "with-meta") :: elsVec
+    return Types.listVal (List.append vecLst elsVec)
+
+  partial def read_atom : Parsec Types :=
+    read_operator_or_number <|> read_float_or_int <|> read_str_val <|> read_keyword <|> read_nil_val <|> read_bool_val <|> read_symbol_val
+
+  partial def read_types : Parsec Types := do
+      let _ ← optional  wspace
+      let _ ← optional (many read_comment)
+      match ← peek? with
+      | none => fail "endofinput"
+      | some _ =>
+        read_list <|> read_vector <|> read_hash_map  <|> read_symbol "'" "quote" <|> read_symbol "`" "quasiquote" <|> read_symbol "~@" "splice-unquote" <|> read_symbol "~" "unquote" <|> read_symbol "@" "deref" <|> read_with_meta <|> read_atom
+end
+
+def read_types_with_env (input : String)  : Except String Types :=
+  match read_types input.trim.iter with
+  | Lean.Parsec.ParseResult.success _ res => Except.ok res
+  | Lean.Parsec.ParseResult.error _ err => Except.error err
+
+def read_str (input : String)  : Except String Types :=
+  read_types_with_env input
diff --git a/impls/lean/LeanMal/step0_repl.lean b/impls/lean/LeanMal/step0_repl.lean
new file mode 100644
index 0000000000..b582913979
--- /dev/null
+++ b/impls/lean/LeanMal/step0_repl.lean
@@ -0,0 +1,25 @@
+universe u
+
+def READ (input : String) := input
+
+def EVAL (input : String) (_: String) := input
+
+def PRINT (input : String) := input
+
+def rep (input : String): String :=
+  PRINT (EVAL (READ input) "")
+
+def main : IO Unit := do
+  let mut donext := true
+  while donext do
+    IO.print "user> "
+    let stdin ← IO.getStdin
+    let input ← stdin.getLine
+    let value := input.trim
+    if value = "exit" then
+      donext := false
+      IO.println "Exiting REPL."
+    if value.isEmpty then
+      donext := false
+    else
+      IO.println (rep value)
diff --git a/impls/lean/LeanMal/step1_read_print.lean b/impls/lean/LeanMal/step1_read_print.lean
new file mode 100644
index 0000000000..7e11624950
--- /dev/null
+++ b/impls/lean/LeanMal/step1_read_print.lean
@@ -0,0 +1,34 @@
+import LeanMal.reader
+import LeanMal.printer
+
+universe u
+
+def READ (input : String) :=
+  read_str input
+
+def EVAL (ast : Types) (_: String) := ast
+
+def PRINT (ast : Types): String :=
+  pr_str true ast
+
+def rep (input : String): String :=
+  match READ input with
+  | Except.ok result =>
+    PRINT (EVAL result "")
+  | Except.error err =>
+    s!"Parsing failed: {err}"
+
+def main : IO Unit := do
+  let mut donext := true
+  while donext do
+    IO.print "user> "
+    let stdin ← IO.getStdin
+    let input ← stdin.getLine
+    let value := input.trim
+    if value = "exit" then
+      donext := false
+      IO.println "Exiting REPL."
+    if value.isEmpty then
+      donext := false
+    else
+      IO.println (rep value)
diff --git a/impls/lean/LeanMal/step2_eval.lean b/impls/lean/LeanMal/step2_eval.lean
new file mode 100644
index 0000000000..a50d72b16c
--- /dev/null
+++ b/impls/lean/LeanMal/step2_eval.lean
@@ -0,0 +1,148 @@
+import LeanMal.reader
+import LeanMal.printer
+
+universe u
+
+def READ (input : String): Except String Types :=
+  read_str input
+
+def sum (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x + y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x + y))
+  | _                                    => throw (IO.userError "+ operator not supported")
+
+def sub (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x - y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x - y))
+  | _                                    => throw (IO.userError "- operator not supported")
+
+def mul (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x * y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x * y))
+  | _                                    => throw (IO.userError "* operator not supported")
+
+def div (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x / y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x / y))
+  | _                                    => throw (IO.userError "/ operator not supported")
+
+def evalFnNative (env : Env) (name: String) (results: List Types): IO (Env × Types) := do
+    match name with
+    | "+" => sum env results
+    | "-" => sub env results
+    | "*" => mul env results
+    | "/" => div env results
+    | _   => throw (IO.userError s!"'{name}' not found")
+
+mutual
+
+  partial def evalTypes (env : Env) (ast : Types) : IO (Env × Types) := do
+    match ast with
+    | Types.symbolVal v   => match env.get (KeyType.strKey v) with
+      | some (_, vi) => return (env, vi)
+      | none    => return (env, Types.symbolVal v )
+    | Types.listVal el    => (evalList env el)
+    | Types.vecVal el     => (evalVec env (toList el))
+    | Types.dictVal el    => (evalDict env el)
+    | x                   => return (env, x)
+
+  partial def evalFunc (env: Env) (head : Types) (args : List Types) : IO (Env × Types) := do
+    let (env2, fn) ← evalTypes env head
+    evalFuncVal env2 fn args
+
+  partial def evalFuncVal (env: Env) (fn: Types) (args: List Types) : IO (Env × Types) := do
+    -- first execute each function argument - reduce computation
+    let (newEnv, results) ← evalFuncArgs env args
+    match fn with
+      | Types.symbolVal name => evalFnNative newEnv name results
+      | Types.funcVal v      => match v with
+        | Fun.builtin name => evalFnNative newEnv name results
+        | Fun.userDefined fenv params body =>
+          let keys: List String := match params with
+            | Types.listVal v => v.map fun x => x.toString false
+            | _               => []
+          let argsDict := (buildDict 0 keys results)
+          let merged := (newEnv.merge fenv).mergeDict (fenv.getLevel + 1) argsDict
+          evalTypes merged body
+        | Fun.macroFn _ _ _ => throw (IO.userError "macro not implemented")
+      | _ => throw (IO.userError s!"`unexpected token, expected: function`")
+
+  partial def evalList (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if List.length lst == 0 then return (env, Types.listVal lst)
+    else
+      let head := lst[0]!
+      match lst[0]! with
+      | Types.symbolVal v => match v with
+        | _ => evalFunc env head (lst.drop 1)
+      | _ => evalFunc env head (lst.drop 1)
+
+  partial def evalVec (env: Env) (elems : List Types) : IO (Env × Types) := do
+    let (newEnv, results) ← evalFuncArgs env elems
+    return (newEnv, Types.vecVal (listToVec results))
+
+  partial def evalDict (env: Env) (lst : Dict) : IO (Env × Types) := do
+    let (newEnv, newDict) ← evalDictInner env lst
+    return (newEnv, Types.dictVal newDict)
+
+  partial def evalDictInner (env: Env) (lst : Dict) : IO (Env × Dict) := do
+    match lst with
+      | Dict.empty => return (env, lst)
+      | Dict.insert k _ v restDict =>
+        let (newEnv, newVal) ← evalTypes env v
+        let (updatedEnv, updatedDict) ← evalDictInner newEnv restDict
+        let newDict := Dict.insert k 0 newVal updatedDict
+        return (updatedEnv, newDict)
+
+  partial def evalFuncArgs (env: Env) (args: List Types) : IO (Env × List Types) := do
+  args.foldlM (fun (res : Env × List Types) (x : Types) => do
+    let (r, acc) := res
+    let (updatedenv, res) ← evalTypes r x
+    return (updatedenv, acc ++ [res])
+  ) (env, [])
+end
+
+def PRINT (ast : Types): String :=
+  pr_str true ast
+
+def rep (input : String): IO String := do
+  match READ input with
+  | Except.ok result =>
+    try
+      let (_, res) ← evalTypes (Env.data 0 Dict.empty) result
+      return PRINT res
+    catch
+      | e => return s!"Error: {e}"
+  | Except.error err =>
+    return s!"Parsing failed: {err}"
+
+def main : IO Unit := do
+  let mut donext := true
+  while donext do
+    IO.print "user> "
+    let stdin ← IO.getStdin
+    let input ← stdin.getLine
+    let value := input.trim
+    if value = "exit" then
+      donext := false
+      IO.println "Exiting REPL."
+    if value.isEmpty then
+      donext := false
+    else
+      let output ← rep value
+      IO.println output
diff --git a/impls/lean/LeanMal/step3_env.lean b/impls/lean/LeanMal/step3_env.lean
new file mode 100644
index 0000000000..61942217d0
--- /dev/null
+++ b/impls/lean/LeanMal/step3_env.lean
@@ -0,0 +1,205 @@
+import LeanMal.reader
+import LeanMal.printer
+import LeanMal.types
+
+universe u
+
+def READ (input : String): Except String Types :=
+  read_str input
+
+def sum (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x + y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x + y))
+  | _                                    => throw (IO.userError "+ operator not supported")
+
+def sub (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x - y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x - y))
+  | _                                    => throw (IO.userError "- operator not supported")
+
+def mul (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x * y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x * y))
+  | _                                    => throw (IO.userError "* operator not supported")
+
+def div (env : Env) (lst: List Types) : IO (Env × Types) := do
+  match lst with
+  | []                                   => return (env, Types.intVal 0)
+  | [Types.intVal x]                     => return (env, Types.intVal x)
+  | [Types.intVal x, Types.intVal y]     => return (env, Types.intVal (x / y))
+  | [Types.floatVal x]                   => return (env, Types.floatVal x)
+  | [Types.floatVal x, Types.floatVal y] => return (env, Types.floatVal (x / y))
+  | _                                    => throw (IO.userError "/ operator not supported")
+
+def evalFnNative (env : Env) (name: String) (results: List Types): IO (Env × Types) := do
+    match name with
+    | "+" => sum env results
+    | "-" => sub env results
+    | "*" => mul env results
+    | "/" => div env results
+    | _   => throw (IO.userError s!"'{name}' not found")
+
+mutual
+
+  partial def evalTypes (env : Env) (ast : Types) : IO (Env × Types) := do
+    match ast with
+    | Types.symbolVal v   => match env.get (KeyType.strKey v) with
+      | some (_, vi) => return (env, vi)
+      | none => throw (IO.userError s!"'{v}' not found")
+    | Types.listVal el    => (evalList env el)
+    | Types.vecVal el     => (evalVec env (toList el))
+    | Types.dictVal el    => (evalDict env el)
+    | x                   => return (env, x)
+
+  partial def evalFunc (env: Env) (head : Types) (args : List Types) : IO (Env × Types) := do
+    let (env2, fn) ← evalTypes env head
+    evalFuncVal env2 fn args
+
+  partial def evalFuncVal (env: Env) (fn: Types) (args: List Types) : IO (Env × Types) := do
+    -- first execute each function argument - reduce computation
+    let (newEnv, results) ← evalFuncArgs env args
+    match fn with
+      | Types.funcVal v      => match v with
+        | Fun.builtin name => evalFnNative newEnv name results
+        | Fun.userDefined fenv params body =>
+          let keys: List String := match params with
+            | Types.listVal v => v.map fun x => x.toString false
+            | _               => []
+          let argsLevel := fenv.getLevel + 1
+          let argsDict := (buildDict argsLevel keys results)
+          let merged := (newEnv.merge fenv).mergeDict argsLevel argsDict
+          evalTypes merged body
+        | Fun.macroFn _ _ _ => throw (IO.userError "macro not implemented")
+      | _ => throw (IO.userError s!"`unexpected token, expected: function`")
+
+  partial def evalList (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if List.length lst == 0 then return (env, Types.listVal lst)
+    else
+      let head := lst[0]!
+      match lst[0]! with
+      | Types.symbolVal v => match v with
+        | "def!" => evalDefn env (lst.drop 1)
+        | "let*" => evalLet env (lst.drop 1)
+        | _ => evalFunc env head (lst.drop 1)
+      | _ => evalFunc env head (lst.drop 1)
+
+  partial def evalVec (env: Env) (elems : List Types) : IO (Env × Types) := do
+    let (newEnv, results) ← evalFuncArgs env elems
+    return (newEnv, Types.vecVal (listToVec results))
+
+  partial def evalDict (env: Env) (lst : Dict) : IO (Env × Types) := do
+    let (newEnv, newDict) ← evalDictInner env lst
+    return (newEnv, Types.dictVal newDict)
+
+  partial def evalDictInner (env: Env) (lst : Dict) : IO (Env × Dict) := do
+    match lst with
+      | Dict.empty => return (env, lst)
+      | Dict.insert k _ v restDict =>
+        let (newEnv, newVal) ← evalTypes env v
+        let (updatedEnv, updatedDict) ← evalDictInner newEnv restDict
+        let newDict := Dict.insert k 0 newVal updatedDict
+        return (updatedEnv, newDict)
+
+  partial def evalFuncArgs (env: Env) (args: List Types) : IO (Env × List Types) := do
+    args.foldlM (fun (res : Env × List Types) (x : Types) => do
+      let (r, acc) := res
+      let (updatedenv, res) ← evalTypes r x
+      return (updatedenv, acc ++ [res])
+    ) (env, [])
+
+  partial def evalDefn (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "def! unexpected syntax")
+    else
+      let key := args[0]!
+      let body := args[1]!
+      let (newEnv, value) ← (evalTypes env body)
+      match key with
+      | Types.symbolVal v =>
+        let envResult := newEnv.add (KeyType.strKey v) env.getLevel value
+        return (envResult, value)
+      | _ => throw (IO.userError s!"def! unexpected token, expected: symbol")
+
+  partial def evalLet (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "let*: unexpected syntax")
+    else
+      let pairs := args[0]!
+      let body := args[1]!
+      let newEnv ← match pairs with
+      | Types.listVal v => evalLetArgs env.increment v
+      | Types.vecVal v => evalLetArgs env.increment (toList v)
+      | _ => throw (IO.userError s!"unexpected token type: ${pairs.toString true}, expected: list or vector")
+
+      -- we do not propagate the let* environment to the parent scope
+      let (_, result) ← evalTypes newEnv body
+      return (env, result)
+
+  partial def evalLetArgs (env: Env) (args : List Types) : IO Env := do
+    match args with
+    | [] => return env
+    | [_] => throw (IO.userError "let*: unexpected syntax")
+    | x :: y :: rest =>
+      match x with
+      | Types.symbolVal key =>
+        let (updatedEnv, value) ← evalTypes env y
+        evalLetArgs (updatedEnv.add (KeyType.strKey key) env.getLevel value) rest
+      | _ => throw (IO.userError "let*: unexpected syntax")
+end
+
+def loadFnNative (env : Env) (name: String) : Env :=
+  env.add (KeyType.strKey name) 0 (Types.funcVal (Fun.builtin name))
+
+def loadFnNativeAll (env: Env) : Env :=
+  loadFnNative (
+    loadFnNative (
+      loadFnNative (
+        loadFnNative env "+"
+      ) "-"
+    ) "*"
+  ) "/"
+
+def PRINT (ast : Types): String :=
+  pr_str true ast
+
+def rep (env: Env) (input : String): IO (Env × String) := do
+  match READ input with
+  | Except.ok result =>
+    try
+      let (newenv, res) ← evalTypes env result
+      return (newenv, PRINT res)
+    catch
+      | e => return (env, s!"Error: {e}")
+  | Except.error err => return (env, s!"Parsing failed: {err}")
+
+def repAndPrint (env: Env) (output : String): IO Env := do
+  if output.endsWith "endofinput" then IO.print ""
+  else IO.println output
+  return env
+
+def main : IO Unit := do
+  let mut env := loadFnNativeAll (Env.data 0 Dict.empty)
+  let mut donext := true
+  while donext do
+    IO.print "user> "
+    let stdin ← IO.getStdin
+    let input ← stdin.getLine
+    let value := input.trim
+    if value = "exit" then
+      donext := false
+      IO.println "Exiting REPL."
+    if value.isEmpty then
+      donext := false
+    else
+      let (newenv, value) ← rep env value
+      env ← repAndPrint newenv value
diff --git a/impls/lean/LeanMal/step4_if_fn_do.lean b/impls/lean/LeanMal/step4_if_fn_do.lean
new file mode 100644
index 0000000000..7fa2090c42
--- /dev/null
+++ b/impls/lean/LeanMal/step4_if_fn_do.lean
@@ -0,0 +1,244 @@
+import LeanMal.reader
+import LeanMal.printer
+import LeanMal.core
+
+universe u
+
+def makeFn (env: Env) (args : List Types) : IO (Env × Types) := do
+  if args.length < 2 then throw (IO.userError "unexpected syntax")
+  else
+    let p := args[0]!
+    let body := args[1]!
+    let params := match p with
+      | Types.vecVal x => Types.listVal (toList x)
+      | _ => p
+    let newfn := Fun.userDefined env.increment params body
+    return (env, Types.funcVal newfn)
+
+def splitOnAmpersand (input : List String) : (List String × List String) :=
+  let rec loop (acc1 : List String) (rest : List String) : (List String × List String) :=
+    match rest with
+    | []         => (acc1, [])  -- If no "&" found, second list is empty
+    | "&" :: xs  => match xs with
+      | [] => (acc1, [])  -- If "&" is the last element, second list is empty
+      | y :: _ => (acc1, [y])  -- Add the next element after "&" to the second list
+    | x :: xs    => loop (acc1 ++ [x]) xs  -- Accumulate elements before "&"
+  loop [] input
+
+mutual
+  partial def evalTypes (env : Env) (ast : Types) : IO (Env × Types) := do
+    if getDebugEval env then IO.println s!"EVAL:{pr_str true ast}"
+    match ast with
+    | Types.symbolVal v   => match env.get (KeyType.strKey v) with
+      | some (_, vi) => return (env, vi)
+      | none => throw (IO.userError s!"'{v}' not found")
+    | Types.listVal el    => (evalList env el)
+    | Types.vecVal el     => (evalVec env (toList el))
+    | Types.dictVal el    => (evalDict env el)
+    | x                   => return (env, x)
+
+  partial def evalFunc (env: Env) (head : Types) (args : List Types) : IO (Env × Types) := do
+    let (env2, fn) ← evalTypes env head
+    let (_, res) ← evalFuncVal env2 fn args
+    return (env, res)
+
+  partial def evalFuncVal (env: Env) (fn: Types) (args: List Types) : IO (Env × Types) := do
+    -- first execute each function argument - reduce computation
+    let (newEnv, results) ← evalFuncArgs env args
+    match fn with
+      | Types.funcVal v      => match v with
+        | Fun.builtin name => evalFnNative newEnv name results
+        | Fun.userDefined fref params body =>
+          let allkeys: List String := match params with
+            | Types.listVal v => v.map fun x => x.toString false
+            | _               => []
+          let (keys, variadic) := splitOnAmpersand allkeys
+          let normalArgs := results.take keys.length
+          let variadicArg := results.drop keys.length
+          let argVals := normalArgs ++ [Types.listVal variadicArg]
+          let argsLevel := if fref.getLevel >= newEnv.getLevel then fref.getLevel + 1 else newEnv.getLevel + 1
+
+          let argsDict := (buildDict argsLevel (keys ++ variadic) argVals)
+          let merged := (newEnv.merge fref).mergeDict argsLevel argsDict
+
+          evalTypes merged body
+        | Fun.macroFn _ _ _ => throw (IO.userError "macro not implemented")
+      | _ => throw (IO.userError s!"`unexpected token, expected: function`")
+
+  partial def evalList (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if List.length lst == 0 then return (env, Types.listVal lst)
+    else
+      let head := lst[0]!
+      match lst[0]! with
+      | Types.symbolVal v => match v with
+        | "def!" => evalDefn env (lst.drop 1)
+        | "let*" => evalLet env (lst.drop 1)
+        | "do" => evalDo env (lst.drop 1)
+        | "if" => evalIf env (lst.drop 1)
+        | "fn*" => makeFn env (lst.drop 1)
+        | _ => evalFunc env head (lst.drop 1)
+      | _ => evalFunc env head (lst.drop 1)
+
+  partial def evalVec (env: Env) (elems : List Types) : IO (Env × Types) := do
+    let (newEnv, results) ← evalFuncArgs env elems
+    return (newEnv, Types.vecVal (listToVec results))
+
+  partial def evalDict (env: Env) (lst : Dict) : IO (Env × Types) := do
+    let (newEnv, newDict) ← evalDictInner env lst
+    return (newEnv, Types.dictVal newDict)
+
+  partial def evalDictInner (env: Env) (lst : Dict) : IO (Env × Dict) := do
+    match lst with
+      | Dict.empty => return (env, lst)
+      | Dict.insert k _ v restDict =>
+        let (newEnv, newVal) ← evalTypes env v
+        let (updatedEnv, updatedDict) ← evalDictInner newEnv restDict
+        let newDict := Dict.insert k 0 newVal updatedDict
+        return (updatedEnv, newDict)
+
+  partial def evalFuncArgs (env: Env) (args: List Types) : IO (Env × List Types) :=
+    args.foldlM (fun (res : Env × List Types) (x : Types) => do
+      let (r, acc) := res
+      let (updatedenv, res) ← evalTypes r x
+      return (updatedenv, acc ++ [res])
+    ) (env, [])
+
+  partial def evalDefn (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "def! unexpected syntax")
+    else
+      let key := args[0]!
+      let body := args[1]!
+      let (newEnv, value) ← (evalTypes env body)
+      match key with
+        | Types.symbolVal v =>
+          let refResult := newEnv.add (KeyType.strKey v) env.getLevel value
+          return (refResult, value)
+        | _ => throw (IO.userError s!"def! unexpected token, expected: symbol")
+
+  partial def evalLet (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "let*: unexpected syntax")
+    else
+      let pairs := args[0]!
+      let body := args[1]!
+      let newEnv ← match pairs with
+      | Types.listVal v => evalLetArgs env.increment v
+      | Types.vecVal v => evalLetArgs env.increment (toList v)
+      | _ => throw (IO.userError s!"unexpected token type: ${pairs.toString true}, expected: list or vector")
+
+       -- only propagate logs from the let* environment to the parent scope
+      let (_, result) ← evalTypes newEnv body
+      return (env, result)
+
+  partial def evalLetArgs (env: Env) (args : List Types) : IO Env := do
+    match args with
+    | [] => return env
+    | [_] => throw (IO.userError "let*: unexpected syntax")
+    | x :: y :: rest =>
+      match x with
+      | Types.symbolVal key =>
+        let (updatedEnv, value) ← evalTypes env y
+        evalLetArgs (updatedEnv.add (KeyType.strKey key) env.getLevel value) rest
+      | _ => throw (IO.userError "let*: unexpected syntax")
+
+  partial def evalDo (env: Env) (args : List Types) : IO (Env × Types) := do
+    -- only return last computation result
+    let (newEnv, results) ← evalFuncArgs env args
+    if results.length == 0 then return (newEnv, Types.Nil)
+    else return (newEnv, results[results.length - 1]!)
+
+  partial def evalIf (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "unexpected syntax")
+    else
+      let condition := args[0]!
+      let thenExpr := args[1]!
+      let hasElse := args.length > 2
+
+      let (newEnv, condResp) ← evalTypes env condition
+      let cond := match condResp with
+      | Types.boolVal v => v
+      | Types.Nil => false
+      | _ => true
+      if cond then evalTypes newEnv thenExpr
+      else if hasElse then evalTypes newEnv args[2]!
+      else return (newEnv, Types.Nil)
+
+  partial def evalFnNative (env : Env) (name: String) (results: List Types): IO (Env × Types) := do
+    match name with
+    | "+" => sum env results
+    | "-" => sub env results
+    | "*" => mul env results
+    | "/" => div env results
+    | "<" => lt env results
+    | "<=" => lte env results
+    | ">" => gt env results
+    | ">=" => gte env results
+    | "=" => eq env results false
+    | "prn" => prnFunc env results
+    | "pr-str" => prStrFunc env results
+    | "str" => strFunc env results
+    | "println" => printlnFunc env results
+    | "list" => return (env, Types.listVal results)
+    | "count" => countFunc env results
+    | _ => match results with
+        | [x] => match x with
+          | Types.listVal x => match name with
+            | "list?" => return (env, Types.boolVal true)
+            | "empty?" => return (env, Types.boolVal (x.length == 0))
+            | _ => return (env, Types.boolVal false)
+          | Types.vecVal x => match name with
+            | "empty?" => return (env, Types.boolVal ((toList x).length == 0))
+            | _ => return (env, Types.boolVal false)
+          | _   => return (env, Types.boolVal false)
+        | _   => throw (IO.userError s!"'{name}' not found")
+
+end
+
+def READ (input : String): Except String Types :=
+  read_str input
+
+def PRINT (ast : Types): String :=
+  pr_str true ast
+
+def rep (env: Env) (input : String): IO (Env × String) := do
+  match READ input with
+  | Except.ok result =>
+    try
+      let (newenv, res) ← evalTypes env result
+      return (newenv, PRINT res)
+    catch
+      | e => return (env, s!"Error: {e}")
+  | Except.error err => return (env, s!"Parsing failed: {err}")
+
+def loadMalFns (env: Env) (fndefs: List String): IO (Env × String) := do
+  fndefs.foldlM (fun (res : Env × String) fndef => do
+    let (ref, msg) := res
+    let (newref, newmsg) ← rep ref fndef
+    return (newref, s!"{msg}¬{newmsg}")
+  ) (env, "")
+
+def fnDefs: List String := [
+    "(def! not (fn* (a) (if a false true)))",
+  ]
+
+def repAndPrint (env: Env) (output : String): IO Env := do
+  if output.endsWith "endofinput" then IO.print ""
+  else IO.println output
+  return env
+
+def main : IO Unit := do
+  let (env0, _) ← loadMalFns (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
+  let mut env := env0
+  let mut donext := true
+  while donext do
+    IO.print "user> "
+    let stdin ← IO.getStdin
+    let input ← stdin.getLine
+    let value := input.trim
+    if value = "exit" then
+      donext := false
+      IO.println "Exiting REPL."
+    if value.isEmpty then
+      donext := false
+    else
+      let (newenv, value) ← rep env value
+      env ← repAndPrint newenv value
diff --git a/impls/lean/LeanMal/step5_tco.lean b/impls/lean/LeanMal/step5_tco.lean
new file mode 100644
index 0000000000..4e7cc22e59
--- /dev/null
+++ b/impls/lean/LeanMal/step5_tco.lean
@@ -0,0 +1,243 @@
+import LeanMal.reader
+import LeanMal.printer
+import LeanMal.core
+
+universe u
+
+def makeFn (env: Env) (args : List Types) : IO (Env × Types) := do
+  if args.length < 2 then throw (IO.userError "unexpected syntax")
+  else
+    let p := args[0]!
+    let body := args[1]!
+    let params := match p with
+      | Types.vecVal x => Types.listVal (toList x)
+      | _ => p
+    let newfn := Fun.userDefined env.increment params body
+    return (env, Types.funcVal newfn)
+
+def splitOnAmpersand (input : List String) : (List String × List String) :=
+  let rec loop (acc1 : List String) (rest : List String) : (List String × List String) :=
+    match rest with
+    | []         => (acc1, [])  -- If no "&" found, second list is empty
+    | "&" :: xs  => match xs with
+      | [] => (acc1, [])  -- If "&" is the last element, second list is empty
+      | y :: _ => (acc1, [y])  -- Add the next element after "&" to the second list
+    | x :: xs    => loop (acc1 ++ [x]) xs  -- Accumulate elements before "&"
+  loop [] input
+
+mutual
+  partial def evalTypes (env : Env) (ast : Types) : IO (Env × Types) := do
+    if getDebugEval env then IO.println s!"EVAL:{pr_str true ast}"
+    match ast with
+    | Types.symbolVal v   => match env.get (KeyType.strKey v) with
+      | some (_, vi) => return (env, vi)
+      | none => throw (IO.userError s!"'{v}' not found")
+    | Types.listVal el    => (evalList env el)
+    | Types.vecVal el     => (evalVec env (toList el))
+    | Types.dictVal el    => (evalDict env el)
+    | x                   => return (env, x)
+
+  partial def evalFunc (env: Env) (head : Types) (args : List Types) : IO (Env × Types) := do
+    let (env2, fn) ← evalTypes env head
+    let (_, res) ← evalFuncVal env2 fn args
+    return (env, res)
+
+  partial def evalFuncVal (env: Env) (fn: Types) (args: List Types) : IO (Env × Types) := do
+    -- first execute each function argument - reduce computation
+    let (newEnv, results) ← evalFuncArgs env args
+    match fn with
+      | Types.funcVal v      => match v with
+        | Fun.builtin name => evalFnNative newEnv name results
+        | Fun.userDefined fref params body =>
+          let allkeys: List String := match params with
+            | Types.listVal v => v.map fun x => x.toString false
+            | _               => []
+          let (keys, variadic) := splitOnAmpersand allkeys
+          let normalArgs := results.take keys.length
+          let variadicArg := results.drop keys.length
+          let argVals := normalArgs ++ [Types.listVal variadicArg]
+          let argsLevel := if fref.getLevel >= newEnv.getLevel then fref.getLevel + 1 else newEnv.getLevel + 1
+
+          let argsDict := (buildDict argsLevel (keys ++ variadic) argVals)
+          let merged := (newEnv.merge fref).mergeDict argsLevel argsDict
+
+          evalTypes merged body
+        | Fun.macroFn _ _ _ => throw (IO.userError "macro not implemented")
+      | _ => throw (IO.userError s!"`unexpected token, expected: function`")
+
+
+  partial def evalList (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if List.length lst == 0 then return (env, Types.listVal lst)
+    else
+      let head := lst[0]!
+      match lst[0]! with
+      | Types.symbolVal v => match v with
+        | "def!" => evalDefn env (lst.drop 1)
+        | "let*" => evalLet env (lst.drop 1)
+        | "do" => evalDo env (lst.drop 1)
+        | "if" => evalIf env (lst.drop 1)
+        | "fn*" => makeFn env (lst.drop 1)
+        | _ => evalFunc env head (lst.drop 1)
+      | _ => evalFunc env head (lst.drop 1)
+
+  partial def evalVec (env: Env) (elems : List Types) : IO (Env × Types) := do
+    let (newEnv, results) ← evalFuncArgs env elems
+    return (newEnv, Types.vecVal (listToVec results))
+
+  partial def evalDict (env: Env) (lst : Dict) : IO (Env × Types) := do
+    let (newEnv, newDict) ← evalDictInner env lst
+    return (newEnv, Types.dictVal newDict)
+
+  partial def evalDictInner (env: Env) (lst : Dict) : IO (Env × Dict) := do
+    match lst with
+      | Dict.empty => return (env, lst)
+      | Dict.insert k _ v restDict =>
+        let (newEnv, newVal) ← evalTypes env v
+        let (updatedEnv, updatedDict) ← evalDictInner newEnv restDict
+        let newDict := Dict.insert k 0 newVal updatedDict
+        return (updatedEnv, newDict)
+
+  partial def evalFuncArgs (env: Env) (args: List Types) : IO (Env × List Types) :=
+    args.foldlM (fun (res : Env × List Types) (x : Types) => do
+      let (r, acc) := res
+      let (updatedenv, res) ← evalTypes r x
+      return (updatedenv, acc ++ [res])
+    ) (env, [])
+
+  partial def evalDefn (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "def! unexpected syntax")
+    else
+      let key := args[0]!
+      let body := args[1]!
+      let (newEnv, value) ← (evalTypes env body)
+      match key with
+        | Types.symbolVal v =>
+          let refResult := newEnv.add (KeyType.strKey v) env.getLevel value
+          return (refResult, value)
+        | _ => throw (IO.userError s!"def! unexpected token, expected: symbol")
+
+  partial def evalLet (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "let*: unexpected syntax")
+    else
+      let pairs := args[0]!
+      let body := args[1]!
+      let newEnv ← match pairs with
+      | Types.listVal v => evalLetArgs env.increment v
+      | Types.vecVal v => evalLetArgs env.increment (toList v)
+      | _ => throw (IO.userError s!"unexpected token type: ${pairs.toString true}, expected: list or vector")
+
+      let (_, result) ← evalTypes newEnv body
+      return (env, result)
+
+  partial def evalLetArgs (env: Env) (args : List Types) : IO Env := do
+    match args with
+    | [] => return env
+    | [_] => throw (IO.userError "let*: unexpected syntax")
+    | x :: y :: rest =>
+      match x with
+      | Types.symbolVal key =>
+        let (updatedEnv, value) ← evalTypes env y
+        evalLetArgs (updatedEnv.add (KeyType.strKey key) env.getLevel value) rest
+      | _ => throw (IO.userError "let*: unexpected syntax")
+
+  partial def evalDo (env: Env) (args : List Types) : IO (Env × Types) := do
+    -- only return last computation result
+    let (newEnv, results) ← evalFuncArgs env args
+    if results.length == 0 then return (newEnv, Types.Nil)
+    else return (newEnv, results[results.length - 1]!)
+
+  partial def evalIf (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "unexpected syntax")
+    else
+      let condition := args[0]!
+      let thenExpr := args[1]!
+      let hasElse := args.length > 2
+
+      let (newEnv, condResp) ← evalTypes env condition
+      let cond := match condResp with
+      | Types.boolVal v => v
+      | Types.Nil => false
+      | _ => true
+      if cond then evalTypes newEnv thenExpr
+      else if hasElse then evalTypes newEnv args[2]!
+      else return (newEnv, Types.Nil)
+
+  partial def evalFnNative (env : Env) (name: String) (results: List Types): IO (Env × Types) := do
+    match name with
+    | "+" => sum env results
+    | "-" => sub env results
+    | "*" => mul env results
+    | "/" => div env results
+    | "<" => lt env results
+    | "<=" => lte env results
+    | ">" => gt env results
+    | ">=" => gte env results
+    | "=" => eq env results false
+    | "prn" => prnFunc env results
+    | "pr-str" => prStrFunc env results
+    | "str" => strFunc env results
+    | "println" => printlnFunc env results
+    | "list" => return (env, Types.listVal results)
+    | "count" => countFunc env results
+    | _ => match results with
+        | [x] => match x with
+          | Types.listVal x => match name with
+            | "list?" => return (env, Types.boolVal true)
+            | "empty?" => return (env, Types.boolVal (x.length == 0))
+            | _ => return (env, Types.boolVal false)
+          | Types.vecVal x => match name with
+            | "empty?" => return (env, Types.boolVal ((toList x).length == 0))
+            | _ => return (env, Types.boolVal false)
+          | _   => return (env, Types.boolVal false)
+        | _   => throw (IO.userError s!"'{name}' not found")
+end
+
+def READ (input : String): Except String Types :=
+  read_str input
+
+def PRINT (ast : Types): String :=
+  pr_str true ast
+
+def rep (env: Env) (input : String): IO (Env × String) := do
+  match READ input with
+  | Except.ok result =>
+    try
+      let (newenv, res) ← evalTypes env result
+      return (newenv, PRINT res)
+    catch
+      | e => return (env, s!"Error: {e}")
+  | Except.error err => return (env, s!"Parsing failed: {err}")
+
+def loadMalFns (env: Env) (fndefs: List String): IO (Env × String) := do
+  fndefs.foldlM (fun (res : Env × String) fndef => do
+    let (ref, msg) := res
+    let (newref, newmsg) ← rep ref fndef
+    return (newref, s!"{msg}¬{newmsg}")
+  ) (env, "")
+
+def fnDefs: List String := [
+    "(def! not (fn* (a) (if a false true)))",
+  ]
+
+def repAndPrint (env: Env) (output : String): IO Env := do
+  if output.endsWith "endofinput" then IO.print ""
+  else IO.println output
+  return env
+
+def main : IO Unit := do
+  let (env0, _) ← loadMalFns (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
+  let mut env := env0
+  let mut donext := true
+  while donext do
+    IO.print "user> "
+    let stdin ← IO.getStdin
+    let input ← stdin.getLine
+    let value := input.trim
+    if value = "exit" then
+      donext := false
+      IO.println "Exiting REPL."
+    if value.isEmpty then
+      donext := false
+    else
+      let (newenv, value) ← rep env value
+      env ← repAndPrint newenv value
diff --git a/impls/lean/LeanMal/step6_file.lean b/impls/lean/LeanMal/step6_file.lean
new file mode 100644
index 0000000000..d59c6fd055
--- /dev/null
+++ b/impls/lean/LeanMal/step6_file.lean
@@ -0,0 +1,300 @@
+import LeanMal.reader
+import LeanMal.printer
+import LeanMal.core
+
+universe u
+
+def makeFn (env: Env) (args : List Types) : IO (Env × Types) := do
+  if args.length < 2 then throw (IO.userError "unexpected syntax")
+  else
+    let p := args[0]!
+    let body := args[1]!
+    let params := match p with
+      | Types.vecVal x => Types.listVal (toList x)
+      | _ => p
+    let newfn := Fun.userDefined env.increment params body
+    return (env, Types.funcVal newfn)
+
+def splitOnAmpersand (input : List String) : (List String × List String) :=
+  let rec loop (acc1 : List String) (rest : List String) : (List String × List String) :=
+    match rest with
+    | []         => (acc1, [])  -- If no "&" found, second list is empty
+    | "&" :: xs  => match xs with
+      | [] => (acc1, [])  -- If "&" is the last element, second list is empty
+      | y :: _ => (acc1, [y])  -- Add the next element after "&" to the second list
+    | x :: xs    => loop (acc1 ++ [x]) xs  -- Accumulate elements before "&"
+  loop [] input
+
+mutual
+   partial def evalTypes (env : Env) (ast : Types) : IO (Env × Types) := do
+    if getDebugEval env then IO.println s!"EVAL:{pr_str true ast}"
+    match ast with
+    | Types.symbolVal v   => match env.get (KeyType.strKey v) with
+      | some (_, vi) => return (env, vi)
+      | none => throw (IO.userError s!"'{v}' not found")
+    | Types.listVal el    => (evalList env el)
+    | Types.vecVal el     => (evalVec env (toList el))
+    | Types.dictVal el    => (evalDict env el)
+    | x                   => return (env, x)
+
+  partial def evalFunc (env: Env) (head : Types) (args : List Types) : IO (Env × Types) := do
+    let (env2, fn) ← evalTypes env head
+    let (fref, res) ← evalFuncVal env2 fn args
+    return ((forwardOuterScopeDefs fref env), res)
+
+  partial def evalFuncVal (env: Env) (fn: Types) (args: List Types) : IO (Env × Types) := do
+    -- first execute each function argument - reduce computation
+    let (newEnv, results) ← evalFuncArgs env args
+    match fn with
+      | Types.funcVal v      => match v with
+        | Fun.builtin name => evalFnNative newEnv name results args
+        | Fun.userDefined fref params body =>
+          let allkeys: List String := match params with
+            | Types.listVal v => v.map fun x => x.toString false
+            | _               => []
+          let (keys, variadic) := splitOnAmpersand allkeys
+          let normalArgs := results.take keys.length
+          let variadicArg := results.drop keys.length
+          let argVals := normalArgs ++ [Types.listVal variadicArg]
+          let argsLevel := if fref.getLevel >= newEnv.getLevel then fref.getLevel + 1 else newEnv.getLevel + 1
+
+          let argsDict := (buildDict argsLevel (keys ++ variadic) argVals)
+          let merged := (newEnv.merge fref).mergeDict argsLevel argsDict
+
+          evalTypes merged body
+        | Fun.macroFn _ _ _ => throw (IO.userError "macro not implemented")
+      | _ => throw (IO.userError s!"`unexpected token, expected: function`")
+
+  partial def evalList (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if List.length lst == 0 then return (env, Types.listVal lst)
+    else
+      let head := lst[0]!
+      match lst[0]! with
+      | Types.symbolVal v => match v with
+        | "def!" => evalDefn env (lst.drop 1)
+        | "let*" => evalLet env (lst.drop 1)
+        | "do" => evalDo env (lst.drop 1)
+        | "if" => evalIf env (lst.drop 1)
+        | "fn*" => makeFn env (lst.drop 1)
+        | _ => evalFunc env head (lst.drop 1)
+      | _ => evalFunc env head (lst.drop 1)
+
+  partial def evalVec (env: Env) (elems : List Types) : IO (Env × Types) := do
+    let (newEnv, results) ← evalFuncArgs env elems
+    return (newEnv, Types.vecVal (listToVec results))
+
+  partial def evalDict (env: Env) (lst : Dict) : IO (Env × Types) := do
+    let (newEnv, newDict) ← evalDictInner env lst
+    return (newEnv, Types.dictVal newDict)
+
+  partial def evalDictInner (env: Env) (lst : Dict) : IO (Env × Dict) := do
+    match lst with
+      | Dict.empty => return (env, lst)
+      | Dict.insert k _ v restDict =>
+        let (newEnv, newVal) ← evalTypes env v
+        let (updatedEnv, updatedDict) ← evalDictInner newEnv restDict
+        let newDict := Dict.insert k 0 newVal updatedDict
+        return (updatedEnv, newDict)
+
+  partial def evalFuncArgs (env: Env) (args: List Types) : IO (Env × List Types) :=
+    args.foldlM (fun (res : Env × List Types) (x : Types) => do
+      let (r, acc) := res
+      let (updatedenv, res) ← evalTypes r x
+      return (updatedenv, acc ++ [res])
+    ) (env, [])
+
+  partial def evalDefn (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "def! unexpected syntax")
+    else
+      let key := args[0]!
+      let body := args[1]!
+      let (newEnv, value) ← (evalTypes env body)
+      match key with
+        | Types.symbolVal v =>
+          let refResult := newEnv.add (KeyType.strKey v) env.getLevel value
+          return (refResult, value)
+        | _ => throw (IO.userError s!"def! unexpected token, expected: symbol")
+
+  partial def evalLet (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "let*: unexpected syntax")
+    else
+      let pairs := args[0]!
+      let body := args[1]!
+      let newEnv ← match pairs with
+      | Types.listVal v => evalLetArgs env.increment v
+      | Types.vecVal v => evalLetArgs env.increment (toList v)
+      | _ => throw (IO.userError s!"unexpected token type: ${pairs.toString true}, expected: list or vector")
+
+      let (letref, result) ← evalTypes newEnv body
+      return ((forwardOuterScopeDefs letref env), result)
+
+  partial def evalLetArgs (env: Env) (args : List Types) : IO Env := do
+    match args with
+    | [] => return env
+    | [_] => throw (IO.userError "let*: unexpected syntax")
+    | x :: y :: rest =>
+      match x with
+      | Types.symbolVal key =>
+        let (updatedEnv, value) ← evalTypes env y
+        evalLetArgs (updatedEnv.add (KeyType.strKey key) env.getLevel value) rest
+      | _ => throw (IO.userError "let*: unexpected syntax")
+
+  partial def evalDo (env: Env) (args : List Types) : IO (Env × Types) := do
+    -- only return last computation result
+    let (newEnv, results) ← evalFuncArgs env args
+    if results.length == 0 then return (newEnv, Types.Nil)
+    else return (newEnv, results[results.length - 1]!)
+
+  partial def evalIf (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "unexpected syntax")
+    else
+      let condition := args[0]!
+      let thenExpr := args[1]!
+      let hasElse := args.length > 2
+
+      let (newEnv, condResp) ← evalTypes env condition
+      let cond := match condResp with
+      | Types.boolVal v => v
+      | Types.Nil => false
+      | _ => true
+      if cond then evalTypes newEnv thenExpr
+      else if hasElse then evalTypes newEnv args[2]!
+      else return (newEnv, Types.Nil)
+
+  partial def swapAtom (env: Env) (lst: List Types) (args: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "swap!: >= 2 argument required")
+  else
+    let first := lst[0]!
+    let fn := lst[1]!
+    let rest := lst.drop 2
+    match args[0]! with
+    | Types.symbolVal sym =>
+      match fn with
+      | Types.funcVal _ =>
+        match env.get (KeyType.strKey sym) with
+        | none => throw (IO.userError s!"{sym} not found")
+        | some (level, _) => match first with
+          | Types.atomVal x => match x with
+            | Atom.v v =>
+              let (_, res) ← evalFuncVal env fn ([v] ++ rest)
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.v res))
+              return (newEnv, res)
+            | Atom.withmeta v meta =>
+              let (_, res) ← evalFuncVal env fn ([v] ++ rest)
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.withmeta res meta))
+              return (newEnv, res)
+          | x => throw (IO.userError s!"swap!: unexpected symbol: {x.toString true}, expected: atom")
+      | x => throw (IO.userError s!"swap!: unexpected symbol: {x.toString true}, expected: function")
+    | x => throw (IO.userError s!"swap!: unexpected token: {x.toString true}, expected: symbol")
+
+  partial def eval (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if lst.length < 1 then throw (IO.userError "eval: unexpected syntax")
+    else
+      let ast := lst[0]!
+      -- any new variables are defined on level 0
+      let env0 := Env.data 0 env.getDict
+      evalTypes env0 ast
+
+  partial def evalFnNative (env : Env) (name: String) (results: List Types) (args: List Types): IO (Env × Types) := do
+    match name with
+    | "+" => sum env results
+    | "-" => sub env results
+    | "*" => mul env results
+    | "/" => div env results
+    | "<" => lt env results
+    | "<=" => lte env results
+    | ">" => gt env results
+    | ">=" => gte env results
+    | "=" => eq env results false
+    | "list" => return (env, Types.listVal results)
+    | "count" => countFunc env results
+    | "atom" => makeAtom env results
+    | "deref" => derefAtom env results
+    | "reset!" => resetAtom env results args
+    | "swap!" => swapAtom env results args
+    | "prn" => prnFunc env results
+    | "pr-str" => prStrFunc env results
+    | "str" => strFunc env results
+    | "println" => printlnFunc env results
+    | "eval" => eval env results
+    | "slurp" => slurp env results
+    | "read-string" =>
+      let res ← readString results env -- readString results Dict.empty
+      return (env, res)
+    | _ => match results with
+        | [x] => match x with
+          | Types.listVal x => match name with
+            | "list?" => return (env, Types.boolVal true)
+            | "empty?" => return (env, Types.boolVal (x.length == 0))
+            | _ => return (env, Types.boolVal false)
+          | Types.vecVal x => match name with
+            | "empty?" => return (env, Types.boolVal ((toList x).length == 0))
+            | _ => return (env, Types.boolVal false)
+          | Types.atomVal _ => match name with
+            | "atom?" => return (env, Types.boolVal true)
+            | _ => return (env, Types.boolVal false)
+          | _   => return (env, Types.boolVal false)
+        | _   => throw (IO.userError s!"'{name}' not found")
+end
+
+def READ (input : String): Except String Types :=
+  read_str input
+
+def PRINT (ast : Types): String :=
+  pr_str true ast
+
+def rep (env: Env) (input : String): IO (Env × String) := do
+  match READ input with
+  | Except.ok result =>
+    try
+      let (newenv, res) ← evalTypes env result
+      return (newenv, PRINT res)
+    catch
+      | e => return (env, s!"Error: {e}")
+  | Except.error err => return (env, s!"Parsing failed: {err}")
+
+def loadMalFns (env: Env) (fndefs: List String): IO (Env × String) := do
+  fndefs.foldlM (fun (res : Env × String) fndef => do
+    let (ref, msg) := res
+    let (newref, newmsg) ← rep ref fndef
+    return (newref, s!"{msg}¬{newmsg}")
+  ) (env, "")
+
+def fnDefs: List String := [
+    "(def! not (fn* (a) (if a false true)))",
+    "(def! load-file (fn* (f) (eval (read-string (str \"(do \" (slurp f) \"\nnil)\")))))",
+  ]
+
+def repAndPrint (env: Env) (output : String): IO Env := do
+  if output.endsWith "endofinput" then IO.print ""
+  else IO.println output
+  return env
+
+def reploop (inienv: Env) : IO Unit := do
+  let mut donext := false
+  let mut env := inienv
+  donext := true
+  while donext do
+    IO.print "user> "
+    let stdin ← IO.getStdin
+    let input ← stdin.getLine
+    let value := input.trim
+    if value = "exit" then
+      donext := false
+      IO.println "Exiting REPL."
+    if value.isEmpty then
+      donext := false
+    else
+      let (newenv, value) ← rep env value
+      env ← repAndPrint newenv value
+
+def main (args : List String) : IO Unit := do
+  let (env0, _) ← loadMalFns (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
+  let env := setSymbol env0 "*ARGV*" (Types.listVal [])
+
+  if args.length > 0 then do
+    let astArgs := ((args.drop 1).map (fun arg => Types.strVal arg))
+    let newenv := setSymbol env0 "*ARGV*" (Types.listVal astArgs)
+    let (_, _) ← rep newenv s!"(load-file \"{args[0]!}\")"
+    IO.Process.exit 0
+  else reploop env
diff --git a/impls/lean/LeanMal/step7_quote.lean b/impls/lean/LeanMal/step7_quote.lean
new file mode 100644
index 0000000000..ed48a6d179
--- /dev/null
+++ b/impls/lean/LeanMal/step7_quote.lean
@@ -0,0 +1,340 @@
+import LeanMal.reader
+import LeanMal.printer
+import LeanMal.core
+
+universe u
+
+def makeFn (env: Env) (args : List Types) : IO (Env × Types) := do
+  if args.length < 2 then throw (IO.userError "unexpected syntax")
+  else
+    let p := args[0]!
+    let body := args[1]!
+    let params := match p with
+      | Types.vecVal x => Types.listVal (toList x)
+      | _ => p
+    let newfn := Fun.userDefined env.increment params body
+    return (env, Types.funcVal newfn)
+
+def splitOnAmpersand (input : List String) : (List String × List String) :=
+  let rec loop (acc1 : List String) (rest : List String) : (List String × List String) :=
+    match rest with
+    | []         => (acc1, [])  -- If no "&" found, second list is empty
+    | "&" :: xs  => match xs with
+      | [] => (acc1, [])  -- If "&" is the last element, second list is empty
+      | y :: _ => (acc1, [y])  -- Add the next element after "&" to the second list
+    | x :: xs    => loop (acc1 ++ [x]) xs  -- Accumulate elements before "&"
+  loop [] input
+
+mutual
+  partial def evalTypes (env : Env) (ast : Types) : IO (Env × Types) := do
+    if getDebugEval env then IO.println s!"EVAL:{pr_str true ast}"
+    match ast with
+    | Types.symbolVal v   => match env.get (KeyType.strKey v) with
+      | some (_, vi) => return (env, vi)
+      | none => throw (IO.userError s!"'{v}' not found")
+    | Types.listVal el    => (evalList env el)
+    | Types.vecVal el     => (evalVec env (toList el))
+    | Types.dictVal el    => (evalDict env el)
+    | x                   => return (env, x)
+
+  partial def evalFunc (env: Env) (head : Types) (args : List Types) : IO (Env × Types) := do
+    let (env2, fn) ← evalTypes env head
+    let (fref, res) ← evalFuncVal env2 fn args
+    return ((forwardOuterScopeDefs fref env), res)
+
+  partial def evalFuncVal (env: Env) (fn: Types) (args: List Types) : IO (Env × Types) := do
+    -- first execute each function argument - reduce computation
+    let (newEnv, results) ← evalFuncArgs env args
+    match fn with
+      | Types.funcVal v      => match v with
+        | Fun.builtin name => evalFnNative newEnv name results args
+        | Fun.userDefined fref params body =>
+          let allkeys: List String := match params with
+            | Types.listVal v => v.map fun x => x.toString false
+            | _               => []
+          let (keys, variadic) := splitOnAmpersand allkeys
+          let normalArgs := results.take keys.length
+          let variadicArg := results.drop keys.length
+          let argVals := normalArgs ++ [Types.listVal variadicArg]
+          let argsLevel := if fref.getLevel >= newEnv.getLevel then fref.getLevel + 1 else newEnv.getLevel + 1
+
+          let argsDict := (buildDict argsLevel (keys ++ variadic) argVals)
+          let merged := (newEnv.merge fref).mergeDict argsLevel argsDict
+
+          evalTypes merged body
+        | Fun.macroFn _ _ _ => throw (IO.userError "macro not implemented")
+      | _ => throw (IO.userError s!"`unexpected token, expected: function`")
+
+  partial def evalList (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if List.length lst == 0 then return (env, Types.listVal lst)
+    else
+      let head := lst[0]!
+      match lst[0]! with
+      | Types.symbolVal v => match v with
+        | "def!" => evalDefn env (lst.drop 1)
+        | "let*" => evalLet env (lst.drop 1)
+        | "do" => evalDo env (lst.drop 1)
+        | "if" => evalIf env (lst.drop 1)
+        | "fn*" => makeFn env (lst.drop 1)
+        | "quote" =>
+          if lst.length < 2 then throw (IO.userError "quote: expected 1 argument")
+          else return (env, lst[1]!)
+        | "quasiquote" =>
+          if lst.length < 2 then throw (IO.userError "quasiquote: expected 1 argument")
+          else evalTypes env (quasiquote lst[1]!)
+        | _ => evalFunc env head (lst.drop 1)
+      | _ => evalFunc env head (lst.drop 1)
+
+  partial def evalVec (env: Env) (elems : List Types) : IO (Env × Types) := do
+    let (newEnv, results) ← evalFuncArgs env elems
+    return (newEnv, Types.vecVal (listToVec results))
+
+  partial def evalDict (env: Env) (lst : Dict) : IO (Env × Types) := do
+    let (newEnv, newDict) ← evalDictInner env lst
+    return (newEnv, Types.dictVal newDict)
+
+  partial def evalDictInner (env: Env) (lst : Dict) : IO (Env × Dict) := do
+    match lst with
+      | Dict.empty => return (env, lst)
+      | Dict.insert k _ v restDict =>
+        let (newEnv, newVal) ← evalTypes env v
+        let (updatedEnv, updatedDict) ← evalDictInner newEnv restDict
+        let newDict := Dict.insert k 0 newVal updatedDict
+        return (updatedEnv, newDict)
+
+  partial def evalFuncArgs (env: Env) (args: List Types) : IO (Env × List Types) :=
+    args.foldlM (fun (res : Env × List Types) (x : Types) => do
+      let (r, acc) := res
+      let (updatedenv, res) ← evalTypes r x
+      return (updatedenv, acc ++ [res])
+    ) (env, [])
+
+  partial def evalDefn (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "def! unexpected syntax")
+    else
+      let key := args[0]!
+      let body := args[1]!
+      let (newEnv, value) ← (evalTypes env body)
+      match key with
+        | Types.symbolVal v =>
+          let refResult := newEnv.add (KeyType.strKey v) env.getLevel value
+          return (refResult, value)
+        | _ => throw (IO.userError s!"def! unexpected token, expected: symbol")
+
+  partial def evalLet (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "let*: unexpected syntax")
+    else
+      let pairs := args[0]!
+      let body := args[1]!
+      let newEnv ← match pairs with
+      | Types.listVal v => evalLetArgs env.increment v
+      | Types.vecVal v => evalLetArgs env.increment (toList v)
+      | _ => throw (IO.userError s!"unexpected token type: ${pairs.toString true}, expected: list or vector")
+
+      let (letref, result) ← evalTypes newEnv body
+      return ((forwardOuterScopeDefs letref env), result)
+
+  partial def evalLetArgs (env: Env) (args : List Types) : IO Env := do
+    match args with
+    | [] => return env
+    | [_] => throw (IO.userError "let*: unexpected syntax")
+    | x :: y :: rest =>
+      match x with
+      | Types.symbolVal key =>
+        let (updatedEnv, value) ← evalTypes env y
+        evalLetArgs (updatedEnv.add (KeyType.strKey key) env.getLevel value) rest
+      | _ => throw (IO.userError "let*: unexpected syntax")
+
+  partial def evalDo (env: Env) (args : List Types) : IO (Env × Types) := do
+    -- only return last computation result
+    let (newEnv, results) ← evalFuncArgs env args
+    if results.length == 0 then return (newEnv, Types.Nil)
+    else return (newEnv, results[results.length - 1]!)
+
+  partial def evalIf (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "unexpected syntax")
+    else
+      let condition := args[0]!
+      let thenExpr := args[1]!
+      let hasElse := args.length > 2
+
+      let (newEnv, condResp) ← evalTypes env condition
+      let cond := match condResp with
+      | Types.boolVal v => v
+      | Types.Nil => false
+      | _ => true
+      if cond then evalTypes newEnv thenExpr
+      else if hasElse then evalTypes newEnv args[2]!
+      else return (newEnv, Types.Nil)
+
+  partial def swapAtom (env: Env) (lst: List Types) (args: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "swap!: >= 2 argument required")
+  else
+    let first := lst[0]!
+    let fn := lst[1]!
+    let rest := lst.drop 2
+    match args[0]! with
+    | Types.symbolVal sym =>
+      match fn with
+      | Types.funcVal _ =>
+        match env.get (KeyType.strKey sym) with
+        | none => throw (IO.userError s!"{sym} not found")
+        | some (level, _) => match first with
+          | Types.atomVal x => match x with
+            | Atom.v v =>
+              let (_, res) ← evalFuncVal env fn ([v] ++ rest)
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.v res))
+              return (newEnv, res)
+            | Atom.withmeta v meta =>
+              let (_, res) ← evalFuncVal env fn ([v] ++ rest)
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.withmeta res meta))
+              return (newEnv, res)
+          | x => throw (IO.userError s!"swap!: unexpected symbol: {x.toString true}, expected: atom")
+      | x => throw (IO.userError s!"swap!: unexpected symbol: {x.toString true}, expected: function")
+    | x => throw (IO.userError s!"swap!: unexpected token: {x.toString true}, expected: symbol")
+
+  partial def eval (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if lst.length < 1 then throw (IO.userError "eval: unexpected syntax")
+    else
+      let ast := lst[0]!
+      -- any new variables are defined on level 0
+      let env0 := Env.data 0 env.getDict
+      evalTypes env0 ast
+
+  partial def starts_with (lst: List Types) (symb: String) : Bool :=
+    if lst.length == 2 then
+      match lst[0]! with
+      | Types.symbolVal v => v == symb
+      | _ => false
+    else false
+
+  partial def qq_loop (elt : Types) (acc: List Types): List Types :=
+    match elt with
+    | Types.listVal v =>
+      if starts_with v "splice-unquote"
+      then
+        [Types.symbolVal "concat", v[1]!, Types.listVal acc]
+      else
+        [Types.symbolVal "cons", quasiquote elt, Types.listVal acc]
+    | _ => [Types.symbolVal "cons", quasiquote elt, Types.listVal acc]
+
+  partial def qq_foldr (lst : List Types): Types :=
+    let res := lst.reverse.foldl (fun acc x => qq_loop x acc) []
+    Types.listVal res
+
+  partial def quasiquote (ast: Types) : Types :=
+    match ast with
+    | Types.symbolVal _ => Types.listVal [Types.symbolVal "quote", ast]
+    | Types.dictVal _ => Types.listVal [Types.symbolVal "quote", ast]
+    | Types.listVal v =>
+      if starts_with v "unquote" then v[1]!
+      else qq_foldr v
+    | Types.vecVal v => Types.listVal [Types.symbolVal "vec", qq_foldr (toList v)]
+    | _ => ast
+
+  partial def evalFnNative (env : Env) (name: String) (results: List Types) (args: List Types): IO (Env × Types) := do
+    match name with
+    | "+" => sum env results
+    | "-" => sub env results
+    | "*" => mul env results
+    | "/" => div env results
+    | "<" => lt env results
+    | "<=" => lte env results
+    | ">" => gt env results
+    | ">=" => gte env results
+    | "=" => eq env results false
+    | "list" => return (env, Types.listVal results)
+    | "count" => countFunc env results
+    | "cons" => cons env results
+    | "concat" => concat env results
+    | "vec" => makeVec env results
+    | "atom" => makeAtom env results
+    | "deref" => derefAtom env results
+    | "reset!" => resetAtom env results args
+    | "swap!" => swapAtom env results args
+    | "prn" => prnFunc env results
+    | "pr-str" => prStrFunc env results
+    | "str" => strFunc env results
+    | "println" => printlnFunc env results
+    | "eval" => eval env results
+    | "read-string" =>
+      let res ← readString results env -- readString results Dict.empty
+      return (env, res)
+    | _ => match results with
+        | [x] => match x with
+          | Types.listVal x => match name with
+            | "list?" => return (env, Types.boolVal true)
+            | "empty?" => return (env, Types.boolVal (x.length == 0))
+            | _ => return (env, Types.boolVal false)
+          | Types.vecVal x => match name with
+            | "empty?" => return (env, Types.boolVal ((toList x).length == 0))
+            | _ => return (env, Types.boolVal false)
+          | Types.atomVal _ => match name with
+            | "atom?" => return (env, Types.boolVal true)
+            | _ => return (env, Types.boolVal false)
+          | _   => return (env, Types.boolVal false)
+        | _   => throw (IO.userError s!"'{name}' not found")
+
+end
+
+def READ (input : String): Except String Types :=
+  read_str input
+
+def PRINT (ast : Types): String :=
+  pr_str true ast
+
+def rep (env: Env) (input : String): IO (Env × String) := do
+  match READ input with
+  | Except.ok result =>
+    try
+      let (newenv, res) ← evalTypes env result
+      return (newenv, PRINT res)
+    catch
+      | e => return (env, s!"Error: {e}")
+  | Except.error err => return (env, s!"Parsing failed: {err}")
+
+def loadMalFns (env: Env) (fndefs: List String): IO (Env × String) := do
+  fndefs.foldlM (fun (res : Env × String) fndef => do
+    let (ref, msg) := res
+    let (newref, newmsg) ← rep ref fndef
+    return (newref, s!"{msg}¬{newmsg}")
+  ) (env, "")
+
+def fnDefs: List String := [
+    "(def! not (fn* (a) (if a false true)))",
+    "(def! load-file (fn* (f) (eval (read-string (str \"(do \" (slurp f) \"\nnil)\")))))",
+  ]
+
+def repAndPrint (env: Env) (output : String): IO Env := do
+  if output.endsWith "endofinput" then IO.print ""
+  else IO.println output
+  return env
+
+def reploop (inienv: Env) : IO Unit := do
+  let mut donext := false
+  let mut env := inienv
+  donext := true
+  while donext do
+    IO.print "user> "
+    let stdin ← IO.getStdin
+    let input ← stdin.getLine
+    let value := input.trim
+    if value = "exit" then
+      donext := false
+      IO.println "Exiting REPL."
+    if value.isEmpty then
+      donext := false
+    else
+      let (newenv, value) ← rep env value
+      env ← repAndPrint newenv value
+
+def main (args : List String) : IO Unit := do
+  let (env0, _) ← loadMalFns (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
+  let env := setSymbol env0 "*ARGV*" (Types.listVal [])
+
+  if args.length > 0 then do
+    let astArgs := ((args.drop 1).map (fun arg => Types.strVal arg))
+    let newenv := setSymbol env0 "*ARGV*" (Types.listVal astArgs)
+    let (_, _) ← rep newenv s!"(load-file \"{args[0]!}\")"
+    IO.Process.exit 0
+  else reploop env
diff --git a/impls/lean/LeanMal/step8_macros.lean b/impls/lean/LeanMal/step8_macros.lean
new file mode 100644
index 0000000000..e09c56c139
--- /dev/null
+++ b/impls/lean/LeanMal/step8_macros.lean
@@ -0,0 +1,390 @@
+import LeanMal.reader
+import LeanMal.printer
+import LeanMal.core
+
+universe u
+
+def makeFn (env: Env) (args : List Types) : IO (Env × Types) := do
+  if args.length < 2 then throw (IO.userError "unexpected syntax")
+  else
+    let p := args[0]!
+    let body := args[1]!
+    let params := match p with
+      | Types.vecVal x => Types.listVal (toList x)
+      | _ => p
+    let newfn := Fun.userDefined env.increment params body
+    return (env, Types.funcVal newfn)
+
+def splitOnAmpersand (input : List String) : (List String × List String) :=
+  let rec loop (acc1 : List String) (rest : List String) : (List String × List String) :=
+    match rest with
+    | []         => (acc1, [])  -- If no "&" found, second list is empty
+    | "&" :: xs  => match xs with
+      | [] => (acc1, [])  -- If "&" is the last element, second list is empty
+      | y :: _ => (acc1, [y])  -- Add the next element after "&" to the second list
+    | x :: xs    => loop (acc1 ++ [x]) xs  -- Accumulate elements before "&"
+  loop [] input
+
+mutual
+  partial def evalTypes (env : Env) (ast : Types) : IO (Env × Types) := do
+    if getDebugEval env then IO.println s!"EVAL:{pr_str true ast}"
+    match ast with
+    | Types.symbolVal v   => match env.get (KeyType.strKey v) with
+      | some (_, vi) => return (env, vi)
+      | none => throw (IO.userError s!"'{v}' not found")
+    | Types.listVal el    => (evalList env el)
+    | Types.vecVal el     => (evalVec env (toList el))
+    | Types.dictVal el    => (evalDict env el)
+    | x                   => return (env, x)
+
+  partial def evalFunc (env: Env) (head : Types) (args : List Types) : IO (Env × Types) := do
+    let (env2, fn) ← evalTypes env head
+    let (fref, res) ← evalFuncVal env2 fn args
+    return ((forwardOuterScopeDefs fref env), res)
+
+  partial def evalFuncVal (env: Env) (fn: Types) (args: List Types) : IO (Env × Types) := do
+    match fn with
+      | Types.funcVal v    => match v with
+        | Fun.builtin name =>
+          let (newEnv, results) ← evalFuncArgs env args
+          evalFnNative newEnv name results args
+        | Fun.userDefined fref params body =>
+          let (newEnv, results) ← evalFuncArgs env args
+          let allkeys: List String := match params with
+            | Types.listVal v => v.map fun x => x.toString false
+            | _               => []
+          let (keys, variadic) := splitOnAmpersand allkeys
+          let normalArgs := results.take keys.length
+          let variadicArg := results.drop keys.length
+          let argVals := normalArgs ++ [Types.listVal variadicArg]
+          let argsLevel := if fref.getLevel >= newEnv.getLevel then fref.getLevel + 1 else newEnv.getLevel + 1
+          let argsDict := (buildDict argsLevel (keys ++ variadic) argVals)
+          let merged := (newEnv.merge fref).mergeDict argsLevel argsDict
+          evalTypes merged body
+        | Fun.macroFn fref params body =>
+          let allkeys: List String := match params with
+              | Types.listVal v => v.map fun x => x.toString false
+              | _               => []
+            let (keys, variadic) := splitOnAmpersand allkeys
+          let normalArgs := args.take keys.length
+          let variadicArg := args.drop keys.length
+          let argVals := normalArgs ++ [Types.listVal variadicArg]
+          let argsLevel := if fref.getLevel >= env.getLevel then fref.getLevel + 1 else env.getLevel + 1
+          let argsDict := (buildDict argsLevel (keys ++ variadic) argVals)
+          let merged := (env.merge fref).mergeDict argsLevel argsDict
+          let (_, newast) ← evalTypes merged body
+          evalTypes env newast
+      | _ => throw (IO.userError s!"`unexpected token, expected: function`")
+
+  partial def evalList (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if List.length lst == 0 then return (env, Types.listVal lst)
+    else
+      let head := lst[0]!
+      match lst[0]! with
+      | Types.symbolVal v => match v with
+        | "def!" => evalDefn env (lst.drop 1)
+        | "let*" => evalLet env (lst.drop 1)
+        | "do" => evalDo env (lst.drop 1)
+        | "if" => evalIf env (lst.drop 1)
+        | "fn*" => makeFn env (lst.drop 1)
+        | "quote" =>
+          if lst.length < 2 then throw (IO.userError "quote: expected 1 argument")
+          else return (env, lst[1]!)
+        | "quasiquote" =>
+          if lst.length < 2 then throw (IO.userError "quasiquote: expected 1 argument")
+          else evalTypes env (quasiquote lst[1]!)
+        | "defmacro!" => evalDefMacro env (lst.drop 1)
+        | _ => evalFunc env head (lst.drop 1)
+      | _ => evalFunc env head (lst.drop 1)
+
+  partial def evalVec (env: Env) (elems : List Types) : IO (Env × Types) := do
+    let (newEnv, results) ← evalFuncArgs env elems
+    return (newEnv, Types.vecVal (listToVec results))
+
+  partial def evalDict (env: Env) (lst : Dict) : IO (Env × Types) := do
+    let (newEnv, newDict) ← evalDictInner env lst
+    return (newEnv, Types.dictVal newDict)
+
+  partial def evalDictInner (env: Env) (lst : Dict) : IO (Env × Dict) := do
+    match lst with
+      | Dict.empty => return (env, lst)
+      | Dict.insert k _ v restDict =>
+        let (newEnv, newVal) ← evalTypes env v
+        let (updatedEnv, updatedDict) ← evalDictInner newEnv restDict
+        let newDict := Dict.insert k 0 newVal updatedDict
+        return (updatedEnv, newDict)
+
+  partial def evalFuncArgs (env: Env) (args: List Types) : IO (Env × List Types) :=
+    args.foldlM (fun (res : Env × List Types) (x : Types) => do
+      let (r, acc) := res
+      let (updatedenv, res) ← evalTypes r x
+      return (updatedenv, acc ++ [res])
+    ) (env, [])
+
+  partial def evalDefn (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "def! unexpected syntax")
+    else
+      let key := args[0]!
+      let body := args[1]!
+      let (newEnv, value) ← (evalTypes env body)
+      match key with
+        | Types.symbolVal v =>
+          let refResult := newEnv.add (KeyType.strKey v) env.getLevel value
+          return (refResult, value)
+        | _ => throw (IO.userError s!"def! unexpected token, expected: symbol")
+
+  partial def evalDefMacro (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "defmacro! unexpected syntax")
+    else
+      let key := args[0]!
+      let body := args[1]!
+      let (newEnv, value) ← evalTypes env body
+      match key with
+      | Types.symbolVal v =>
+        match value with
+        | Types.funcVal func =>
+          match func with
+          | Fun.macroFn _ _ _ =>
+            let refResult := newEnv.add (KeyType.strKey v) env.getLevel value
+            return (refResult, value)
+          | Fun.userDefined fref params body =>
+            let res := (Types.funcVal (Fun.macroFn fref params body))
+            let refResult := newEnv.add (KeyType.strKey v) env.getLevel res
+            return (refResult, res)
+          | _ => throw (IO.userError s!"defmacro!: unexpected builtin function")
+        | x => throw (IO.userError s!"unexpected token type: {x.toString true}, expected: function")
+      | _ => throw (IO.userError s!"def! unexpected token, expected: symbol")
+
+  partial def evalLet (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "let*: unexpected syntax")
+    else
+      let pairs := args[0]!
+      let body := args[1]!
+      let newEnv ← match pairs with
+      | Types.listVal v => evalLetArgs env.increment v
+      | Types.vecVal v => evalLetArgs env.increment (toList v)
+      | _ => throw (IO.userError s!"unexpected token type: ${pairs.toString true}, expected: list or vector")
+
+      let (letref, result) ← evalTypes newEnv body
+      return ((forwardOuterScopeDefs letref env), result)
+
+  partial def evalLetArgs (env: Env) (args : List Types) : IO Env := do
+    match args with
+    | [] => return env
+    | [_] => throw (IO.userError "let*: unexpected syntax")
+    | x :: y :: rest =>
+      match x with
+      | Types.symbolVal key =>
+        let (updatedEnv, value) ← evalTypes env y
+        evalLetArgs (updatedEnv.add (KeyType.strKey key) env.getLevel value) rest
+      | _ => throw (IO.userError "let*: unexpected syntax")
+
+  partial def evalDo (env: Env) (args : List Types) : IO (Env × Types) := do
+    -- only return last computation result
+    let (newEnv, results) ← evalFuncArgs env args
+    if results.length == 0 then return (newEnv, Types.Nil)
+    else return (newEnv, results[results.length - 1]!)
+
+  partial def evalIf (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "unexpected syntax")
+    else
+      let condition := args[0]!
+      let thenExpr := args[1]!
+      let hasElse := args.length > 2
+
+      let (newEnv, condResp) ← evalTypes env condition
+      let cond := match condResp with
+      | Types.boolVal v => v
+      | Types.Nil => false
+      | _ => true
+      if cond then evalTypes newEnv thenExpr
+      else if hasElse then evalTypes newEnv args[2]!
+      else return (newEnv, Types.Nil)
+
+  partial def swapAtom (env: Env) (lst: List Types) (args: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "swap!: >= 2 argument required")
+  else
+    let first := lst[0]!
+    let fn := lst[1]!
+    let rest := lst.drop 2
+    match args[0]! with
+    | Types.symbolVal sym =>
+      match fn with
+      | Types.funcVal _ =>
+        match env.get (KeyType.strKey sym) with
+        | none => throw (IO.userError s!"{sym} not found")
+        | some (level, _) => match first with
+          | Types.atomVal x => match x with
+            | Atom.v v =>
+              let (_, res) ← evalFuncVal env fn ([v] ++ rest)
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.v res))
+              return (newEnv, res)
+            | Atom.withmeta v meta =>
+              let (_, res) ← evalFuncVal env fn ([v] ++ rest)
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.withmeta res meta))
+              return (newEnv, res)
+          | x => throw (IO.userError s!"swap!: unexpected symbol: {x.toString true}, expected: atom")
+      | x => throw (IO.userError s!"swap!: unexpected symbol: {x.toString true}, expected: function")
+    | x => throw (IO.userError s!"swap!: unexpected token: {x.toString true}, expected: symbol")
+
+  partial def eval (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if lst.length < 1 then throw (IO.userError "eval: unexpected syntax")
+    else
+      let ast := lst[0]!
+      -- any new variables are defined on level 0
+      let env0 := Env.data 0 env.getDict
+      evalTypes env0 ast
+
+  partial def starts_with (lst: List Types) (symb: String) : Bool :=
+    if lst.length == 2 then
+      match lst[0]! with
+      | Types.symbolVal v => v == symb
+      | _ => false
+    else false
+
+  partial def qq_loop (elt : Types) (acc: List Types): List Types :=
+    match elt with
+    | Types.listVal v =>
+      if starts_with v "splice-unquote"
+      then
+        [Types.symbolVal "concat", v[1]!, Types.listVal acc]
+      else
+        [Types.symbolVal "cons", quasiquote elt, Types.listVal acc]
+    | _ => [Types.symbolVal "cons", quasiquote elt, Types.listVal acc]
+
+  partial def qq_foldr (lst : List Types): Types :=
+    let res := lst.reverse.foldl (fun acc x => qq_loop x acc) []
+    Types.listVal res
+
+  partial def quasiquote (ast: Types) : Types :=
+    match ast with
+    | Types.symbolVal _ => Types.listVal [Types.symbolVal "quote", ast]
+    | Types.dictVal _ => Types.listVal [Types.symbolVal "quote", ast]
+    | Types.listVal v =>
+      if starts_with v "unquote" then v[1]!
+      else qq_foldr v
+    | Types.vecVal v => Types.listVal [Types.symbolVal "vec", qq_foldr (toList v)]
+    | _ => ast
+
+  partial def evalFnNative (env : Env) (name: String) (results: List Types) (args: List Types): IO (Env × Types) := do
+    match name with
+    | "+" => sum env results
+    | "-" => sub env results
+    | "*" => mul env results
+    | "/" => div env results
+    | "<" => lt env results
+    | "<=" => lte env results
+    | ">" => gt env results
+    | ">=" => gte env results
+    | "=" => eq env results false
+    | "list" => return (env, Types.listVal results)
+    | "count" => countFunc env results
+    | "cons" => cons env results
+    | "concat" => concat env results
+    | "vec" => makeVec env results
+    | "nth" => nthSeq env results
+    | "first" => firstSeq env results
+    | "rest" => restSeq env results
+    | "atom" => makeAtom env results
+    | "deref" => derefAtom env results
+    | "reset!" => resetAtom env results args
+    | "swap!" => swapAtom env results args
+    | "prn" => prnFunc env results
+    | "pr-str" => prStrFunc env results
+    | "str" => strFunc env results
+    | "println" => printlnFunc env results
+    | "eval" => eval env results
+    | "read-string" =>
+      let res ← readString results env -- readString results Dict.empty
+      return (env, res)
+    | _ => match results with
+        | [x] => match x with
+          | Types.listVal x => match name with
+            | "list?" => return (env, Types.boolVal true)
+            | "empty?" => return (env, Types.boolVal (x.length == 0))
+            | _ => return (env, Types.boolVal false)
+          | Types.vecVal x => match name with
+            | "empty?" => return (env, Types.boolVal ((toList x).length == 0))
+            | _ => return (env, Types.boolVal false)
+          | Types.atomVal _ => match name with
+            | "atom?" => return (env, Types.boolVal true)
+            | _ => return (env, Types.boolVal false)
+          | Types.funcVal func =>
+            match name with
+            | "fn?" => match func with
+              | Fun.builtin _ => return (env, Types.boolVal true)
+              | Fun.userDefined _ _ _ => return (env, Types.boolVal true)
+              | Fun.macroFn _ _ _ =>  return (env, Types.boolVal false)
+            | "macro?" => match func with
+              | Fun.builtin _ => return (env, Types.boolVal false)
+              | Fun.userDefined _ _ _ => return (env, Types.boolVal false)
+              | Fun.macroFn _ _ _ => return (env, Types.boolVal true)
+            | _ => return (env, Types.boolVal false)
+          | _   => return (env, Types.boolVal false)
+        | _   => throw (IO.userError s!"'{name}' not found")
+
+end
+
+def READ (input : String): Except String Types :=
+  read_str input
+
+def PRINT (ast : Types): String :=
+  pr_str true ast
+
+def rep (env: Env) (input : String): IO (Env × String) := do
+  match READ input with
+  | Except.ok result =>
+    try
+      let (newenv, res) ← evalTypes env result
+      return (newenv, PRINT res)
+    catch
+      | e => return (env, s!"Error: {e}")
+  | Except.error err => return (env, s!"Parsing failed: {err}")
+
+def loadMalFns (env: Env) (fndefs: List String): IO (Env × String) := do
+  fndefs.foldlM (fun (res : Env × String) fndef => do
+    let (ref, msg) := res
+    let (newref, newmsg) ← rep ref fndef
+    return (newref, s!"{msg}¬{newmsg}")
+  ) (env, "")
+
+def fnDefs: List String := [
+    "(def! *host-language* \"Lean\")",
+    "(def! not (fn* (a) (if a false true)))",
+    "(def! load-file (fn* (f) (eval (read-string (str \"(do \" (slurp f) \"\nnil)\")))))",
+    "(defmacro! cond (fn* (& xs) (if (> (count xs) 0) (list 'if (first xs) (if (> (count xs) 1) (nth xs 1) (throw \"odd number of forms to cond\")) (cons 'cond (rest (rest xs)))))))",
+  ]
+
+def repAndPrint (env: Env) (output : String): IO Env := do
+  if output.endsWith "endofinput" then IO.print ""
+  else IO.println output
+  return env
+
+def reploop (inienv: Env) : IO Unit := do
+  let mut donext := false
+  let mut env := inienv
+  donext := true
+  while donext do
+    IO.print "user> "
+    let stdin ← IO.getStdin
+    let input ← stdin.getLine
+    let value := input.trim
+    if value = "exit" then
+      donext := false
+      IO.println "Exiting REPL."
+    if value.isEmpty then
+      donext := false
+    else
+      let (newenv, value) ← rep env value
+      env ← repAndPrint newenv value
+
+def main (args : List String) : IO Unit := do
+  let (env0, _) ← loadMalFns (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
+  let env := setSymbol env0 "*ARGV*" (Types.listVal [])
+
+  if args.length > 0 then do
+    let astArgs := ((args.drop 1).map (fun arg => Types.strVal arg))
+    let newenv := setSymbol env0 "*ARGV*" (Types.listVal astArgs)
+    let (_, _) ← rep newenv s!"(load-file \"{args[0]!}\")"
+    IO.Process.exit 0
+  else reploop env
diff --git a/impls/lean/LeanMal/step9_try.lean b/impls/lean/LeanMal/step9_try.lean
new file mode 100644
index 0000000000..86c5093f48
--- /dev/null
+++ b/impls/lean/LeanMal/step9_try.lean
@@ -0,0 +1,496 @@
+import LeanMal.reader
+import LeanMal.printer
+import LeanMal.core
+
+universe u
+
+def makeFn (env: Env) (args : List Types) : IO (Env × Types) := do
+  if args.length < 2 then throw (IO.userError "unexpected syntax")
+  else
+    let p := args[0]!
+    let body := args[1]!
+    let params := match p with
+      | Types.vecVal x => Types.listVal (toList x)
+      | _ => p
+    let newfn := Fun.userDefined env.increment params body
+    return (env, Types.funcVal newfn)
+
+def splitOnAmpersand (input : List String) : (List String × List String) :=
+  let rec loop (acc1 : List String) (rest : List String) : (List String × List String) :=
+    match rest with
+    | []         => (acc1, [])  -- If no "&" found, second list is empty
+    | "&" :: xs  => match xs with
+      | [] => (acc1, [])  -- If "&" is the last element, second list is empty
+      | y :: _ => (acc1, [y])  -- Add the next element after "&" to the second list
+    | x :: xs    => loop (acc1 ++ [x]) xs  -- Accumulate elements before "&"
+  loop [] input
+
+mutual
+  partial def evalTypes (env : Env) (ast : Types) : IO (Env × Types) := do
+    if getDebugEval env then IO.println s!"EVAL:{pr_str true ast}"
+    match ast with
+    | Types.symbolVal v   => match env.get (KeyType.strKey v) with
+      | some (_, vi) => return (env, vi)
+      | none => throw (IO.userError s!"'{v}' not found")
+    | Types.listVal el    => (evalList env el)
+    | Types.vecVal el     => (evalVec env (toList el))
+    | Types.dictVal el    => (evalDict env el)
+    | x                   => return (env, x)
+
+  partial def evalFunc (env: Env) (head : Types) (args : List Types) : IO (Env × Types) := do
+    let (env2, fn) ← evalTypes env head
+    let (fref, res) ← evalFuncVal env2 fn args true
+    return ((forwardOuterScopeDefs fref env), res)
+
+  partial def evalFuncVal (env: Env) (fn: Types) (args: List Types) (evaluateArgs: Bool) : IO (Env × Types) := do
+    match fn with
+      | Types.funcVal v    => match v with
+        | Fun.builtin name =>
+          let (newEnv, results) ← if !evaluateArgs then
+            pure (env, args)
+          else
+            evalFuncArgs env args
+          evalFnNative newEnv name results args
+        | Fun.userDefined fenv params body =>
+          let (newEnv, results) ← if !evaluateArgs then
+            pure (env, args)
+          else
+            evalFuncArgs env args
+
+          let allkeys: List String := match params with
+            | Types.listVal v => v.map fun x => x.toString false
+            | _               => []
+          let (keys, variadic) := splitOnAmpersand allkeys
+          let normalArgs := results.take keys.length
+          let variadicArg := results.drop keys.length
+          let argVals := normalArgs ++ [Types.listVal variadicArg]
+          let argsLevel := if fenv.getLevel >= newEnv.getLevel then fenv.getLevel + 1 else newEnv.getLevel + 1
+          let argsDict := (buildDict argsLevel (keys ++ variadic) argVals)
+          let merged := (newEnv.merge fenv).mergeDict argsLevel argsDict
+          evalTypes merged body
+        | Fun.macroFn fenv params body =>
+          let allkeys: List String := match params with
+              | Types.listVal v => v.map fun x => x.toString false
+              | _               => []
+            let (keys, variadic) := splitOnAmpersand allkeys
+          let normalArgs := args.take keys.length
+          let variadicArg := args.drop keys.length
+          let argVals := normalArgs ++ [Types.listVal variadicArg]
+          let argsLevel := if fenv.getLevel >= env.getLevel then fenv.getLevel + 1 else env.getLevel + 1
+          let argsDict := (buildDict argsLevel (keys ++ variadic) argVals)
+          let merged := (env.merge fenv).mergeDict argsLevel argsDict
+          let (_, newast) ← evalTypes merged body
+          evalTypes env newast
+      | _ => throw (IO.userError s!"`unexpected token, expected: function`")
+
+  partial def evalList (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if List.length lst == 0 then return (env, Types.listVal lst)
+    else
+      let head := lst[0]!
+      match head with
+      | Types.symbolVal v => match v with
+        | "def!" => evalDefn env (lst.drop 1)
+        | "let*" => evalLet env (lst.drop 1)
+        | "do" => evalDo env (lst.drop 1)
+        | "if" => evalIf env (lst.drop 1)
+        | "fn*" => makeFn env (lst.drop 1)
+        | "try*" => evalTry env (lst.drop 1)
+        | "quote" =>
+          if lst.length < 2 then throw (IO.userError "quote: expected 1 argument")
+          else return (env, lst[1]!)
+        | "quasiquote" =>
+          if lst.length < 2 then throw (IO.userError "quasiquote: expected 1 argument")
+          else evalTypes env (quasiquote lst[1]!)
+        | "defmacro!" => evalDefMacro env (lst.drop 1)
+        | _ => evalFunc env head (lst.drop 1)
+      | _ => evalFunc env head (lst.drop 1)
+
+  partial def evalVec (env: Env) (elems : List Types) : IO (Env × Types) := do
+    let (newEnv, results) ← evalFuncArgs env elems
+    return (newEnv, Types.vecVal (listToVec results))
+
+  partial def evalDict (env: Env) (lst : Dict) : IO (Env × Types) := do
+    let (newEnv, newDict) ← evalDictInner env lst
+    return (newEnv, Types.dictVal newDict)
+
+  partial def evalDictInner (env: Env) (lst : Dict) : IO (Env × Dict) := do
+    match lst with
+      | Dict.empty => return (env, lst)
+      | Dict.insert k _ v restDict =>
+        let (newEnv, newVal) ← evalTypes env v
+        let (updatedEnv, updatedDict) ← evalDictInner newEnv restDict
+        let newDict := Dict.insert k 0 newVal updatedDict
+        return (updatedEnv, newDict)
+
+  partial def evalFuncArgs (env: Env) (args: List Types) : IO (Env × List Types) :=
+    args.foldlM (fun (res : Env × List Types) (x : Types) => do
+      let (r, acc) := res
+      let (updatedenv, res) ← evalTypes r x
+      return (updatedenv, acc ++ [res])
+    ) (env, [])
+
+  partial def evalDefn (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "def! unexpected syntax")
+    else
+      let key := args[0]!
+      let body := args[1]!
+      let (newEnv, value) ← (evalTypes env body)
+      match key with
+        | Types.symbolVal v =>
+          let envResult := newEnv.add (KeyType.strKey v) env.getLevel value
+          return (envResult, value)
+        | _ => throw (IO.userError s!"def! unexpected token, expected: symbol")
+
+  partial def evalDefMacro (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "def! unexpected syntax")
+    else
+      let key := args[0]!
+      let body := args[1]!
+      let (newEnv, value) ← evalTypes env body
+      match key with
+      | Types.symbolVal v =>
+        match value with
+        | Types.funcVal func =>
+          match func with
+          | Fun.macroFn _ _ _ =>
+            let envResult := newEnv.add (KeyType.strKey v) env.getLevel value
+            return (envResult, value)
+          | Fun.userDefined fenv params body =>
+            let envResult := newEnv.add (KeyType.strKey v) env.getLevel (Types.funcVal (Fun.macroFn fenv params body))
+            return (envResult, value)
+          | _ => throw (IO.userError s!"defmacro!: unexpected builtin function")
+        | x => throw (IO.userError s!"unexpected token type: {x.toString true}, expected: function")
+      | _ => throw (IO.userError s!"def! unexpected token, expected: symbol")
+
+  partial def evalLet (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "let*: unexpected syntax")
+    else
+      let pairs := args[0]!
+      let body := args[1]!
+      let newEnv ← match pairs with
+      | Types.listVal v => evalLetArgs env.increment v
+      | Types.vecVal v => evalLetArgs env.increment (toList v)
+      | _ => throw (IO.userError s!"unexpected token type: ${pairs.toString true}, expected: list or vector")
+
+      let (letenv, result) ← evalTypes newEnv body
+      return ((forwardOuterScopeDefs letenv env), result)
+
+  partial def evalLetArgs (env: Env) (args : List Types) : IO Env := do
+    match args with
+    | [] => return env
+    | [_] => throw (IO.userError "let*: unexpected syntax")
+    | x :: y :: rest =>
+      match x with
+      | Types.symbolVal key =>
+        let (updatedEnv, value) ← evalTypes env y
+        evalLetArgs (updatedEnv.add (KeyType.strKey key) env.getLevel value) rest
+      | _ => throw (IO.userError "let*: unexpected syntax")
+
+  partial def evalDo (env: Env) (args : List Types) : IO (Env × Types) := do
+    -- only return last computation result
+    let (newEnv, results) ← evalFuncArgs env args
+    if results.length == 0 then return (newEnv, Types.Nil)
+    else return (newEnv, results[results.length - 1]!)
+
+  partial def evalIf (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "unexpected syntax")
+    else
+      let condition := args[0]!
+      let thenExpr := args[1]!
+      let hasElse := args.length > 2
+
+      let (newEnv, condResp) ← evalTypes env condition
+      let cond := match condResp with
+      | Types.boolVal v => v
+      | Types.Nil => false
+      | _ => true
+      if cond then evalTypes newEnv thenExpr
+      else if hasElse then evalTypes newEnv args[2]!
+      else return (newEnv, Types.Nil)
+
+  partial def evalTry (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if lst.length < 1 then throw (IO.userError "try*: unexpected syntax")
+    else
+      try
+        let (newEnv, result) ← evalTypes env lst[0]!
+        return (newEnv, result)
+      catch
+      | evalErr =>
+        if lst.length < 2 then throw evalErr
+        else
+          match lst[1]! with
+          | Types.listVal catchBody =>
+            if catchBody.length < 1 then throw (IO.userError "try*: unexpected syntax")
+            else
+              match catchBody[0]! with
+              | Types.symbolVal catchSymbol =>
+                if catchSymbol == "catch*" then
+                  if catchBody.length < 2 then throw (IO.userError "try*: unexpected syntax")
+                  else
+                    let es := catchBody[1]!
+                    match es with
+                    | Types.symbolVal errorSymbol =>
+                      let err := Types.strVal evalErr.toString
+                      if catchBody.length < 2 then throw (IO.userError "try*: unexpected syntax")
+                      else
+                        let toeval := catchBody[2]!
+                        let built := buildDictWithSymbols env.getDict env.getLevel [errorSymbol] [err]
+                        let merged := env.mergeDict (env.getLevel + 1) built
+                        evalTypes merged toeval
+                    | _ => throw (IO.userError s!"unexpected return type, expected: symbol")
+                else throw evalErr
+              | _ => throw evalErr
+          -- | Types.vecVal v => -- TODO
+          | _ => throw evalErr
+
+  partial def swapAtom (env: Env) (lst: List Types) (args: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "swap!: >= 2 argument required")
+  else
+    let first := lst[0]!
+    let fn := lst[1]!
+    let rest := lst.drop 2
+    match args[0]! with
+    | Types.symbolVal sym =>
+      match fn with
+      | Types.funcVal _ =>
+        match env.get (KeyType.strKey sym) with
+        | none => throw (IO.userError s!"{sym} not found")
+        | some (level, _) => match first with
+          | Types.atomVal x => match x with
+            | Atom.v v =>
+              let (_, res) ← evalFuncVal env fn ([v] ++ rest) false
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.v res))
+              return (newEnv, res)
+            | Atom.withmeta v meta =>
+              let (_, res) ← evalFuncVal env fn ([v] ++ rest) false
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.withmeta res meta))
+              return (newEnv, res)
+          | x => throw (IO.userError s!"swap!: unexpected symbol: {x.toString true}, expected: atom")
+      | x => throw (IO.userError s!"swap!: unexpected symbol: {x.toString true}, expected: function")
+    | x => throw (IO.userError s!"swap!: unexpected token: {x.toString true}, expected: symbol")
+
+  partial def eval (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if lst.length < 1 then throw (IO.userError "eval: unexpected syntax")
+    else
+      let ast := lst[0]!
+      -- any new variables are defined on level 0
+      let env0 := Env.data 0 env.getDict
+      evalTypes env0 ast
+
+  partial def starts_with (lst: List Types) (symb: String) : Bool :=
+    if lst.length == 2 then
+      match lst[0]! with
+      | Types.symbolVal v => v == symb
+      | _ => false
+    else false
+
+  partial def qq_loop (elt : Types) (acc: List Types): List Types :=
+    match elt with
+    | Types.listVal v =>
+      if starts_with v "splice-unquote"
+      then
+        [Types.symbolVal "concat", v[1]!, Types.listVal acc]
+      else
+        [Types.symbolVal "cons", quasiquote elt, Types.listVal acc]
+    | _ => [Types.symbolVal "cons", quasiquote elt, Types.listVal acc]
+
+  partial def qq_foldr (lst : List Types): Types :=
+    let res := lst.reverse.foldl (fun acc x => qq_loop x acc) []
+    Types.listVal res
+
+  partial def quasiquote (ast: Types) : Types :=
+    match ast with
+    | Types.symbolVal _ => Types.listVal [Types.symbolVal "quote", ast]
+    | Types.dictVal _ => Types.listVal [Types.symbolVal "quote", ast]
+    | Types.listVal v =>
+      if starts_with v "unquote" then v[1]!
+      else qq_foldr v
+    | Types.vecVal v => Types.listVal [Types.symbolVal "vec", qq_foldr (toList v)]
+    | _ => ast
+
+  partial def nativeMapOverList (env: Env) (fn: Types) (args: List Types) : IO (Env × Types) := do
+  let finalResult ← args.foldlM (fun (res : (Env × List Types)) (x : Types) => do
+    let (r, acc) := res
+    let (updatedRef, res) ← evalFuncVal r fn [x] false
+    pure (updatedRef, acc ++ [res])
+  ) (env, [])
+
+  let (newEnv, results) := finalResult
+  pure (newEnv, Types.listVal results)
+
+  partial def nativeMap (env: Env) (lst: List Types) : IO (Env × Types) := do
+    if lst.length < 2 then throw (IO.userError "map: unexpected syntax")
+    else
+      let fn := lst[0]!
+      let params := lst[1]!
+      match fn with
+      | Types.funcVal _ =>
+        match params with
+        | Types.listVal v => nativeMapOverList env fn v
+        | Types.vecVal v => nativeMapOverList env fn (toList v)
+        | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: list or vector")
+      | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: function")
+
+  partial def nativeApply (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if lst.length < 2 then throw (IO.userError "apply: unexpected syntax")
+    else
+      let fn := lst[0]!
+      let vecargs := lst[lst.length-1]!
+      let n := lst.length-2
+      let firstargs := lst.drop 1 |>.take n
+      match vecargs with
+        | Types.listVal v =>
+          evalFuncVal env fn (firstargs ++ v) false
+        | Types.vecVal v =>
+          evalFuncVal env fn (firstargs ++ (toList v)) false
+        | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: list or vector")
+
+  partial def evalFnNative (env : Env) (name: String) (results: List Types) (args: List Types): IO (Env × Types) := do
+      match name with
+      | "+" => sum env results
+      | "-" => sub env results
+      | "*" => mul env results
+      | "/" => div env results
+      | "<" => lt env results
+      | "<=" => lte env results
+      | ">" => gt env results
+      | ">=" => gte env results
+      | "=" => eq env results false
+      | "list" => return (env, Types.listVal results)
+      | "count" => countFunc env results
+      | "cons" => cons env results
+      | "concat" => concat env results
+      | "map" => nativeMap env results
+      | "apply" => nativeApply env results
+      | "vec" => makeVec env results
+      | "vector" => makeVector env results
+      | "nth" => nthSeq env results
+      | "first" => firstSeq env results
+      | "rest" => restSeq env results
+      | "conj" => conj env results
+      | "seq" => seq env results
+      | "hash-map" => makeDict env results
+      | "assoc" => assocDict env results
+      | "dissoc" => dissocDict env results
+      | "get" => getDict env results
+      | "contains?" => containsDict env results
+      | "keys" => getKeysDict env results
+      | "vals" => getValuesDict env results
+      | "throw" => throwFn env results
+      | "symbol" => makeSymbol env results
+      | "keyword" => makeKeyword env results
+      | "atom" => makeAtom env results
+      | "deref" => derefAtom env results
+      | "reset!" => resetAtom env results args
+      | "swap!" => swapAtom env results args
+      | "prn" => prnFunc env results
+      | "pr-str" => prStrFunc env results
+      | "str" => strFunc env results
+      | "println" => printlnFunc env results
+      | "eval" => eval env results
+      | "read-string" =>
+      let res ← readString results env -- readString results Dict.empty
+      return (env, res)
+      | _ => match results with
+          | [x] => match x with
+            | Types.Nil => if name == "nil?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.intVal _ => if name == "number?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.floatVal _ => if name == "number?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.strVal _ => if name == "string?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.symbolVal _ => if name == "symbol?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.keywordVal _ => if name == "keyword?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.dictVal _ => if name == "map?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.listVal x => match name with
+              | "list?" => return (env, Types.boolVal true)
+              | "sequential?" => return (env, Types.boolVal true)
+              | "empty?" => return (env, Types.boolVal (x.length == 0))
+              | _ => return (env, Types.boolVal false)
+            | Types.vecVal x => match name with
+              | "sequential?" => return (env, Types.boolVal true)
+              | "vector?" => return (env, Types.boolVal true)
+              | "empty?" => return (env, Types.boolVal ((toList x).length == 0))
+              | _ => return (env, Types.boolVal false)
+            | Types.boolVal x => match name with
+              | "true?" => return (env, Types.boolVal x)
+              | "false?" => return (env, Types.boolVal !x)
+              | _ => return (env, Types.boolVal false)
+            | Types.atomVal _ => match name with
+              | "atom?" => return (env, Types.boolVal true)
+              | _ => return (env, Types.boolVal false)
+            | Types.funcVal func => match name with
+              | "fn?" => match func with
+                | Fun.builtin _ => return (env, Types.boolVal true)
+                | Fun.userDefined _ _ _ => return (env, Types.boolVal true)
+                | Fun.macroFn _ _ _ =>  return (env, Types.boolVal false)
+              | "macro?" => match func with
+                | Fun.builtin _ => return (env, Types.boolVal false)
+                | Fun.userDefined _ _ _ => return (env, Types.boolVal false)
+                | Fun.macroFn _ _ _ =>  return (env, Types.boolVal true)
+              | _ => return (env, Types.boolVal false)
+          | _   => throw (IO.userError s!"'{name}' not found")
+
+end
+
+def READ (input : String): Except String Types :=
+  read_str input
+
+def PRINT (ast : Types): String :=
+  pr_str true ast
+
+def rep (env: Env) (input : String): IO (Env × String) := do
+  match READ input with
+  | Except.ok result =>
+    try
+      let (newenv, res) ← evalTypes env result
+      return (newenv, PRINT res)
+    catch
+      | e => return (env, s!"Error: {e}")
+  | Except.error err => return (env, s!"Parsing failed: {err}")
+
+def loadMalFns (env: Env) (fndefs: List String): IO (Env × String) := do
+  fndefs.foldlM (fun (res : Env × String) fndef => do
+    let (ref, msg) := res
+    let (newref, newmsg) ← rep ref fndef
+    return (newref, s!"{msg}¬{newmsg}")
+  ) (env, "")
+
+def fnDefs: List String := [
+    "(def! *host-language* \"Lean\")",
+    "(def! not (fn* (a) (if a false true)))",
+    "(def! load-file (fn* (f) (eval (read-string (str \"(do \" (slurp f) \"\nnil)\")))))",
+    "(defmacro! cond (fn* (& xs) (if (> (count xs) 0) (list 'if (first xs) (if (> (count xs) 1) (nth xs 1) (throw \"odd number of forms to cond\")) (cons 'cond (rest (rest xs)))))))",
+  ]
+
+def repAndPrint (env: Env) (output : String): IO Env := do
+  if output.endsWith "endofinput" then IO.print ""
+  else IO.println output
+  return env
+
+def reploop (inienv: Env) : IO Unit := do
+  let mut donext := false
+  let mut env := inienv
+  donext := true
+  while donext do
+    IO.print "user> "
+    let stdin ← IO.getStdin
+    let input ← stdin.getLine
+    let value := input.trim
+    if value = "exit" then
+      donext := false
+      IO.println "Exiting REPL."
+    if value.isEmpty then
+      donext := false
+    else
+      let (newenv, value) ← rep env value
+      env ← repAndPrint newenv value
+
+def main (args : List String) : IO Unit := do
+  let (env0, _) ← loadMalFns (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
+  let env := setSymbol env0 "*ARGV*" (Types.listVal [])
+
+  if args.length > 0 then do
+    let astArgs := ((args.drop 1).map (fun arg => Types.strVal arg))
+    let newenv := setSymbol env0 "*ARGV*" (Types.listVal astArgs)
+    let (_, _) ← rep newenv s!"(load-file \"{args[0]!}\")"
+    IO.Process.exit 0
+  else reploop env
diff --git a/impls/lean/LeanMal/stepA_mal.lean b/impls/lean/LeanMal/stepA_mal.lean
new file mode 100644
index 0000000000..d7206709fc
--- /dev/null
+++ b/impls/lean/LeanMal/stepA_mal.lean
@@ -0,0 +1,502 @@
+import LeanMal.reader
+import LeanMal.printer
+import LeanMal.core
+
+universe u
+
+def makeFn (env: Env) (args : List Types) : IO (Env × Types) := do
+  if args.length < 2 then throw (IO.userError "unexpected syntax")
+  else
+    let p := args[0]!
+    let body := args[1]!
+    let params := match p with
+      | Types.vecVal x => Types.listVal (toList x)
+      | _ => p
+    let newfn := Fun.userDefined env.increment params body
+    return (env, Types.funcVal newfn)
+
+def splitOnAmpersand (input : List String) : (List String × List String) :=
+  let rec loop (acc1 : List String) (rest : List String) : (List String × List String) :=
+    match rest with
+    | []         => (acc1, [])  -- If no "&" found, second list is empty
+    | "&" :: xs  => match xs with
+      | [] => (acc1, [])  -- If "&" is the last element, second list is empty
+      | y :: _ => (acc1, [y])  -- Add the next element after "&" to the second list
+    | x :: xs    => loop (acc1 ++ [x]) xs  -- Accumulate elements before "&"
+  loop [] input
+
+mutual
+  partial def evalTypes (env : Env) (ast : Types) : IO (Env × Types) := do
+    if getDebugEval env then IO.println s!"EVAL:{pr_str true ast}"
+    match ast with
+    | Types.symbolVal v   => match env.get (KeyType.strKey v) with
+      | some (_, vi) => return (env, vi)
+      | none => throw (IO.userError s!"'{v}' not found")
+    | Types.listVal el    => (evalList env el)
+    | Types.vecVal el     => (evalVec env (toList el))
+    | Types.dictVal el    => (evalDict env el)
+    | x                   => return (env, x)
+
+  partial def evalFunc (env: Env) (head : Types) (args : List Types) : IO (Env × Types) := do
+    let (env2, fn) ← evalTypes env head
+    let (fref, res) ← evalFuncVal env2 fn args true
+    return ((forwardOuterScopeDefs fref env), res)
+
+  partial def evalFuncVal (env: Env) (fn: Types) (args: List Types) (evaluateArgs: Bool) : IO (Env × Types) := do
+    match fn with
+      | Types.funcVal v    => match v with
+        | Fun.builtin name =>
+          let (newEnv, results) ← if !evaluateArgs then
+            pure (env, args)
+          else
+            evalFuncArgs env args
+          evalFnNative newEnv name results args
+        | Fun.userDefined fenv params body =>
+          let (newEnv, results) ← if !evaluateArgs then
+            pure (env, args)
+          else
+            evalFuncArgs env args
+
+          let allkeys: List String := match params with
+            | Types.listVal v => v.map fun x => x.toString false
+            | _               => []
+          let (keys, variadic) := splitOnAmpersand allkeys
+          let normalArgs := results.take keys.length
+          let variadicArg := results.drop keys.length
+          let argVals := normalArgs ++ [Types.listVal variadicArg]
+          let argsLevel := if fenv.getLevel >= newEnv.getLevel then fenv.getLevel + 1 else newEnv.getLevel + 1
+          let argsDict := (buildDict argsLevel (keys ++ variadic) argVals)
+          let merged := (newEnv.merge fenv).mergeDict argsLevel argsDict
+          evalTypes merged body
+        | Fun.macroFn fenv params body =>
+          let allkeys: List String := match params with
+              | Types.listVal v => v.map fun x => x.toString false
+              | _               => []
+            let (keys, variadic) := splitOnAmpersand allkeys
+          let normalArgs := args.take keys.length
+          let variadicArg := args.drop keys.length
+          let argVals := normalArgs ++ [Types.listVal variadicArg]
+          let argsLevel := if fenv.getLevel >= env.getLevel then fenv.getLevel + 1 else env.getLevel + 1
+          let argsDict := (buildDict argsLevel (keys ++ variadic) argVals)
+          let merged := (env.merge fenv).mergeDict argsLevel argsDict
+          let (_, newast) ← evalTypes merged body
+          evalTypes env newast
+      | _ => throw (IO.userError s!"`unexpected token, expected: function`")
+
+  partial def evalList (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if List.length lst == 0 then return (env, Types.listVal lst)
+    else
+      let head := lst[0]!
+      match head with
+      | Types.symbolVal v => match v with
+        | "def!" => evalDefn env (lst.drop 1)
+        | "let*" => evalLet env (lst.drop 1)
+        | "do" => evalDo env (lst.drop 1)
+        | "if" => evalIf env (lst.drop 1)
+        | "fn*" => makeFn env (lst.drop 1)
+        | "try*" => evalTry env (lst.drop 1)
+        | "quote" =>
+          if lst.length < 2 then throw (IO.userError "quote: expected 1 argument")
+          else return (env, lst[1]!)
+        | "quasiquote" =>
+          if lst.length < 2 then throw (IO.userError "quasiquote: expected 1 argument")
+          else evalTypes env (quasiquote lst[1]!)
+        | "defmacro!" => evalDefMacro env (lst.drop 1)
+        | _ => evalFunc env head (lst.drop 1)
+      | _ => evalFunc env head (lst.drop 1)
+
+  partial def evalVec (env: Env) (elems : List Types) : IO (Env × Types) := do
+    let (newEnv, results) ← evalFuncArgs env elems
+    return (newEnv, Types.vecVal (listToVec results))
+
+  partial def evalDict (env: Env) (lst : Dict) : IO (Env × Types) := do
+    let (newEnv, newDict) ← evalDictInner env lst
+    return (newEnv, Types.dictVal newDict)
+
+  partial def evalDictInner (env: Env) (lst : Dict) : IO (Env × Dict) := do
+    match lst with
+      | Dict.empty => return (env, lst)
+      | Dict.insert k _ v restDict =>
+        let (newEnv, newVal) ← evalTypes env v
+        let (updatedEnv, updatedDict) ← evalDictInner newEnv restDict
+        let newDict := Dict.insert k 0 newVal updatedDict
+        return (updatedEnv, newDict)
+
+  partial def evalFuncArgs (env: Env) (args: List Types) : IO (Env × List Types) :=
+    args.foldlM (fun (res : Env × List Types) (x : Types) => do
+      let (r, acc) := res
+      let (updatedenv, res) ← evalTypes r x
+      return (updatedenv, acc ++ [res])
+    ) (env, [])
+
+  partial def evalDefn (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "def! unexpected syntax")
+    else
+      let key := args[0]!
+      let body := args[1]!
+      let (newEnv, value) ← (evalTypes env body)
+      match key with
+        | Types.symbolVal v =>
+          let envResult := newEnv.add (KeyType.strKey v) env.getLevel value
+          return (envResult, value)
+        | _ => throw (IO.userError s!"def! unexpected token, expected: symbol")
+
+  partial def evalDefMacro (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "def! unexpected syntax")
+    else
+      let key := args[0]!
+      let body := args[1]!
+      let (newEnv, value) ← evalTypes env body
+      match key with
+      | Types.symbolVal v =>
+        match value with
+        | Types.funcVal func =>
+          match func with
+          | Fun.macroFn _ _ _ =>
+            let envResult := newEnv.add (KeyType.strKey v) env.getLevel value
+            return (envResult, value)
+          | Fun.userDefined fenv params body =>
+            let envResult := newEnv.add (KeyType.strKey v) env.getLevel (Types.funcVal (Fun.macroFn fenv params body))
+            return (envResult, value)
+          | _ => throw (IO.userError s!"defmacro!: unexpected builtin function")
+        | x => throw (IO.userError s!"unexpected token type: {x.toString true}, expected: function")
+      | _ => throw (IO.userError s!"def! unexpected token, expected: symbol")
+
+  partial def evalLet (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "let*: unexpected syntax")
+    else
+      let pairs := args[0]!
+      let body := args[1]!
+      let newEnv ← match pairs with
+      | Types.listVal v => evalLetArgs env.increment v
+      | Types.vecVal v => evalLetArgs env.increment (toList v)
+      | _ => throw (IO.userError s!"unexpected token type: ${pairs.toString true}, expected: list or vector")
+
+      let (letenv, result) ← evalTypes newEnv body
+      return ((forwardOuterScopeDefs letenv env), result)
+
+  partial def evalLetArgs (env: Env) (args : List Types) : IO Env := do
+    match args with
+    | [] => return env
+    | [_] => throw (IO.userError "let*: unexpected syntax")
+    | x :: y :: rest =>
+      match x with
+      | Types.symbolVal key =>
+        let (updatedEnv, value) ← evalTypes env y
+        evalLetArgs (updatedEnv.add (KeyType.strKey key) env.getLevel value) rest
+      | _ => throw (IO.userError "let*: unexpected syntax")
+
+  partial def evalDo (env: Env) (args : List Types) : IO (Env × Types) := do
+    -- only return last computation result
+    let (newEnv, results) ← evalFuncArgs env args
+    if results.length == 0 then return (newEnv, Types.Nil)
+    else return (newEnv, results[results.length - 1]!)
+
+  partial def evalIf (env: Env) (args : List Types) : IO (Env × Types) := do
+    if args.length < 2 then throw (IO.userError "unexpected syntax")
+    else
+      let condition := args[0]!
+      let thenExpr := args[1]!
+      let hasElse := args.length > 2
+
+      let (newEnv, condResp) ← evalTypes env condition
+      let cond := match condResp with
+      | Types.boolVal v => v
+      | Types.Nil => false
+      | _ => true
+      if cond then evalTypes newEnv thenExpr
+      else if hasElse then evalTypes newEnv args[2]!
+      else return (newEnv, Types.Nil)
+
+  partial def evalTry (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if lst.length < 1 then throw (IO.userError "try*: unexpected syntax")
+    else
+      try
+        let (newEnv, result) ← evalTypes env lst[0]!
+        return (newEnv, result)
+      catch
+      | evalErr =>
+        if lst.length < 2 then throw evalErr
+        else
+          match lst[1]! with
+          | Types.listVal catchBody =>
+            if catchBody.length < 1 then throw (IO.userError "try*: unexpected syntax")
+            else
+              match catchBody[0]! with
+              | Types.symbolVal catchSymbol =>
+                if catchSymbol == "catch*" then
+                  if catchBody.length < 2 then throw (IO.userError "try*: unexpected syntax")
+                  else
+                    let es := catchBody[1]!
+                    match es with
+                    | Types.symbolVal errorSymbol =>
+                      let err := Types.strVal evalErr.toString
+                      if catchBody.length < 2 then throw (IO.userError "try*: unexpected syntax")
+                      else
+                        let toeval := catchBody[2]!
+                        let built := buildDictWithSymbols env.getDict env.getLevel [errorSymbol] [err]
+                        let merged := env.mergeDict (env.getLevel + 1) built
+                        evalTypes merged toeval
+                    | _ => throw (IO.userError s!"unexpected return type, expected: symbol")
+                else throw evalErr
+              | _ => throw evalErr
+          -- | Types.vecVal v => -- TODO
+          | _ => throw evalErr
+
+  partial def swapAtom (env: Env) (lst: List Types) (args: List Types) : IO (Env × Types) := do
+  if lst.length < 2 then throw (IO.userError "swap!: >= 2 argument required")
+  else
+    let first := lst[0]!
+    let fn := lst[1]!
+    let rest := lst.drop 2
+    match args[0]! with
+    | Types.symbolVal sym =>
+      match fn with
+      | Types.funcVal _ =>
+        match env.get (KeyType.strKey sym) with
+        | none => throw (IO.userError s!"{sym} not found")
+        | some (level, _) => match first with
+          | Types.atomVal x => match x with
+            | Atom.v v =>
+              let (_, res) ← evalFuncVal env fn ([v] ++ rest) false
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.v res))
+              return (newEnv, res)
+            | Atom.withmeta v meta =>
+              let (_, res) ← evalFuncVal env fn ([v] ++ rest) false
+              let newEnv := env.add (KeyType.strKey sym) level (Types.atomVal (Atom.withmeta res meta))
+              return (newEnv, res)
+          | x => throw (IO.userError s!"swap!: unexpected symbol: {x.toString true}, expected: atom")
+      | x => throw (IO.userError s!"swap!: unexpected symbol: {x.toString true}, expected: function")
+    | x => throw (IO.userError s!"swap!: unexpected token: {x.toString true}, expected: symbol")
+
+  partial def eval (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if lst.length < 1 then throw (IO.userError "eval: unexpected syntax")
+    else
+      let ast := lst[0]!
+      -- any new variables are defined on level 0
+      let env0 := Env.data 0 env.getDict
+      evalTypes env0 ast
+
+  partial def starts_with (lst: List Types) (symb: String) : Bool :=
+    if lst.length == 2 then
+      match lst[0]! with
+      | Types.symbolVal v => v == symb
+      | _ => false
+    else false
+
+  partial def qq_loop (elt : Types) (acc: List Types): List Types :=
+    match elt with
+    | Types.listVal v =>
+      if starts_with v "splice-unquote"
+      then
+        [Types.symbolVal "concat", v[1]!, Types.listVal acc]
+      else
+        [Types.symbolVal "cons", quasiquote elt, Types.listVal acc]
+    | _ => [Types.symbolVal "cons", quasiquote elt, Types.listVal acc]
+
+  partial def qq_foldr (lst : List Types): Types :=
+    let res := lst.reverse.foldl (fun acc x => qq_loop x acc) []
+    Types.listVal res
+
+  partial def quasiquote (ast: Types) : Types :=
+    match ast with
+    | Types.symbolVal _ => Types.listVal [Types.symbolVal "quote", ast]
+    | Types.dictVal _ => Types.listVal [Types.symbolVal "quote", ast]
+    | Types.listVal v =>
+      if starts_with v "unquote" then v[1]!
+      else qq_foldr v
+    | Types.vecVal v => Types.listVal [Types.symbolVal "vec", qq_foldr (toList v)]
+    | _ => ast
+
+  partial def nativeMapOverList (env: Env) (fn: Types) (args: List Types) : IO (Env × Types) := do
+  let finalResult ← args.foldlM (fun (res : (Env × List Types)) (x : Types) => do
+    let (r, acc) := res
+    let (updatedRef, res) ← evalFuncVal r fn [x] false
+    pure (updatedRef, acc ++ [res])
+  ) (env, [])
+
+  let (newEnv, results) := finalResult
+  pure (newEnv, Types.listVal results)
+
+  partial def nativeMap (env: Env) (lst: List Types) : IO (Env × Types) := do
+    if lst.length < 2 then throw (IO.userError "map: unexpected syntax")
+    else
+      let fn := lst[0]!
+      let params := lst[1]!
+      match fn with
+      | Types.funcVal _ =>
+        match params with
+        | Types.listVal v => nativeMapOverList env fn v
+        | Types.vecVal v => nativeMapOverList env fn (toList v)
+        | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: list or vector")
+      | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: function")
+
+  partial def nativeApply (env: Env) (lst : List Types) : IO (Env × Types) := do
+    if lst.length < 2 then throw (IO.userError "apply: unexpected syntax")
+    else
+      let fn := lst[0]!
+      let vecargs := lst[lst.length-1]!
+      let n := lst.length-2
+      let firstargs := lst.drop 1 |>.take n
+      match vecargs with
+        | Types.listVal v =>
+          evalFuncVal env fn (firstargs ++ v) false
+        | Types.vecVal v =>
+          evalFuncVal env fn (firstargs ++ (toList v)) false
+        | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: list or vector")
+
+  partial def evalFnNative (env : Env) (name: String) (results: List Types) (args: List Types): IO (Env × Types) := do
+      match name with
+      | "+" => sum env results
+      | "-" => sub env results
+      | "*" => mul env results
+      | "/" => div env results
+      | "<" => lt env results
+      | "<=" => lte env results
+      | ">" => gt env results
+      | ">=" => gte env results
+      | "=" => eq env results false
+      | "list" => return (env, Types.listVal results)
+      | "count" => countFunc env results
+      | "cons" => cons env results
+      | "concat" => concat env results
+      | "map" => nativeMap env results
+      | "apply" => nativeApply env results
+      | "vec" => makeVec env results
+      | "vector" => makeVector env results
+      | "nth" => nthSeq env results
+      | "first" => firstSeq env results
+      | "rest" => restSeq env results
+      | "conj" => conj env results
+      | "seq" => seq env results
+      | "hash-map" => makeDict env results
+      | "assoc" => assocDict env results
+      | "dissoc" => dissocDict env results
+      | "get" => getDict env results
+      | "contains?" => containsDict env results
+      | "keys" => getKeysDict env results
+      | "vals" => getValuesDict env results
+      | "throw" => throwFn env results
+      | "symbol" => makeSymbol env results
+      | "keyword" => makeKeyword env results
+      | "atom" => makeAtom env results
+      | "deref" => derefAtom env results
+      | "reset!" => resetAtom env results args
+      | "swap!" => swapAtom env results args
+      | "prn" => prnFunc env results
+      | "pr-str" => prStrFunc env results
+      | "str" => strFunc env results
+      | "println" => printlnFunc env results
+      | "eval" => eval env results
+      | "read-string" =>
+      let res ← readString results env -- readString results Dict.empty
+      return (env, res)
+      | "time-ms" => throw (IO.userError "Not implemented")
+      | "meta" => throw (IO.userError  "Not implemented")
+      | "with-meta" => throw (IO.userError  "Not implemented")
+      | "readline" => readline env results
+      | _ => match results with
+          | [x] => match x with
+            | Types.Nil => if name == "nil?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.intVal _ => if name == "number?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.floatVal _ => if name == "number?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.strVal _ => if name == "string?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.symbolVal _ => if name == "symbol?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.keywordVal _ => if name == "keyword?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.dictVal _ => if name == "map?" then return (env, Types.boolVal true) else return (env, Types.boolVal false)
+            | Types.listVal x => match name with
+              | "list?" => return (env, Types.boolVal true)
+              | "sequential?" => return (env, Types.boolVal true)
+              | "empty?" => return (env, Types.boolVal (x.length == 0))
+              | _ => return (env, Types.boolVal false)
+            | Types.vecVal x => match name with
+              | "sequential?" => return (env, Types.boolVal true)
+              | "vector?" => return (env, Types.boolVal true)
+              | "empty?" => return (env, Types.boolVal ((toList x).length == 0))
+              | _ => return (env, Types.boolVal false)
+            | Types.boolVal x => match name with
+              | "true?" => return (env, Types.boolVal x)
+              | "false?" => return (env, Types.boolVal !x)
+              | _ => return (env, Types.boolVal false)
+            | Types.atomVal _ => match name with
+              | "atom?" => return (env, Types.boolVal true)
+              | _ => return (env, Types.boolVal false)
+            | Types.funcVal func => match name with
+              | "fn?" => match func with
+                | Fun.builtin _ => return (env, Types.boolVal true)
+                | Fun.userDefined _ _ _ => return (env, Types.boolVal true)
+                | Fun.macroFn _ _ _ =>  return (env, Types.boolVal false)
+              | "macro?" => match func with
+                | Fun.builtin _ => return (env, Types.boolVal false)
+                | Fun.userDefined _ _ _ => return (env, Types.boolVal false)
+                | Fun.macroFn _ _ _ =>  return (env, Types.boolVal true)
+              | _ => return (env, Types.boolVal false)
+          | _   => throw (IO.userError s!"'{name}' not found")
+
+end
+
+def READ (input : String): Except String Types :=
+  read_str input
+
+def PRINT (ast : Types): String :=
+  pr_str true ast
+
+def rep (env: Env) (input : String): IO (Env × String) := do
+  match READ input with
+  | Except.ok result =>
+    try
+      let (newenv, res) ← evalTypes env result
+      return (newenv, PRINT res)
+    catch
+      | e => return (env, s!"Error: {e}")
+  | Except.error err => return (env, s!"Parsing failed: {err}")
+
+def loadMalFns (env: Env) (fndefs: List String): IO (Env × String) := do
+  fndefs.foldlM (fun (res : Env × String) fndef => do
+    let (ref, msg) := res
+    let (newref, newmsg) ← rep ref fndef
+    return (newref, s!"{msg}¬{newmsg}")
+  ) (env, "")
+
+def fnDefs: List String := [
+    "(def! *host-language* \"Lean\")",
+    "(def! not (fn* (a) (if a false true)))",
+    "(def! load-file (fn* (f) (eval (read-string (str \"(do \" (slurp f) \"\nnil)\")))))",
+    "(defmacro! cond (fn* (& xs) (if (> (count xs) 0) (list 'if (first xs) (if (> (count xs) 1) (nth xs 1) (throw \"odd number of forms to cond\")) (cons 'cond (rest (rest xs)))))))",
+  ]
+
+def repAndPrint (env: Env) (output : String): IO Env := do
+  if output.endsWith "endofinput" then IO.print ""
+  else IO.println output
+  return env
+
+def reploop (inienv: Env) : IO Unit := do
+  let (_, _) ← rep inienv s!"(println (str \"Mal [\" *host-language* \"]\"))"
+
+  let mut donext := false
+  let mut env := inienv
+  donext := true
+  while donext do
+    IO.print "user> "
+    let stdin ← IO.getStdin
+    let input ← stdin.getLine
+    let value := input.trim
+    if value = "exit" then
+      donext := false
+      IO.println "Exiting REPL."
+    if value.isEmpty then
+      donext := false
+    else
+      let (newenv, value) ← rep env value
+      env ← repAndPrint newenv value
+
+def main (args : List String) : IO Unit := do
+  let (env0, _) ← loadMalFns (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
+  let env := setSymbol env0 "*ARGV*" (Types.listVal [])
+
+  if args.length > 0 then do
+    let astArgs := ((args.drop 1).map (fun arg => Types.strVal arg))
+    let newenv := setSymbol env0 "*ARGV*" (Types.listVal astArgs)
+    let (_, _) ← rep newenv s!"(load-file \"{args[0]!}\")"
+    IO.Process.exit 0
+  else reploop env
diff --git a/impls/lean/LeanMal/types.lean b/impls/lean/LeanMal/types.lean
new file mode 100644
index 0000000000..aff8a74ed8
--- /dev/null
+++ b/impls/lean/LeanMal/types.lean
@@ -0,0 +1,288 @@
+import Lean.Data.RBMap
+import Lean
+
+set_option diagnostics true
+set_option genSizeOfSpec false
+set_option diagnostics.threshold 5000
+
+universe u
+
+inductive Vec (α : Type u) : Nat → Type u
+| nil  : Vec α 0
+| cons : α → Vec α n → Vec α (n + 1)
+deriving Repr
+
+-- Define the map function for Vec
+def map {α : Type u} {β : Type v} {n : Nat} (f : α → β) : Vec α n → Vec β n
+| Vec.nil          => Vec.nil
+| Vec.cons x xs    => Vec.cons (f x) (map f xs)
+
+-- Function to convert Vec to List
+def toList {α : Type u} {n : Nat} : Vec α n → List α
+| Vec.nil          => []
+| Vec.cons x xs    => x :: toList xs
+
+def listToVec  : (lst : List Types) → Vec Types lst.length
+  | []      => Vec.nil
+  | x :: xs => Vec.cons x (listToVec xs)
+
+inductive KeyType
+    | strKey : String → KeyType
+    | keywordKey : String → KeyType
+    deriving Repr
+
+mutual
+
+  inductive Types : Type u
+    | strVal (v : String)
+    | intVal (v : Int)
+    | floatVal (v : Float)
+    | boolVal (v : Bool)
+    | symbolVal (sym: String)
+    | keywordVal (key: String)
+    | listVal (el : List Types)
+    | funcVal (el: Fun)
+    | vecVal {n : Nat} (el : Vec Types n)
+    | dictVal (el : Dict)
+    | atomVal (el: Atom)
+    | Nil
+    deriving Repr
+
+  inductive Fun : Type u
+    | builtin (name : String)
+    | userDefined (env: Env) (params : Types) (body : Types)
+    | macroFn (env: Env) (params : Types) (body : Types)
+
+  inductive Dict: Type u
+    | empty : Dict
+    | insert: KeyType → Nat → Types → Dict → Dict
+    deriving Repr
+
+  inductive Env: Type u
+  | data: Nat → Dict → Env
+
+  inductive Atom
+  | v : Types -> Atom
+  | withmeta : Types → Types → Atom
+  deriving Repr
+
+end
+
+instance : Inhabited Env where
+  default := Env.data 0 Dict.empty
+
+instance : Inhabited Dict where
+  default := Dict.empty
+
+instance : Inhabited Types where
+  default := Types.Nil
+
+instance : Inhabited (List Types) where
+  default := []
+
+instance : Inhabited (Dict × Types) where
+  default := (default, default)
+
+def Dict.get : Dict → KeyType → Option (Nat × Types)
+  | Dict.empty, _ => default
+  | Dict.insert k l v d, key =>
+    match k, key with
+    | KeyType.strKey ks, KeyType.strKey keyg => if ks = keyg then some (l, v) else d.get key
+    | KeyType.keywordKey ks, KeyType.keywordKey keyg => if ks = keyg then some (l, v) else d.get key
+    | KeyType.strKey ks, KeyType.keywordKey keyg => if ks = keyg then some (l, v) else d.get key
+    | KeyType.keywordKey ks, KeyType.strKey keyg => if ks = keyg then some (l, v) else d.get key
+
+def Dict.keys : Dict → List KeyType
+  | Dict.empty => []
+  | Dict.insert k _ _ d =>
+    let restKeys := d.keys
+    k :: restKeys
+
+def Dict.values : Dict → List Types
+  | Dict.empty => []
+  | Dict.insert _ _ v d =>
+    let restValues := d.values
+    v :: restValues
+
+def Dict.remove (d : Dict) (key : KeyType) : Dict :=
+  match d with
+  | Dict.empty => Dict.empty
+  | Dict.insert k l v rest =>
+    match k, key with
+      | KeyType.strKey ks, KeyType.strKey keyg => if ks = keyg then rest.remove key else Dict.insert k l v (rest.remove key)
+      | KeyType.keywordKey ks, KeyType.keywordKey keyg => if ks = keyg then rest.remove key else Dict.insert k l v (rest.remove key)
+      | KeyType.strKey ks, KeyType.keywordKey keyg => if ks = keyg then rest.remove key else Dict.insert k l v (rest.remove key)
+      | KeyType.keywordKey ks, KeyType.strKey keyg => if ks = keyg then rest.remove key else Dict.insert k l v (rest.remove key)
+
+def Dict.add : Dict → KeyType → Nat → Types → Dict
+  | Dict.empty, key, level, value => Dict.insert key level value Dict.empty
+  | Dict.insert k _ v d, key, level, value =>
+    match k, key with
+      | KeyType.strKey ks, KeyType.strKey keyg => if ks = keyg then Dict.insert k level value d else Dict.insert k level v (d.add key level value)
+      | KeyType.keywordKey ks, KeyType.keywordKey keyg => if ks = keyg then Dict.insert k level value d else Dict.insert k level v (d.add key level value)
+      | KeyType.strKey ks, KeyType.keywordKey keyg => if ks = keyg then Dict.insert k level value d else Dict.insert k level v (d.add key level value)
+      | KeyType.keywordKey ks, KeyType.strKey keyg => if ks = keyg then Dict.insert k level value d else Dict.insert k level v (d.add key level value)
+
+-- Helper function to fold over all elements in a Dict
+partial def Dict.fold (d : Dict) (init : α) (f : KeyType → Nat → Types → α → α) : α :=
+  match d with
+  | Dict.empty => init
+  | Dict.insert k l v d' => d'.fold (f k l v init) f
+
+-- Function to merge two Dicts.
+def Dict.merge (baseDict overwriteDict : Dict) : Dict :=
+  let merged := overwriteDict.fold baseDict (fun key l v acc =>
+    match acc.get key with
+    | some (lBase, _) =>
+      if l > lBase then acc.add key l v else acc
+    | none => acc.add key l v)
+  merged
+
+-- Function to extract the string from a Types.symbolVal
+def getSymbol (t : Types) : Option String :=
+  match t with
+  | Types.symbolVal sym => some sym
+  | _ => none
+
+def getKeyword (t : Types) : Option String :=
+  match t with
+  | Types.keywordVal key => some key
+  | _ => none
+
+def buildDictWithSymbols (ref: Dict) (level: Nat) (keys : List String) (values : List Types) : Dict :=
+  match keys, values with
+  | [], _ => Dict.empty
+  | _, [] => Dict.empty
+  | key :: keyTail, value :: valueTail =>
+    let val := match value with
+    | Types.symbolVal v =>
+      let entry := ref.get (KeyType.strKey v)
+      match entry with
+      | some (_, v) => v
+      | none => Types.Nil
+    | _ => value
+    let restDict := buildDictWithSymbols ref level keyTail valueTail
+    Dict.insert (KeyType.strKey key) level val restDict
+
+def buildDict (level: Nat) (keys : List String) (values : List Types) : Dict :=
+  match keys, values with
+  | [], _ => Dict.empty
+  | _, [] => Dict.empty
+  | key :: keyTail, value :: valueTail =>
+    let restDict := buildDict level keyTail valueTail
+    Dict.insert (KeyType.strKey key) level value restDict
+
+def Env.getLevel : Env → Nat
+  | Env.data l _ => l
+
+def Env.getDict : Env → Dict
+  | Env.data _ d => d
+
+def Env.get : Env → KeyType → Option (Nat × Types)
+  | Env.data _ d, key => d.get key
+
+def Env.keys : Env → List KeyType
+  | Env.data _ d => d.keys
+
+def Env.values : Env → List KeyType
+  | Env.data _ d => d.keys
+
+def Env.remove : Env → KeyType → Dict
+  | Env.data _ d, key => d.remove key
+
+def Env.add : Env → KeyType → Nat → Types → Env
+  | Env.data l d, key, level, value => Env.data l (d.add key level value)
+
+def Env.increment : Env → Env
+  | Env.data l d => Env.data (l + 1) d
+
+def Env.merge : Env → Env → Env
+  | Env.data _ d, e2 =>  Env.data e2.getLevel (d.merge e2.getDict)
+
+def Env.mergeDict : Env → Nat → Dict → Env
+  | Env.data _ d, level2, d2 =>  Env.data level2 (d.merge d2)
+
+def Types.toBool: Types -> Bool
+  | Types.boolVal v => if v then true else false
+  | Types.Nil => false
+  | _ => true
+
+def getFirst! (lst : List Types) : Types :=
+  match lst with
+  | []      => default
+  | x :: _  => x
+
+def escapeString (input : String) : String :=
+  input.foldl (fun acc c =>
+    acc ++ match c with
+      | '\\' => "\\\\"
+      -- | '"' => "\\\""
+      | '\"' => "\\\""
+      | '\n' => "\\n"
+      | _ => String.singleton c
+  ) ""
+
+mutual
+  partial def Types.toString (readably: Bool) (t:Types) : String :=
+    match t with
+    | Types.strVal v => stringToString readably v
+    | Types.intVal v => s!"{v}"
+    | Types.floatVal v => s!"{v}"
+    | Types.boolVal v => s!"{v}"
+    | Types.funcVal el => Fun.toString readably el
+    -- | Types.funcVal v => "(" ++ s!"{(Types.toString v)}" ++ ")"
+    | Types.listVal el => s!"({String.intercalate " " (el.map (Types.toString readably))})"
+    | Types.dictVal el => "{" ++ s!"{Dict.toString readably el}" ++ "}"
+    | Types.Nil => "nil"
+    | Types.symbolVal sym => s!"{sym}"
+    | Types.keywordVal key => s!":{key}"
+    | Types.vecVal el =>
+      let content := toList el
+      s!"[{String.intercalate " " (content.map (Types.toString readably))}]"
+    | Types.atomVal el => Atom.toString readably el
+
+  partial def stringToString (readably: Bool) (v:String) : String :=
+    if readably then s!"\"{escapeString v}\""
+    else v
+
+  partial def Atom.toString (readably: Bool) (t:Atom) : String :=
+    match t with
+    | Atom.v v => s!"(atom {v.toString readably})"
+    | Atom.withmeta v _ => s!"(atom {v.toString readably})"
+
+  partial def Fun.toString (readably: Bool) (t:Fun) : String :=
+    match t with
+    | Fun.userDefined _ params body => "(fn* " ++ s!"{(Types.toString readably params)}" ++ s!"{(Types.toString readably body)}" ++ ")"
+    | Fun.macroFn _ params body => "(fn* " ++ s!"{(Types.toString readably params)}" ++ s!"{(Types.toString readably body)}" ++ ")"
+    | Fun.builtin name => s!"{name}"
+
+  partial def Dict.toString (readably: Bool) (d:Dict) : String :=
+    match d with
+    | Dict.empty => ""
+    | Dict.insert key _ value Dict.empty =>
+      match key with
+      | KeyType.strKey k => s!"\"{k}\" {Types.toString readably value}"
+      | KeyType.keywordKey k => s!":{k} {Types.toString readably value}"
+    | Dict.insert key _ value rest =>
+      let restStr := Dict.toString readably rest
+      match key with
+      | KeyType.strKey k => s!"{restStr} \"{k}\" {Types.toString readably value}"
+      | KeyType.keywordKey k => s!"{restStr} :{k} {Types.toString readably value}"
+
+  partial def Dict.toStringWithLevels (readably: Bool) (d:Dict) : String :=
+    match d with
+    | Dict.empty => ""
+    | Dict.insert key l value Dict.empty =>
+      match key with
+      | KeyType.strKey k => s!"\"{k}\" ({l}) {Types.toString readably value}"
+      | KeyType.keywordKey k => s!":{k} ({l}) {Types.toString readably value}"
+    | Dict.insert key l value rest =>
+      let restStr := Dict.toStringWithLevels readably rest
+      match key with
+      | KeyType.strKey k => s!"{restStr} \"{k}\" ({l}) {Types.toString readably value}"
+      | KeyType.keywordKey k => s!"{restStr} :{k} ({l}) {Types.toString readably value}"
+end
+
+def Env.toString (readably: Bool) (e:Env) : String :=
+  match e with
+  | Env.data l d => s!"level: {l} dict: {d.toStringWithLevels readably}"
diff --git a/impls/lean/Makefile b/impls/lean/Makefile
new file mode 100644
index 0000000000..93795e1d1c
--- /dev/null
+++ b/impls/lean/Makefile
@@ -0,0 +1,22 @@
+# List of Lean binaries you want to produce
+LEAN_BINARIES = step0_repl step1_read_print step2_eval step3_env \
+                step4_if_fn_do step5_tco step6_file step7_quote \
+                step8_macros step9_try stepA_mal
+
+# Default target to build all binaries
+all: $(LEAN_BINARIES)
+
+# Target for each Lean binary
+$(LEAN_BINARIES): % : .lake/build/bin/%
+	cp $< ./
+
+# Trigger the Lean build if binaries do not exist
+.lake/build/bin/%:
+	lake build
+
+# Phony targets to avoid file name conflicts
+.PHONY: all clean
+
+# Clean up all generated binaries
+clean:
+	rm -f $(LEAN_BINARIES) && rm -rf ./.lake/build/bin
diff --git a/impls/lean/README.md b/impls/lean/README.md
new file mode 100644
index 0000000000..180ffcfa72
--- /dev/null
+++ b/impls/lean/README.md
@@ -0,0 +1 @@
+# mal
diff --git a/impls/lean/lake-manifest.json b/impls/lean/lake-manifest.json
new file mode 100644
index 0000000000..dafe18e287
--- /dev/null
+++ b/impls/lean/lake-manifest.json
@@ -0,0 +1,95 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a975dea2c4d8258a55b4f9861c537e2bb0f9ef63",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "776a5a8f9c789395796e442d78a9d4cb9c4c9d03",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.41",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b72af9fce632c0cc0fa928dc1a55efb9f0aa68da",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "9447739fe9714f8a091192bad5cd5e7b5a8ae1e4",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-parser",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a145b9deb3272fb8af7d26d06f5ab70ae5e3d575",
+   "name": "Parser",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.toml"}],
+ "name": "mal",
+ "lakeDir": ".lake"}
diff --git a/impls/lean/lakefile.lean b/impls/lean/lakefile.lean
new file mode 100644
index 0000000000..319790024a
--- /dev/null
+++ b/impls/lean/lakefile.lean
@@ -0,0 +1,75 @@
+import Lake
+open Lake DSL
+
+package "mal" where
+  -- Settings applied to both builds and interactive editing
+  leanOptions := #[
+    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
+  ]
+  -- add any additional package configuration options here
+
+require Parser from git "https://github.com/fgdorais/lean4-parser" @ "main"
+
+@[default_target]
+lean_lib LeanMal where
+  -- add any library configuration options here
+
+@[default_target]
+lean_exe "step0_repl" {
+  root := `LeanMal.step0_repl
+}
+
+@[default_target]
+lean_exe "step1_read_print" {
+  root := `LeanMal.step1_read_print
+}
+
+@[default_target]
+lean_exe "step2_eval" {
+  root := `LeanMal.step2_eval
+}
+
+@[default_target]
+lean_exe "step3_env" {
+  root := `LeanMal.step3_env
+}
+
+@[default_target]
+lean_exe "step4_if_fn_do" {
+  root := `LeanMal.step4_if_fn_do
+}
+
+@[default_target]
+lean_exe "step5_tco" {
+  root := `LeanMal.step5_tco
+}
+
+@[default_target]
+lean_exe "step6_file" {
+  root := `LeanMal.step6_file
+}
+
+@[default_target]
+lean_exe "step7_quote" {
+  root := `LeanMal.step7_quote
+}
+
+@[default_target]
+lean_exe "step8_macros" {
+  root := `LeanMal.step8_macros
+}
+
+@[default_target]
+lean_exe "step9_try" {
+  root := `LeanMal.step9_try
+}
+
+@[default_target]
+lean_exe "stepA_mal" {
+  root := `LeanMal.stepA_mal
+}
+
+@[default_target]
+lean_exe "mal" {
+  root := `LeanMal.step1_read_print
+}
diff --git a/impls/lean/lean-toolchain b/impls/lean/lean-toolchain
new file mode 100644
index 0000000000..e7a4f40b89
--- /dev/null
+++ b/impls/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.11.0-rc2
diff --git a/impls/lean/run b/impls/lean/run
new file mode 100755
index 0000000000..8ba68a5484
--- /dev/null
+++ b/impls/lean/run
@@ -0,0 +1,2 @@
+#!/bin/bash
+exec $(dirname $0)/${STEP:-stepA_mal} "${@}"