diff --git a/core/src/eval/macro_expand.rs b/core/src/eval/macro_expand.rs
index 6e691a7..14ad2be 100644
--- a/core/src/eval/macro_expand.rs
+++ b/core/src/eval/macro_expand.rs
@@ -1,5 +1,18 @@
+use crate::Map;
 use crate::term::module::LoadedModules;
-use crate::term::{Decl, SourceContext};
+use crate::term::{
+  Constructor, Decl, Def, Identifier, Literal, ModulePath, NameRef, Par, SourceContext,
+  Term::{self, Ann, App, Con, Ctx, Forall, Lam, Lit, Pi, Quote, Var},
+  app, apps, case, forall, lam, match_term, param, pi_name,
+};
+
+/// Recursively strip Ctx wrappers from a term.
+fn strip_ctx(term: Term) -> Term {
+  match term {
+    Ctx { term: t, .. } => strip_ctx(*t),
+    other => other,
+  }
+}
 
 /// Maximum macro expansion depth to prevent infinite recursion
 const MAX_EXPANSION_DEPTH: u64 = 64;
@@ -20,9 +33,7 @@ impl std::fmt::Display for MacroError {
       MacroError::NonTermReturn { name } => {
         write!(f, "macro `{name}` did not return a Term value")
       }
-      MacroError::MacroNotFound { name } => {
-        write!(f, "macro `{name}` not found")
-      }
+      MacroError::MacroNotFound { name } => write!(f, "macro `{name}` not found"),
       MacroError::Generic(msg) => write!(f, "{msg}"),
     }
   }
