diff --git a/spectec/doc/Language.md b/spectec/doc/Language.md
index 486a93330f..5d118eb533 100644
--- a/spectec/doc/Language.md
+++ b/spectec/doc/Language.md
@@ -228,12 +228,14 @@ arg ::=
   exp
   "syntax" typ
   "grammar" sym
+  "def" defid
 
 params ::= ("(" list(param ",") ")")?
 param ::=
   (varid ":") typ
   "syntax" synid
   "grammar" gramid ":" typ
+  "def" "$" defid params ":" typ
 
 def ::=
   "syntax" varid params hint*                               syntax declaration
diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml
index a33efefa66..0a0ae8a5b1 100644
--- a/spectec/src/backend-latex/render.ml
+++ b/spectec/src/backend-latex/render.ml
@@ -1268,6 +1268,7 @@ and render_arg env arg =
   | ExpA e -> render_exp env e
   | TypA t -> render_typ env t
   | GramA g -> render_sym env g
+  | DefA id -> render_defid env id
 
 and render_args env args =
   match List.map (render_arg env) args with
@@ -1279,6 +1280,7 @@ let render_param env p =
   | ExpP (id, t) -> if id.it = "_" then render_typ env t else render_varid env id
   | TypP id -> render_typid env id
   | GramP (id, _t) -> render_gramid env id
+  | DefP (id, _ps, _t) -> render_defid env id
 
 let _render_params env = function
   | [] -> ""
diff --git a/spectec/src/el/ast.ml b/spectec/src/el/ast.ml
index 0ad62232c2..900c2e3c63 100644
--- a/spectec/src/el/ast.ml
+++ b/spectec/src/el/ast.ml
@@ -175,12 +175,14 @@ and param' =
   | ExpP of id * typ                         (* varid `:` typ *)
   | TypP of id                               (* `syntax` varid *)
   | GramP of id * typ                        (* `grammar` gramid `:` typ *)
+  | DefP of id * param list * typ            (* `def` `$` defid params `:` typ *)
 
 and arg = arg' ref phrase
 and arg' =
   | ExpA of exp                              (* exp *)
   | TypA of typ                              (* `syntax` typ *)
   | GramA of sym                             (* `grammar` sym *)
+  | DefA of id                               (* `def` defid *)
 
 and def = def' phrase
 and def' =
diff --git a/spectec/src/el/convert.ml b/spectec/src/el/convert.ml
index 64dbaee182..45dbf4f89c 100644
--- a/spectec/src/el/convert.ml
+++ b/spectec/src/el/convert.ml
@@ -173,13 +173,15 @@ let exp_of_arg a =
   | ExpA e -> e
   | _ -> error a.at "malformed expression"
 
-let param_of_arg a =
+let rec param_of_arg a =
   (match !(a.it) with
   | ExpA e ->
     (match e.it with
     | TypE ({it = VarE (id, []); _}, t) -> ExpP (id, t)
     | VarE (id, args) ->
       ExpP (id, typ_of_exp (VarE (strip_var_suffix id, args) $ e.at))
+    | TypE ({it = CallE (id, as_); _}, t) ->
+      DefP (id, List.map param_of_arg as_, t)
     | _ -> ExpP ("_" $ e.at, typ_of_exp e)
     )
   | TypA {it = VarT (id, []); _} ->
@@ -188,7 +190,7 @@ let param_of_arg a =
     TypP id
   | GramA {it = AttrG ({it = VarE (id, []); _}, g); _} ->
     GramP (id, typ_of_exp (exp_of_sym g))
-  | _ -> error a.at "malformed grammar"
+  | _ -> error a.at "malformed parameter"
   ) $ a.at
 
 let arg_of_param p =
@@ -196,4 +198,5 @@ let arg_of_param p =
   | ExpP (id, _t) -> ExpA ((*TypE ( *)VarE (id, []) $ id.at(*, t) $ p.at*))
   | TypP id -> TypA (VarT (id, []) $ id.at)
   | GramP (id, _t) -> GramA (VarG (id, []) $ id.at)
+  | DefP (id, _params, _t) -> DefA id
   ) |> ref $ p.at
diff --git a/spectec/src/el/eq.ml b/spectec/src/el/eq.ml
index bfd7d89581..aeb6a6ebc7 100644
--- a/spectec/src/el/eq.ml
+++ b/spectec/src/el/eq.ml
@@ -165,6 +165,7 @@ and eq_arg a1 a2 =
   | ExpA e1, ExpA e2 -> eq_exp e1 e2
   | TypA t1, TypA t2 -> eq_typ t1 t2
   | GramA g1, GramA g2 -> eq_sym g1 g2
+  | DefA id1, DefA id2 -> eq_id id1 id2
   | _, _ -> false
 
 and eq_param p1 p2 =
@@ -172,4 +173,6 @@ and eq_param p1 p2 =
   | ExpP (id1, t1), ExpP (id2, t2) -> eq_id id1 id2 && eq_typ t1 t2
   | TypP id1, TypP id2 -> eq_id id1 id2
   | GramP (id1, t1), GramP (id2, t2) -> eq_id id1 id2 && eq_typ t1 t2
+  | DefP (id1, ps1, t1), DefP (id2, ps2, t2) ->
+    eq_id id1 id2 && eq_list eq_param ps1 ps2 && eq_typ t1 t2
   | _, _ -> false
diff --git a/spectec/src/el/free.ml b/spectec/src/el/free.ml
index cabe33d015..aea56bde91 100644
--- a/spectec/src/el/free.ml
+++ b/spectec/src/el/free.ml
@@ -73,6 +73,7 @@ let free_defid id = {empty with defid = Set.singleton id.it}
 let bound_typid id = if id.it = "_" then empty else free_typid id
 let bound_gramid id = if id.it = "_" then empty else free_gramid id
 let bound_varid id = if id.it = "_" then empty else free_varid id
+let bound_defid id = if id.it = "_" then empty else free_defid id
 
 
 (* Iterations *)
@@ -280,30 +281,35 @@ and free_arg a =
   | ExpA e -> free_exp e
   | TypA t -> free_typ t
   | GramA g -> free_sym g
+  | DefA id -> free_defid id
 
 and det_arg a =
   match !(a.it) with
   | ExpA e -> det_exp e
   | TypA t -> free_typ t  (* must be an id *)
   | GramA g -> free_sym g (* must be an id *)
+  | DefA id -> free_defid id
 
 and idx_arg a =
   match !(a.it) with
   | ExpA e -> idx_exp e
   | TypA _ -> empty
   | GramA _ -> empty
+  | DefA _ -> empty
 
 and free_param p =
   match p.it with
   | ExpP (_, t) -> free_typ t
   | TypP _ -> empty
   | GramP (_, t) -> free_typ t
+  | DefP (_, ps, t) -> free_params ps + free_typ t - bound_params ps
 
 and bound_param p =
   match p.it with
   | ExpP (id, _) -> bound_varid id
   | TypP id -> bound_typid id
   | GramP (id, _) -> bound_gramid id
