diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean
index 92b9608e9..901dbeb90 100644
--- a/Strata/DDM/AST.lean
+++ b/Strata/DDM/AST.lean
@@ -141,6 +141,44 @@ termination_by d
 
 end TypeExprF
 
+/-- Separator format for sequence formatting -/
+inductive SepFormat where
+| none           -- No separator (original Seq)
+| comma          -- Comma separator (CommaSepBy)
+| space          -- Space separator (SpaceSepBy)
+| spacePrefix    -- Space before each element (SpacePrefixSepBy)
+deriving Inhabited, Repr, BEq
+
+namespace SepFormat
+
+def toString : SepFormat → String
+  | .none => "seq"
+  | .comma => "commaSepBy"
+  | .space => "spaceSepBy"
+  | .spacePrefix => "spacePrefixSepBy"
+
+def toIonName : SepFormat → String
+  | .none => "seq"
+  | .comma => "commaSepList"
+  | .space => "spaceSepList"
+  | .spacePrefix => "spacePrefixedList"
+
+def fromIonName? : String → Option SepFormat
+  | "seq" => some .none
+  | "commaSepList" => some .comma
+  | "spaceSepList" => some .space
+  | "spacePrefixedList" => some .spacePrefix
+  | _ => none
+
+theorem fromIonName_toIonName_roundtrip (sep : SepFormat) :
+  fromIonName? (toIonName sep) = some sep := by
+  cases sep <;> rfl
+
+instance : ToString SepFormat where
+  toString := SepFormat.toString
+
+end SepFormat
+
 mutual
 
 inductive ExprF (α : Type) : Type where
@@ -167,8 +205,7 @@ inductive ArgF (α : Type) : Type where
 | strlit (ann : α) (i : String)
 | bytes (ann : α) (a : ByteArray)
 | option (ann : α) (l : Option (ArgF α))
-| seq (ann : α) (l : Array (ArgF α))
-| commaSepList (ann : α) (l : Array (ArgF α))
+| seq (ann : α) (sep : SepFormat) (l : Array (ArgF α))
 deriving Inhabited, Repr
 
 end
@@ -192,8 +229,7 @@ def ArgF.ann {α : Type} : ArgF α → α
 | .bytes ann _ => ann
 | .strlit ann _ => ann
 | .option ann _ => ann
-| .seq ann _ => ann
-| .commaSepList ann _ => ann
+| .seq ann _ _ => ann
 
 end
 
@@ -289,10 +325,8 @@ private def ArgF.beq {α} [BEq α] (a1 a2 : ArgF α) : Bool :=
     | .none, .none => true
     | .some v1, .some v2 => ArgF.beq v1 v2
     | _, _ => false
-  | .seq a1 v1, .seq a2 v2 =>
-    a1 == a2 && ArgF.array_beq v1 v2
-  | .commaSepList a1 v1, .commaSepList a2 v2 =>
-    a1 == a2 && ArgF.array_beq v1 v2
+  | .seq a1 sep1 v1, .seq a2 sep2 v2 =>
+    a1 == a2 && sep1 == sep2 && ArgF.array_beq v1 v2
   | _, _ => false
 termination_by sizeOf a1
 
@@ -1549,8 +1583,7 @@ partial def foldOverArgBindingSpecs {α β}
   | .expr _ | .type _ | .cat _ | .ident .. | .num .. | .decimal .. | .bytes .. | .strlit .. => init
   | .option _ none => init
   | .option _ (some a) => foldOverArgBindingSpecs m f init a
-  | .seq _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a
-  | .commaSepList _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a
+  | .seq _ _ a => a.attach.foldl (init := init) fun init ⟨a, _⟩ => foldOverArgBindingSpecs m f init a
 
 /--
 Invoke a function `f` over each of the declaration specifications for an operator.
