diff --git a/effekt/shared/src/main/scala/effekt/Parser.scala b/effekt/shared/src/main/scala/effekt/Parser.scala
index 053943b4a..f5b1f7c75 100644
--- a/effekt/shared/src/main/scala/effekt/Parser.scala
+++ b/effekt/shared/src/main/scala/effekt/Parser.scala
@@ -270,40 +270,92 @@ class Parser(tokens: Seq[Token], source: Source) {
           else ExprStmt(e, stmts(inBraces), span())
       }) labelled "statements"
 
-  // ATTENTION: here the grammar changed (we added `with val` to disambiguate)
-  // with val <ID> (: <TYPE>)? = <EXPR>; <STMTS>
-  // with val (<ID> (: <TYPE>)?...) = <EXPR>
+  // with val <PATTERN> (, <PATTERN>)* = <EXPR>; <STMTS>
+  // with def <BLOCKPARAM> = <EXPR>; <STMTS>
   // with <EXPR>; <STMTS>
   def withStmt(inBraces: Boolean): Stmt = `with` ~> peek.kind match {
     case `val` =>
-      val params = (`val` ~> peek.kind match {
-        case `(` => valueParamsOpt()
-        case _ => List(valueParamOpt()) // TODO copy position
-      })
-      desugarWith(params, Nil, `=` ~> expr(), semi() ~> stmts(inBraces), span())
+      consume(`val`)
+      val patterns = some(matchPattern, `,`)
+      val call = `=` ~> expr()
+      val body = semi() ~> stmts(inBraces)
+      desugarWithPatterns(patterns, call, body, span())
 
     case `def` =>
       val params = (`def` ~> peek.kind match {
         case `{` => blockParamsOpt()
         case _ => List(blockParamOpt()) // TODO copy position
       })
-      desugarWith(Nil, params, `=` ~> expr(), semi() ~> stmts(inBraces), span())
+      val call = `=` ~> expr()
+      val body = semi() ~> stmts(inBraces)
+      val blockLit: BlockLiteral = BlockLiteral(Nil, Nil, params, body, body.span.synthesized)
+      desugarWith(call, blockLit, span())
+
+    case _ =>
+      val call = expr()
+      val body = semi() ~> stmts(inBraces)
+      val blockLit: BlockLiteral = BlockLiteral(Nil, Nil, Nil, body, body.span.synthesized)
+      desugarWith(call, blockLit, span())
+  }
+
+  // Desugar `with val` with pattern(s)
+  def desugarWithPatterns(patterns: Many[MatchPattern], call: Term, body: Stmt, withSpan: Span): Stmt = {
+    // Check if all patterns are simple variable bindings or ignored
+    val allSimpleVars = patterns.unspan.forall {
+      case AnyPattern(_, _) => true
+      case IgnorePattern(_) => true
+      case _ => false
+    }
+
+    val blockLit: BlockLiteral = if (allSimpleVars) {
+      // Simple case: all patterns are just variable names (or ignored)
+      // Desugar to: call { (x, y, _, ...) => body }
+      val vparams: List[ValueParam] = patterns.unspan.map {
+        case AnyPattern(id, span) => ValueParam(id, None, span)
+        case IgnorePattern(span) => ValueParam(IdDef(s"__ignored", span.synthesized), None, span)
+        case _ => sys.error("impossible: checked above")
+      }
+      BlockLiteral(Nil, vparams, Nil, body, body.span.synthesized)
+    } else {
+      // Complex case: at least one pattern needs matching
+      // Desugar to: call { case pat1, pat2, ...  => body }
+      // This requires one argument per pattern, matching against multiple scrutinees
+      val patternList = patterns.unspan
+      val names = List.tabulate(patternList.length) { n => s"__withArg${n}" }
+      val argSpans = patternList.map(_.span)
+
+      val vparams: List[ValueParam] = names.zip(argSpans).map { (name, span) =>
+        ValueParam(IdDef(name, span.synthesized), None, span.synthesized)
+      }
+      val scrutinees = names.zip(argSpans).map { (name, span) =>
+        Var(IdRef(Nil, name, span.synthesized), span.synthesized)
+      }
+
+      val pattern: MatchPattern = patterns match {
+        case Many(List(single), _) => single
+        case Many(ps, span) => MultiPattern(ps, span)
+      }
+
+      val clause = MatchClause(pattern, Nil, body, Span(source, pattern.span.from, body.span.to, Synthesized))
+      val matchExpr = Match(scrutinees, List(clause), None, withSpan.synthesized)
+      val matchBody = Return(matchExpr, withSpan.synthesized)
+      BlockLiteral(Nil, vparams, Nil, matchBody, withSpan.synthesized)
+    }
 
-    case _ => desugarWith(Nil, Nil, expr(), semi() ~> stmts(inBraces), span())
+    desugarWith(call, blockLit, withSpan)
   }
 