+  | DefP (id, _, _) -> bound_defid id
 
 and free_args as_ = free_list free_arg as_
 and det_args as_ = free_list det_arg as_
diff --git a/spectec/src/el/iter.ml b/spectec/src/el/iter.ml
index e753ad39cb..a5f5b81243 100644
--- a/spectec/src/el/iter.ml
+++ b/spectec/src/el/iter.ml
@@ -202,12 +202,14 @@ and arg a =
   | ExpA e -> exp e
   | TypA t -> typ t
   | GramA g -> sym g
+  | DefA x -> defid x
 
 and param p =
   match p.it with
   | ExpP (x, t) -> varid x; typ t
   | TypP x -> typid x
   | GramP (x, t) -> gramid x; typ t
+  | DefP (x, ps, t) -> defid x; params ps; typ t
 
 and args as_ = list arg as_
 and params ps = list param ps
@@ -309,6 +311,7 @@ and clone_arg a =
   | ExpA e -> ExpA (clone_exp e)
   | TypA t -> TypA (clone_typ t)
   | GramA _ as a' -> a'
+  | DefA _ as a' -> a'
   ) |> ref $ a.at
 
 and clone_hint hint = {hint with hintexp = clone_exp hint.hintexp}
diff --git a/spectec/src/el/print.ml b/spectec/src/el/print.ml
index 013ad0dbd9..db16f0ef86 100644
--- a/spectec/src/el/print.ml
+++ b/spectec/src/el/print.ml
@@ -247,18 +247,20 @@ and string_of_arg a =
   | ExpA e -> string_of_exp e
   | TypA t -> "syntax " ^ string_of_typ t
   | GramA g -> "grammar " ^ string_of_sym g
+  | DefA id -> "def " ^ string_of_defid id
 
 and string_of_args = function
   | [] -> ""
   | args -> "(" ^ concat ", " (List.map string_of_arg args) ^ ")"
 
-let string_of_param p =
+let rec string_of_param p =
   match p.it with
   | ExpP (id, t) -> (if id.it = "_" then "" else string_of_varid id ^ " : ") ^ string_of_typ t
   | TypP id -> "syntax " ^ string_of_typid id
   | GramP (id, t) -> "grammar " ^ string_of_gramid id ^ " : " ^ string_of_typ t
+  | DefP (id, ps, t) -> "def " ^ string_of_defid id ^ string_of_params ps ^ " : " ^ string_of_typ t
 
-let string_of_params = function
+and string_of_params = function
   | [] -> ""
   | ps -> "(" ^ concat ", " (List.map string_of_param ps) ^ ")"
 
diff --git a/spectec/src/el/subst.ml b/spectec/src/el/subst.ml
index 29db1e62ab..37b05c3bd9 100644
--- a/spectec/src/el/subst.ml
+++ b/spectec/src/el/subst.ml
@@ -10,6 +10,7 @@ type subst =
   { varid : exp Map.t;
     typid : typ Map.t;
     gramid : sym Map.t;
+    defid : id Map.t;
   }
 
 type t = subst
@@ -18,20 +19,24 @@ let empty =
   { varid = Map.empty;
     typid = Map.empty;
     gramid = Map.empty;
+    defid = Map.empty;
   }
 
 let mem_varid s id = Map.mem id.it s.varid
 let mem_typid s id = Map.mem id.it s.typid
 let mem_gramid s id = Map.mem id.it s.gramid
+let mem_defid s id = Map.mem id.it s.defid
 
 let add_varid s id e = if id.it = "_" then s else {s with varid = Map.add id.it e s.varid}
 let add_typid s id t = if id.it = "_" then s else {s with typid = Map.add id.it t s.typid}
 let add_gramid s id g = if id.it = "_" then s else {s with gramid = Map.add id.it g s.gramid}
+let add_defid s id id' = if id.it = "_" then s else {s with defid = Map.add id.it id' s.defid}
 
 let union s1 s2 =
   { varid = Map.union (fun _ _e1 e2 -> Some e2) s1.varid s2.varid;
     typid = Map.union (fun _ _t1 t2 -> Some t2) s1.typid s2.typid;
     gramid = Map.union (fun _ _g1 g2 -> Some g2) s1.gramid s2.gramid;
+    defid = Map.union (fun _ _id1 id2 -> Some id2) s1.defid s2.defid;
   }
 
 
@@ -58,6 +63,11 @@ let subst_gramid s id =
   | Some {it = VarG (id', []); _} -> id'
   | Some _ -> raise (Invalid_argument "subst_gramid")
 
+let subst_defid s id =
+  match Map.find_opt id.it s.defid with
+  | None -> id
+  | Some id' -> id'
+
 
 (* Iterations *)
 
@@ -134,7 +144,7 @@ and subst_exp s e =
   | TupE es -> TupE (subst_list subst_exp s es)
   | InfixE (e1, atom, e2) -> InfixE (subst_exp s e1, atom, subst_exp s e2)
   | BrackE (l, e1, r) -> BrackE (l, subst_exp s e1, r)
-  | CallE (id, args) -> CallE (id, subst_list subst_arg s args)
+  | CallE (id, args) -> CallE (subst_defid s id, subst_list subst_arg s args)
   | IterE (e1, iter) -> IterE (subst_exp s e1, subst_iter s iter)
   | TypE (e1, t) -> TypE (subst_exp s e1, subst_typ s t)
   | ArithE e1 -> ArithE (subst_exp s e1)
@@ -210,6 +220,7 @@ and subst_arg s a =
   | ExpA e -> ExpA (subst_exp s e)
   | TypA t -> TypA (subst_typ s t)
   | GramA g -> GramA (subst_sym s g)
+  | DefA id -> DefA (subst_defid s id)
   ) $ a.at
 
 and subst_param s p =
@@ -217,4 +228,5 @@ and subst_param s p =
   | ExpP (id, t) -> ExpP (id, subst_typ s t)
   | TypP id -> TypP id
   | GramP (id, t) -> GramP (id, subst_typ s t)
+  | DefP (id, ps, t) -> DefP (id, List.map (subst_param s) ps, subst_typ s t)
   ) $ p.at
diff --git a/spectec/src/el/subst.mli b/spectec/src/el/subst.mli
index 07ca0839ad..ce82253a9f 100644
--- a/spectec/src/el/subst.mli
+++ b/spectec/src/el/subst.mli
@@ -6,6 +6,7 @@ type subst =
   { varid : exp Map.t;
     typid : typ Map.t;
     gramid : sym Map.t;
+    defid : id Map.t;
   }
 type t = subst
 
@@ -15,10 +16,12 @@ val union : subst -> subst -> subst (* right overrides *)
 val add_varid : subst -> id -> exp -> subst
 val add_typid : subst -> id -> typ -> subst
 val add_gramid : subst -> id -> sym -> subst
+val add_defid : subst -> id -> id -> subst
 
 val mem_varid : subst -> id -> bool
 val mem_typid : subst -> id -> bool
 val mem_gramid : subst -> id -> bool
+val mem_defid : subst -> id -> bool
 
 val subst_iter : subst -> iter -> iter
 val subst_typ : subst -> typ -> typ
diff --git a/spectec/src/frontend/dim.ml b/spectec/src/frontend/dim.ml
index d13249f7aa..457e24943c 100644
--- a/spectec/src/frontend/dim.ml
+++ b/spectec/src/frontend/dim.ml
@@ -233,8 +233,9 @@ and check_arg env ctx a =
   | ExpA e -> check_exp env ctx e
   | TypA t -> check_typ env ctx t
   | GramA g -> check_sym env ctx g
+  | DefA _id -> ()
 
-let check_param env ctx p =
+and check_param env ctx p =
   match p.it with
   | ExpP (id, t) ->
     check_varid env ctx id;
@@ -243,6 +244,9 @@ let check_param env ctx p =
   | GramP (id, t) ->
     check_gramid env ctx id;
     check_typ env ctx t
+  | DefP (_id, ps, t) ->
+    List.iter (check_param env ctx) ps;
+    check_typ env ctx t
 
 let check_def d : env =
   let env = ref Env.empty in
@@ -455,6 +459,7 @@ and annot_arg env a : Il.Ast.arg * occur =
       let e', occur1 = annot_exp env e in
       ExpA e', occur1
     | TypA t -> TypA t, Env.empty
+    | DefA id -> DefA id, Env.empty
   in {a with it}, occur
 
 and annot_prem env prem : Il.Ast.prem * occur =
diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml
index 3e847c987b..b239dd1f6d 100644
--- a/spectec/src/frontend/elab.ml
+++ b/spectec/src/frontend/elab.ml
@@ -1670,7 +1670,7 @@ and make_binds_iter_arg env free dims dims' : Il.bind list ref * (module Iter.Ar
           let fwd = Free.(inter (free_typ t) !left) in
           if fwd <> Free.empty then
             error id.at ("the type of `" ^ id.it ^ "` depends on " ^
-              ( Free.Set.(elements fwd.typid @ elements fwd.gramid @ elements fwd.varid) |>
+              ( Free.Set.(elements fwd.typid @ elements fwd.gramid @ elements fwd.varid @ elements fwd.defid) |>
                 List.map (fun id -> "`" ^ id ^ "`") |>
                 String.concat ", " ) ^
               ", which only occur(s) to its right; try to reorder parameters or premises");
@@ -1688,20 +1688,38 @@ and make_binds_iter_arg env free dims dims' : Il.bind list ref * (module Iter.Ar
           let fwd = Free.(inter free' !left) in
           if fwd <> Free.empty then
             error id.at ("the type of `" ^ id.it ^ "` depends on " ^
-              ( Free.Set.(elements fwd.typid @ elements fwd.gramid @ elements fwd.varid) |>
+              ( Free.Set.(elements fwd.typid @ elements fwd.gramid @ elements fwd.varid @ elements fwd.defid) |>
                 List.map (fun id -> "`" ^ id ^ "`") |>
                 String.concat ", " ) ^
               ", which only occur(s) to its right; try to reorder parameters or premises");
           left := Free.{!left with varid = Set.remove id.it !left.gramid};
         )
+
+      let visit_defid id =
+        if Free.Set.mem id.it !left.defid then (
+          let ps, t, _ = find "definition" env.defs id in
+          let env' = local_env env in
+          let ps' = elab_params env' ps in
+          let t' = elab_typ env' t in
+          let free' = Free.(union (free_params ps) (diff (free_typ t) (bound_params ps))) in
+          let fwd = Free.(inter free' !left) in
+          if fwd <> Free.empty then
+            error id.at ("the type of `" ^ (spaceid "definition" id).it ^ "` depends on " ^
+              ( Free.Set.(elements fwd.typid @ elements fwd.gramid @ elements fwd.varid @ elements fwd.defid) |>
+                List.map (fun id -> "`" ^ id ^ "`") |>
+                String.concat ", " ) ^
+              ", which only occur(s) to its right; try to reorder parameters or premises");
+          acc := !acc @ [Il.DefB (id, ps', t') $ id.at];
+          left := Free.{!left with defid = Set.remove id.it !left.defid};
+        )
     end
   in Arg.acc, (module Arg)
 
 and elab_arg in_lhs env a p s : Il.arg option * Subst.subst =
   (match !(a.it), p.it with  (* HACK: handle shorthands *)
   | ExpA e, TypP _ -> a.it := TypA (typ_of_exp e)
-  | ExpA e, GramP _ ->
-   a.it := GramA (sym_of_exp e)
+  | ExpA e, GramP _ -> a.it := GramA (sym_of_exp e)
+  | ExpA {it = CallE (id, []); _}, DefP _ -> a.it := DefA id
   | _, _ -> ()
   );
   match !(a.it), (Subst.subst_param s p).it with
@@ -1727,13 +1745,26 @@ and elab_arg in_lhs env a p s : Il.arg option * Subst.subst =
       error_typ2 env a.at "argument" t' t "";
     (* Grammar args are erased *)
     None, Subst.add_gramid s' id g
+  | DefA id, DefP (id', ps', t') when in_lhs = `Lhs ->
+    env.defs <- bind "definition" env.defs id (ps', t', []);
+    Some (Il.DefA id $ a.at), Subst.add_defid s id' id
+  | DefA id, DefP (id', ps', t') ->
+    let ps, t, _ = find "definition" env.defs id in
+    if not (Eval.equiv_functyp (to_eval_env env) (ps, t) (ps', t')) then
+      error a.at ("type mismatch in function argument, expected `" ^
+        (spaceid "definition" id').it ^ Print.(string_of_params ps' ^ " : " ^ string_of_typ t') ^
+        "` but got `" ^
+        (spaceid "definition" id).it ^ Print.(string_of_params ps ^ " : " ^ string_of_typ t ^ "`")
+      );
+    Some (Il.DefA id $ a.at), Subst.add_defid s id id'
   | _, _ ->
     error a.at "sort mismatch for argument"
 
 and elab_args in_lhs env as_ ps at : Il.arg list * Subst.subst =
-  Debug.(log_in_at "el.elab_args" at
-    (fun _ -> fmt "%s : %s" (list el_arg as_) (list el_param ps))
-  );
+  Debug.(log_at "el.elab_args" at
+    (fun _ -> fmt "(%s) : (%s)" (list el_arg as_) (list el_param ps))
+    (fun (r, _) -> fmt "(%s)" (list il_arg r))
+  ) @@ fun _ ->
   elab_args' in_lhs env as_ ps [] Subst.empty at
 
 and elab_args' in_lhs env as_ ps aos' s at : Il.arg list * Subst.subst =
@@ -1760,7 +1791,7 @@ and subst_implicit env s t t' : Subst.subst =
     | _ -> s
   in inst s t t'
 
-let elab_params env ps : Il.param list =
+and elab_params env ps : Il.param list =
   List.fold_left (fun ps' p ->
     match p.it with
     | ExpP (id, t) ->
@@ -1800,6 +1831,12 @@ let elab_params env ps : Il.param list =
       ) free.typid;
       let _t' = elab_typ env t in
       ps'  (* Grammar parameters are erased *)
+    | DefP (id, ps, t) ->
+      let env' = local_env env in
+      let ps'' = elab_params env' ps in
+      let t' = elab_typ env' t in
+      env.defs <- bind "definition" env.defs id (ps, t, []);
+      ps' @ [Il.DefP (id, ps'', t') $ p.at]
   ) [] ps
 
 
diff --git a/spectec/src/frontend/eval.ml b/spectec/src/frontend/eval.ml
index 26320ffd5e..ee691870b4 100644
--- a/spectec/src/frontend/eval.ml
+++ b/spectec/src/frontend/eval.ml
@@ -335,6 +335,7 @@ and reduce_arg env a : arg =
   | ExpA e -> ref (ExpA (reduce_exp env e)) $ a.at
   | TypA _t -> a  (* types are reduced on demand *)
   | GramA _g -> a
+  | DefA _id -> a
 
 and reduce_exp_call env id args at = function
   | [] ->
@@ -608,6 +609,9 @@ and match_arg env s a1 a2 : subst option =
   | ExpA e1, ExpA e2 -> match_exp env s e1 e2
   | TypA t1, TypA t2 -> match_typ env s t1 t2
   | GramA g1, GramA g2 -> match_sym env s g1 g2
+  | DefA id1, DefA id2 ->
+    if id2.it = "_" then Some s else
+    Some (Subst.add_defid s id2 id1)
   | _, _ -> assert false
 
 
@@ -676,9 +680,34 @@ and equiv_arg env a1 a2 =
   | ExpA e1, ExpA e2 -> equiv_exp env e1 e2
   | TypA t1, TypA t2 -> equiv_typ env t1 t2
   | GramA g1, GramA g2 -> Eq.eq_sym g1 g2
+  | DefA id1, DefA id2 -> id1.it = id2.it
   | _, _ -> false
 
 
+and equiv_functyp env (ps1, t1) (ps2, t2) =
+  List.length ps1 = List.length ps2 &&
+  match equiv_params env ps1 ps2 with
+  | None -> false
+  | Some s -> equiv_typ env t1 (Subst.subst_typ s t2)
+
+and equiv_params env ps1 ps2 =
+  List.fold_left2 (fun s_opt p1 p2 ->
+    let* s = s_opt in
+    match p1.it, (Subst.subst_param s p2).it with
+    | ExpP (id1, t1), ExpP (id2, t2) ->
+      if not (equiv_typ env t1 t2) then None else
+      Some (Subst.add_varid s id2 (VarE (id1, []) $ p1.at))
+    | TypP _, TypP _ -> Some s
+    | GramP (id1, t1), GramP (id2, t2) ->
+      if not (equiv_typ env t1 t2) then None else
+      Some (Subst.add_gramid s id2 (VarG (id1, []) $ p1.at))
+    | DefP (id1, ps1, t1), DefP (id2, ps2, t2) ->
+      if not (equiv_functyp env (ps1, t1) (ps2, t2)) then None else
+      Some (Subst.add_defid s id2 id1)
+    | _, _ -> None
+  ) (Some Subst.empty) ps1 ps2
+
+
 (* Subtyping *)
 
 and sub_typ env t1 t2 =
@@ -804,5 +833,6 @@ and disj_arg env a1 a2 =
   match !(a1.it), !(a2.it) with
   | ExpA e1, ExpA e2 -> disj_exp env e1 e2
   | TypA t1, TypA t2 -> disj_typ env t1 t2
-  | GramA g1, GramA g2 -> not (Eq.eq_sym g1 g2)
+  | GramA _, GramA _ -> false
+  | DefA _, DefA _ -> false
   | _, _ -> false
diff --git a/spectec/src/frontend/eval.mli b/spectec/src/frontend/eval.mli
index 0048150d27..a2eb11ece0 100644
--- a/spectec/src/frontend/eval.mli
+++ b/spectec/src/frontend/eval.mli
@@ -14,6 +14,7 @@ val reduce_exp : env -> exp -> exp
 val reduce_typ : env -> typ -> typ
 val reduce_arg : env -> arg -> arg
 
+val equiv_functyp : env -> param list * typ -> param list * typ -> bool
 val equiv_typ : env -> typ -> typ -> bool
 val sub_typ : env -> typ -> typ -> bool
 
diff --git a/spectec/src/frontend/parser.mly b/spectec/src/frontend/parser.mly
index 8b94ad0b25..f00c7cc992 100644
--- a/spectec/src/frontend/parser.mly
+++ b/spectec/src/frontend/parser.mly
@@ -509,6 +509,7 @@ exp_var_ :
   | REAL { VarE ("real" $ $sloc, []) }
   | TEXT { VarE ("text" $ $sloc, []) }
 
+exp_call : exp_call_ { $1 $ $sloc }
 exp_call_ :
   | DOLLAR defid { CallE ($2, []) }
   | DOLLAR defid_lparen comma_list(arg) RPAREN { CallE ($2, $3) }
@@ -760,6 +761,9 @@ arg_ :
   | SYNTAX typ { TypA $2 }
   | SYNTAX atomid_ { Id.make_var $2; TypA (VarT ($2 $ $loc($2), []) $ $loc($2)) }
   | GRAMMAR sym { GramA $2 }
+  | DEF DOLLAR defid { DefA $3 }
+  (* HACK for representing def parameters as args *)
+  | DEF exp_call COLON typ { ExpA (TypE ($2, $4) $ $sloc) }
 
 param : param_ { $1 $ $sloc }
 param_ :
@@ -770,6 +774,10 @@ param_ :
       in ExpP (id, $1) }
   | SYNTAX varid_bind { TypP $2 }
   | GRAMMAR gramid COLON typ { GramP ($2, $4) }
+  | DEF DOLLAR defid COLON typ
+    { DefP ($3, [], $5) }
+  | DEF DOLLAR defid_lparen enter_scope comma_list(param) RPAREN COLON typ exit_scope
+    { DefP ($3, $5, $8) }
 
 
 def : def_ { $1 $ $sloc }
diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml
index 87592dcbee..0d7298956c 100644
--- a/spectec/src/il/ast.ml
+++ b/spectec/src/il/ast.ml
@@ -122,16 +122,19 @@ and arg = arg' phrase
 and arg' =
   | ExpA of exp                                       (* exp *)
   | TypA of typ                                       (* `syntax` typ *)
+  | DefA of id                                        (* `def` defid *)
 
 and bind = bind' phrase
 and bind' =
   | ExpB of id * typ * iter list
   | TypB of id
+  | DefB of id * param list * typ
 
 and param = param' phrase
 and param' =
   | ExpP of id * typ                                  (* varid `:` typ *)
   | TypP of id                                        (* `syntax` varid *)
+  | DefP of id * param list * typ                     (* `def` defid params `:` typ *)
 
 and def = def' phrase
 and def' =
diff --git a/spectec/src/il/eq.ml b/spectec/src/il/eq.ml
index a847009399..9b06f15699 100644
--- a/spectec/src/il/eq.ml
+++ b/spectec/src/il/eq.ml
@@ -131,4 +131,5 @@ and eq_arg a1 a2 =
   match a1.it, a2.it with
   | ExpA e1, ExpA e2 -> eq_exp e1 e2
   | TypA t1, TypA t2 -> eq_typ t1 t2
+  | DefA id1, DefA id2 -> eq_id id1 id2
   | _, _ -> false
diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml
index 5cbe02abf3..4ff84d0c98 100644
--- a/spectec/src/il/eval.ml
+++ b/spectec/src/il/eval.ml
@@ -393,6 +393,7 @@ and reduce_arg env a : arg =
   match a.it with
   | ExpA e -> ExpA (reduce_exp env e) $ a.at
   | TypA _t -> a  (* types are reduced on demand *)
+  | DefA _id -> a
 
 and reduce_exp_call env id args at = function
   | [] ->
@@ -652,6 +653,7 @@ and match_arg env s a1 a2 : subst option =
   match a1.it, a2.it with
   | ExpA e1, ExpA e2 -> match_exp env s e1 e2
   | TypA t1, TypA t2 -> match_typ env s t1 t2
+  | DefA id1, DefA id2 -> Some (Subst.add_defid s id1 id2)
   | _, _ -> assert false
 
 
@@ -722,9 +724,31 @@ and equiv_arg env a1 a2 =
   match a1.it, a2.it with
   | ExpA e1, ExpA e2 -> equiv_exp env e1 e2
   | TypA t1, TypA t2 -> equiv_typ env t1 t2
+  | DefA id1, DefA id2 -> id1.it = id2.it
   | _, _ -> false
 
 
+and equiv_functyp env (ps1, t1) (ps2, t2) =
+  List.length ps1 = List.length ps2 &&
+  match equiv_params env ps1 ps2 with
+  | None -> false
+  | Some s -> equiv_typ env t1 (Subst.subst_typ s t2)
+
+and equiv_params env ps1 ps2 =
+  List.fold_left2 (fun s_opt p1 p2 ->
+    let* s = s_opt in
+    match p1.it, (Subst.subst_param s p2).it with
+    | ExpP (id1, t1), ExpP (id2, t2) ->
+      if not (equiv_typ env t1 t2) then None else
+      Some (Subst.add_varid s id2 (VarE id1 $$ p1.at % t1))
+    | TypP _, TypP _ -> Some s
+    | DefP (id1, ps1, t1), DefP (id2, ps2, t2) ->
+      if not (equiv_functyp env (ps1, t1) (ps2, t2)) then None else
+      Some (Subst.add_defid s id2 id1)
+    | _, _ -> assert false
+  ) (Some Subst.empty) ps1 ps2
+
+
 (* Subtyping *)
 
 and sub_typ env t1 t2 =
diff --git a/spectec/src/il/eval.mli b/spectec/src/il/eval.mli
index e118caa1e7..56e35894d6 100644
--- a/spectec/src/il/eval.mli
+++ b/spectec/src/il/eval.mli
@@ -14,6 +14,7 @@ val reduce_typ : env -> typ -> typ
 val reduce_typdef : env -> typ -> deftyp
 val reduce_arg : env -> arg -> arg
 
+val equiv_functyp : env -> param list * typ -> param list * typ -> bool
 val equiv_typ : env -> typ -> typ -> bool
 val sub_typ : env -> typ -> typ -> bool
 
diff --git a/spectec/src/il/free.ml b/spectec/src/il/free.ml
index 6164be507f..6a186ef478 100644
--- a/spectec/src/il/free.ml
+++ b/spectec/src/il/free.ml
@@ -59,6 +59,7 @@ let free_defid id = {empty with defid = Set.singleton id.it}
 
 let bound_typid id = if id.it = "_" then empty else free_typid id
 let bound_varid id = if id.it = "_" then empty else free_varid id
+let bound_defid id = if id.it = "_" then empty else free_defid id
 
 
 (* Iterations *)
@@ -151,26 +152,31 @@ and free_arg a =
   match a.it with
   | ExpA e -> free_exp e
   | TypA t -> free_typ t
+  | DefA id -> free_defid id
 
 and free_bind b =
   match b.it with
   | ExpB (_, t, _) -> free_typ t
   | TypB _ -> empty
+  | DefB (_, ps, t) -> free_params ps + free_typ t - bound_params ps
 
 and free_param p =
   match p.it with
   | ExpP (_, t) -> free_typ t
   | TypP _ -> empty
+  | DefP (_, ps, t) -> free_params ps + free_typ t - bound_params ps
 
 and bound_bind b =
   match b.it with
   | ExpB (id, _, _) -> bound_varid id
   | TypB id -> bound_typid id
+  | DefB (id, _, _) -> bound_defid id
 
 and bound_param p =
   match p.it with
   | ExpP (id, _) -> bound_varid id
   | TypP id -> bound_typid id
+  | DefP (id, _, _) -> bound_defid id
 
 and free_args as_ = free_list free_arg as_
 and free_binds bs = free_list_dep free_bind bound_bind bs
diff --git a/spectec/src/il/iter.ml b/spectec/src/il/iter.ml
index 0d84cbdb83..cc88b7f4cf 100644
--- a/spectec/src/il/iter.ml
+++ b/spectec/src/il/iter.ml
@@ -167,16 +167,19 @@ and arg a =
   match a.it with
   | ExpA e -> exp e
   | TypA t -> typ t
+  | DefA x -> defid x
 
 and bind b =
   match b.it with
   | ExpB (id, t, its) -> varid id; typ t; list iter its
   | TypB id -> typid id
+  | DefB (id, ps, t) -> defid id; params ps; typ t
 
 and param p =
   match p.it with
   | ExpP (x, t) -> varid x; typ t
   | TypP x -> typid x
+  | DefP (x, ps, t) -> defid x; params ps; typ t
 
 and args as_ = list arg as_
 and binds bs = list bind bs
diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml
index 82da11575c..213c51ec70 100644
--- a/spectec/src/il/print.ml
+++ b/spectec/src/il/print.ml
@@ -200,6 +200,7 @@ and string_of_arg a =
   match a.it with
   | ExpA e -> string_of_exp e
   | TypA t -> "syntax " ^ string_of_typ t
+  | DefA id -> "def $" ^ id.it
 
 and string_of_args = function
   | [] -> ""
@@ -211,17 +212,19 @@ and string_of_bind bind =
     let dim = String.concat "" (List.map string_of_iter iters) in
     id.it ^ dim ^ " : " ^ string_of_typ t ^ dim
   | TypB id -> "syntax " ^ id.it
+  | DefB (id, ps, t) -> "def $" ^ id.it ^ string_of_params ps ^ " : " ^ string_of_typ t
 
 and string_of_binds = function
   | [] -> ""
   | bs -> "{" ^ concat ", " (List.map string_of_bind bs) ^ "}"
 
-let string_of_param p =
+and string_of_param p =
   match p.it with
   | ExpP (id, t) -> (if id.it = "_" then "" else id.it ^ " : ") ^ string_of_typ t
   | TypP id -> "syntax " ^ id.it
+  | DefP (id, ps, t) -> "def $" ^ id.it ^ string_of_params ps ^ " : " ^ string_of_typ t
 
-let string_of_params = function
+and string_of_params = function
   | [] -> ""
   | ps -> "(" ^ concat ", " (List.map string_of_param ps) ^ ")"
 
diff --git a/spectec/src/il/subst.ml b/spectec/src/il/subst.ml
index b814b7f5e7..a130cbe23b 100644
--- a/spectec/src/il/subst.ml
+++ b/spectec/src/il/subst.ml
@@ -6,20 +6,23 @@ open Ast
 
 module Map = Map.Make(String)
 
-type subst = {varid : exp Map.t; typid : typ Map.t}
+type subst = {varid : exp Map.t; typid : typ Map.t; defid : id Map.t}
 type t = subst
 
-let empty = {varid = Map.empty; typid = Map.empty}
+let empty = {varid = Map.empty; typid = Map.empty; defid = Map.empty}
 
 let mem_varid s id = Map.mem id.it s.varid
 let mem_typid s id = Map.mem id.it s.typid
+let mem_defid s id = Map.mem id.it s.defid
 
 let add_varid s id e = if id.it = "_" then s else {s with varid = Map.add id.it e s.varid}
 let add_typid s id t = if id.it = "_" then s else {s with typid = Map.add id.it t s.typid}
+let add_defid s id x = if id.it = "_" then s else {s with defid = Map.add id.it x s.defid}
 
 let union s1 s2 =
   { varid = Map.union (fun _ _e1 e2 -> Some e2) s1.varid s2.varid;
     typid = Map.union (fun _ _t1 t2 -> Some t2) s1.typid s2.typid;
+    defid = Map.union (fun _ _x1 x2 -> Some x2) s1.defid s2.defid;
   }
 
 let remove_varid' s id' = {s with varid = Map.remove id' s.varid}
@@ -48,6 +51,11 @@ let subst_varid s id =
   | Some {it = VarE id'; _} -> id'
   | Some _ -> raise (Invalid_argument "subst_varid")
 
+let subst_defid s id =
+  match Map.find_opt id.it s.defid with
+  | None -> id
+  | Some id' -> id'
+
 
 (* Iterations *)
 
@@ -112,7 +120,7 @@ and subst_exp s e =
   | CompE (e1, e2) -> CompE (subst_exp s e1, subst_exp s e2)
   | LenE e1 -> LenE (subst_exp s e1)
   | TupE es -> TupE (subst_list subst_exp s es)
-  | CallE (id, as_) -> CallE (id, subst_args s as_)
+  | CallE (id, as_) -> CallE (subst_defid s id, subst_args s as_)
   | IterE (e1, iterexp) -> IterE (subst_exp s e1, subst_iterexp s iterexp)
   | ProjE (e1, i) -> ProjE (subst_exp s e1, i)
   | UncaseE (e1, op) -> UncaseE (subst_exp s e1, op)
@@ -197,18 +205,25 @@ and subst_arg s a =
   (match a.it with
   | ExpA e -> ExpA (subst_exp s e)
   | TypA t -> TypA (subst_typ s t)
+  | DefA id -> DefA (subst_defid s id)
   ) $ a.at
 
 and subst_bind s b =
   (match b.it with
   | ExpB (id, t, iters) -> ExpB (id, subst_typ s t, iters)
   | TypB id -> TypB id
+  | DefB (id, ps, t) ->
+    let ps', s' = subst_params s ps in
+    DefB (id, ps', subst_typ s' t)
   ) $ b.at
 
 and subst_param s p =
   (match p.it with
   | ExpP (id, t) -> ExpP (id, subst_typ s t)
   | TypP id -> TypP id
+  | DefP (id, ps, t) ->
+    let ps', s' = subst_params s ps in
+    DefP (id, ps', subst_typ s' t)
   ) $ p.at
 
 and subst_args s as_ = subst_list subst_arg s as_
diff --git a/spectec/src/il/subst.mli b/spectec/src/il/subst.mli
index 36c6e25893..52286ea203 100644
--- a/spectec/src/il/subst.mli
+++ b/spectec/src/il/subst.mli
@@ -2,7 +2,7 @@ open Ast
 
 module Map : Map.S with type key = string with type 'a t = 'a Map.Make(String).t
 
-type subst = {varid : exp Map.t; typid : typ Map.t}
+type subst = {varid : exp Map.t; typid : typ Map.t; defid : id Map.t}
 type t = subst
 
 val empty : subst
@@ -10,9 +10,11 @@ val union : subst -> subst -> subst (* right overrides *)
 
 val add_varid : subst -> id -> exp -> subst
 val add_typid : subst -> id -> typ -> subst
+val add_defid : subst -> id -> id -> subst
 
 val mem_varid : subst -> id -> bool
 val mem_typid : subst -> id -> bool
+val mem_defid : subst -> id -> bool
 
 val subst_iter : subst -> iter -> iter
 val subst_typ : subst -> typ -> typ
diff --git a/spectec/src/il/valid.ml b/spectec/src/il/valid.ml
index a246ddecd6..04f6e51620 100644
--- a/spectec/src/il/valid.ml
+++ b/spectec/src/il/valid.ml
@@ -32,7 +32,7 @@ let new_env () =
     defs = Env.empty;
   }
 
-let local_env env = {env with vars = env.vars; typs = env.typs}
+let local_env env = {env with vars = env.vars; typs = env.typs; defs = env.defs}
 
 (* TODO(3, rossberg): avoid repeated copying of environment *)
 let to_eval_env env =
@@ -554,10 +554,17 @@ and valid_arg env a p s =
   Debug.(log_at "il.valid_arg" a.at
     (fun _ -> fmt "%s : %s" (il_arg a) (il_param p)) (Fun.const "ok")
   ) @@ fun _ ->
-  match a.it, p.it with
-  | ExpA e, ExpP (id, t) -> valid_exp env e (Subst.subst_typ s t); Subst.add_varid s id e
+  match a.it, (Subst.subst_param s p).it with
+  | ExpA e, ExpP (id, t) -> valid_exp env e t; Subst.add_varid s id e
   | TypA t, TypP id -> valid_typ env t; Subst.add_typid s id t
-  | _, _ -> error a.at "sort mismatch for argument"
+  | DefA id, DefP (id', ps', t') ->
+    let ps, t, _ = find "function" env.defs id in
+    if not (Eval.equiv_functyp (to_eval_env env) (ps, t) (ps', t')) then
+      error a.at "type mismatch in function argument";
+    Subst.add_defid s id id'
+  | _, _ ->
+    error a.at ("sort mismatch for argument, expected `" ^
+      Print.string_of_param p ^ "`, got `" ^ Print.string_of_arg a ^ "`")
 
 and valid_args env as_ ps s at : Subst.t =
   Debug.(log_if "il.valid_args" (as_ <> [] || ps <> [])
@@ -578,14 +585,24 @@ and valid_bind env b =
     env.vars <- bind "variable" env.vars id (t, dim)
   | TypB id ->
     env.typs <- bind "syntax" env.typs id ([], [])
+  | DefB (id, ps, t) ->
+    let env' = local_env env in
+    List.iter (valid_param env') ps;
+    valid_typ env' t;
+    env.defs <- bind "definition" env.defs id (ps, t, [])
 
-let valid_param env p =
+and valid_param env p =
   match p.it with
   | ExpP (id, t) ->
     valid_typ env t;
     env.vars <- bind "variable" env.vars id (t, [])
   | TypP id ->
     env.typs <- bind "syntax" env.typs id ([], [])
+  | DefP (id, ps, t) ->
+    let env' = local_env env in
+    List.iter (valid_param env') ps;
+    valid_typ env' t;
+    env.defs <- bind "definition" env.defs id (ps, t, [])
 
 let valid_inst env ps inst =
   Debug.(log_in "il.valid_inst" line);
diff --git a/spectec/src/il2al/free.ml b/spectec/src/il2al/free.ml
index 7f664024de..157026e9e5 100644
--- a/spectec/src/il2al/free.ml
+++ b/spectec/src/il2al/free.ml
@@ -11,6 +11,7 @@ include Il.Free
 let empty =
   {typid = Set.empty; relid = Set.empty; varid = Set.empty; defid = Set.empty}
 let free_varid id = {empty with varid = Set.singleton id.it}
+let free_defid id = {empty with defid = Set.singleton id.it}
 
 let rec free_exp ignore_listN e =
   let f = free_exp ignore_listN in
@@ -45,6 +46,7 @@ and free_arg ignore_listN arg =
   match arg.it with
   | ExpA e -> f e
   | TypA _ -> empty
+  | DefA id -> free_defid id
 
 and free_path ignore_listN p =
   let f = free_exp ignore_listN in
diff --git a/spectec/src/il2al/il2il.ml b/spectec/src/il2al/il2il.ml
index 5c202da14b..996c085cb8 100644
--- a/spectec/src/il2al/il2il.ml
+++ b/spectec/src/il2al/il2il.ml
@@ -55,7 +55,8 @@ let rec transform_expr f e =
 and transform_arg f a =
   { a with it = match a.it with
     | ExpA e -> ExpA (transform_expr f e)
-    | TypA t -> TypA t }
+    | TypA t -> TypA t
+    | DefA id -> DefA id }
 
 (* Change right_assoc cat into left_assoc cat *)
 let to_left_assoc_cat =
@@ -181,6 +182,7 @@ and overlap_arg a1 a2 = if eq_arg a1 a2 then a1 else
   (match a1.it, a2.it with
     | ExpA e1, ExpA e2 -> ExpA (overlap e1 e2)
     | TypA _, TypA _ -> a1.it
+    | DefA _, DefA _ -> a1.it
     | _, _ -> assert false
   ) $ a1.at
 
@@ -236,6 +238,7 @@ let rec collect_unified template e = if eq_exp template e then [], [] else
 and collect_unified_arg template a = if eq_arg template a then [], [] else match template.it, a.it with
   | ExpA template', ExpA e -> collect_unified template' e
   | TypA _, TypA _ -> [], []
+  | DefA _, DefA _ -> [], []
   | _ -> Util.Error.error a.at "prose transformation" "cannot unify the argument"
 
 and collect_unified_args as1 as2 =
diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml
index 80f7a7d2e7..bdb8ba82cb 100644
--- a/spectec/src/il2al/translate.ml
+++ b/spectec/src/il2al/translate.ml
@@ -276,7 +276,8 @@ and translate_argexp exp =
 and translate_args args = List.concat_map ( fun arg ->
   match arg.it with
   | Il.ExpA el -> [ translate_exp el ]
-  | Il.TypA _ -> [] ) args
+  | Il.TypA _ -> []
+  | Il.DefA _ -> [] (* TODO: handle functions *) ) args
 
 (* `Il.path` -> `path list` *)
 and translate_path path =
diff --git a/spectec/src/middlend/sideconditions.ml b/spectec/src/middlend/sideconditions.ml
index 61ad0ce5db..354f501d89 100644
--- a/spectec/src/middlend/sideconditions.ml
+++ b/spectec/src/middlend/sideconditions.ml
@@ -122,6 +122,7 @@ and t_path env path = match path.it with
 and t_arg env arg = match arg.it with
   | ExpA exp -> t_exp env exp
   | TypA _ -> []
+  | DefA _ -> []
 
 
 let rec t_prem env prem = match prem.it with
@@ -161,7 +162,7 @@ let t_rule' = function
     let env = List.fold_left (fun env bind ->
       match bind.it with
       | ExpB (v, t, i) -> Env.add v.it (t, i) env
-      | TypB _ -> error bind.at "unexpected type argument in rule") Env.empty binds
+      | TypB _ | DefB _ -> error bind.at "unexpected type argument in rule") Env.empty binds
     in
     let extra_prems = t_prems env prems @ t_exp env exp in
     let prems' = reduce_prems (extra_prems @ prems) in
diff --git a/spectec/src/middlend/sub.ml b/spectec/src/middlend/sub.ml
index bdbdce19c4..b05cd8c85c 100644
--- a/spectec/src/middlend/sub.ml
+++ b/spectec/src/middlend/sub.ml
@@ -62,6 +62,7 @@ let arg_of_param param =
   match param.it with
   | ExpP (id, t) -> ExpA (VarE id $$ param.at % t) $ param.at
   | TypP id -> TypA (VarT (id, []) $ param.at) $ param.at
+  | DefP (id, _ps, _t) -> DefA id $ param.at
 
 let register_variant (env : env) (id : id) params (cases : typcase list) =
   if M.mem id.it env.typ then
@@ -74,6 +75,7 @@ let subst_of_args =
     match arg.it, param.it with
     | ExpA e, ExpP (id, _) -> Il.Subst.add_varid s id e
     | TypA t, TypP id -> Il.Subst.add_typid s id t
+    | DefA x, DefP (id, _, _) -> Il.Subst.add_defid s id x
     | _, _ -> assert false
   ) Il.Subst.empty
 
@@ -179,18 +181,21 @@ and t_path env x = { x with it = t_path' env x.it; note = t_typ env x.note }
 and t_arg' env = function
   | ExpA exp -> ExpA (t_exp env exp)
   | TypA t -> TypA t
+  | DefA id -> DefA id
 
 and t_arg env x = { x with it = t_arg' env x.it }
 
 and t_bind' env = function
   | ExpB (id, t, dim) -> ExpB (id, t_typ env t, dim)
   | TypB id -> TypB id
+  | DefB (id, ps, t) -> DefB (id, t_params env ps, t_typ env t)
 
 and t_bind env x = { x with it = t_bind' env x.it }
 
 and t_param' env = function
   | ExpP (id, t) -> ExpP (id, t_typ env t)
   | TypP id -> TypP id
+  | DefP (id, ps, t) -> DefP (id, t_params env ps, t_typ env t)
 
 and t_param env x = { x with it = t_param' env x.it }
 
@@ -277,6 +282,10 @@ let rec rename_params s = function
     let id' = (id.it ^ "_2") $ id.at in
     (TypP id' $ at) ::
       rename_params (Il.Subst.add_typid s id (VarT (id', []) $ id.at)) params
+  | { it = DefP (id, ps, t); at; _ } :: params ->
+    let id' = (id.it ^ "_2") $ id.at in
+    (DefP (id', ps, t) $ at) ::
+      rename_params (Il.Subst.add_typid s id (VarT (id', []) $ id.at)) params
 
 let insert_injections env (def : def) : def list =
   add_type_info env def;
@@ -297,7 +306,7 @@ let insert_injections env (def : def) : def list =
         let xes = List.map (fun bind ->
           match bind.it with
           | ExpB (x, arg_typ_i, _) -> VarE x $$ no_region % arg_typ_i
-          | TypB _ -> assert false) binds
+          | TypB _ | DefB _ -> assert false) binds
         in
         let xe = TupE xes $$ no_region % arg_typ in
         DefD (binds,
diff --git a/spectec/src/middlend/totalize.ml b/spectec/src/middlend/totalize.ml
index 5057d1e397..c11f6bf20e 100644
--- a/spectec/src/middlend/totalize.ml
+++ b/spectec/src/middlend/totalize.ml
@@ -120,18 +120,21 @@ and t_path env x = { x with it = t_path' env x.it; note = t_typ env x.note }
 and t_arg' env = function
   | ExpA exp -> ExpA (t_exp env exp)
   | TypA t -> TypA (t_typ env t)
+  | DefA id -> DefA id
 
 and t_arg env x = { x with it = t_arg' env x.it }
 
 and t_bind' env = function
   | ExpB (id, t, dim) -> ExpB (id, t_typ env t, List.map (t_iter env) dim)
   | TypB id -> TypB id
+  | DefB (id, ps, t) -> DefB (id, t_params env ps, t_typ env t)
 
 and t_bind env x = { x with it = t_bind' env x.it }
 
 and t_param' env = function
   | ExpP (id, t) -> ExpP (id, t_typ env t)
   | TypP id -> TypP id
+  | DefP (id, ps, t) -> DefP (id, t_params env ps, t_typ env t)
 
 and t_param env x = { x with it = t_param' env x.it }
 
@@ -188,6 +191,7 @@ let rec t_def' env = function
           let x = ("x" ^ string_of_int i) $ no_region in
           [ExpB (x, typI, []) $ x.at], ExpA (VarE x $$ no_region % typI) $ no_region
         | TypP id -> [], TypA (VarT (id, []) $ no_region) $ no_region
+        | DefP (id, _, _) -> [], DefA id $ no_region
         ) params' |> List.split in
       let catch_all = DefD (List.concat binds, args,
         OptE None $$ no_region % typ'', []) $ no_region in
diff --git a/spectec/src/middlend/unthe.ml b/spectec/src/middlend/unthe.ml
index eb312ab83f..6aa615c122 100644
--- a/spectec/src/middlend/unthe.ml
+++ b/spectec/src/middlend/unthe.ml
@@ -43,7 +43,7 @@ let under_iterexp (iter, vs) eqns : iterexp * eqns =
    let new_vs = List.map (fun (bind, _) ->
      match bind.it with
      | ExpB (v, t, _) -> (v, t)
-     | TypB _ -> error bind.at "unexpected type binding") eqns in
+     | TypB _ | DefB _ -> error bind.at "unexpected type binding") eqns in
    let iterexp' = (iter, vs @ new_vs) in
    let eqns' = List.map (fun (bind, pr) ->
      match bind.it with
@@ -51,7 +51,7 @@ let under_iterexp (iter, vs) eqns : iterexp * eqns =
        let pr_iterexp = update_iterexp_vars (Il.Free.free_prem pr) (iter, vs @ new_vs) in
        let pr' = IterPr (pr, pr_iterexp) $ no_region in
        (ExpB (v, t, is@[iter]) $ bind.at, pr')
-     | TypB _ -> error bind.at "unexpected type binding") eqns in
+     | TypB _ | DefB _ -> error bind.at "unexpected type binding") eqns in
    iterexp', eqns'
 
 
@@ -176,6 +176,7 @@ and t_arg n = phrase t_arg' n
 and t_arg' n arg = match arg with
   | ExpA exp -> unary t_exp n exp (fun exp' -> ExpA exp')
   | TypA _ -> [], arg
+  | DefA _ -> [], arg
 
 let rec t_prem n : prem -> eqns * prem = phrase t_prem' n
 
diff --git a/spectec/src/middlend/wild.ml b/spectec/src/middlend/wild.ml
index 8a5ba03266..870664de79 100644
--- a/spectec/src/middlend/wild.ml
+++ b/spectec/src/middlend/wild.ml
@@ -75,12 +75,12 @@ let under_iterexp (iter, vs) binds : iterexp * bind list =
    let new_vs = List.map (fun bind ->
      match bind.it with
      | ExpB (v, t, _) -> (v, t)
-     | TypB _ -> error bind.at "unexpected type binding") binds in
+     | TypB _ | DefB _ -> error bind.at "unexpected type binding") binds in
    let iterexp' = (iter, vs @ new_vs) in
    let binds' = List.map (fun bind ->
      match bind.it with
      | ExpB (v, t, is) -> ExpB (v, t, is@[iter]) $ bind.at
-     | TypB _ -> assert false) binds in
+     | TypB _ | DefB _ -> assert false) binds in
    iterexp', binds'
 
 (* Generic traversal helpers *)
@@ -197,6 +197,7 @@ and t_arg env = phrase t_arg' env
 and t_arg' env arg = match arg with
   | ExpA exp -> unary t_exp env exp (fun exp' -> ExpA exp')
   | TypA _ -> [], arg
+  | DefA _ -> [], arg
 
 let rec t_prem env : prem -> bind list * prem = phrase t_prem' env
 
diff --git a/spectec/test-frontend/test.watsup b/spectec/test-frontend/test.watsup
index 606f4c5c8b..bed43f2320 100644
--- a/spectec/test-frontend/test.watsup
+++ b/spectec/test-frontend/test.watsup
@@ -95,3 +95,18 @@ def $testemptyn6(notation6) : nat
 def $testemptyn6(eps 0) = 0
 ;;def $testemptyn6(0) = 0
 def $testemptyn6("" 0) = 0
+
+
+
+;;
+;; Parameterisation
+;;
+
+def $f(syntax X, X) : X
+def $f(syntax X, x) = x
+
+def $g(def $h(syntax X, X) : X, syntax Y, Y) : Y
+def $g(def $h, syntax Y, y) = $h(Y, y)
+
+def $x : nat
+def $x = $($g(def $f, syntax nat, 1) + $g($f, nat, 2))