diff --git a/Strata/DDM/BuiltinDialects/Init.lean b/Strata/DDM/BuiltinDialects/Init.lean
index b74c4ae00..20ebfda38 100644
--- a/Strata/DDM/BuiltinDialects/Init.lean
+++ b/Strata/DDM/BuiltinDialects/Init.lean
@@ -18,6 +18,8 @@ namespace Strata
 def SyntaxCat.mkOpt (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.Option, args := #[c] }
 def SyntaxCat.mkSeq (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.Seq, args := #[c] }
 def SyntaxCat.mkCommaSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.CommaSepBy, args := #[c] }
+def SyntaxCat.mkSpaceSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpaceSepBy, args := #[c] }
+def SyntaxCat.mkSpacePrefixSepBy (c:SyntaxCat) : SyntaxCat := { ann := .none, name := q`Init.SpacePrefixSepBy, args := #[c] }
 
 def initDialect : Dialect := BuiltinM.create! "Init" #[] do
   let Ident : ArgDeclKind := .cat <| .atom .none q`Init.Ident
@@ -50,6 +52,10 @@ def initDialect : Dialect := BuiltinM.create! "Init" #[] do
 
   declareCat q`Init.CommaSepBy #["a"]
 
+  declareCat q`Init.SpaceSepBy #["a"]
+
+  declareCat q`Init.SpacePrefixSepBy #["a"]
+
   let QualifiedIdent := q`Init.QualifiedIdent
   declareCat QualifiedIdent
   declareOp {
diff --git a/Strata/DDM/BuiltinDialects/StrataDDL.lean b/Strata/DDM/BuiltinDialects/StrataDDL.lean
index c61411ea4..417a84af7 100644
--- a/Strata/DDM/BuiltinDialects/StrataDDL.lean
+++ b/Strata/DDM/BuiltinDialects/StrataDDL.lean
@@ -156,6 +156,7 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
 
   declareMetadata { name := "scope", args := #[.mk "scope" .ident] }
   declareMetadata { name := "unwrap", args := #[] }
+  declareMetadata { name := "nonempty", args := #[] }
   -- Metadata for marking an operation as a constructor definition
   declareMetadata { name := "constructor", args := #[.mk "name" .ident, .mk "fields" .ident] }
   -- Metadata for marking an operation as a constructor list atom (single constructor)
diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean
index 4f356af69..e67e56b72 100644
--- a/Strata/DDM/Elab/Core.lean
+++ b/Strata/DDM/Elab/Core.lean
@@ -1165,28 +1165,28 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T
     let a := c.args[0]!
     elabOption (catElaborator a)
   |  q`Init.Seq =>
-    assert! c.args.size = 1
-    let a := c.args[0]!
-    let f := elabManyElement (catElaborator a)
-    fun tctx stx => do
-      let some loc := mkSourceRange? stx
-        | panic! "seq missing source location"
-      let (args, resultCtx) ← stx.getArgs.foldlM f (#[], tctx)
-      let info : SeqInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx }
-      pure <| .node (.ofSeqInfo info) args
+    elabSeqWith c .none "seq" (·.getArgs)
   | q`Init.CommaSepBy =>
+    elabSeqWith c .comma "commaSepBy" (·.getSepArgs)
+  | q`Init.SpaceSepBy =>
+    elabSeqWith c .space "spaceSepBy" (·.getSepArgs)
+  | q`Init.SpacePrefixSepBy =>
+    elabSeqWith c .spacePrefix "spacePrefixSepBy" (·.getArgs)
+  | _ =>
+    assert! c.args.isEmpty
+    elabOperation
+
+where
+  elabSeqWith (c : SyntaxCat) (sep : SepFormat) (name : String) (getArgsFrom : Syntax → Array Syntax) : TypingContext → Syntax → ElabM Tree :=
     assert! c.args.size = 1
     let a := c.args[0]!
     let f := elabManyElement (catElaborator a)
     fun tctx stx => do
       let some loc := mkSourceRange? stx
-        | panic! s!"commaSepBy missing source location {repr stx}"
-      let (args, resultCtx) ← stx.getSepArgs.foldlM f (#[], tctx)
-      let info : CommaSepInfo := { inputCtx := tctx, loc := loc, args := args.map (·.arg), resultCtx }
-      pure <| .node (.ofCommaSepInfo info) args
-  | _ =>
-    assert! c.args.isEmpty
-    elabOperation
+        | panic! s!"{name} missing source location {repr stx}"
+      let (args, resultCtx) ← (getArgsFrom stx).foldlM f (#[], tctx)
+      let info : SeqInfo := { inputCtx := tctx, loc := loc, sep := sep, args := args.map (·.arg), resultCtx }
+      pure <| .node (.ofSeqInfo info) args
 
 partial def elabExpr (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do
   match stx.getKind with
diff --git a/Strata/DDM/Elab/Tree.lean b/Strata/DDM/Elab/Tree.lean
index ddb9535dd..be2a17e8f 100644
--- a/Strata/DDM/Elab/Tree.lean
+++ b/Strata/DDM/Elab/Tree.lean
@@ -246,11 +246,7 @@ structure OptionInfo extends ElabInfo where
   deriving Inhabited, Repr
 
 structure SeqInfo extends ElabInfo where
-  args : Array Arg
-  resultCtx : TypingContext
-deriving Inhabited, Repr
-
-structure CommaSepInfo extends ElabInfo where
+  sep : SepFormat
   args : Array Arg
   resultCtx : TypingContext
 deriving Inhabited, Repr
@@ -267,7 +263,6 @@ inductive Info
 | ofBytesInfo (info : ConstInfo ByteArray)
 | ofOptionInfo (info : OptionInfo)
 | ofSeqInfo (info : SeqInfo)
-| ofCommaSepInfo (info : CommaSepInfo)
 deriving Inhabited, Repr
 
 namespace Info
@@ -301,7 +296,6 @@ def elabInfo (info : Info) : ElabInfo :=
   | .ofBytesInfo info => info.toElabInfo
   | .ofOptionInfo info => info.toElabInfo
   | .ofSeqInfo info => info.toElabInfo
-  | .ofCommaSepInfo info => info.toElabInfo
 
 def inputCtx (info : Info) : TypingContext := info.elabInfo.inputCtx
 
@@ -347,8 +341,7 @@ def arg : Tree → Arg
       | #[x] => some x.arg
       | _ => panic! "Unexpected option"
     .option info.loc r
-  | .ofSeqInfo info => .seq info.loc info.args
-  | .ofCommaSepInfo info => .commaSepList info.loc info.args
+  | .ofSeqInfo info => .seq info.loc info.sep info.args
 
 theorem sizeOf_children (t : Tree) (i : Nat) (p : i < t.children.size) : sizeOf t[i] < sizeOf t := by
   match t with
@@ -370,7 +363,6 @@ def resultContext (t : Tree) : TypingContext :=
     else
       info.inputCtx
   | .ofSeqInfo info => info.resultCtx
-  | .ofCommaSepInfo info => info.resultCtx
 termination_by t
 
 def isSpecificOp (tree : Tree) (expected : QualifiedIdent) : Bool :=
@@ -384,14 +376,20 @@ def asOption? (t : Tree) : Option (Option Tree) :=
   | _ => none
 
 def asCommaSepInfo? (t : Tree) : Option (Array Tree) :=
-  if let .ofCommaSepInfo _ := t.info then
-    some t.children
+  if let .ofSeqInfo info := t.info then
+    if info.sep == .comma then
+      some t.children
+    else
+      none
   else
     none
 
 def asCommaSepInfo! (t : Tree) : Array Tree :=
-  if let .ofCommaSepInfo _ := t.info then
-    t.children
+  if let .ofSeqInfo info := t.info then
+    if info.sep == .comma then
+      t.children
+    else
+      panic! "Expected commaSepInfo"
   else
     panic! "Expected commaSepInfo"
 
diff --git a/Strata/DDM/Format.lean b/Strata/DDM/Format.lean
index dac6c77d9..03b761c7f 100644
--- a/Strata/DDM/Format.lean
+++ b/Strata/DDM/Format.lean
@@ -378,16 +378,28 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat
   match ma with
   | none => pure (.atom .nil)
   | some a => a.mformatM
-| .seq _ entries => do
-  .atom <$> entries.foldlM (init := .nil) fun p a =>
-    return (p ++ (← a.mformatM).format)
-| .commaSepList _ entries => do
-  if z : entries.size = 0 then
-    pure (.atom .nil)
-  else do
-    let f i q s := return s ++ ", " ++ (← entries[i].mformatM).format
-    let a := (← entries[0].mformatM).format
-    .atom <$> entries.size.foldlM f (start := 1) a
+| .seq _ sep entries => do
+  match sep with
+  | .none =>
+    .atom <$> entries.foldlM (init := .nil) fun p a =>
+      return (p ++ (← a.mformatM).format)
+  | .comma =>
+    if z : entries.size = 0 then
+      pure (.atom .nil)
+    else do
+      let f i q s := return s ++ ", " ++ (← entries[i].mformatM).format
+      let a := (← entries[0].mformatM).format
+      .atom <$> entries.size.foldlM f (start := 1) a
+  | .space =>
+    if z : entries.size = 0 then
+      pure (.atom .nil)
+    else do
+      let f i q s := return s ++ " " ++ (← entries[i].mformatM).format
+      let a := (← entries[0].mformatM).format
+      .atom <$> entries.size.foldlM f (start := 1) a
+  | .spacePrefix =>
+    .atom <$> entries.foldlM (init := .nil) fun p a =>
+      return (p ++ " " ++ (← a.mformatM).format)
 
 private partial def ppArgs (f : StrataFormat) (rargs : Array Arg) : FormatM PrecFormat :=
   if rargs.isEmpty then
diff --git a/Strata/DDM/Integration/Lean/Gen.lean b/Strata/DDM/Integration/Lean/Gen.lean
index e472f8d16..79aa80ab5 100644
--- a/Strata/DDM/Integration/Lean/Gen.lean
+++ b/Strata/DDM/Integration/Lean/Gen.lean
@@ -562,6 +562,10 @@ partial def ppCatWithUnwrap (annType : Ident) (c : SyntaxCat) (unwrap : Bool) :
   match c.name, eq : args.size with
   | q`Init.CommaSepBy, 1 =>
     return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType]
+  | q`Init.SpaceSepBy, 1 =>
+    return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType]
+  | q`Init.SpacePrefixSepBy, 1 =>
+    return mkCApp ``Ann #[mkCApp ``Array #[args[0]], annType]
   | q`Init.Option, 1 =>
     return mkCApp ``Ann #[mkCApp ``Option #[args[0]], annType]
   | q`Init.Seq, 1 =>
@@ -669,6 +673,21 @@ def mkAnnWithTerm (argCtor : Name) (annTerm v : Term) : Term :=
 def annToAst (argCtor : Name) (annTerm : Term) : Term :=
   mkCApp argCtor #[mkCApp ``Ann.ann #[annTerm], mkCApp ``Ann.val #[annTerm]]
 
+mutual
+
+partial def toAstApplyArgSeq (v : Ident) (cat : SyntaxCat) (sepFormat : Name) : GenM Term := do
+  assert! cat.args.size = 1
+  let c := cat.args[0]!
+  let e ← genFreshLeanName "e"
+  let canE ← genIdentFrom e (canonical := true)
+  let t ← toAstApplyArg e c
+  let args := mkCApp ``Array.map #[
+        ←`(fun ⟨$canE, _⟩ => $t),
+        mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]]
+  ]
+  let sepExpr := mkCApp sepFormat #[]
+  return mkCApp ``ArgF.seq #[mkCApp ``Ann.ann #[v], sepExpr, args]
+
 partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false) : GenM Term := do
   let v := mkIdentFrom (←read).src vn
   match cat.name with
@@ -720,16 +739,13 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false)
     let toAst ← toAstIdentM cat.name
     ``($toAst $v)
   | q`Init.CommaSepBy => do
-    assert! cat.args.size = 1
-    let c := cat.args[0]!
-    let e ← genFreshLeanName "e"
-    let canE ← genIdentFrom e (canonical := true)
-    let t ← toAstApplyArg e c
-    let args := mkCApp ``Array.map #[
-          ←`(fun ⟨$canE, _⟩ => $t),
-          mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]]
-    ]
-    return mkAnnWithTerm ``ArgF.commaSepList v args
+    toAstApplyArgSeq v cat ``SepFormat.comma
+  | q`Init.SpaceSepBy => do
+    toAstApplyArgSeq v cat ``SepFormat.space
+  | q`Init.SpacePrefixSepBy => do
+    toAstApplyArgSeq v cat ``SepFormat.spacePrefix
+  | q`Init.Seq => do
+    toAstApplyArgSeq v cat ``SepFormat.none
   | q`Init.Option => do
     assert! cat.args.size = 1
     let c := cat.args[0]!
@@ -741,22 +757,13 @@ partial def toAstApplyArg (vn : Name) (cat : SyntaxCat) (unwrap : Bool := false)
           mkCApp ``Option.attach #[mkCApp ``Ann.val #[v]]
     ]
     return mkAnnWithTerm ``ArgF.option v args
-  | q`Init.Seq => do
-    assert! cat.args.size = 1
-    let c := cat.args[0]!
-    let e ← genFreshLeanName "e"
-    let canE ← genIdentFrom e (canonical := true)
-    let t ← toAstApplyArg e c
-    let args := mkCApp ``Array.map #[
-          ←`(fun ⟨$canE, _⟩ => $t),
-          mkCApp ``Array.attach #[mkCApp ``Ann.val #[v]]
-    ]
-    return mkAnnWithTerm ``ArgF.seq v args
   | qid => do
     assert! cat.args.size = 0
     let toAst ← toAstIdentM qid
     ``(ArgF.op ($toAst $v))
 
+end
+
 abbrev MatchAlt := TSyntax ``Lean.Parser.Term.matchAlt
 
 def toAstBuiltinMatches (cat : QualifiedIdent) : GenM (Array MatchAlt) := do