@@ -34,6 +45,461 @@ pub fn expand_macros(
   decls: Vec<SourceContext<Decl>>,
   _loaded: &LoadedModules,
 ) -> Result<Vec<SourceContext<Decl>>, MacroError> {
-  // TODO: implement macro expansion
-  Ok(decls)
+  let macro_defs: Map<ModulePath, Def> = decls
+    .iter()
+    .filter_map(|ctx| match ctx.value() {
+      Decl::DefMacro(def) => Some((def.name.clone(), def.clone())),
+      _ => None,
+    })
+    .collect();
+
+  decls
+    .into_iter()
+    .map(|ctx| expand_decl(ctx, &macro_defs))
+    .collect()
+}
+
+fn expand_decl(
+  ctx: SourceContext<Decl>,
+  macro_defs: &Map<ModulePath, Def>,
+) -> Result<SourceContext<Decl>, MacroError> {
+  let decl = ctx.value().clone();
+  match decl {
+    Decl::DefMacro(_) => Ok(ctx),
+    Decl::Def(mut def) => {
+      def.term = expand_term(def.term, macro_defs, 0)?;
+      Ok(ctx.map(|_| Decl::Def(def)))
+    }
+    other => Ok(ctx.map(|_| other)),
+  }
+}
+
+/// Walk a term and expand macro calls.
+fn expand_term(
+  term: Term,
+  macro_defs: &Map<ModulePath, Def>,
+  depth: u64,
+) -> Result<Term, MacroError> {
+  if depth > MAX_EXPANSION_DEPTH {
+    return Err(MacroError::DepthLimitExceeded);
+  }
+  match term {
+    App { fun, arg } => {
+      // Check for name! macro call
+      if let Var {
+        name: NameRef::Macro(name),
+      } = &*fun
+      {
+        let path = ModulePath::single(name.clone());
+        if let Some(def) = macro_defs.get(&path) {
+          let arg = expand_term(*arg, macro_defs, depth)?;
+          return apply_macro(def, vec![arg], macro_defs, depth);
+        }
+      }
+      // Check for chained name! a b macro call
+      if let App { .. } = &*fun {
+        let child_fun = fun.clone();
+        let child_arg = arg.clone();
+        if let Some((name, mut args)) = collect_macro_args(*child_fun, *child_arg) {
+          let path = ModulePath::single(name.clone());
+          if let Some(def) = macro_defs.get(&path) {
+            for a in args.iter_mut() {
+              let old = std::mem::replace(a, Term::Hole);
+              *a = expand_term(old, macro_defs, depth)?;
+            }
+            // Now args has the original fun and arg, so we continue with the next iteration
+            // but the macro has already been looked up, so this won't match again
+            return apply_macro(def, args, macro_defs, depth);
+          }
+        }
+      }
+      // Not a macro call (or macro not found) — recurse normally
+      Ok(App {
+        fun: Box::new(expand_term(*fun, macro_defs, depth)?),
+        arg: Box::new(expand_term(*arg, macro_defs, depth)?),
+      })
+    }
+    Lam { param, body } => Ok(Lam {
+      param,
+      body: Box::new(expand_term(*body, macro_defs, depth)?),
+    }),
+    Quote { term } => Ok(Quote {
+      term: Box::new(resolve_quote(*term, macro_defs, depth)?),
+    }),
+    Ctx { loc, term } => Ok(Ctx {
+      loc,
+      term: Box::new(expand_term(*term, macro_defs, depth)?),
+    }),
+    Pi {
+      arg_name,
+      arg,
+      ret,
+      mult,
+    } => Ok(Pi {
+      arg_name,
+      arg: Box::new(expand_term(*arg, macro_defs, depth)?),
+      ret: Box::new(expand_term(*ret, macro_defs, depth)?),
+      mult,
+    }),
+    Forall { name, typ, body } => Ok(Forall {
+      name,
+      typ: Box::new(expand_term(*typ, macro_defs, depth)?),
+      body: Box::new(expand_term(*body, macro_defs, depth)?),
+    }),
+    Ann { term, typ } => Ok(Ann {
+      term: Box::new(expand_term(*term, macro_defs, depth)?),
+      typ: Box::new(expand_term(*typ, macro_defs, depth)?),
+    }),
+    Lit {
+      value: Literal::Match { value, cases },
+    } => {
+      let value = expand_term(*value, macro_defs, depth)?;
+      let cases = cases
+        .into_iter()
+        .map(|c| {
+          let value = expand_term(*c.value, macro_defs, depth)?;
+          Ok(case(c.name, c.args, value))
+        })
+        .collect::<Result<Vec<_>, MacroError>>()?;
+      Ok(match_term(value, cases))
+    }
+    Lit {
+      value: Literal::If { value, then, els },
+    } => {
+      let value = expand_term(*value, macro_defs, depth)?;
+      let then = expand_term(*then, macro_defs, depth)?;
+      let els = expand_term(*els, macro_defs, depth)?;
+      Ok(Term::Lit {
+        value: Literal::If {
+          value: Box::new(value),
+          then: Box::new(then),
+          els: Box::new(els),
+        },
+      })
+    }
+    Con(Constructor {
+      typ_name,
+      args,
+      name,
+      num_args,
+    }) => {
+      let args: Vec<Option<Term>> = args
+        .into_iter()
+        .map(|a| a.map(|t| expand_term(t, macro_defs, depth)).transpose())
+        .collect::<Result<Vec<_>, MacroError>>()?;
+      Ok(Con(Constructor {
+        name,
+        typ_name,
+        args,
+        num_args,
+      }))
+    }
+    other => Ok(other),
+  }
+}
+
+/// Resolve unquote calls inside a Quote body and expand any macro calls.
+fn resolve_quote(
+  term: Term,
+  macro_defs: &Map<ModulePath, Def>,
+  depth: u64,
+) -> Result<Term, MacroError> {
+  match term {
+    App { fun, arg } => {
+      // Check for unquote
+      if let Var {
+        name: NameRef::Id(n),
+      } = &*fun
+        && n.as_str() == "unquote"
+      {
+        // unquote(arg): splice arg into the output, then expand it
+        let arg = resolve_quote(*arg, macro_defs, depth)?;
+        // The spliced result may contain macro calls
+        expand_term(arg, macro_defs, depth)
+      } else {
+        // Check for name! macro call
+        if let Var {
+          name: NameRef::Macro(name),
+        } = &*fun
+        {
+          let path = ModulePath::single(name.clone());
+          if let Some(def) = macro_defs.get(&path) {
+            let arg = resolve_quote(*arg, macro_defs, depth)?;
+            return apply_macro(def, vec![arg], macro_defs, depth);
+          }
+        }
+        // Check for chained name! a b macro call
+        if let App { .. } = &*fun {
+          let child_fun = fun.clone();
+          let child_arg = arg.clone();
+          if let Some((name, mut args)) = collect_macro_args(*child_fun, *child_arg) {
+            let path = ModulePath::single(name.clone());
+            if let Some(def) = macro_defs.get(&path) {
+              for a in args.iter_mut() {
+                let old = std::mem::replace(a, Term::Hole);
+                *a = resolve_quote(old, macro_defs, depth)?;
+              }
+              return apply_macro(def, args, macro_defs, depth);
+            }
+          }
+        }
+        // Not a macro call — recurse
+        Ok(App {
+          fun: Box::new(resolve_quote(*fun, macro_defs, depth)?),
+          arg: Box::new(resolve_quote(*arg, macro_defs, depth)?),
+        })
+      }
+    }
+    Lam { param, body } => Ok(Lam {
+      param,
+      body: Box::new(resolve_quote(*body, macro_defs, depth)?),
+    }),
+    Quote { term } => {
+      // Nested quote — don't resolve unquotes (they belong to the inner quote)
+      Ok(Quote {
+        term: Box::new(resolve_quote(*term, macro_defs, depth)?),
+      })
+    }
+    Ctx { loc, term } => Ok(Ctx {
+      loc,
+      term: Box::new(resolve_quote(*term, macro_defs, depth)?),
+    }),
+    Pi {
+      arg_name,
+      arg,
+      ret,
+      mult,
+    } => Ok(Pi {
+      arg_name,
+      arg: Box::new(resolve_quote(*arg, macro_defs, depth)?),
+      ret: Box::new(resolve_quote(*ret, macro_defs, depth)?),
+      mult,
+    }),
+    Forall { name, typ, body } => Ok(Forall {
+      name,
+      typ: Box::new(resolve_quote(*typ, macro_defs, depth)?),
+      body: Box::new(resolve_quote(*body, macro_defs, depth)?),
+    }),
+    Ann { term, typ } => Ok(Ann {
+      term: Box::new(resolve_quote(*term, macro_defs, depth)?),
+      typ: Box::new(resolve_quote(*typ, macro_defs, depth)?),
+    }),
+    Lit {
+      value: Literal::Match { value, cases },
+    } => {
+      let value = resolve_quote(*value, macro_defs, depth)?;
+      let cases = cases
+        .into_iter()
+        .map(|c| {
+          let value = resolve_quote(*c.value, macro_defs, depth)?;
+          Ok(case(c.name, c.args, value))
+        })
+        .collect::<Result<Vec<_>, MacroError>>()?;
+      Ok(match_term(value, cases))
+    }
+    Lit {
+      value: Literal::If { value, then, els },
+    } => {
+      let value = resolve_quote(*value, macro_defs, depth)?;
+      let then = resolve_quote(*then, macro_defs, depth)?;
+      let els = resolve_quote(*els, macro_defs, depth)?;
+      Ok(Term::Lit {
+        value: Literal::If {
+          value: Box::new(value),
+          then: Box::new(then),
+          els: Box::new(els),
+        },
+      })
+    }
+    Con(Constructor {
+      typ_name,
+      args,
+      name,
+      num_args,
+    }) => {
+      let args: Vec<Option<Term>> = args
+        .into_iter()
+        .map(|a| a.map(|t| resolve_quote(t, macro_defs, depth)).transpose())
+        .collect::<Result<Vec<_>, MacroError>>()?;
+      Ok(Con(Constructor {
+        name,
+        typ_name,
+        args,
+        num_args,
+      }))
+    }
+    other => Ok(other),
+  }
+}
+
+/// Check if a term has a macro call somewhere in a chain of Apps.
+fn has_macro_in_chain(term: &Term) -> bool {
+  match term {
+    Var {
+      name: NameRef::Macro(_),
+    } => true,
+    App { fun, arg: _ } => has_macro_in_chain(fun),
+    _ => false,
+  }
+}
+
+/// Collect arguments from a chained App, checking if it's a macro call.
+/// Returns None if not a macro call.
+/// Returns Some((name, args)) if it is, with args in left-to-right order.
+fn collect_macro_args(fun: Term, arg: Term) -> Option<(Identifier, Vec<Term>)> {
+  match fun {
+    Var {
+      name: NameRef::Macro(name),
+    } => Some((name, vec![arg])),
+    App {
+      fun: inner_fun,
+      arg: inner_arg,
+    } => {
+      let (name, mut args) = collect_macro_args(*inner_fun, *inner_arg)?;
+      args.push(arg);
+      Some((name, args))
+    }
+    _ => None,
+  }
+}
+
+/// Apply macro to args, producing the expanded term.
+fn apply_macro(
+  def: &Def,
+  args: Vec<Term>,
+  macro_defs: &Map<ModulePath, Def>,
+  depth: u64,
+) -> Result<Term, MacroError> {
+  if depth > MAX_EXPANSION_DEPTH {
+    return Err(MacroError::DepthLimitExceeded);
+  }
+
+  // Peel off one Lam per arg and substitute
+  let mut body = def.term.clone();
+  for arg in args {
+    body = match body {
+      Lam { param, body: b } => match param {
+        Par::P(p) => subst_macro(*b, &NameRef::Id(p.name.clone()), &arg),
+        Par::I { .. } => {
+          return Err(MacroError::Generic("macro with implicit parameter".into()));
+        }
+      },
+      _ => {
+        return Err(MacroError::Generic("too many arguments for macro".into()));
+      }
+    };
+  }
+
+  // Strip Ctx wrappers and find the Quote body
+  let body = strip_ctx(body);
+  match body {
+    Quote { term } => resolve_quote(*term, macro_defs, depth),
+    _ => Err(MacroError::NonTermReturn {
+      name: def.name.to_string(),
+    }),
+  }
+}
+
+/// Substitute variable references in a term WITHOUT capture-avoiding rename
+/// of lambda binders. This is used for macro parameter substitution where
+/// the outer lambda wrapping the macro body is being consumed, not protected.
+fn subst_macro(term: Term, name: &NameRef, replacement: &Term) -> Term {
+  match term {
+    Var { name: n } if &n == name => replacement.clone(),
+    Lam { param: p, body: b } => {
+      let should_skip = match (&p, name) {
+        (Par::P(p_name), NameRef::Id(n)) => &p_name.name == n,
+        _ => false,
+      };
+      if should_skip {
+        Lam { param: p, body: b }
+      } else {
+        Lam {
+          param: p,
+          body: Box::new(subst_macro(*b, name, replacement)),
+        }
+      }
+    }
+    App { fun, arg } => App {
+      fun: Box::new(subst_macro(*fun, name, replacement)),
+      arg: Box::new(subst_macro(*arg, name, replacement)),
+    },
+    Pi {
+      arg_name,
+      arg,
+      ret,
+      mult,
+    } => Pi {
+      arg_name,
+      arg: Box::new(subst_macro(*arg, name, replacement)),
+      ret: Box::new(subst_macro(*ret, name, replacement)),
+      mult,
+    },
+    Forall {
+      name: n,
+      typ,
+      body: b,
+    } => {
+      if let NameRef::Id(id) = name
+        && &n == id
+      {
+        Forall {
+          name: n,
+          typ,
+          body: b,
+        }
+      } else {
+        Forall {
+          name: n,
+          typ: Box::new(subst_macro(*typ, name, replacement)),
+          body: Box::new(subst_macro(*b, name, replacement)),
+        }
+      }
+    }
+    Quote { term: t } => Quote {
+      term: Box::new(subst_macro(*t, name, replacement)),
+    },
+    Ctx { loc, term: t } => Ctx {
+      loc,
+      term: Box::new(subst_macro(*t, name, replacement)),
+    },
+    Ann { term: t, typ } => Ann {
+      term: Box::new(subst_macro(*t, name, replacement)),
+      typ: Box::new(subst_macro(*typ, name, replacement)),
+    },
+    Con(Constructor {
+      typ_name,
+      args,
+      name: n,
+      num_args,
+    }) => Con(Constructor {
+      name: n,
+      typ_name,
+      num_args,
+      args: args
+        .into_iter()
+        .map(|a| a.map(|t| subst_macro(t, name, replacement)))
+        .collect(),
+    }),
+    Lit {
+      value: Literal::Match { value, cases },
+    } => {
+      let value = subst_macro(*value, name, replacement);
+      let cases = cases
+        .into_iter()
+        .map(|c| case(c.name, c.args, subst_macro(*c.value, name, replacement)))
+        .collect();
+      match_term(value, cases)
+    }
+    Lit {
+      value: Literal::If { value, then, els },
+    } => Term::Lit {
+      value: Literal::If {
+        value: Box::new(subst_macro(*value, name, replacement)),
+        then: Box::new(subst_macro(*then, name, replacement)),
+        els: Box::new(subst_macro(*els, name, replacement)),
+      },
+    },
+    other => other,
+  }
 }
