diff --git a/mx-rust-semantics/main/expression/rust-to-mx.md b/mx-rust-semantics/main/expression/rust-to-mx.md
index 755f511..c16264e 100644
--- a/mx-rust-semantics/main/expression/rust-to-mx.md
+++ b/mx-rust-semantics/main/expression/rust-to-mx.md
@@ -8,6 +8,7 @@ module MX-RUST-EXPRESSION-RUST-TO-MX
imports private MX-COMMON-SYNTAX
imports private MX-RUST-REPRESENTATION-CONVERSIONS
imports private RUST-EXECUTION-CONFIGURATION
+ imports private RUST-REPRESENTATION
rule V:MxValue ~> rustToMx => rustToMx(V)
@@ -38,6 +39,9 @@ module MX-RUST-EXPRESSION-RUST-TO-MX
rule concat(V:Value, L:ValueList) => V , L
rule concat(_:Value, E:SemanticsError) => E
rule concat(E:SemanticsError, _:ValueListOrError) => E
+ rule concat(E:ValueOrError, L:ValueListOrError)
+ => error("unexpected branch (concat(ValueOrError, ValueListOrError))", ListItem(E) ListItem(L))
+ [owise]
syntax ValueListOrError ::= ptrListToValueList(PtrListOrError, Map) [function, total]
rule ptrListToValueList(E:SemanticsError, _:Map) => E
diff --git a/rust-semantics/execution/let.md b/rust-semantics/execution/let.md
index 872e46b..50bca4e 100644
--- a/rust-semantics/execution/let.md
+++ b/rust-semantics/execution/let.md
@@ -1,11 +1,12 @@
```k
module RUST-LET
- imports COMMON-K-CELL
- imports RUST-CASTS
- imports RUST-EXECUTION-CONFIGURATION
- imports RUST-VALUE-SYNTAX
- imports RUST-SHARED-SYNTAX
+ imports private COMMON-K-CELL
+ imports private RUST-CASTS
+ imports private RUST-EXECUTION-CONFIGURATION
+ imports private RUST-REPRESENTATION
+ imports private RUST-SHARED-SYNTAX
+ imports private RUST-VALUE-SYNTAX
// Not all cases are implemented
rule
diff --git a/rust-semantics/expression/assignments.md b/rust-semantics/expression/assignments.md
index a88f0b4..19196b8 100644
--- a/rust-semantics/expression/assignments.md
+++ b/rust-semantics/expression/assignments.md
@@ -9,7 +9,7 @@ module RUST-EXPRESSION-ASSIGNMENTS
rule
ptrValue(ptr(P:Int), _) = ptrValue(_, V:Value)
- => ptrValue(null, ())
+ => ptrValue(null, tuple(.ValueList))
...
diff --git a/rust-semantics/expression/constants.md b/rust-semantics/expression/constants.md
index 11a3187..cec9339 100644
--- a/rust-semantics/expression/constants.md
+++ b/rust-semantics/expression/constants.md
@@ -6,7 +6,7 @@ module RUST-EXPRESSION-CONSTANTS
imports private RUST-REPRESENTATION
imports private RUST-PREPROCESSING-CONFIGURATION
- rule Name:Identifier::.PathExprSegments => ptrValue(null, V) ...
+ rule Name:Identifier => ptrValue(null, V) ...
Name
V:Value
requires notBool isLocalVariable(Name)