-  def desugarWith(vparams: List[ValueParam], bparams: List[BlockParam], call: Term, body: Stmt, withSpan: Span): Stmt = call match {
-     case m@MethodCall(receiver, id, tps, vargs, bargs, callSpan) =>
-       Return(MethodCall(receiver, id, tps, vargs, bargs :+ (BlockLiteral(Nil, vparams, bparams, body, body.span.synthesized)), callSpan), withSpan.synthesized)
-     case c@Call(callee, tps, vargs, bargs, callSpan) =>
-       Return(Call(callee, tps, vargs, bargs :+ (BlockLiteral(Nil, vparams, bparams, body, body.span.synthesized)), callSpan), withSpan.synthesized)
-     case Var(id, varSpan) =>
-       val tgt = IdTarget(id)
-       Return(Call(tgt, Nil, Nil, (BlockLiteral(Nil, vparams, bparams, body, body.span.synthesized)) :: Nil, varSpan), withSpan.synthesized)
-     case Do(id, targs, vargs, bargs, doSpan) =>
-      Return(Do(id, targs, vargs, bargs :+ BlockLiteral(Nil, vparams, bparams, body, body.span.synthesized), doSpan), withSpan.synthesized)
-     case term =>
-       Return(Call(ExprTarget(term), Nil, Nil, (BlockLiteral(Nil, vparams, bparams, body, body.span.synthesized)) :: Nil, term.span.synthesized), withSpan.synthesized)
+  def desugarWith(call: Term, blockLit: BlockLiteral, withSpan: Span): Stmt = call match {
+    case MethodCall(receiver, id, tps, vargs, bargs, callSpan) =>
+      Return(MethodCall(receiver, id, tps, vargs, bargs :+ blockLit, callSpan), withSpan.synthesized)
+    case Call(callee, tps, vargs, bargs, callSpan) =>
+      Return(Call(callee, tps, vargs, bargs :+ blockLit, callSpan), withSpan.synthesized)
+    case Var(id, varSpan) =>
+      Return(Call(IdTarget(id), Nil, Nil, blockLit :: Nil, varSpan), withSpan.synthesized)
+    case Do(id, targs, vargs, bargs, doSpan) =>
+      Return(Do(id, targs, vargs, bargs :+ blockLit, doSpan), withSpan.synthesized)
+    case term =>
+      Return(Call(ExprTarget(term), Nil, Nil, blockLit :: Nil, term.span.synthesized), withSpan.synthesized)
   }
 
   def maybeSemi(): Unit = if isSemi then semi()
diff --git a/effekt/shared/src/main/scala/effekt/source/Tree.scala b/effekt/shared/src/main/scala/effekt/source/Tree.scala
index 1d637e778..0682e5010 100644
--- a/effekt/shared/src/main/scala/effekt/source/Tree.scala
+++ b/effekt/shared/src/main/scala/effekt/source/Tree.scala
@@ -678,7 +678,7 @@ enum MatchPattern extends Tree {
    *
    *   case a, b => ...
    *
-   * Currently should *only* occur in lambda-cases during Parsing
+   * Currently should *only* occur in lambda-cases & `with` statements during parsing
    */
   case MultiPattern(patterns: List[MatchPattern], span: Span) extends MatchPattern
 }
diff --git a/examples/pos/with_val_many_args.check b/examples/pos/with_val_many_args.check
new file mode 100644
index 000000000..c401a39fc
--- /dev/null
+++ b/examples/pos/with_val_many_args.check
@@ -0,0 +1 @@
+42, 100; a
\ No newline at end of file
diff --git a/examples/pos/with_val_many_args.effekt b/examples/pos/with_val_many_args.effekt
new file mode 100644
index 000000000..0c506782b
--- /dev/null
+++ b/examples/pos/with_val_many_args.effekt
@@ -0,0 +1,9 @@
+module with_val_many_args
+
+def callback { f: (Int, Int, String, Char) => Unit }: Unit =
+  f(42, 100, "hello", 'a')
+
+def main() = {
+  with val i, j, _, c = callback;
+  println(show(i) ++ ", " ++ show(j) ++ "; " ++ show(c))
+}
\ No newline at end of file
diff --git a/examples/pos/with_val_many_ignored_args.check b/examples/pos/with_val_many_ignored_args.check
new file mode 100644
index 000000000..c59ed4d66
--- /dev/null
+++ b/examples/pos/with_val_many_ignored_args.check
@@ -0,0 +1,4 @@
+before
+called!
+called!
+after
\ No newline at end of file
diff --git a/examples/pos/with_val_many_ignored_args.effekt b/examples/pos/with_val_many_ignored_args.effekt
new file mode 100644
index 000000000..a82e058f8
--- /dev/null
+++ b/examples/pos/with_val_many_ignored_args.effekt
@@ -0,0 +1,13 @@
+module with_val_many_ignored_args
+
+def callback { f: (Int, Int, String, Char) => Unit }: Unit = {
+  println("before")
+  f(42, 100, "hello", 'a')
+  f(0, 0, "", '0')
+  println("after")
+}
+
+def main() = {
+  with val _, _, _, _ = callback;
+  println("called!")
+}
\ No newline at end of file
diff --git a/examples/pos/with_val_pair.check b/examples/pos/with_val_pair.check
new file mode 100644
index 000000000..6220905b8
--- /dev/null
+++ b/examples/pos/with_val_pair.check
@@ -0,0 +1,4 @@
+0: a
+1: b
+2: c
+3: d
\ No newline at end of file
diff --git a/examples/pos/with_val_pair.effekt b/examples/pos/with_val_pair.effekt
new file mode 100644
index 000000000..118e649b4
--- /dev/null
+++ b/examples/pos/with_val_pair.effekt
@@ -0,0 +1,6 @@
+module with_val_pair
+
+def main() = {
+  with val (i, x) = [(0, 'a'), (1, 'b'), (2, 'c'), (3, 'd')].foreach;
+  println(show(i) ++ ": " ++ show(x))
+}
\ No newline at end of file
diff --git a/examples/pos/with_val_pair_complex.check b/examples/pos/with_val_pair_complex.check
new file mode 100644
index 000000000..850b9934c
--- /dev/null
+++ b/examples/pos/with_val_pair_complex.check
@@ -0,0 +1,3 @@
+1=1: a
+2=2: b
+3=3: c
\ No newline at end of file
diff --git a/examples/pos/with_val_pair_complex.effekt b/examples/pos/with_val_pair_complex.effekt
new file mode 100644
index 000000000..030cefe1d
--- /dev/null
+++ b/examples/pos/with_val_pair_complex.effekt
@@ -0,0 +1,7 @@
+module with_val_pair_complex
+
+record Pos(i: Int, x: Char)
+def main() = {
+  with val (i, Pos(j, x)) = [(1, Pos(1, 'a')), (2, Pos(2, 'b')), (3, Pos(3, 'c'))].foreach;
+  println(show(i) ++ "=" ++ show(j) ++ ": " ++ show(x))
+}
\ No newline at end of file
diff --git a/examples/pos/with_val_pair_explicit.check b/examples/pos/with_val_pair_explicit.check
new file mode 100644
index 000000000..6220905b8
--- /dev/null
+++ b/examples/pos/with_val_pair_explicit.check
@@ -0,0 +1,4 @@
+0: a
+1: b
+2: c
+3: d
\ No newline at end of file
diff --git a/examples/pos/with_val_pair_explicit.effekt b/examples/pos/with_val_pair_explicit.effekt
new file mode 100644
index 000000000..f26856299
--- /dev/null
+++ b/examples/pos/with_val_pair_explicit.effekt
@@ -0,0 +1,6 @@
+module with_val_pair_explicit
+
+def main() = {
+  with val Tuple2(i, x) = [(0, 'a'), (1, 'b'), (2, 'c'), (3, 'd')].foreach;
+  println(show(i) ++ ": " ++ show(x))
+}
\ No newline at end of file
diff --git a/examples/pos/with_val_two_args.check b/examples/pos/with_val_two_args.check
new file mode 100644
index 000000000..6220905b8
--- /dev/null
+++ b/examples/pos/with_val_two_args.check
@@ -0,0 +1,4 @@
+0: a
+1: b
+2: c
+3: d
\ No newline at end of file
diff --git a/examples/pos/with_val_two_args.effekt b/examples/pos/with_val_two_args.effekt
new file mode 100644
index 000000000..cda674a37
--- /dev/null
+++ b/examples/pos/with_val_two_args.effekt
@@ -0,0 +1,6 @@
+module with_val_two_args
+
+def main() = {
+  with val i, x = ['a', 'b', 'c', 'd'].foreachIndex;
+  println(show(i) ++ ": " ++ show(x))
+}
\ No newline at end of file
diff --git a/examples/pos/with_val_two_args_complex.check b/examples/pos/with_val_two_args_complex.check
new file mode 100644
index 000000000..a00684ff8
--- /dev/null
+++ b/examples/pos/with_val_two_args_complex.check
@@ -0,0 +1,3 @@
+0: a
+1: b
+2: c
\ No newline at end of file
diff --git a/examples/pos/with_val_two_args_complex.effekt b/examples/pos/with_val_two_args_complex.effekt
new file mode 100644
index 000000000..0128f71b1
--- /dev/null
+++ b/examples/pos/with_val_two_args_complex.effekt
@@ -0,0 +1,7 @@
+module with_val_two_args_complex
+
+record Pos(i: Int, x: Char)
+def main() = {
+  with val i, Pos(j, x) = [Pos(1, 'a'), Pos(2, 'b'), Pos(3, 'c')].foreachIndex;
+  println(show(i) ++ ": " ++ show(x))
+}
\ No newline at end of file
diff --git a/examples/pos/withdefstatement.effekt b/examples/pos/withdefstatement.effekt
index ebf580572..e92ec520b 100644
--- a/examples/pos/withdefstatement.effekt
+++ b/examples/pos/withdefstatement.effekt
@@ -15,7 +15,7 @@ def fresh[T](init: Int) { prog: {Cell} => T }: T = {
 }
 
 def main() = {
-  with def target = fresh(0)
+  with def {target} = fresh(0)
   with def c1 = fresh(0)
   with def c2 = fresh(0)
   c1.set(1);
diff --git a/examples/pos/withstatement.effekt b/examples/pos/withstatement.effekt
index bf164cd6d..bf3c7f5e8 100644
--- a/examples/pos/withstatement.effekt
+++ b/examples/pos/withstatement.effekt
@@ -11,8 +11,8 @@ def bar { f: (Int, String) => Unit / {}}: Unit =
 
 def user(): Unit = {
     with printer;
-    with val x: Int = foreach([1,2,3]);
-    with val (a, b) = bar;
+    with val x = foreach([1,2,3]);
+    with val a, b = bar;
     println(show(x) ++ b);
     val z = {
         val x = 2;