diff --git a/core/src/eval/macro_test.rs b/core/src/eval/macro_test.rs
index 1c4e3f3..ddaf3bf 100644
--- a/core/src/eval/macro_test.rs
+++ b/core/src/eval/macro_test.rs
@@ -317,7 +317,6 @@ fn expand_fails(input: &str) -> String {
 }
 
 #[test]
-#[ignore = "expand_macros is a stub"]
 fn test_macro_identity() {
   let r = expand_and_type_check(
     r#"
@@ -325,18 +324,20 @@ fn test_macro_identity() {
         def main : I64 := id! 42
         "#,
   );
+  if let Err(e) = &r {
+    eprintln!("identity error: {e}");
+  }
   assert!(r.is_ok(), "identity macro should succeed");
 }
 
 #[test]
-#[ignore = "expand_macros is a stub"]
 fn test_macro_add_one() {
   let r = expand_and_type_check(
-    r#"
-        defmacro add1 x := quote { unquote(x) + 1 }
-        def main : I64 := add1! 41
-        "#,
+    "defmacro add1 x := quote { unquote x + 1 }\ndef main : I64 := add1! 41\n",
   );
+  if let Err(e) = &r {
+    eprintln!("add1 error: {e}");
+  }
   assert!(r.is_ok(), "add1 macro should succeed");
 }
 
@@ -345,7 +346,7 @@ fn test_macro_add_one() {
 fn test_macro_multiple_args() {
   let r = expand_and_type_check(
     r#"
-        defmacro pair a b := quote { (unquote(a), unquote(b)) }
+        defmacro pair a b := quote { (unquote a, unquote b) }
         def main : (I64, I64) := pair! 1 2
         "#,
   );
@@ -357,7 +358,7 @@ fn test_macro_multiple_args() {
 fn test_macro_in_let_binding() {
   let r = expand_and_type_check(
     r#"
-        defmacro add1 x := quote { unquote(x) + 1 }
+        defmacro add1 x := quote { unquote x + 1 }
         def main : I64 :=
             let x := add1! 1
             x + 1
@@ -397,7 +398,7 @@ fn test_macro_not_found_fails() {
 fn test_macro_depth_limit_exceeded() {
   let msg = expand_fails(
     r#"
-        defmacro recurse x := quote { recurse! unquote(x) }
+        defmacro recurse x := quote { recurse! unquote x }
         def main : I64 := recurse! 0
         "#,
   );
@@ -409,8 +410,8 @@ fn test_macro_depth_limit_exceeded() {
 fn test_macro_nested_calls() {
   let r = expand_and_type_check(
     r#"
-        defmacro add1 x := quote { unquote(x) + 1 }
-        defmacro add2 x := quote { add1! (add1! unquote(x)) }
+        defmacro add1 x := quote { unquote x + 1 }
+        defmacro add2 x := quote { add1! (add1! unquote x) }
         def main : I64 := add2! 5
         "#,
   );
@@ -422,7 +423,7 @@ fn test_macro_nested_calls() {
 fn test_macro_as_function_arg() {
   let r = expand_and_type_check(
     r#"
-        defmacro wrap x := quote { unquote(x) }
+        defmacro wrap x := quote { unquote x }
         def id (x : I64) : I64 := x
         def main : I64 := id (wrap! 42)
         "#,
@@ -451,7 +452,7 @@ fn test_macro_expanded_in_type_position_fails() {
 fn test_hygiene_no_capture_of_user_var() {
   let r = expand_and_type_check(
     r#"
-        defmacro wrap x := quote { let y := 1 in unquote(x) + y }
+        defmacro wrap x := quote { let y := 1 in unquote x + y }
         def main : I64 :=
             let y := 100
             wrap! (y + 2)
@@ -465,7 +466,7 @@ fn test_hygiene_no_capture_of_user_var() {
 fn test_hygiene_user_var_captured_by_macro() {
   let r = expand_and_type_check(
     r#"
-        defmacro add_one x := quote { unquote(x) + 1 }
+        defmacro add_one x := quote { unquote x + 1 }
         def main : I64 :=
             let x := 10
             add_one! x
@@ -479,7 +480,7 @@ fn test_hygiene_user_var_captured_by_macro() {
 fn test_hygiene_multiple_expansions_independent() {
   let r = expand_and_type_check(
     r#"
-        defmacro wrap x := quote { let y := 1 in unquote(x) + y }
+        defmacro wrap x := quote { let y := 1 in unquote x + y }
         def main : I64 :=
             let y := 100
             wrap! (wrap! (y + 2))
@@ -496,7 +497,7 @@ fn test_macro_unless_example() {
   let r = expand_and_type_check(
     r#"
         defmacro unless cond body :=
-            quote { if Bool.not unquote(cond) then unquote(body) else () }
+            quote { if Bool.not unquote cond then unquote body else () }
         def main : IO Unit :=
             unless! (Bool.true) { println "should not print" }
         "#,
@@ -526,8 +527,8 @@ fn test_macro_define_getter() {
 fn test_macro_twice() {
   let r = expand_and_type_check(
     r#"
-        defmacro twice f x := quote { unquote(f) (unquote(f) unquote(x)) }
-        defmacro add1 x := quote { unquote(x) + 1 }
+        defmacro twice f x := quote { unquote f) (unquote f) unquote x) }
+        defmacro add1 x := quote { unquote x + 1 }
         def main : I64 := twice! add1! 5
         "#,
   );
diff --git a/core/src/eval/type.rs b/core/src/eval/type.rs
index 1b4fe20..e10fedb 100644
--- a/core/src/eval/type.rs
+++ b/core/src/eval/type.rs
@@ -1,7 +1,9 @@
 use std::fmt::Display;
 
 use crate::{
-  Map, Set, empty_set, set_of,
+  Map, Set, empty_set,
+  eval::macro_expand,
+  set_of,
   term::{
     Ann, ClassDefRef, Decl, Def, Identifier, Inductive, InductiveVariant, Instance, InstanceKey,
     Literal, ModulePath, Multiplicity, NameRef, Named, NumSuffix, SourceContext,
@@ -1768,6 +1770,8 @@ pub fn type_check_module_decls(
   loaded: &LoadedModules,
 ) -> Result<Vec<SourceContext<Decl>>, TypeError> {
   let decls = elaborate_decls(decls, loaded);
+  let decls = macro_expand::expand_macros(decls, loaded)
+    .map_err(|e| TypeError::Generic(format!("macro expansion failed: {e}")))?;
   let global = loaded.scope_of_decls(path, &decls);
 
   let (oks, errs) = type_check_decls(decls.clone(), &global.scope());
diff --git a/core/src/parser.rs b/core/src/parser.rs
index 7a61543..0bffa36 100644
--- a/core/src/parser.rs
+++ b/core/src/parser.rs
@@ -759,11 +759,11 @@ fn base_term<X: Clone>(input: Span<X>) -> Res<Term, X> {
     match_parser,
     type_expression,
     ann_parser,
+    application,
     variable,
     operator_var,
     literal,
     lambda,
-    application,
     parens,
   ))
   .parse(input)