@@ -897,26 +904,32 @@ partial def getOfIdentArgWithUnwrap (varName : String) (cat : SyntaxCat) (unwrap
     let ofAst ← ofAstIdentM cid
     pure <| mkApp ofAst #[e]
   | q`Init.CommaSepBy => do
-    let c := cat.args[0]!
-    let (vc, vi) ← genFreshIdentPair varName
-    let body ← getOfIdentArg varName c vi
-    ``(OfAstM.ofCommaSepByM $e fun $vc _ => $body)
+    getOfIdentArgSeq varName cat e ``SepFormat.comma
+  | q`Init.SpaceSepBy => do
+    getOfIdentArgSeq varName cat e ``SepFormat.space
+  | q`Init.SpacePrefixSepBy => do
+    getOfIdentArgSeq varName cat e ``SepFormat.spacePrefix
+  | q`Init.Seq => do
+    getOfIdentArgSeq varName cat e ``SepFormat.none
   | q`Init.Option => do
     let c := cat.args[0]!
     let (vc, vi) ← genFreshIdentPair varName
     let body ← getOfIdentArg varName c vi
     ``(OfAstM.ofOptionM $e fun $vc _ => $body)
-  | q`Init.Seq => do
-    let c := cat.args[0]!
-    let (vc, vi) ← genFreshIdentPair varName
-    let body ← getOfIdentArg "e" c vi
-    ``(OfAstM.ofSeqM $e fun $vc _ => $body)
   | cid => do
     assert! cat.args.isEmpty
     let (vc, vi) ← genFreshIdentPair varName
     let ofAst ← ofAstIdentM cid
     ``(OfAstM.ofOperationM $e fun $vc _ => $ofAst $vi)
 
+where
+  getOfIdentArgSeq (varName : String) (cat : SyntaxCat) (e : Term) (sepFormat : Name) : GenM Term := do
+    let c := cat.args[0]!
+    let (vc, vi) ← genFreshIdentPair varName
+    let body ← getOfIdentArg varName c vi
+    let sepFormatTerm := mkCApp sepFormat #[]
+    ``(OfAstM.ofSeqM $sepFormatTerm $e fun $vc _ => $body)
+
 end
 
 def ofAstArgs (argDecls : Array GenArgDecl) (argsVar : Ident) : GenM (Array Ident × Array (TSyntax ``doSeqItem)) := do
@@ -1091,6 +1104,8 @@ def checkInhabited (cat : QualifiedIdent) (ops : Array DefaultCtor) : StateT Inh
         match arg.cat.name with
         | q`Init.Seq => true
         | q`Init.CommaSepBy => true
+        | q`Init.SpaceSepBy => true
+        | q`Init.SpacePrefixSepBy => true
         | q`Init.Option => true
         | c => c ∈ inhabited
     if !isInhabited then
diff --git a/Strata/DDM/Integration/Lean/OfAstM.lean b/Strata/DDM/Integration/Lean/OfAstM.lean
index 58f85370d..91b0a3d90 100644
--- a/Strata/DDM/Integration/Lean/OfAstM.lean
+++ b/Strata/DDM/Integration/Lean/OfAstM.lean
@@ -166,27 +166,20 @@ def ofOptionM {α β} [Repr α] [SizeOf α]
       (fun v => { ann := ann, val := some v }) <$> act v (by decreasing_tactic)
   | _ => throwExpected "option" arg
 
-def ofCommaSepByM {α β} [Repr α] [SizeOf α]
-      (arg : ArgF α)
-      (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β)
-      : OfAstM (Ann (Array β) α) :=
-  match arg with
-  | .commaSepList ann a => do
-    let val ← a.attach.mapM fun ⟨v, vIn⟩  => do
-      act v (by decreasing_tactic)
-    pure { ann := ann, val := val }
-  | _ => throwExpected "seq" arg
-
 def ofSeqM {α β} [Repr α] [SizeOf α]
+      (sep : SepFormat)
       (arg : ArgF α)
       (act : ∀(e : ArgF α), sizeOf e < sizeOf arg → OfAstM β)
       : OfAstM (Ann (Array β) α) :=
   match arg with
-  | .seq ann a => do
-    let val ← a.attach.mapM fun ⟨v, vIn⟩ =>
-      act v (by decreasing_tactic)
-    pure { ann := ann, val := val }
-  | _ => throwExpected "seq" arg
+  | .seq ann sep' a =>
+    if sep == sep' then do
+      let val ← a.attach.mapM fun ⟨v, vIn⟩ =>
+        act v (by decreasing_tactic)
+      pure { ann := ann, val := val }
+    else
+      throwExpected sep.toString arg
+  | _ => throwExpected sep.toString arg
 
 /--
 Get the expression at index `lvl` in the arguments.
diff --git a/Strata/DDM/Integration/Lean/ToExpr.lean b/Strata/DDM/Integration/Lean/ToExpr.lean
index 72a72cca5..02d74f65b 100644
--- a/Strata/DDM/Integration/Lean/ToExpr.lean
+++ b/Strata/DDM/Integration/Lean/ToExpr.lean
@@ -19,6 +19,18 @@ namespace Strata
 
 open Lean
 
+namespace SepFormat
+
+instance : ToExpr SepFormat where
+  toTypeExpr := private mkConst ``SepFormat
+  toExpr
+    | .none => mkConst ``SepFormat.none
+    | .comma => mkConst ``SepFormat.comma
+    | .space => mkConst ``SepFormat.space
+    | .spacePrefix => mkConst ``SepFormat.spacePrefix
+
+end SepFormat
+
 namespace QualifiedIdent
 
 instance : ToExpr QualifiedIdent where
@@ -159,12 +171,9 @@ private def ArgF.toExpr {α} [ToExpr α] : ArgF α → Lean.Expr
 | .option ann a =>
   let tpe := ArgF.typeExpr α
   astAnnExpr! ArgF.option ann (optionToExpr tpe <| a.attach.map fun ⟨e, _⟩ => e.toExpr)
-| .seq ann a =>
-  let tpe := ArgF.typeExpr α
-  astAnnExpr! ArgF.seq ann <| arrayToExpr .zero tpe <| a.map (·.toExpr)
-| .commaSepList ann a =>
+| .seq ann sep a =>
   let tpe := ArgF.typeExpr α
-  astAnnExpr! ArgF.commaSepList ann <| arrayToExpr .zero tpe <| a.map (·.toExpr)
+  astAnnExpr! ArgF.seq ann (toExpr sep) <| arrayToExpr .zero tpe <| a.map (·.toExpr)
 termination_by a => sizeOf a
 
 private protected def OperationF.toExpr {α} [ToExpr α] (op : OperationF α) : Lean.Expr :=
diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean
index 1f84e6b43..160367da3 100644
--- a/Strata/DDM/Ion.lean
+++ b/Strata/DDM/Ion.lean
@@ -505,21 +505,19 @@ private protected def ArgF.toIon {α} [ToIon α] (refs : SymbolIdCache) (arg : A
       | some a =>
         args := args.push (← a.toIon refs )
       return .sexp args
-    | .seq ann l => do
-      let args : Array (Ion _) := #[ ionSymbol! "seq", ← toIon ann ]
-      let args ← l.attach.mapM_off (init := args) fun ⟨v, _⟩ => v.toIon refs
-      return .sexp args
-    | .commaSepList ann l => do
-      let args : Array (Ion _) := #[ ionSymbol! "commaSepList", ← toIon ann ]
+    | .seq ann sep l => do
+      let annIon ← toIon ann
+      let sepName := sep.toIonName
+      let symb := if sepName == "seq" then ionSymbol! "seq"
+                  else if sepName == "commaSepList" then ionSymbol! "commaSepList"
+                  else if sepName == "spaceSepList" then ionSymbol! "spaceSepList"
+                  else ionSymbol! "spacePrefixedList"
+      let args : Array (Ion _) := #[ symb, annIon ]
       let args ← l.attach.mapM_off (init := args) fun ⟨v, _⟩ => v.toIon refs
       return .sexp args
   termination_by sizeOf arg
   decreasing_by
-    · decreasing_tactic
-    · decreasing_tactic
-    · decreasing_tactic
-    · decreasing_tactic
-    · decreasing_tactic
+    all_goals decreasing_tactic
 
 end
 
@@ -617,32 +615,30 @@ private protected def ArgF.fromIon {α} [FromIon α] (v : Ion SymbolId) : FromIo
       | 3 => some <$> Strata.ArgF.fromIon sexp[2]
       | _ => throw "Option expects at most one value."
     return .option ann v
-  | "seq" => do
-    let ⟨p⟩ ← .checkArgMin "seq" sexp 2
-    let ann ← fromIon sexp[1]
-    let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ =>
-      Strata.ArgF.fromIon u
-    return .seq ann args
-  | "commaSepList" => do
-    let ⟨p⟩ ← .checkArgMin "seq" sexp 2
-    let ann ← fromIon sexp[1]
-    let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ =>
-      Strata.ArgF.fromIon u
-    return .commaSepList ann args
   | str =>
-    throw s!"Unexpected identifier {str}"
+    match SepFormat.fromIonName? str with
+    | some sep => do
+      let ⟨p⟩ ← .checkArgMin str sexp 2
+      let ann ← fromIon sexp[1]
+      let args ← sexp.attach.mapM_off (start := 2) fun ⟨u, _⟩ =>
+        Strata.ArgF.fromIon u
+      return .seq ann sep args
+    | none =>
+      throw s!"Unexpected identifier {str}"
 termination_by v
 decreasing_by
-  · have _ : sizeOf sexp[1] < sizeOf sexp := by decreasing_tactic
-    decreasing_tactic
-  · have _ : sizeOf sexp[1] < sizeOf sexp := by decreasing_tactic
-    decreasing_tactic
-  · have _ : sizeOf sexp[2] < sizeOf sexp := by decreasing_tactic
-    decreasing_tactic
-  · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic
-    decreasing_tactic
-  · have _ : sizeOf u < sizeOf sexp := by decreasing_tactic
-    decreasing_tactic
+  all_goals
+    first
+    | have h : sizeOf sexp[1] < sizeOf sexp := by decreasing_tactic
+      have : sizeOf sexp < sizeOf v := sexpP.2
+      omega
+    | have h : sizeOf sexp[2] < sizeOf sexp := by decreasing_tactic
+      have : sizeOf sexp < sizeOf v := sexpP.2
+      omega
+    | have h : sizeOf u < sizeOf sexp := by decreasing_tactic
+      have : sizeOf sexp < sizeOf v := sexpP.2
+      omega
+    | decreasing_tactic
 
 end
 
diff --git a/Strata/DDM/Parser.lean b/Strata/DDM/Parser.lean
index 7f9e81112..eb4d3df02 100644
--- a/Strata/DDM/Parser.lean
+++ b/Strata/DDM/Parser.lean
@@ -767,29 +767,20 @@ def checkLeftRec (thisCatName : QualifiedIdent) (argDecls : ArgDecls) (as : List
     let .isTrue lt := inferInstanceAs (Decidable (v < argDecls.size))
       | return panic! "Invalid index"
     let cat := argDecls[v].kind.categoryOf
-    match cat.name with
-    | q`Init.CommaSepBy =>
+    let isListCategory := cat.name == q`Init.CommaSepBy ||
+                          cat.name == q`Init.SpaceSepBy ||
+                          cat.name == q`Init.SpacePrefixSepBy ||
+                          cat.name == q`Init.Seq ||
+                          cat.name == q`Init.Option
+    if isListCategory then
       assert! cat.args.size = 1
       let c := cat.args[0]!
       if c.name == thisCatName then
         .invalid mf!"Leading symbol cannot be recursive call to {c}"
       else
         .isLeading as
-    | q`Init.Option =>
-      assert! cat.args.size = 1
-      let c := cat.args[0]!
-      if c.name == thisCatName then
-        .invalid mf!"Leading symbol cannot be recursive call to {c}"
-      else
-        .isLeading as
-    | q`Init.Seq =>
-      assert! cat.args.size = 1
-      let c := cat.args[0]!
-      if c.name == thisCatName then
-        .invalid mf!"Leading symbol cannot be recursive call to {c}"
-      else
-        .isLeading as
-    | qid =>
+    else
+      let qid := cat.name
       if cat.args.size > 0 then
         panic! s!"Unknown parametric category '{eformat cat}' is not supported."
       if qid == thisCatName then
@@ -840,6 +831,24 @@ private def sepByParser (p sep : Parser) (allowTrailingSep : Bool := false) : Pa
         s
 }
 
+private def sepBy1Parser (p sep : Parser) (allowTrailingSep : Bool := false) : Parser := {
+  info := sepByInfo p.info sep.info
+  fn   := fun c s =>
+    let s := sepByFn allowTrailingSep p.fn sep.fn c s
+    if s.hasError then
+      s
+    else
+      match s.stxStack.back with
+      | .node .none k args =>
+        if args.isEmpty then
+          -- Require at least one element
+          s.mkError "expected at least one element"
+        else
+          s
+      | _ =>
+        s
+}
+
 def manyParser (p : Parser) : Parser := {
   info := noFirstTokenInfo p.info
   fn   := fun c s =>
@@ -857,18 +866,44 @@ def manyParser (p : Parser) : Parser := {
         s
 }
 
+def many1Parser (p : Parser) : Parser := {
+  info := p.info
+  fn   := fun c s =>
+    let s := manyFn p.fn c s
+    if s.hasError then
+      s
+    else
+      match s.stxStack.back with
+      | .node .none _k args =>
+        if args.isEmpty then
+          s.mkError "expected at least one element"
+        else
+          s
+      | _ =>
+        s
+}
+
+/-- Helper to choose between sepByParser and sepBy1Parser based on nonempty flag -/
+private def commaSepByParserHelper (nonempty : Bool) (p : Parser) : Parser :=
+  if nonempty then
+    sepBy1Parser p (symbolNoAntiquot ",")
+  else
+    sepByParser p (symbolNoAntiquot ",")
+
 /-- Parser function for given syntax category -/
-partial def catParser (ctx : ParsingContext) (cat : SyntaxCat) : Except SyntaxCat Parser :=
+partial def catParser (ctx : ParsingContext) (cat : SyntaxCat) (metadata : Metadata := {}) : Except SyntaxCat Parser :=
   match cat.name with
   | q`Init.CommaSepBy =>
     assert! cat.args.size = 1
-    (sepByParser · (symbolNoAntiquot ",")) <$> catParser ctx cat.args[0]!
+    let isNonempty := q`StrataDDL.nonempty ∈ metadata
+    commaSepByParserHelper isNonempty <$> catParser ctx cat.args[0]!
+  | q`Init.SpaceSepBy | q`Init.SpacePrefixSepBy | q`Init.Seq =>
+    assert! cat.args.size = 1
+    let isNonempty := q`StrataDDL.nonempty ∈ metadata
+    (if isNonempty then many1Parser else manyParser) <$> catParser ctx cat.args[0]!
   | q`Init.Option =>
     assert! cat.args.size = 1
     optionalNoAntiquot <$> catParser ctx cat.args[0]!
-  | q`Init.Seq =>
-    assert! cat.args.size = 1
-    manyParser <$> catParser ctx cat.args[0]!
   | qid =>
     if cat.args.isEmpty then
       .ok (atomCatParser ctx qid)
@@ -888,7 +923,7 @@ private def prependSyntaxDefAtomParser (ctx : ParsingContext) (argDecls : ArgDec
     let addParser (p : Parser) :=
       let q : Parser := Lean.Parser.adaptCacheableContext ({ · with prec }) p
       q >> r
-    match catParser ctx argDecls[v].kind.categoryOf with
+    match catParser ctx argDecls[v].kind.categoryOf argDecls[v].metadata with
     | .ok p =>
       addParser p
     | .error c =>
diff --git a/Strata/DL/SMT/DDMTransform/Parse.lean b/Strata/DL/SMT/DDMTransform/Parse.lean
index e573c74f3..41406cba7 100644
--- a/Strata/DL/SMT/DDMTransform/Parse.lean
+++ b/Strata/DL/SMT/DDMTransform/Parse.lean
@@ -160,10 +160,6 @@ op simple_symbol_some () : SimpleSymbol => "some";
 category Symbol;
 op symbol (@[unwrap] s:SimpleSymbol) : Symbol => s;
 
-category SymbolList; // For spacing, has at least one element
-op symbol_list_one (se:Symbol) : SymbolList => se;
-op symbol_list_cons (se:Symbol, sse:SymbolList) : SymbolList => se " " sse;
-
 category Keyword;
 op kw_symbol (@[unwrap] s:SimpleSymbol) : Keyword => ":" s;
 
@@ -191,11 +187,7 @@ op se_symbol (s:Symbol) : SExpr => s;
 op se_reserved (s:Reserved) : SExpr => s;
 op se_keyword (s:Keyword) : SExpr => s;
 
-category SExprList; // For spacing, has at least one element
-op sexpr_list_one (se:SExpr) : SExprList => se;
-op sexpr_list_cons (se:SExpr, sse:SExprList) : SExprList => se " " sse;
-
-op se_ls (s:Option SExprList) : SExpr => "(" s ")";
+op se_ls (s:SpaceSepBy SExpr) : SExpr => "(" s ")";
 
 
 category SMTIdentifier;
@@ -207,11 +199,7 @@ op ind_symbol (@[unwrap] s:Symbol) : Index => s;
 
 op iden_simple (s:Symbol) : SMTIdentifier => s;
 
-category IndexList; // For spacing; has at least one element
-op index_list_one (i:Index) : IndexList => i;
-op index_list_cons (i:Index, spi:IndexList) : IndexList => i " " spi;
-
-op iden_indexed (s:Symbol, si:IndexList) : SMTIdentifier =>
+op iden_indexed (s:Symbol, @[nonempty] si:SpaceSepBy Index) : SMTIdentifier =>
   "(" "_ " s " " si ")";
 
 
@@ -219,11 +207,7 @@ op iden_indexed (s:Symbol, si:IndexList) : SMTIdentifier =>
 category SMTSort;
 op smtsort_ident (s:SMTIdentifier) : SMTSort => s;
 
-category SMTSortList; // For spacing; has at least one element
-op smtsort_list_one (i:SMTSort) : SMTSortList => i;
-op smtsort_list_cons (i:SMTSort, spi:SMTSortList) : SMTSortList => i " " spi;
-
-op smtsort_param (s:SMTIdentifier, sl:SMTSortList) : SMTSort
+op smtsort_param (s:SMTIdentifier, @[nonempty] sl:SpaceSepBy SMTSort) : SMTSort
   => "(" s " " sl ")";
 
 
@@ -236,10 +220,6 @@ op av_sel (s:Seq SExpr) : AttributeValue => "(" s ")";
 category Attribute;
 op att_kw (k:Keyword, av:Option AttributeValue) : Attribute => k av;
 
-category AttributeList; // For spacing; has at least one element
-op att_list_one (i:Attribute) : AttributeList => i;
-op att_list_cons (i:Attribute, spi:AttributeList) : AttributeList => i " " spi;
-
 
 // 6. Terms
 category QualIdentifier;
@@ -249,41 +229,29 @@ op qi_isort (i:SMTIdentifier, s:SMTSort) : QualIdentifier =>
 
 category Term; // Forward declaration
 
-category TermList; // For Spacing
-op term_list_one (i:Term) : TermList => i:0;
-op term_list_cons (i:Term, spi:TermList) : TermList => i:0 " " spi:0;
-
 category ValBinding;
 op val_binding (s:Symbol, t:Term) : ValBinding => "(" s " " t ")";
 
-category ValBindingList; // For spacing; has at least one element
-op val_binding_list_one (i:ValBinding) : ValBindingList => i;
-op val_binding_list_cons (i:ValBinding, spi:ValBindingList) : ValBindingList => i " " spi;
-
 category SortedVar;
 op sorted_var (s:Symbol, so:SMTSort) : SortedVar => "(" s " " so ")";
 
-category SortedVarList; // For spacing; has at least one element
-op sorted_var_list_one (i:SortedVar) : SortedVarList => i;
-op sorted_var_list_cons (i:SortedVar, spi:SortedVarList) : SortedVarList => i " " spi;
-
 // TODO: support the match statement
 // category Pattern;
 
 op spec_constant_term (sc:SpecConstant) : Term => sc;
 op qual_identifier (qi:QualIdentifier) : Term => qi;
-op qual_identifier_args (qi:QualIdentifier, ts:TermList) : Term =>
+op qual_identifier_args (qi:QualIdentifier, @[nonempty] ts:SpaceSepBy Term) : Term =>
   "(" qi " " ts ")";
 
-op let_smt (vbps: ValBindingList, t:Term) : Term =>
+op let_smt (@[nonempty] vbps: SpaceSepBy ValBinding, t:Term) : Term =>
   "(" "let" "(" vbps ")" t ")";
-op lambda_smt (svs: SortedVarList, t:Term) : Term =>
+op lambda_smt (@[nonempty] svs: SpaceSepBy SortedVar, t:Term) : Term =>
   "(" "lambda" "(" svs ")" t ")";
-op forall_smt (svs: SortedVarList, t:Term) : Term =>
+op forall_smt (@[nonempty] svs: SpaceSepBy SortedVar, t:Term) : Term =>
   "(" "forall" "(" svs ")" t ")";
-op exists_smt (svs: SortedVarList, t:Term) : Term =>
+op exists_smt (@[nonempty] svs: SpaceSepBy SortedVar, t:Term) : Term =>
   "(" "exists" "(" svs ")" t ")";
-op bang (t:Term, attrs:AttributeList) : Term =>
+op bang (t:Term, @[nonempty] attrs:SpaceSepBy Attribute) : Term =>
   "(" "!" t " " attrs ")";
 
 
@@ -345,41 +313,19 @@ op smtoption_attr (a:Attribute) : SMTOption => a;
 category SortDec;
 op sort_dec (s:Symbol, n:Num) : SortDec => "(" s n ")";
 
-category SortDecList; // For spacing; has at least one element
-op sort_dec_list_one (i:SortDec) : SortDecList => i;
-op sort_dec_list_cons (i:SortDec, spi:SortDecList) : SortDecList =>
-  i " " spi;
-
 category SelectorDec;
 op selector_dec (s:Symbol, so:SMTSort) : SelectorDec => "(" s so ")";
 
-category SelectorDecList; // For spacing; has at least one element
-op selector_dec_list_one (i:SelectorDec) : SelectorDecList => i;
-op selector_dec_list_cons (i:SelectorDec, spi:SelectorDecList) : SelectorDecList =>
-  i " " spi;
-
 category ConstructorDec;
-op constructor_dec (s:Symbol, sdl:Option SelectorDecList) : ConstructorDec =>
-  "(" s " " sdl ")";
-
-category ConstructorDecList; // For spacing; has at least one element
-op constructor_list_one (i:ConstructorDec) : ConstructorDecList => i;
-op constructor_list_cons (i:ConstructorDec, spi:ConstructorDecList)
-  : ConstructorDecList =>
-  i " " spi;
+op constructor_dec (s:Symbol, sdl:SpaceSepBy SelectorDec) : ConstructorDec =>
+  "(" s sdl ")";
 
 category DatatypeDec;
-op datatype_dec (cs:ConstructorDecList) : DatatypeDec
+op datatype_dec (@[nonempty] cs:SpaceSepBy ConstructorDec) : DatatypeDec
   => "(" cs ")";
-op datatype_dec_par (symbols: SymbolList, cs:ConstructorDecList) : DatatypeDec
+op datatype_dec_par (@[nonempty] symbols: SpaceSepBy Symbol, @[nonempty] cs:SpaceSepBy ConstructorDec) : DatatypeDec
   => "(" "par " "(" symbols ")" "(" cs ")" ")";
 
-category DatatypeDecList; // For spacing; has at least one element
-op datatype_dec_list_one (i:DatatypeDec) : DatatypeDecList => i;
-op datatype_dec_list_cons (i:DatatypeDec, spi:DatatypeDecList)
-  : DatatypeDecList =>
-  i " " spi;
-
 category FunctionDec;
 op function_dec (s:Symbol, sv:Seq SortedVar, so:SMTSort) : FunctionDec
   => "(" s "(" sv ")" so ")";
@@ -388,12 +334,6 @@ category FunctionDef;
 op function_def (s:Symbol, sv:Seq SortedVar, so:SMTSort, t:Term) : FunctionDef
   => s "(" sv ")" so t;
 
-category FunctionDefList; // For spacing; has at least one element
-op function_def_list_one (i:FunctionDef) : FunctionDefList => i;
-op function_def_list_cons (i:FunctionDef, spi:FunctionDefList)
-  : FunctionDefList =>
-  i " " spi;
-
 #end
 
 
@@ -408,17 +348,17 @@ import SMTCore;
 // cmd_' is necessary, otherwise it raises "unexpected token 'assert'; expected identifier"
 op cmd_assert (t:Term) : Command => "(" "assert " t ")";
 op check_sat () : Command => "(" "check-sat" ")";
-op check_sat_assuming (ts:Option TermList) : Command =>
-  "(" "check-sat-assuming " ts ")";
+op check_sat_assuming (ts:SpacePrefixSepBy Term) : Command =>
+  "(" "check-sat-assuming" ts ")";
 op declare_const (s:Symbol, so:SMTSort) : Command =>
   "(" "declare-const " s so ")";
 op declare_datatype (s:Symbol, so:DatatypeDec) : Command =>
   "(" "declare-datatype " s so ")";
 // The size of SortDec and DatatypeDec must be equal, but omit the check in
 // this DDM definition because its representation can be quite ugly.
-op declare_datatypes (s:SortDecList, so:DatatypeDecList) : Command =>
+op declare_datatypes (@[nonempty] s:SpaceSepBy SortDec, @[nonempty] so:SpaceSepBy DatatypeDec) : Command =>
   "(" "declare-datatypes" "(" s ")" "(" so ")" ")";
-op declare_fun (s:Symbol, sol:Option SMTSortList, range:SMTSort) : Command =>
+op declare_fun (s:Symbol, sol:SpaceSepBy SMTSort, range:SMTSort) : Command =>
   "(" "declare-fun " s "(" sol ")" range ")";
 op declare_sort (s:Symbol, n:Num) : Command =>
   "(" "declare-sort " s n ")";
@@ -430,7 +370,7 @@ op define_fun (fdef:FunctionDef) : Command =>
   "(" "define-fun " fdef ")";
 op define_fun_rec (fdef:FunctionDef) : Command =>
   "(" "define-fun-rec " fdef ")";
-op define_funs_rec (fdefs:FunctionDefList, terms:TermList) : Command =>
+op define_funs_rec (@[nonempty] fdefs:SpaceSepBy FunctionDef, @[nonempty] terms:SpaceSepBy Term) : Command =>
   "(" "define-funs-rec" "(" fdefs ")" "(" terms ")" ")";
 op define_sort (s:Symbol, sl:Seq Symbol, so:SMTSort) : Command =>
   "(" "define-sort " s "(" sl ")" so ")";
@@ -444,7 +384,7 @@ op get_option (kw:Keyword) : Command => "(" "get-option " kw ")";
 op get_proof () : Command => "(" "get-proof" ")";
 op get_unsat_assumptions () : Command => "(" "get-unsat-assumptions" ")";
 op get_unsat_core () : Command => "(" "get-unsat-core" ")";
-op get_value (tl:TermList) : Command =>
+op get_value (@[nonempty] tl:SpaceSepBy Term) : Command =>
   "(" "get-value" "(" tl ")" ")";
 op cmd_pop (n:Num) : Command => "(" "pop " n ")";
 op cmd_push (n:Num) : Command => "(" "push " n ")";
@@ -481,12 +421,6 @@ op mr_deffunrec (fdef:FunctionDef) : ModelResponse =>
   "(" "define-fun-rec " fdef ")";
 // TODO: define-funs-rec
 
-category SeqModelResponse;
-op seqmr_nil () : SeqModelResponse => ;
-op seqmr_one (i: ModelResponse) : SeqModelResponse => i;
-op seqmr_cons (i: ModelResponse, is: SeqModelResponse) : SeqModelResponse
-  => i is;
-
 category InfoResponse;
 op ir_stack_levels (n:Num) : InfoResponse => ":assertion-stack-response " n;
 op ir_authors (s:Str) : InfoResponse => ":authors " s;
@@ -496,29 +430,12 @@ op ir_unknown (r:ReasonUnknown) : InfoResponse => ":reason-unknown " r;
 op ir_ver (s:Str) : InfoResponse => ":version " s;
 op ir_attr (a:Attribute) : InfoResponse => a;
 
-category InfoResponseList;
-op ir_list_one (i: InfoResponse) : InfoResponseList => i;
-op ir_list_cons (i: InfoResponse, is: InfoResponseList) : InfoResponseList
-  => i is;
-
 category ValuationPair;
 op valuation_pair (t1:Term, t2:Term) : ValuationPair => "(" t1 " " t2 ")";
 
-category ValuationPairList;
-op valuation_pair_list_one (i: ValuationPair) : ValuationPairList => i;
-op valuation_pair_list_cons (i: ValuationPair, is: ValuationPairList)
-  : ValuationPairList
-  => i is;
-
 category TValuationPair;
 op t_valuation_pair (t1:Symbol, t2:BValue) : TValuationPair => "(" t1 " " t2 ")";
 
-category TValuationPairList;
-op t_valuation_pair_list_one (i: TValuationPair) : TValuationPairList => i;
-op t_valuation_pair_list_cons (i: TValuationPair, is: TValuationPairList)
-  : TValuationPairList
-  => i is;
-
 category CheckSatResponse;
 op csr_sat () : CheckSatResponse => "sat";
 op csr_unsat () : CheckSatResponse => "unsat";
@@ -528,20 +445,20 @@ category EchoResponse;
 op echo_response (s:Str) : EchoResponse => s;
 
 category GetAssertionsResponse;
-op get_assertions_response (t:Option TermList) : GetAssertionsResponse =>
+op get_assertions_response (t:SpaceSepBy Term) : GetAssertionsResponse =>
   "(" t ")";
 
 category GetAssignmentResponse;
-op get_assignment_response (t:Option TValuationPairList)
+op get_assignment_response (t:SpaceSepBy TValuationPair)
     : GetAssignmentResponse =>
   "(" t ")";
 
 category GetInfoResponse;
-op get_info_response (i2:InfoResponseList) : GetInfoResponse =>
+op get_info_response (i2:SpaceSepBy InfoResponse) : GetInfoResponse =>
   "(" i2 ")";
 
 category GetModelResponse;
-op get_model_response (mr:SeqModelResponse) : GetModelResponse =>
+op get_model_response (mr:SpaceSepBy ModelResponse) : GetModelResponse =>
   "(" mr ")";
 
 category GetOptionResponse;
@@ -551,15 +468,15 @@ category GetProofResponse;
 op get_proof_response (s:SExpr) : GetProofResponse => s;
 
 category GetUnsatAssumpResponse;
-op get_unsat_assump_response (ts:Option TermList) : GetUnsatAssumpResponse =>
+op get_unsat_assump_response (ts:SpaceSepBy Term) : GetUnsatAssumpResponse =>
   "(" ts ")";
 
 category GetUnsatCoreResponse;
-op get_unsat_core_response (ss:Option SymbolList) : GetUnsatCoreResponse =>
+op get_unsat_core_response (ss:SpaceSepBy Symbol) : GetUnsatCoreResponse =>
   "(" ss ")";
 
 category GetValueResponse;
-op get_value_response (vps:Option ValuationPairList)
+op get_value_response (vps:SpaceSepBy ValuationPair)
   : GetValueResponse => "(" vps ")";
 
 category SpecificSuccessResponse;
@@ -816,23 +733,23 @@ namespace SMTDDM
 deriving instance BEq for
   -- Sequences
   SpecConstant, QualifiedIdent, SimpleSymbol,
-  Symbol, SymbolList,
-  SortDec, SortDecList,
+  Symbol,
+  SortDec,
   Reserved,
   Keyword, SExpr, AttributeValue, BValue,
-  Attribute, AttributeList,
+  Attribute,
   SMTOption,
-  Index, IndexList,
+  Index,
   SMTIdentifier,
-  SMTSort, SMTSortList,
-  SortedVar, SortedVarList,
+  SMTSort,
+  SortedVar,
   QualIdentifier, ValBinding,
-  Term, TermList,
+  Term,
   InfoFlag,
-  SelectorDec, SelectorDecList,
-  ConstructorDec, ConstructorDecList,
-  DatatypeDec, DatatypeDecList,
-  FunctionDef, FunctionDefList,
+  SelectorDec,
+  ConstructorDec,
+  DatatypeDec,
+  FunctionDef,
   Command
 
 end SMTDDM
diff --git a/Strata/DL/SMT/DDMTransform/Translate.lean b/Strata/DL/SMT/DDMTransform/Translate.lean
index ec5a7f853..50ab8637e 100644
--- a/Strata/DL/SMT/DDMTransform/Translate.lean
+++ b/Strata/DL/SMT/DDMTransform/Translate.lean
@@ -71,22 +71,14 @@ private def translateFromTermPrim (t:SMT.TermPrim):
     let bvty := mkSymbol (s!"bv{bv.toNat}")
     let val:Index SourceRange := .ind_numeral srnone bv.width
     return (.qual_identifier srnone
-      (.qi_ident srnone (.iden_indexed srnone bvty (.index_list_one srnone val))))
+      (.qi_ident srnone (.iden_indexed srnone bvty (Ann.mk srnone #[val]))))
   | .string s =>
     return .spec_constant_term srnone (.sc_str srnone s)
 
--- List of SMTSort to SeqPSMTSort.
--- Hope this could be elided away later. :(
+-- List of SMTSort to Array.
 private def translateFromSMTSortList (l: List (SMTSort SourceRange)):
-    Option (SMTSortList SourceRange) :=
-  let srnone := SourceRange.none
-  match l with
-  | [] => .none
-  | h::[] => .some (.smtsort_list_one srnone h)
-  | h1::h2::t => .some (
-    match translateFromSMTSortList t with
-    | .none => .smtsort_list_cons srnone h1 (.smtsort_list_one srnone h2)
-    | .some t => .smtsort_list_cons srnone h1 (.smtsort_list_cons srnone h2 t))
+    Array (SMTSort SourceRange) :=
+  l.toArray
 
 private def translateFromTermType (t:SMT.TermType):
     Except String (SMTDDM.SMTSort SourceRange) := do
@@ -95,10 +87,11 @@ private def translateFromTermType (t:SMT.TermType):
   | .prim tp =>
     match tp with
     | .bitvec n =>
+      let idx : Index SourceRange := .ind_numeral srnone n
       return (.smtsort_ident srnone
         (.iden_indexed srnone
           (mkSymbol "BitVec")
-          (.index_list_one srnone (.ind_numeral srnone n))))
+          (Ann.mk srnone #[idx])))
     | .trigger =>
       throw "don't know how to translate a trigger type"
     | _ =>
@@ -114,37 +107,11 @@ private def translateFromTermType (t:SMT.TermType):
     throw "don't know how to translate an option type"
   | .constr id args =>
     let argtys <- args.mapM translateFromTermType
-    match translateFromSMTSortList argtys with
-    | .none => throw "empty argument to type constructor"
-    | .some argtys =>
-      return .smtsort_param srnone (mkIdentifier id) argtys
-
--- List of SortedVar to SeqPSortedVar.
--- Hope this could be elided away later. :(
-private def translateFromSortedVarList (l: List (SortedVar SourceRange)):
-    Option (SortedVarList SourceRange) :=
-  let srnone := SourceRange.none
-  match l with
-  | [] => .none
-  | h::[] => .some (.sorted_var_list_one srnone h)
-  | h1::h2::t => .some (
-    match translateFromSortedVarList t with
-    | .none => .sorted_var_list_cons srnone h1 (.sorted_var_list_one srnone h2)
-    | .some t =>
-      .sorted_var_list_cons srnone h1 (.sorted_var_list_cons srnone h2 t))
-
--- List of SortedVar to SeqPSortedVar.
--- Hope this could be elided away later. :(
-private def translateFromTermList (l: List (Term SourceRange)):
-    Option (TermList SourceRange) :=
-  let srnone := SourceRange.none
-  match l with
-  | [] => .none
-  | h::[] => .some (.term_list_one srnone h)
-  | h1::h2::t => .some (
-    match translateFromTermList t with
-    | .none => .term_list_cons srnone h1 (.term_list_one srnone h2)
-    | .some t => .term_list_cons srnone h1 (.term_list_cons srnone h2 t))
+    let argtys_array := translateFromSMTSortList argtys
+    if argtys_array.isEmpty then
+      throw "empty argument to type constructor"
+    else
+      return .smtsort_param srnone (mkIdentifier id) (Ann.mk srnone argtys_array)
 
 def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term SourceRange) := do
   let srnone := SourceRange.none
@@ -156,27 +123,28 @@ def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term SourceRange) := d
   | .none _ | .some _ => throw "don't know how to translate none and some"
   | .app op args _ =>
     let args' <- args.mapM translateFromTerm
-    match translateFromTermList args' with
-    | .some args =>
-      return (.qual_identifier_args srnone
-        (.qi_ident srnone (mkIdentifier op.mkName)) args)
-    | .none =>
+    let args_array := args'.toArray
+    if args_array.isEmpty then
       return (.qual_identifier srnone (.qi_ident srnone (mkIdentifier op.mkName)))
+    else
+      return (.qual_identifier_args srnone
+        (.qi_ident srnone (mkIdentifier op.mkName)) (Ann.mk srnone args_array))
   | .quant qkind args _tr body =>
     let args_sorted:List (SMTDDM.SortedVar SourceRange) <-
       args.mapM
         (fun ⟨name,ty⟩ => do
           let ty' <- translateFromTermType ty
           return .sorted_var srnone (mkSymbol name) ty')
-    match translateFromSortedVarList args_sorted with
-    | .none => throw "empty quantifier"
-    | .some args_sorted =>
+    let args_array := args_sorted.toArray
+    if args_array.isEmpty then
+      throw "empty quantifier"
+    else
       let body <- translateFromTerm body
       match qkind with
       | .all =>
-        return .forall_smt srnone args_sorted body
+        return .forall_smt srnone (Ann.mk srnone args_array) body
       | .exist =>
-        return .exists_smt srnone args_sorted body
+        return .exists_smt srnone (Ann.mk srnone args_array) body
 
 
 private def dummy_prg_for_toString :=
diff --git a/Strata/Languages/Boogie/DDMTransform/Translate.lean b/Strata/Languages/Boogie/DDMTransform/Translate.lean
index ab1b3bd4f..0c563dbb4 100644
--- a/Strata/Languages/Boogie/DDMTransform/Translate.lean
+++ b/Strata/Languages/Boogie/DDMTransform/Translate.lean
@@ -89,7 +89,7 @@ def checkOpArg (arg : Arg) (name : QualifiedIdent) (argc : Nat) : TransM (Array
 
 def translateCommaSep [Inhabited α] (f : Strata.Arg → TransM α) (arg : Strata.Arg) :
   TransM (Array α) := do
-  let .commaSepList _ args := arg
+  let .seq _ .comma args := arg
     | TransM.error s!"Expected commaSepList: {repr arg}"
   args.mapM f
 
@@ -300,7 +300,7 @@ def translateTypeSynonym (bindings : TransBindings) (op : Operation) :
               let bargs ← checkOpArg arg q`Boogie.mkBindings 1
               let args ←
                   match bargs[0]! with
-                  | .commaSepList _ args =>
+                  | .seq _ .comma args =>
                     let (arr, bindings) ← translateTypeBindings bindings args
                     return (arr.toList, bindings)
                   | _ => TransM.error
@@ -325,7 +325,7 @@ def translateTypeDecl (bindings : TransBindings) (op : Operation) :
               let bargs ← checkOpArg arg q`Boogie.mkBindings 1
               let numargs ←
                   match bargs[0]! with
-                  | .commaSepList _ args => pure args.size
+                  | .seq _ .comma args => pure args.size
                   | _ => TransM.error
                           s!"translateTypeDecl expects a comma separated list: {repr bargs[0]!}")
                     op.args[1]!
@@ -1024,7 +1024,7 @@ partial def translateStmt (p : Program) (bindings : TransBindings) (arg : Arg) :
 partial def translateBlock (p : Program) (bindings : TransBindings) (arg : Arg) :
   TransM ((List Boogie.Statement) × TransBindings) := do
   let args ← checkOpArg arg q`Boogie.block 1
-  let .seq _ stmts := args[0]!
+  let .seq _ .none stmts := args[0]!
     | TransM.error s!"Invalid block {repr args[0]!}"
   let (a, bindings) ← stmts.foldlM (init := (#[], bindings)) fun (a, b) s => do
       let (s, b) ← translateStmt p b s
@@ -1064,7 +1064,7 @@ def translateBindings (bindings : TransBindings) (op : Arg) :
   TransM (ListMap BoogieIdent LMonoTy) := do
   let bargs ← checkOpArg op q`Boogie.mkBindings 1
   match bargs[0]! with
-  | .commaSepList _ args =>
+  | .seq _ .comma args =>
     let arr ← translateInitMkBindings bindings args
     return arr.toList
   | _ =>
@@ -1121,7 +1121,7 @@ def translateSpecElem (p : Program) (name : BoogieIdent) (count : Nat) (bindings
 partial def translateSpec (p : Program) (name : BoogieIdent) (bindings : TransBindings) (arg : Arg) :
   TransM (List BoogieIdent × ListMap BoogieLabel Procedure.Check × ListMap BoogieLabel Procedure.Check) := do
   let sargs ← checkOpArg arg q`Boogie.spec_mk 1
-  let .seq _ args := sargs[0]!
+  let .seq _ .none args := sargs[0]!
     | TransM.error s!"Invalid specs {repr sargs[0]!}"
   go 0 args.size args
   where go (count max : Nat) (args : Array Arg) := do
@@ -1332,7 +1332,7 @@ def translateDatatype (p : Program) (bindings : TransBindings) (op : Operation)
               let bargs ← checkOpArg arg q`Boogie.mkBindings 1
               let args ←
                   match bargs[0]! with
-                  | .commaSepList _ args =>
+                  | .seq _ .comma args =>
                     let (arr, bindings) ← translateTypeBindings bindings args
                     return (arr.toList, bindings)
                   | _ => TransM.error
diff --git a/Strata/Languages/C_Simp/DDMTransform/Translate.lean b/Strata/Languages/C_Simp/DDMTransform/Translate.lean
index 8cae3842f..b7df8b3b4 100644
--- a/Strata/Languages/C_Simp/DDMTransform/Translate.lean
+++ b/Strata/Languages/C_Simp/DDMTransform/Translate.lean
@@ -77,7 +77,7 @@ def checkOpArg (arg : Arg) (name : QualifiedIdent) (argc : Nat) : TransM (Array
 
 def translateCommaSep [Inhabited α] (f : Strata.Arg → TransM α) (arg : Strata.Arg) :
   TransM (Array α) := do
-  let .commaSepList _ args := arg
+  let .seq _ .comma args := arg
     | TransM.error s!"Expected commaSepList: {repr arg}"
   args.mapM f
 
@@ -338,7 +338,7 @@ def translateBindings (bindings : TransBindings) (op : Arg) :
   TransM (ListMap Expression.Ident LMonoTy) := do
   let bargs ← checkOpArg op q`C_Simp.mkBindings 1
   match bargs[0]! with
-  | .commaSepList _ args =>
+  | .seq _ .comma args =>
     let arr ← args.mapM (fun op => do
       let bargs ← checkOpArg op q`C_Simp.mkBinding 2
       let id ← translateIdent bargs[0]!
@@ -411,7 +411,7 @@ partial def translateStmt (bindings : TransBindings) (arg : Arg) :
 partial def translateBlock (bindings : TransBindings) (arg : Arg) :
   TransM (List Statement) := do
   let args ← checkOpArg arg q`C_Simp.block 1
-  let .seq _ stmts := args[0]!
+  let .seq _ .none stmts := args[0]!
     | TransM.error s!"Invalid block {repr args[0]!}"
   let (a, _) ← stmts.foldlM (init := (#[], bindings)) fun (a, b) s => do
       let (s, b) ← translateStmt b s
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index dddb18df2..e79088187 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -108,7 +108,7 @@ def translateParameter (arg : Arg) : TransM Parameter := do
 
 def translateParameters (arg : Arg) : TransM (List Parameter) := do
   match arg with
-  | .commaSepList _ args =>
+  | .seq _ .comma args =>
     args.toList.mapM translateParameter
   | _ => pure []
 
@@ -184,7 +184,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
         | .Identifier name => name
         | _ => ""
       let argsList ← match argsSeq with
-        | .commaSepList _ args => args.toList.mapM translateStmtExpr
+        | .seq _ .comma args => args.toList.mapM translateStmtExpr
         | _ => pure []
       return .StaticCall calleeName argsList
     | q`Laurel.return, #[arg0] =>
@@ -209,7 +209,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
   | _ => TransM.error s!"translateStmtExpr expects operation"
 
 partial def translateSeqCommand (arg : Arg) : TransM (List StmtExpr) := do
-  let .seq _ args := arg
+  let .seq _ .none args := arg
     | TransM.error s!"translateSeqCommand expects seq"
   let mut stmts : List StmtExpr := []
   for arg in args do
@@ -264,7 +264,7 @@ def parseProgram (prog : Strata.Program) : TransM Laurel.Program := do
     if prog.commands.size == 1 && prog.commands[0]!.name == q`Laurel.program then
       -- Extract procedures from the program operation's first argument (Seq Procedure)
       match prog.commands[0]!.args[0]! with
-      | .seq _ procs => procs.filterMap fun arg =>
+      | .seq _ .none procs => procs.filterMap fun arg =>
           match arg with
           | .op op => some op
           | _ => none
diff --git a/StrataTest/DDM/Gen.lean b/StrataTest/DDM/Gen.lean
index ed073024f..71fddb740 100644
--- a/StrataTest/DDM/Gen.lean
+++ b/StrataTest/DDM/Gen.lean
@@ -145,7 +145,7 @@ info: Strata.ExprF.app ()
       (Strata.ArgF.type (Strata.TypeExprF.ident () { dialect := "TestDialect", name := "bool" } (Array.mkEmpty 0))))
     (Strata.ArgF.op
       { ann := (), name := { dialect := "TestDialect", name := "mkBindings" },
-        args := (Array.mkEmpty 1).push (Strata.ArgF.commaSepList () (Array.mkEmpty 0)) }))
+        args := (Array.mkEmpty 1).push (Strata.ArgF.seq () Strata.SepFormat.comma (Array.mkEmpty 0)) }))
   (Strata.ArgF.expr (Strata.ExprF.fn () { dialect := "TestDialect", name := "trueExpr" }))
 -/
 #guard_msgs in
diff --git a/StrataTest/DDM/Integration/Java/TestGen.lean b/StrataTest/DDM/Integration/Java/TestGen.lean
index 8dc4012e5..40d390af4 100644
--- a/StrataTest/DDM/Integration/Java/TestGen.lean
+++ b/StrataTest/DDM/Integration/Java/TestGen.lean
@@ -314,7 +314,7 @@ elab "#testRoundtrip" : command => do
     if prog.commands.size != 1 then Lean.logError "Expected 1 command"; return
     let cmd := prog.commands[0]!
     if cmd.name != (⟨"Simple", "block"⟩ : Strata.QualifiedIdent) then Lean.logError "Expected block command"; return
-    if let .seq _ stmts := cmd.args[0]! then
+    if let .seq _ _ stmts := cmd.args[0]! then
       if stmts.size != 4 then Lean.logError s!"Expected 4 statements, got {stmts.size}"
     else Lean.logError "Expected seq argument"
 
diff --git a/StrataTest/DDM/NonemptyAttribute.lean b/StrataTest/DDM/NonemptyAttribute.lean
new file mode 100644
index 000000000..ee176a85c
--- /dev/null
+++ b/StrataTest/DDM/NonemptyAttribute.lean
@@ -0,0 +1,124 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DDM.Integration.Lean
+
+/-!
+# Tests for @[nonempty] attribute on list constructs
+
+This file tests that the @[nonempty] attribute properly enforces non-empty lists
+for CommaSepBy, SpaceSepBy, and SpacePrefixSepBy constructs.
+-/
+
+#dialect
+dialect NonemptyTest;
+
+category Item;
+op item (n : Num) : Item => n;
+
+// Operations with @[nonempty] - require at least one element
+op comma1 (@[nonempty] items : CommaSepBy Item) : Command => "comma1(" items ")";
+op space1 (@[nonempty] items : SpaceSepBy Item) : Command => "space1(" items ")";
+op prefixed1 (@[nonempty] items : SpacePrefixSepBy Item) : Command => "prefixed1(" items ")";
+op seq1 (@[nonempty] items : Seq Item) : Command => "seq1(" items ")";
+
+// Operations without @[nonempty] - allow zero elements
+op comma0 (items : CommaSepBy Item) : Command => "comma0(" items ")";
+op space0 (items : SpaceSepBy Item) : Command => "space0(" items ")";
+op seq0 (items : Seq Item) : Command => "seq0(" items ")";
+
+#end
+
+namespace NonemptyTest
+
+#strata_gen NonemptyTest
+
+end NonemptyTest
+
+namespace NonemptyTest.Tests
+
+-- Test that @[nonempty] CommaSepBy accepts non-empty lists
+#guard_msgs in
+private def test_nonempty_comma_success := #strata
+program NonemptyTest;
+comma1(1, 2, 3)
+#end
+
+-- Test that @[nonempty] CommaSepBy rejects empty lists
+/-- error: expected expected at least one element -/
+#guard_msgs in
+private def test_nonempty_comma_empty := #strata
+program NonemptyTest;
+comma1()
+#end
+
+-- Test that @[nonempty] SpaceSepBy accepts non-empty lists
+#guard_msgs in
+private def test_nonempty_space_success := #strata
+program NonemptyTest;
+space1(1 2 3)
+#end
+
+-- Test that @[nonempty] SpaceSepBy rejects empty lists
+/-- error: expected expected at least one element -/
+#guard_msgs in
+private def test_nonempty_space_empty := #strata
+program NonemptyTest;
+space1()
+#end
+
+-- Test that @[nonempty] SpacePrefixSepBy accepts non-empty lists
+#guard_msgs in
+private def test_nonempty_prefixed_success := #strata
+program NonemptyTest;
+prefixed1(1 2 3)
+#end
+
+-- Test that @[nonempty] SpacePrefixSepBy rejects empty lists
+/-- error: expected expected at least one element -/
+#guard_msgs in
+private def test_nonempty_prefixed_empty := #strata
+program NonemptyTest;
+prefixed1()
+#end
+
+-- Test that regular (non-@[nonempty]) CommaSepBy allows empty lists
+#guard_msgs in
+private def test_maybe_empty_comma := #strata
+program NonemptyTest;
+comma0()
+#end
+
+-- Test that regular (non-@[nonempty]) SpaceSepBy allows empty lists
+#guard_msgs in
+private def test_maybe_empty_space := #strata
+program NonemptyTest;
+space0()
+#end
+
+end NonemptyTest.Tests
+
+-- Test that @[nonempty] Seq accepts non-empty lists
+#guard_msgs in
+private def test_nonempty_seq_success := #strata
+program NonemptyTest;
+seq1(1 2 3)
+#end
+
+-- Test that @[nonempty] Seq rejects empty lists
+/-- error: expected expected at least one element -/
+#guard_msgs in
+private def test_nonempty_seq_empty := #strata
+program NonemptyTest;
+seq1()
+#end
+
+-- Test that regular (non-@[nonempty]) Seq allows empty lists
+#guard_msgs in
+private def test_maybe_empty_seq := #strata
+program NonemptyTest;
+seq0()
+#end
diff --git a/StrataTest/Languages/B3/DDMFormatTests.lean b/StrataTest/Languages/B3/DDMFormatTests.lean
index 2f321f143..e28b39423 100644
--- a/StrataTest/Languages/B3/DDMFormatTests.lean
+++ b/StrataTest/Languages/B3/DDMFormatTests.lean
@@ -114,8 +114,7 @@ mutual
     | .strlit () s => .strlit default s
     | .bytes () v => .bytes default v
     | .option () ma => .option default (ma.map argFUnitToSourceRange)
-    | .seq () entries => .seq default (entries.map argFUnitToSourceRange)
-    | .commaSepList () entries => .commaSepList default (entries.map argFUnitToSourceRange)
+    | .seq () sep entries => .seq default sep (entries.map argFUnitToSourceRange)
 
   partial def typeExprFUnitToSourceRange : TypeExprF Unit → TypeExprF SourceRange
     | .ident () tp a => .ident default tp (a.map typeExprFUnitToSourceRange)
diff --git a/docs/verso/DDMDoc.lean b/docs/verso/DDMDoc.lean
index 02cf893e2..477cf933c 100644
--- a/docs/verso/DDMDoc.lean
+++ b/docs/verso/DDMDoc.lean
@@ -373,6 +373,8 @@ metadata scope(name : Ident);
 metadata declare(name : Ident, type : TypeOrCat);
 -- Declares a new variable in the resulting scope with metadata determined
 -- by an argument.
+-- Marks a list argument as requiring at least one element
+metadata nonempty;
 ```
 
 As an example, Boogie variable declaration syntax can be defined in Strata using the
@@ -417,9 +419,20 @@ be defined in user definable dialects.
     `c` may be read in or the empty string.
 
   * `Init.Seq c` denotes a sequence of values with category `c`.  Each value of `c` is
-    separated by whitespace.
+    separated by whitespace. When formatted, values are concatenated with no separator.
 
-  * `Init.CommaSepBy c` denotes a comma-separated list of values of type `c`.
+  * `Init.CommaSepBy c` denotes a comma-separated list of values of type `c`. When formatted,
+    values are separated by `, ` (comma followed by space).
+
+  * `Init.SpaceSepBy c` denotes a space-separated list of values of type `c`. Parsing is
+    identical to `Init.Seq`, but when formatted, values are separated by a single space.
+
+  * `Init.SpacePrefixSepBy c` denotes a space-prefix-separated list of values of type `c`.
+    Parsing is identical to `Init.Seq`, but when formatted, each value is prefixed with a space.
+
+  All list categories (`CommaSepBy`, `SpaceSepBy`, `SpacePrefixSepBy`, `Seq`) can be marked
+  with the `@[nonempty]` metadata attribute to require at least one element during parsing.
+  For example: `@[nonempty] items : SpaceSepBy Item` will reject empty lists with a parse error.
 
 * Parsing for primitive literals and identifiers cannot be directly in syntax definitions.
   To accomodate this, the `Init` dialect introduces the syntactic categories for this: