diff --git a/semantics/c/language/translation/typing/canonicalization.k b/semantics/c/language/translation/typing/canonicalization.k
index 9c4d93539..4cf4b115a 100644
--- a/semantics/c/language/translation/typing/canonicalization.k
+++ b/semantics/c/language/translation/typing/canonicalization.k
@@ -87,7 +87,7 @@ module C-TYPING-CANONICALIZATION
           requires cfg:reservedKeywordSupported(Tok)
           [structural]
      rule (.K => SE("TCANON2","Unsupported reserved identifier "+String Tok +String " (reserved variant of restrict)."))
-          ~> addMods(Mods::List ListItem(RestrictReserved(Tok::String, Loc::CabsLoc)), T:Type)
+          ~> addMods(_Mods::List ListItem(RestrictReserved(Tok::String, _::CabsLoc)), _:Type)
           requires notBool cfg:reservedKeywordSupported(Tok)
           [structural]
      rule addMods(Mods::List ListItem(Restrict()), T:Type)
@@ -123,7 +123,7 @@ module C-TYPING-CANONICALIZATION
      context addMods(_ ListItem(AlignasExpression(HOLE:KItem)), _)
      rule addMods(_::List ListItem(AlignasExpression(tv(A:Int, _)) => alignas(A)), _)
           [structural]
-     rule addMods(Mods::List (ListItem(S:KItem) => .List), _:KResult)
+     rule addMods(_Mods::List (ListItem(S:KItem) => .List), _:KResult)
           requires notBool isModifier(S)
                andBool notBool isQualifier(S)
                andBool notBool isReducibleModifier(S)
diff --git a/semantics/c/language/translation/typing/expr.k b/semantics/c/language/translation/typing/expr.k
index fcbba4361..cac38a381 100644
--- a/semantics/c/language/translation/typing/expr.k
+++ b/semantics/c/language/translation/typing/expr.k
@@ -120,7 +120,7 @@ module C-TYPING-EXPR
      rule typeof(+ T:Type => tryPromote(T))
      rule typeof(- T:Type => tryPromote(T))
      rule typeof(~ T:Type => tryPromote(T:Type))
-     rule typeof(! T:Type => type(int))
+     rule typeof(! _:Type => type(int))
 
      rule typeof(SizeofExpression(T:Type) => SizeofType(T, .K))
      rule typeof(SizeofType(T:Type, _)
@@ -257,10 +257,10 @@ module C-TYPING-EXPR
           requires stripQualifiers(T) ==Type stripQualifiers(T')
                andBool SizeofExpression(...) :/=K K
 
-     rule elaborateDone(V:K, V':K) ~> typeof(_ ? t(...) : (t(...) #as T'::Type))
+     rule elaborateDone(V:K, _V':K) ~> typeof(_ ? t(...) : (t(...) #as T'::Type))
           => typeof(stripQualifiers(T'))
           requires isNPC(V) andBool isPointerType(T')
-     rule elaborateDone(V:K, V':K) ~> typeof(_ ? (t(...) #as T::Type) : t(...))
+     rule elaborateDone(_V:K, V':K) ~> typeof(_ ? (t(...) #as T::Type) : t(...))
           => typeof(stripQualifiers(T))
           requires isNPC(V') andBool isPointerType(T)
 
diff --git a/semantics/c/language/translation/typing/interpretation.k b/semantics/c/language/translation/typing/interpretation.k
index 2effa0e8d..1274b21b1 100644
--- a/semantics/c/language/translation/typing/interpretation.k
+++ b/semantics/c/language/translation/typing/interpretation.k
@@ -75,7 +75,7 @@ module C-TYPING-INTERPRETATION
           ~> ArrayType(_, tv(_:Float, _), _)
           [structural]
      rule (.K => CV("CTI2", "Arrays must have positive length."))
-          ~> ArrayType(T:Type, tv(Len:Int, _), _)
+          ~> ArrayType(_:Type, tv(Len:Int, _), _)
           requires Len <=Int 0
           [structural]
      rule (.K => CV("CTI5", "Structs containing a flexible array member must not be array elements."))
diff --git a/semantics/common/bits.k b/semantics/common/bits.k
index 3116640f0..e0533636d 100644
--- a/semantics/common/bits.k
+++ b/semantics/common/bits.k
@@ -84,11 +84,11 @@ module BITS
           [owise]
 
      syntax Bool ::= piecesJoinable(Bits, Bits) [function]
-     rule piecesJoinable(piece(N:Int, _), piece(N':Int, _)) => true
-     rule piecesJoinable(piece(unknown(N:Int), _), piece(unknown(N':Int), _)) => true
+     rule piecesJoinable(piece(_N:Int, _), piece(_N':Int, _)) => true
+     rule piecesJoinable(piece(unknown(_N:Int), _), piece(unknown(_N':Int), _)) => true
      rule piecesJoinable(piece(trap, _), piece(trap, _)) => true
-     rule piecesJoinable(piece(encodedPtr(N::PtrValue, From::Int, To::Int), _), piece(encodedPtr(N, To, _), _)) => true
-     rule piecesJoinable(piece(encodedValue(N::EncodableValue, From::Int, To::Int), _), piece(encodedValue(N, To, _), _)) => true
+     rule piecesJoinable(piece(encodedPtr(N::PtrValue, _From::Int, To::Int), _), piece(encodedPtr(N, To, _), _)) => true
+     rule piecesJoinable(piece(encodedValue(N::EncodableValue, _From::Int, To::Int), _), piece(encodedValue(N, To, _), _)) => true
      rule piecesJoinable(_, _) => false [owise]
 
      syntax Bits ::= joinPieces(Bits, Bits) [function]
diff --git a/semantics/common/compat.k b/semantics/common/compat.k
index 792c58016..2b2b9773e 100644
--- a/semantics/common/compat.k
+++ b/semantics/common/compat.k
@@ -86,7 +86,7 @@ module COMPAT-KAST [kast]
      imports BOOL
      imports K-EQUAL
 
-     rule some(.Map::Map, Lbl:K) => false
+     rule some(.Map::Map, _Lbl:K) => false
      rule some(K1:KItem |-> K2:KItem M::Map, #klabel(Lbl:KLabel)) => Lbl(K1, K2) orBool some(M, #klabel(Lbl)) [owise]
 
      rule mapList(ListItem(K:KItem) L:List, #klabel(Lbl:KLabel)) => ListItem(Lbl(K)) mapList(L, #klabel(Lbl))
diff --git a/semantics/common/symloc.k b/semantics/common/symloc.k
index cf00892c9..e08df4625 100644
--- a/semantics/common/symloc.k
+++ b/semantics/common/symloc.k
@@ -288,7 +288,7 @@ module SYMLOC
      rule stripFromArray(Loc:SymLoc) => Loc [owise]
 
      rule getFromArray(loc(_, _, SetItem(fromArray(...) #as F::Provenance) _)) => F
-     rule getFromArray(Loc::SymLoc) => .K [owise]
+     rule getFromArray(_::SymLoc) => .K [owise]
 
      rule stripProv(loc(Base:SymBase, Offset:Int, _)) => loc(Base, Offset)
      rule stripProv(loc(Base:SymBase, Offset:Int)) => loc(Base, Offset)
diff --git a/semantics/cpp/language/translation/decl/class.k b/semantics/cpp/language/translation/decl/class.k
index ebfec3a82..fabd72eaa 100644
--- a/semantics/cpp/language/translation/decl/class.k
+++ b/semantics/cpp/language/translation/decl/class.k
@@ -1196,7 +1196,7 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)]
             <class-id> C </class-id>
             <class-type> Key::ClassKey </class-type>
             <cenv> CE::Map => CE[X, T <- classOffset(NaOffset, Offset)] </cenv>
-            <dsize> V::Int => Offset +Int #if isBaseClass(X) #then nvSizeof(T) #else bitSizeofType(T) #fi </dsize>
+            <dsize> _::Int => Offset +Int #if isBaseClass(X) #then nvSizeof(T) #else bitSizeofType(T) #fi </dsize>
             <align> M::Int => maxInt(M, #if isBaseClass(X) #then nvAlignof(T) #else byteAlignofType(T) #fi) </align>
             <sizeof> V2::Int => maxInt(V2, Offset +Int #if isBaseClass(X) #then nvSizeof(T) #else bitSizeofType(T) #fi) </sizeof>
           ...</class>
@@ -1271,11 +1271,11 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)]
      rule getTypesAtOffsetForLayout(t(... st: classType(_ :: Class(Union(), _, _))) #as T::CPPType, 0)
           => SetItem(utype(T)) getTypesAtOffsetForLayoutInUnion(T, getClassInfo(T), 0)
 
-     rule getTypesAtOffsetForLayout(t(... st: arrayType(InnerT::CPPType, _)) #as T::CPPType, Offset::Int)
+     rule getTypesAtOffsetForLayout(t(... st: arrayType(InnerT::CPPType, _)) #as _::CPPType, Offset::Int)
           => getTypesAtOffsetForLayout(InnerT, Offset %Int bitSizeofType(InnerT))
           requires Offset >Int 0
 
-     rule getTypesAtOffsetForLayout(t(... st: incompleteArrayType(InnerT::CPPType)) #as T::CPPType, Offset::Int)
+     rule getTypesAtOffsetForLayout(t(... st: incompleteArrayType(InnerT::CPPType)) #as _::CPPType, Offset::Int)
           => getTypesAtOffsetForLayout(InnerT, Offset %Int bitSizeofType(InnerT))
           requires Offset >Int 0
 
@@ -1305,9 +1305,9 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)]
      rule getTypesAtOffsetForLayoutInStruct(_, <class>...
                <non-static-data-members>... ListItem(Class.DataMember(X::CId, T::CPPType)) => .List </non-static-data-members>
                <cenv>... X |-> (_::Map stripType(T) |-> (_, uninitialized)) ...</cenv>
-          ...</class>, Offset::Int)
+          ...</class>, _Offset::Int)
 
-     rule getTypesAtOffsetForLayoutInStruct(T::CPPType, <class>...
+     rule getTypesAtOffsetForLayoutInStruct(_::CPPType, <class>...
                <non-static-data-members>... ListItem(Class.DataMember(X::CId, T'::CPPType)) </non-static-data-members>
                <cenv>... X |-> (_::Map stripType(T') |-> (_, classOffset(_, FOffset::Int))) ...</cenv>
           ...</class>, Offset::Int)
@@ -1318,18 +1318,18 @@ syntax Stmt ::= Defaulted(SpecialMemberFunction, Class) [klabel(DefaultedSMF)]
                <base-classes>... ListItem(C:Class) => ListItem(type(classType(C))) </base-classes>
           ...</class>, _)
 
-     rule getTypesAtOffsetForLayoutInStruct(T::CPPType, <class>...
+     rule getTypesAtOffsetForLayoutInStruct(_::CPPType, <class>...
                <base-classes>... ListItem(t(... st: classType(C::Class)) #as T'::CPPType) => .List </base-classes>
                <non-static-data-members> .List </non-static-data-members>
                <cenv>... baseClass(C) |-> (_::Map stripType(T') |-> (_, classOffset(_, FOffset::Int))) ...</cenv>
           ...</class>, Offset::Int)
           requires FOffset >Int Offset
 
-     rule getTypesAtOffsetForLayoutInStruct(T::CPPType, <class>...
+     rule getTypesAtOffsetForLayoutInStruct(_::CPPType, <class>...
                <base-classes>... ListItem(t(... st: classType(C::Class)) #as T'::CPPType) => .List </base-classes>
                <non-static-data-members> .List </non-static-data-members>
                <cenv>... baseClass(C) |-> (_::Map stripType(T') |-> (_, uninitialized)) ...</cenv>
-          ...</class>, Offset::Int)
+          ...</class>, _Offset::Int)
 
      rule getTypesAtOffsetForLayoutInStruct(T::CPPType, <class>...
                <base-classes>... ListItem(t(... st: classType(C::Class)) #as T'::CPPType) </base-classes>
diff --git a/semantics/cpp/language/translation/decl/declarator.k b/semantics/cpp/language/translation/decl/declarator.k
index 6cbc1c2f6..f4d4389d5 100644
--- a/semantics/cpp/language/translation/decl/declarator.k
+++ b/semantics/cpp/language/translation/decl/declarator.k
@@ -124,7 +124,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      rule getPreviousLinkage(_, _, _, _) => .K [owise]
 
      // @ref n4296 3.5:3.1
-     rule getLinkage(S::Set, _, _:NamespaceScope, Q::Quals, _, _) => InternalLinkage
+     rule getLinkage(S::Set, _, _:NamespaceScope, _::Quals, _, _) => InternalLinkage
           requires Static() in S
 
      // @ref n4296 3.5:3.2
@@ -140,7 +140,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
           requires Static() in S
             orBool isFunctionDeclarationType(Type)
 
-     rule getLinkage(_, C:Class, _, _, L:Linkage, _) => L
+     rule getLinkage(_, _:Class, _, _, L:Linkage, _) => L
 
      // @ref n4296 3.5:4
      rule getClassLinkage(Parent:Namespace :: _) => getNamespaceLinkage(Parent)
@@ -151,7 +151,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      rule getClassLinkage(_:LocalQualifier :: _) => NoLinkage
 
      // @ref n4296 3.5:4
-     rule getNamespaceLinkage(N:UnnamedNamespace) => InternalLinkage
+     rule getNamespaceLinkage(_:UnnamedNamespace) => InternalLinkage
 
      rule getNamespaceLinkage(GlobalNamespace()) => ExternalLinkage
 
@@ -173,7 +173,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
      rule getDuration(S::Set, _) => ThreadStorage
           requires ThreadLocal() in S
 
-     rule getDuration(S::Set, Scope:BlockScope) => AutoStorage
+     rule getDuration(S::Set, _:BlockScope) => AutoStorage
           requires notBool Static() in S andBool notBool Extern() in S
 
      rule getDuration(_, _) => StaticStorage [owise]
@@ -199,9 +199,9 @@ module CPP-TRANSLATION-DECL-DECLARATOR
 
      syntax CId ::= getCName(CPPType, CId, CId, LanguageLinkage, Set) [function]
 
-     rule getCName(T::CPPType, X::CId, _, CLinkage, _) => X
+     rule getCName(_::CPPType, X::CId, _, CLinkage, _) => X
 
-     rule getCName(t(... st: functionType(...)) #as T::CPPType, X::CId, Mangled::CId, LangLinkage::LanguageLinkage, Opts::Set) => Mangled
+     rule getCName(t(... st: functionType(...)) #as _::CPPType, X::CId, Mangled::CId, LangLinkage::LanguageLinkage, Opts::Set) => Mangled
           requires (LangLinkage =/=K CLinkage) andBool (X =/=K Mangled)
                andBool notBool (NoNativeFallback() in Opts)
 
@@ -277,10 +277,10 @@ module CPP-TRANSLATION-DECL-DECLARATOR
                    ~> lazyDefineObject(N, X, CName, T, Init, Type, S, Base)
 
           // ExternalLinkage, StaticStorage, redeclare incomplete array
-          rule <k> declareObjectWithLinkage(N::Namespace, LN::Namespace, X::CId, t(... st: _:CPPSimpleArrayType) #as T::CPPType, Init::Init, Type::DeclarationType, StaticStorage, S::Set, _, ExternalLinkage) ...</k>
+          rule <k> declareObjectWithLinkage(_::Namespace, LN::Namespace, X::CId, t(... st: _:CPPSimpleArrayType) #as T::CPPType, _::Init, _::DeclarationType, StaticStorage, _::Set, _, ExternalLinkage) ...</k>
                <curr-tr-tu> Tu::String </curr-tr-tu>
                <tu-id> Tu </tu-id>
-               <externals>... LN :: X |-> ((_::CPPType => stripType(T)) |-> (T'::CPPType => T, declState(Base::SymBase, _))) ...</externals>
+               <externals>... LN :: X |-> ((_::CPPType => stripType(T)) |-> (T'::CPPType => T, declState(_::SymBase, _))) ...</externals>
                requires isCPPArrayType(T') andBool notBool isCompleteType(T') andBool innerType(T) ==Type innerType(T') andBool getQuals(T) ==K getQuals(T')
 
           // ExternalLinkage, StaticStorage, redeclare complete type
@@ -417,7 +417,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
 
      syntax CPPType ::= completeDeclaration(CPPType, Init) [function]
 
-     rule completeDeclaration(T::CPPType, (ExprLoc(_, I:Init) => I))
+     rule completeDeclaration(_::CPPType, (ExprLoc(_, I:Init) => I))
 
      // @ref n4296 8.5.4:3.2 (char x[] = {"foo"})
      rule completeDeclaration(t(Q::Quals, Mods::Set, incompleteArrayType(t(Q'::Quals, Mods'::Set, T:CPPSimpleCharType))), BraceInit(ListItem(StringLiteral(Narrow::CharKind, S::String)))) => t(Q, Mods, arrayType(t(Q', Mods', T), lengthString(S) +Int 1))
@@ -478,7 +478,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
 
      syntax Decl ::= lazyDefineObject(NNSVal, CId, CId, CPPType, Init, DeclarationType, Set, SymBase)
 
-     rule lazyDefineObject(N::NNSVal, X::CId, CName::CId, T::CPPType, Init::Init, Type::DeclarationType, S::Set, Base::SymBase)
+     rule lazyDefineObject(N::NNSVal, X::CId, CName::CId, T::CPPType, Init::Init, Type::DeclarationType, S::Set, _::SymBase)
           => defineObject(N, X, CName, T, Init, Type, S)
           requires notBool isInitOnlyIfOdrUsed(Init)
 
@@ -492,8 +492,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
                     scope(namespaceScope(GlobalNamespace()), clearScope() ~> defineObject(N, X, CName, T, Init, Type, S))
                  )
           ...</k>
-          <curr-tr-scope> Sc::Scope </curr-tr-scope>
-
+          <curr-tr-scope> _::Scope </curr-tr-scope>
 
      rule defineObject(_, _, _, _, NoInit(), Function(_), _) => .K
 
@@ -539,7 +538,7 @@ module CPP-TRANSLATION-DECL-DECLARATOR
 
      syntax Decl ::= defineLocalStaticObject(CId, SymBase, CPPType, Init, DeclarationType, Set)
 
-     rule defineLocalStaticObject(X::CId, Base::SymBase, T::CPPType, Init::Init, Var(Type::InitType), S::Set)
+     rule defineLocalStaticObject(X::CId, Base::SymBase, T::CPPType, Init::Init, Var(Type::InitType), _::Set)
           => addToEnv(NoNamespace() :: X, T, Base, false)
           ~> Odr.newDef(NoNamespace() :: X, T, Base)
           ~> Odr.newDecl(#NoName, NoNamespace() :: X, T, Base)
diff --git a/semantics/cpp/language/translation/decl/enum.k b/semantics/cpp/language/translation/decl/enum.k
index e283c48dd..217acf8e7 100644
--- a/semantics/cpp/language/translation/decl/enum.k
+++ b/semantics/cpp/language/translation/decl/enum.k
@@ -73,7 +73,7 @@ module CPP-TRANSLATION-DECL-ENUM
 
      syntax KItem ::= enumContext(CId, CPPType, List, fixed: Bool, ut: CPPType, opaque: Bool)
 
-     rule enumContext(X::CId, E::CPPType, Enumerators:List, Fixed::Bool, UT::CPPType, Opaque:Bool)
+     rule enumContext(X::CId, E::CPPType, Enumerators:List, Fixed::Bool, _UT::CPPType, Opaque:Bool)
           => newEnum(getEnumId(E), E, Fixed, Opaque)
           ~> addEnumToEnv(X, E)
           ~> #if Opaque #then .K #else inEnumScope(E, declareEnumerators(E, 0, 0, 0, int, Enumerators, Fixed, true)) #fi
@@ -178,13 +178,13 @@ module CPP-TRANSLATION-DECL-ENUM
      // Type of an enumerator inside the declaration is enum's underlying type
      // if it is fixed, and type of initializing expression otherwise,
      // Hence we need to store the type of underlying expression...
-     rule declareEnumerators(T::CPPType, Min::Int, Max::Int, Next::Int, _, ListItem(Enumerator(X::CId, prv(V::Int, _, t(_, _, EType:CPPSimpleType)) #as Pr::PRVal)) L::List, Fixed:Bool, First:Bool)
+     rule declareEnumerators(T::CPPType, Min::Int, Max::Int, _Next::Int, _, ListItem(Enumerator(X::CId, prv(V::Int, _, t(_, _, EType:CPPSimpleType)) #as Pr::PRVal)) L::List, Fixed:Bool, First:Bool)
           => declareEnumerator(getEnumId(T), X, Pr, Fixed, underlyingType(T))
           ~> declareEnumerators(T, #if First #then V #else minInt(Min, V) #fi, #if First #then V #else maxInt(Max, V) #fi, V +Int 1, EType, L, Fixed, false)
      requires notBool isCPPSimpleUnscopedEnumType(EType)
 
      // Enums with fixed underlying type are finished by now.
-     rule declareEnumerators(T::CPPType, _, _, _, _, .List, true, _) => .
+     rule declareEnumerators(_::CPPType, _, _, _, _, .List, true, _) => .
 
      rule declareEnumerators(T::CPPType, Min::Int, Max::Int, _, _, .List, false, _) => calculateEnumValues(T, Min, Max)
 
@@ -302,7 +302,7 @@ module CPP-TRANSLATION-DECL-ENUM
 
      syntax SetEnumMinMaxUt ::= setEnumMinMaxUt(CPPType, min: Int, max: Int, ut: CPPType)
 
-     rule <k> setEnumMinMaxUt(t(_, _, unscopedEnum(_ :: Enum(X::CId) #as E::Enum, _, Fixed:Bool)) #as T::CPPType, Min::Int, Max::Int, cppIntegerType #as UT::CPPType)
+     rule <k> setEnumMinMaxUt(t(_, _, unscopedEnum(_ :: Enum(X::CId) #as E::Enum, _, Fixed:Bool)) #as _::CPPType, Min::Int, Max::Int, cppIntegerType #as UT::CPPType)
           => addEnumToEnv(X, t(noQuals, .Set, unscopedEnum(E, UT, Fixed))) ... </k>
           <enum-id> E </enum-id>
           <enum-type> _ => t(noQuals, .Set, unscopedEnum(E, UT, Fixed)) </enum-type>
@@ -312,7 +312,7 @@ module CPP-TRANSLATION-DECL-ENUM
 
 
      // @ref n4296 7.2/3: ... An opaque-enum-declaration is either a redeclaration of an enumeration in the current scope...
-     rule <k> OpaqueEnumDeclaration(X::CId, Scoped::Bool, UT::CPPType) => . ...</k>
+     rule <k> OpaqueEnumDeclaration(X::CId, _Scoped::Bool, _UT::CPPType) => . ...</k>
           <curr-tr-scope> namespaceScope(N::Namespace) </curr-tr-scope>
           <enum-id> N::Namespace :: Enum(X) </enum-id>
 
diff --git a/semantics/cpp/language/translation/decl/initializer.k b/semantics/cpp/language/translation/decl/initializer.k
index a4e29abcb..389603dc1 100644
--- a/semantics/cpp/language/translation/decl/initializer.k
+++ b/semantics/cpp/language/translation/decl/initializer.k
@@ -225,7 +225,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
           => listInit(Base, DestT, Type, L, CT, D)
 
      // @ref n4296 8.5:17.2 (reference destination type)
-     rule #figureInit(Base:LVal, cppRefType #as DestT::CPPType, _, E:Expr, _, _, _, D::Duration)
+     rule #figureInit(Base:LVal, cppRefType #as _DestT::CPPType, _, E:Expr, _, _, _, D::Duration)
           => bindReference(Base, E, D)
           requires ExprLoc(...) :/=K E
 
@@ -417,7 +417,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
 
      rule #evalBraceOrEqualInitializer(_, _, NoInit()) => BraceInit(.List)
 
-     rule #evalBraceOrEqualInitializer(_, _, ExprLoc(L::CabsLoc, I:Init) => I)
+     rule #evalBraceOrEqualInitializer(_, _, ExprLoc(_::CabsLoc, I:Init) => I)
 
      rule #evalBraceOrEqualInitializer(C::Class, Base::Expr, BraceInit(L::List))
        => BraceInit(#evalBraceOrEqualInitializers(C, Base, L))
@@ -477,7 +477,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
           arrayInit(...
                type:     t(... st: arrayType(T::CPPType, Size::Int)),
                current:  I::Int,
-               initList: (ListItem(Init::Init) _) #as L::List
+               initList: (ListItem(Init::Init) _) #as _::List
           )
           requires notBool #isBraceInit(Init)
            andBool isAggregateType(T)
@@ -499,7 +499,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
           requires notBool isSpuriousExpr(HOLE) [result(ValueCategory)]
 
      rule braceElisionMaybe2(...
-               init:     From::Expr,
+               init:     _From::Expr,
                initType: FromT:CPPType,
                initCat:  FromC:ValueCategory,
                destType: ToT::CPPType
@@ -518,7 +518,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
      rule (braceElisionNo() => #figureInit0(Base[I], T, CopyInit(), Init, CT, D)) ~>
           arrayInit(...
                base:     Base::LVal,
-               type:     t(... st: arrayType(T::CPPType, Size::Int)),
+               type:     t(... st: arrayType(T::CPPType, _Size::Int)),
                current:  (I::Int => I +Int 1),
                initList: (ListItem(Init::Init) => .List) _,
                ctype:    CT::ConstructorType,
@@ -534,9 +534,9 @@ module CPP-TRANSLATION-DECL-INITIALIZER
      rule (braceElisionYes() => #figureInit0(Base[I], T, CopyInit(), BraceInit(L), CT, D)) ~>
           arrayInit(...
                base:     Base::LVal,
-               type:     t(... st: arrayType(T::CPPType, Size::Int)),
+               type:     t(... st: arrayType(T::CPPType, _Size::Int)),
                current:  (I::Int => I +Int 1),
-               initList: (ListItem(Init::Init) _) #as L::List => .List,
+               initList: (ListItem(_::Init) _) #as L::List => .List,
                ctype:    CT::ConstructorType,
                duration: D::Duration
           )
@@ -577,7 +577,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
 
      rule <k> (.K => resolveOverload(cSet(#if Type ==K DirectInit() #then M #else stripExplicit(M) #fi, C :: ConstructorId(X)), list(L), constructor)
               ~> stripResolveOverloadResult())
-              ~> constructorInit(Base::LVal, Type::InitType, _ :: Class(_, X::CId, _) #as C::Class, L::List, _)
+              ~> constructorInit(_Base::LVal, Type::InitType, _ :: Class(_, X::CId, _) #as C::Class, L::List, _)
           ...</k>
           <curr-tr-tu> Tu::String </curr-tr-tu>
           <tu-id> Tu </tu-id>
@@ -618,7 +618,7 @@ module CPP-TRANSLATION-DECL-INITIALIZER
      rule (V:Val => .K)
           ~> strInit(_, _, _, _, _, (E::MaybeExpr => compoundInitJoin(E, V)))
 
-     rule strInit(Base:LVal, t(Q::Quals, Mods::Set, arrayType(T::CPPType, N::Int)), _, "", N, E::MaybeExpr)
+     rule strInit(Base:LVal, t(_::Quals, _Mods::Set, arrayType(_::CPPType, N::Int)), _, "", N, E::MaybeExpr)
           => compoundInitJoin(E, Base)
 
      rule compoundInit(V:TExpr, LV:LVal) => le(compoundInit(stripCompoundInit(V), LV), noTrace, type(LV))
diff --git a/semantics/cpp/language/translation/decl/linkage.k b/semantics/cpp/language/translation/decl/linkage.k
index eba4dc9da..ae789328c 100644
--- a/semantics/cpp/language/translation/decl/linkage.k
+++ b/semantics/cpp/language/translation/decl/linkage.k
@@ -17,7 +17,7 @@ module CPP-TRANSLATION-DECL-LINKAGE
               ~> listToK(Decls)
               ~> setLinkage(OldLinkage, OldExtern)
           ...</k>
-          <curr-tr-scope> N:NamespaceScope </curr-tr-scope>
+          <curr-tr-scope> _:NamespaceScope </curr-tr-scope>
           <curr-lang-linkage> OldLinkage:LanguageLinkage </curr-lang-linkage>
           <curr-extern> OldExtern::Bool </curr-extern>
 
diff --git a/semantics/cpp/language/translation/decl/template.k b/semantics/cpp/language/translation/decl/template.k
index 903c34346..09cc6fba9 100644
--- a/semantics/cpp/language/translation/decl/template.k
+++ b/semantics/cpp/language/translation/decl/template.k
@@ -150,7 +150,7 @@ module CPP-TRANSLATION-DECL-TEMPLATE
           <curr-template-context> templateInfo(...) </curr-template-context>
           requires Init =/=K NoInit()
 
-     rule <k> addParam(X::CId) => .K ...</k>
+     rule <k> addParam(_::CId) => .K ...</k>
           <curr-function> dependent </curr-function>
 
      rule <k> (elaborateDone(K:K) ~> calculateGotoMap => .K) ~> _:KItem ~> setScope(_) ~> _:KItem
@@ -182,7 +182,7 @@ module CPP-TRANSLATION-DECL-TEMPLATE
           ...</k>
           <template-arguments> Old::Map => updateMap(Old, Args) </template-arguments>
 
-     rule <k> templateSpecialization(T:CPPType, _, _) ~> (setTemplateArgs(_, _, Old::Map) => .K) ...</k>
+     rule <k> templateSpecialization(_:CPPType, _, _) ~> (setTemplateArgs(_, _, Old::Map) => .K) ...</k>
           <template-arguments> _ => Old </template-arguments>
 
      rule TemplateDefinitionStmt(K:K) => K
diff --git a/semantics/cpp/language/translation/elaborator.k b/semantics/cpp/language/translation/elaborator.k
index 32e60c0aa..cf68330a4 100644
--- a/semantics/cpp/language/translation/elaborator.k
+++ b/semantics/cpp/language/translation/elaborator.k
@@ -59,7 +59,7 @@ module CPP-TRANSLATION-ELABORATOR
 
      rule (.K => K) ~> runInit(K:K)
 
-     rule K:Val ~> runInit(_) => .K
+     rule _:Val ~> runInit(_) => .K
 
      rule elaborate(K1:K, K2:K) => elaborate(K1) ~> elaborate(K2)
 
diff --git a/semantics/cpp/language/translation/expr/literal.k b/semantics/cpp/language/translation/expr/literal.k
index 9fb84f9c7..edb71397e 100644
--- a/semantics/cpp/language/translation/expr/literal.k
+++ b/semantics/cpp/language/translation/expr/literal.k
@@ -78,7 +78,7 @@ module CPP-TRANSLATION-EXPR-LITERAL
                ~> initString(Loc +bytes 1, butFirstChar(S))
           requires S =/=String ""
 
-     rule initString(Loc::SymLoc, "")
+     rule initString(_::SymLoc, "")
           => .K
 
 endmodule
diff --git a/semantics/cpp/language/translation/expr/new.k b/semantics/cpp/language/translation/expr/new.k
index f988c980c..a47033066 100644
--- a/semantics/cpp/language/translation/expr/new.k
+++ b/semantics/cpp/language/translation/expr/new.k
@@ -138,7 +138,7 @@ module CPP-TRANSLATION-EXPR-NEW
 
      syntax List ::= #getSecondDeleteArg(Map, CPPType, CPPType, PRVal) [function]
 
-     rule #getSecondDeleteArg((stripType(T1) |-> _) (stripType(T2) |-> _) M::Map, T1::CPPType, T2::CPPType, V::PRVal) => ListItem(V)
+     rule #getSecondDeleteArg((stripType(T1) |-> _) (stripType(T2) |-> _) _::Map, T1::CPPType, T2::CPPType, V::PRVal) => ListItem(V)
 
      rule #getSecondDeleteArg(...) => .List [owise]
 
@@ -149,7 +149,7 @@ module CPP-TRANSLATION-EXPR-NEW
           requires isCPPPointerType(type(V)) andBool #fun(InnerT::CPPType => notBool isCPPClassType(InnerT) orBool notBool hasDestructorThat(InnerT, isVirtualDestructor))(innerType(type(V)))
 
      rule (
-            cSet(Cands::Map, Q::QualId) #as C:CandidateSet
+            cSet(Cands::Map, _::QualId) #as C:CandidateSet
             => resolveOverload(
                  C,
                  list(
diff --git a/semantics/cpp/language/translation/expr/reference.k b/semantics/cpp/language/translation/expr/reference.k
index 92738693a..9346692f5 100644
--- a/semantics/cpp/language/translation/expr/reference.k
+++ b/semantics/cpp/language/translation/expr/reference.k
@@ -109,11 +109,11 @@ module CPP-TRANSLATION-EXPR-REFERENCE
 
      rule bindReference'(L:LVal, R:Val) => le(bindReferenceExec(L, R), trace(L), type(L))
 
-     rule <k> le(E::Expr, Tr::Trace, cppRefType #as T::CPPType => innerType(T)) ...</k>
+     rule <k> le(_::Expr, _::Trace, cppRefType #as T::CPPType => innerType(T)) ...</k>
           <unreference> true </unreference>
           <compile-time-evaluation> false </compile-time-evaluation>
 
-     rule <k> xe(E::Expr, Tr::Trace, cppRefType #as T::CPPType => innerType(T)) ...</k>
+     rule <k> xe(_::Expr, _::Trace, cppRefType #as T::CPPType => innerType(T)) ...</k>
           <unreference> true </unreference>
           <compile-time-evaluation> false </compile-time-evaluation>
 
diff --git a/semantics/cpp/language/translation/io.k b/semantics/cpp/language/translation/io.k
index 8e2ab7279..a748bcefa 100644
--- a/semantics/cpp/language/translation/io.k
+++ b/semantics/cpp/language/translation/io.k
@@ -13,9 +13,9 @@ module CPP-TRANSLATION-IO
      imports DELETE-OBJECT-SYNTAX
      imports SYMLOC-SYNTAX
 
-     rule freeNativeObject(B::SymBase) => .K
+     rule freeNativeObject(_::SymBase) => .K
 
-     rule writeNativeByte(L::SymLoc, K::K) => .List
+     rule writeNativeByte(_::SymLoc, _::K) => .List
 
 
      rule <k> initBytes(loc(Base::SymBase, Offset::Int), ListItem(V::Bits) L::List)
diff --git a/semantics/cpp/language/translation/name.k b/semantics/cpp/language/translation/name.k
index 54893f216..1c25b634b 100644
--- a/semantics/cpp/language/translation/name.k
+++ b/semantics/cpp/language/translation/name.k
@@ -112,7 +112,7 @@ module CPP-TRANSLATION-NAME
           <tu-id> Tu </tu-id>
           <ns-id> N </ns-id>
           <inline-namespaces> InlineS::Set </inline-namespaces>
-          <nusing-namespaces> UsingS::Set </nusing-namespaces>
+          <nusing-namespaces> _UsingS::Set </nusing-namespaces>
 
      rule <k> nameLookupInUsingDirectives(... set: (SetItem(N::Namespace) => .Set) _,
                    usingS: (.Set => UsingS) _)
@@ -347,7 +347,7 @@ module CPP-TRANSLATION-NAME
                andBool notBool isIgnoredClassSet(C2, B2)
                andBool notBool isIgnoredClassSet(B2, C2)
 
-     rule mergeClassSet(classSet(_, C1::QualId, C2::Set), classSet(_, B1::QualId, B2::Set))
+     rule mergeClassSet(classSet(_, C1::QualId, C2::Set), classSet(_, _::QualId, B2::Set))
           => classSet(ambiguous, C1, C2 B2) [owise]
 
      syntax Bool ::= isIgnoredClassSet(Set, Set) [function]
@@ -381,7 +381,7 @@ module CPP-TRANSLATION-NAME
 
      rule (.K => argDependentNameLookup(X, Args)) ~> CallExpr(Name(NoNNS(), X::CId), Args::StrictList, krlist(.List))
 
-     rule <k> CallExpr((ExprLoc(L::CabsLoc, E:Expr) => E), Args::StrictList, krlist(.List)) ...</k>
+     rule <k> CallExpr((ExprLoc(L::CabsLoc, E:Expr) => E), _Args::StrictList, krlist(.List)) ...</k>
           <curr-tr-program-loc> _ => L </curr-tr-program-loc>
 
      context CallExpr(Name(HOLE:NNS, _), _, _)
@@ -394,7 +394,7 @@ module CPP-TRANSLATION-NAME
 
      rule (.K => qualifiedNameLookup(X, C, defaultMask)) ~> CallExpr((le(_, _, t(... st: classType(C::Class))) #Or xe(_, _, t(... st: classType(C::Class))) #Or pre(_, _, t(... st: classType(C::Class)))) . no-template Name(NoNNS(), X::CId), _, krlist(.List))
 
-     rule (.K => qualifiedNameLookup(X, C, defaultMask)) ~> CallExpr(V:Val . no-template Name(C:NNSVal, X::CId), _, _)
+     rule (.K => qualifiedNameLookup(X, C, defaultMask)) ~> CallExpr(_:Val . no-template Name(C:NNSVal, X::CId), _, _)
 
      rule cSet(Y::Map, X::QualId) ~> CallExpr(E::Expr, Args::StrictList, krlist(.List))
           => resolveOverload(cSet(Y, X), Args, E)
@@ -521,7 +521,7 @@ module CPP-TRANSLATION-NAME
      rule <k> (.K => isDependentName(X, Args, Types)) ~> argDependentNameLookup(X::CId, list(Args::List), krlist(Types::List), _:CandidateSet) ...</k>
           <curr-template-context> templateInfo(...) </curr-template-context>
 
-     rule <k> (.K => false) ~> argDependentNameLookup(X::CId, list(Args::List), krlist(Types::List), _:CandidateSet) ...</k>
+     rule <k> (.K => false) ~> argDependentNameLookup(_::CId, list(_Args::List), krlist(_Types::List), _:CandidateSet) ...</k>
           <curr-template-context> noTemplate </curr-template-context>
 
      // TODO(dwightguth): class member stuff
@@ -535,7 +535,7 @@ module CPP-TRANSLATION-NAME
 
      rule isDependentName(_, .List, .List) => false
 
-     rule <k> false ~> argDependentNameLookup(X::CId, Args::StrictList, Types::StrictList, cSet(Y::Map, QX::QualId)) => cSet(Y, QX) ...</k>
+     rule <k> false ~> argDependentNameLookup(X::CId, _Args::StrictList, _Types::StrictList, cSet(Y::Map, QX::QualId)) => cSet(Y, QX) ...</k>
            <tr-env> Env::Map </tr-env>
            requires hasSpecialDeclInArgLookup(X, Y, Env)
 
@@ -552,13 +552,13 @@ module CPP-TRANSLATION-NAME
 
      // associated namespaces
      rule <k> (.K => getFunctionAddressTypes(Args))
-              ~> false ~> argDependentNameLookup(X::CId, list(Args::List), krlist(Types::List), cSet(... candidates: Y::Map)) ...</k>
+              ~> false ~> argDependentNameLookup(X::CId, list(Args::List), krlist(_Types::List), cSet(... candidates: Y::Map)) ...</k>
           <tr-env> Env::Map </tr-env>
           requires notBool hasSpecialDeclInArgLookup(X, Y, Env)
 
      rule <k> (.K => getFunctionAddressTypes(Args))
-              ~> false ~> argDependentNameLookup(X::CId, list(Args::List), krlist(Types::List), notFound(_)) ...</k>
-          <tr-env> Env::Map </tr-env>
+              ~> false ~> argDependentNameLookup(_::CId, list(Args::List), krlist(_Types::List), notFound(_)) ...</k>
+          <tr-env> _Env::Map </tr-env>
 
      // if the argument is the name or address of a set of overloaded functions
      // and/or function templates, its associated classes and namespaces are
@@ -578,9 +578,9 @@ module CPP-TRANSLATION-NAME
 
      syntax Bool ::= isAddressOfName(Init) [function]
 
-     rule isAddressOfName(& N:Name) => true
+     rule isAddressOfName(& _:Name) => true
 
-     rule isAddressOfName(UnaryOperator(operator&, N:Name)) => true
+     rule isAddressOfName(UnaryOperator(operator&, _:Name)) => true
 
      rule isAddressOfName(_) => false [owise]
 
@@ -597,7 +597,7 @@ module CPP-TRANSLATION-NAME
                    | getTemplateArgTypes(TemplateArgs) [function]
 
      // @ref n4296 3.4.2:2.1
-     rule getAssociatedNamespaces((ListItem(cppFundamentalType #as T::CPPType) => .List) _, _)
+     rule getAssociatedNamespaces((ListItem(cppFundamentalType #as _::CPPType) => .List) _, _)
 
      rule getAssociatedNamespaces((ListItem(t(_, _, no-type)) => .List) _, _)
 
@@ -647,7 +647,7 @@ module CPP-TRANSLATION-NAME
 
      rule getTemplateArgTypes(.TemplateArgs) => .List
 
-     rule #argDependentNameLookup(X::CId, Args::StrictList, Types::List, .Set, Y:CandidateSet) => Y
+     rule #argDependentNameLookup(_::CId, _Args::StrictList, _Types::List, .Set, Y:CandidateSet) => Y
 
      rule (.K => qualifiedNameLookup(X, N, SetItem(function))) ~> #argDependentNameLookup(X::CId, _, _, (SetItem(N::Namespace) => .Set) _, _)
 
@@ -661,7 +661,7 @@ module CPP-TRANSLATION-NAME
      rule resolveElabSpecifier(templateRef(Q::QualId, T::CPPType), krlist(Args::List))
           => specializeTypeTemplate(Q, T, Args)
 
-     rule <k> specializeTypeTemplate(X::QualId, t(Q::Quals, Mods::Set, classType(N::Namespace :: Class(Tag::Tag, C::CId, .TemplateArgs))), Args::List)
+     rule <k> specializeTypeTemplate(_::QualId, t(Q::Quals, Mods::Set, classType(N::Namespace :: Class(Tag::Tag, C::CId, .TemplateArgs))), Args::List)
                => t(Q, Mods, classType(N :: Class(Tag, C, toTemplateArgs(Args))))
           ...</k>
 
diff --git a/semantics/cpp/language/translation/odr.k b/semantics/cpp/language/translation/odr.k
index 3d3610c79..7b444aba5 100644
--- a/semantics/cpp/language/translation/odr.k
+++ b/semantics/cpp/language/translation/odr.k
@@ -34,7 +34,7 @@ module CPP-TRANSLATION-ODR
           <odr-decls> Decls::Map => Decls[Base += odrDecl(Tu, Q, CName, LangLinkage, T)] </odr-decls>
 
      rule <k> Odr.doWhenUsed(Base::SymBase, K:KItem) => .K ...</k>
-          <odr-uses> Uses::Set </odr-uses>
+          <odr-uses> _Uses::Set </odr-uses>
           <curr-tr-tu> Tu::String </curr-tr-tu>
           <tu-id> Tu </tu-id>
           <when-odr-used>... .Map => Base |-> K </when-odr-used>
diff --git a/semantics/cpp/language/translation/overloading.k b/semantics/cpp/language/translation/overloading.k
index c7b926cb2..7d36a757e 100644
--- a/semantics/cpp/language/translation/overloading.k
+++ b/semantics/cpp/language/translation/overloading.k
@@ -99,11 +99,11 @@ module CPP-TRANSLATION-OVERLOADING
      syntax List ::= getArgs(List, QualId, Expr, K) [function]
 
      // @ref n4296 13.3.1.1.1:2
-     rule getArgs(Args::List, C:Class :: _, Obj::Expr . no-template _, _)
+     rule getArgs(Args::List, _:Class :: _, Obj::Expr . no-template _, _)
           => ListItem(Obj) Args
 
      // @ref n4296 13.3.1.1.1:3 case (1)
-     rule getArgs(Args::List, N:Namespace :: _, _, _) => Args
+     rule getArgs(Args::List, _:Namespace :: _, _, _) => Args
 
      // @ref n4296 13.3.1.1.1:3 case (2) when this is in scope
      rule getArgs(Args::List, C:Class :: _, _:Name, Obj:PRVal)
@@ -226,7 +226,7 @@ module CPP-TRANSLATION-OVERLOADING
      rule #notViableTypes(... params: .List, types: .List, cats: .List) => false
 
      // default arguments
-     rule #notViableTypes(ListItem(P:CPPType) _, .List => ListItem(A) DAs, ListItem(A::CPPType) DAs::List, .List => DCs, DCs::List, _)
+     rule #notViableTypes(ListItem(_:CPPType) _, .List => ListItem(A) DAs, ListItem(A::CPPType) DAs::List, .List => DCs, DCs::List, _)
 
      rule canBeImplicitlyConvertedTo(...
                fromType: FromType::CPPType,
@@ -381,7 +381,7 @@ module CPP-TRANSLATION-OVERLOADING
 
      rule #computeUDC(CS1:ConversionSequence, CS2:ConversionSequence)
           =>
-          resolveUDC(ListItem(CS1) ListItem(CS1))
+          resolveUDC(ListItem(CS1) ListItem(CS1))  // TODO: Should the last one be CS2?
 
 
      syntax KItem ::= computeUDCTo(Class, ClassInfo, CPPType, ValueCategory)
@@ -407,7 +407,7 @@ module CPP-TRANSLATION-OVERLOADING
           ) ~>
           #computeUDCTo(
                _ :: Class(_, X::CId, _) #as P::Class,
-               (ListItem(t(... st: functionType(... returnType: Ret::CPPType, paramTypes: Param::CPPType)) #as FuncT::CPPType) => .List) L::List,
+               (ListItem(t(... st: functionType(... returnType: Ret::CPPType, paramTypes: Param::CPPType)) #as FuncT::CPPType) => .List) _::List,
                A::CPPType,
                C::ValueCategory,
                _
@@ -435,7 +435,7 @@ module CPP-TRANSLATION-OVERLOADING
           ~>
           #computeUDCFrom(
                P::CPPType,
-               (ListItem(t(... st: functionType(... returnType: Ret::CPPType)) #as FuncT::CPPType) => .List) L::List,
+               (ListItem(t(... st: functionType(... returnType: Ret::CPPType)) #as FuncT::CPPType) => .List) _::List,
                A::Class,
                C::ValueCategory,
                _
@@ -499,14 +499,14 @@ module CPP-TRANSLATION-OVERLOADING
      rule computeSCS2(C::Conversion, cppIntegerType #as P::CPPType, t(... st: _:CPPSimpleUnscopedEnumType) #as A::CPPType, _) => computeSCS3(C, integralConversion, P, P)
           requires utype(P) =/=Type utype(A) andBool promote(A) =/=Type P andBool promote(promote(A)) =/=Type P andBool notBool isCPPBoolType(P)
 
-     rule computeSCS2(C::Conversion, t(... st: _:CPPSimpleFloatingType) #as P::CPPType, t(... st: _:CPPSimpleFloatingType) #as A::CPPType, _) => computeSCS3(C, floatingConversion, P, P)
+     rule computeSCS2(C::Conversion, t(... st: _:CPPSimpleFloatingType) #as P::CPPType, t(... st: _:CPPSimpleFloatingType) #as _::CPPType, _) => computeSCS3(C, floatingConversion, P, P)
           requires notBool (simpleType(P) ==K double andBool simpleType(P) ==K float)
 
-     rule computeSCS2(C::Conversion, cppIntegerType #as P::CPPType, t(... st: _:CPPSimpleFloatingType) #as A::CPPType, _) => computeSCS3(C, floatingIntegralConversion, P, P)
+     rule computeSCS2(C::Conversion, cppIntegerType #as P::CPPType, t(... st: _:CPPSimpleFloatingType) #as _::CPPType, _) => computeSCS3(C, floatingIntegralConversion, P, P)
 
-     rule computeSCS2(C::Conversion, t(... st: _:CPPSimpleFloatingType) #as P::CPPType, cppIntegerType #as A::CPPType, _) => computeSCS3(C, floatingIntegralConversion, P, P)
+     rule computeSCS2(C::Conversion, t(... st: _:CPPSimpleFloatingType) #as P::CPPType, cppIntegerType #as _::CPPType, _) => computeSCS3(C, floatingIntegralConversion, P, P)
 
-     rule computeSCS2(C::Conversion, t(... st: _:CPPSimpleFloatingType) #as P::CPPType, t(... st: _:CPPSimpleUnscopedEnumType) #as A::CPPType, _) => computeSCS3(C, floatingIntegralConversion, P, P)
+     rule computeSCS2(C::Conversion, t(... st: _:CPPSimpleFloatingType) #as P::CPPType, t(... st: _:CPPSimpleUnscopedEnumType) #as _::CPPType, _) => computeSCS3(C, floatingIntegralConversion, P, P)
 
      rule computeSCS2(C::Conversion, t(... st: pointerType(...)) #as P::CPPType, cppIntegerType #as A::CPPType, _) => computeSCS3(C, pointerConversion(P, A), P, P)
 
@@ -604,7 +604,7 @@ module CPP-TRANSLATION-OVERLOADING
 
      // do not actually perform overload resolution, this was a function call
      // in which the postfix expression was a function pointer
-     rule #resolveOverload2(cSet(... candidates: _::CPPType |-> (T::CPPType, envEntry(... base: Base::SymBase)), id: X::QualId), list(Args::List), _, _, E::Expr, _)
+     rule #resolveOverload2(cSet(... candidates: _::CPPType |-> (T::CPPType, envEntry(... base: Base::SymBase)), id: _::QualId), list(Args::List), _, _, E::Expr, _)
           => Odr.newUse(Base)
           ~> updateExternalUses(Base)
           ~> checkAccess(CallExpr(lv(lnew(Base), hasTrace(E), T), list(Args), krlist(getDefaultArgsVals(emptyDefaultArguments(innerType(T))))))
@@ -616,16 +616,16 @@ module CPP-TRANSLATION-OVERLOADING
 
      // only one viable candidate
      rule bestViable(T::CPPType, envEntry(... base: Base::SymBase, defaultArgs: defArgs(... vals: DArgs::StrictListResult)))
-          ~> #resolveOverload2(cSet(... id: X::QualId), list(Args::List), _, _, E::Expr, _)
+          ~> #resolveOverload2(cSet(... id: _::QualId), list(Args::List), _, _, E::Expr, _)
           => #if isMethodPure(T) andBool isVirtualCall(hasTrace(E), T) #then .K #else Odr.newUse(Base) #fi
           ~> updateExternalUses(Base)
           ~> checkAccess(CallExpr(lv(lnew(Base), hasTrace(E), T), list(Args), DArgs))
 
-     rule bestViable(T::CPPType, builtinOp(E::Expr)) ~> #resolveOverload2(...)
+     rule bestViable(_::CPPType, builtinOp(E::Expr)) ~> #resolveOverload2(...)
           => resolveOverloadResult(E)
 
      rule (.K => computeBestViable(M, Types, Cats, O))
-          ~> #resolveOverload2(cSet(... candidates: M::Map), list(Args::List), krlist(Types::List), krlist(Cats::List), _, O::OverloadType)
+          ~> #resolveOverload2(cSet(... candidates: M::Map), list(_Args::List), krlist(Types::List), krlist(Cats::List), _, O::OverloadType)
           requires allFunctionTypes(M)
 
      syntax Bool ::= allFunctionTypes(Map) [function]
@@ -699,7 +699,7 @@ module CPP-TRANSLATION-OVERLOADING
                _,
                _,
                _,
-               (ListItem(kpair(T2::CPPType, K2:K)) => .List) _
+               (ListItem(kpair(_::CPPType, _:K)) => .List) _
           )
 
      rule false ~> checkIsBest(...) => noBestViable [owise]
@@ -722,12 +722,12 @@ module CPP-TRANSLATION-OVERLOADING
      rule #isBetterFunctionThan(
                HasWorseCS:Bool,
                HasBetterCS:Bool,
-               F1::CPPType,
+               _F1::CPPType,
                K1:K,
-               F2::CPPType,
+               _F2::CPPType,
                K2:K,
-               Types::List,
-               Cats::List,
+               _Types::List,
+               _Cats::List,
                NotConversionOverload()
           )
           => notBool HasWorseCS andBool (HasBetterCS orBool (notBool isTemplateSpecialization(K1) andBool isTemplateSpecialization(K2)))
@@ -802,8 +802,8 @@ module CPP-TRANSLATION-OVERLOADING
                (ListItem(P:CPPType) => .List) _,
                (ListItem(A::CPPType) => .List) _,
                (ListItem(C::ValueCategory) => .List) _,
-               B1::Bool,
-               B2::Bool,
+               _::Bool,
+               _::Bool,
                _
           )
 
@@ -821,20 +821,20 @@ module CPP-TRANSLATION-OVERLOADING
           ~> #getConversionSequences(... result: (.List => ListItem(CS)) _)
 
      rule #getConversionSequences(
-               ListItem(implicitObjectParameter(_)) Ps::List,
-               ListItem(_) As::List,
-               ListItem(_) Cs::List,
-               IsNonStaticRefNone::Bool,
+               ListItem(implicitObjectParameter(_)) _Ps::List,
+               ListItem(_) _As::List,
+               ListItem(_) _Cs::List,
+               _IsNonStaticRefNone::Bool,
                true,
                (.List => ListItem(bottomConversionSequence)) _
           )
 
      rule #getConversionSequences(
                ListItem(variadic),
-               (ListItem(_) => .List) As::List,
-               (ListItem(_) => .List) Cs::List,
-               B1::Bool,
-               B2::Bool,
+               (ListItem(_) => .List) _As::List,
+               (ListItem(_) => .List) _Cs::List,
+               _::Bool,
+               _::Bool,
                (.List => ListItem(ellipsisConversionSequence)) _
           )
 
@@ -1022,7 +1022,7 @@ module CPP-TRANSLATION-OVERLOADING
      // to which the reference is bound.
      rule standardConversionSequence(... isNonStaticRefNone: false, param: t(... st: rvRefType(...)) #as S1::CPPType)
           >CS
-          standardConversionSequence(... isNonStaticRefNone: false, param: t(... st: lvRefType(...)) #as S2::CPPType)
+          standardConversionSequence(... isNonStaticRefNone: false, param: t(... st: lvRefType(...)))
           => true
           requires notBool isCPPFunctionType(innerType(S1))
 
@@ -1071,7 +1071,7 @@ module CPP-TRANSLATION-OVERLOADING
      rule (lv(loc(Base::SymBase, 0), _, _) => .K)
           ~> bestViable(T::CPPType, (_ => envEntry(Base, false, emptyDefaultArguments(T))))
 
-     rule resolveUniqueDecl(cSet(... candidates: _::CPPType |-> (T::CPPType, envEntry(... base: Base::SymBase)), id: X::QualId), E::Expr, _)
+     rule resolveUniqueDecl(cSet(... candidates: _::CPPType |-> (T::CPPType, envEntry(... base: Base::SymBase)), id: _::QualId), E::Expr, _)
           => Odr.newUse(Base)
           ~> updateExternalUses(Base)
           ~> lv(lnew(Base), hasTrace(E), T)
@@ -1111,6 +1111,6 @@ module CPP-TRANSLATION-OVERLOADING
 
      rule typeof(contrivedObject(T::CPPType) => T)
 
-     rule contrivedObject(T::CPPType) => noObject()
+     rule contrivedObject(_::CPPType) => noObject()
           requires Translation()
 endmodule
diff --git a/semantics/cpp/language/translation/process-label.k b/semantics/cpp/language/translation/process-label.k
index 5d46ce5cd..7c6104957 100644
--- a/semantics/cpp/language/translation/process-label.k
+++ b/semantics/cpp/language/translation/process-label.k
@@ -196,7 +196,7 @@ module CPP-TRANSLATION-PROCESS-LABEL
      rule <k> waitingOnGotoMap ...</k>
           <goto-calc>
                <computation>
-                    TryStmt(_, (ListItem(CatchOp(T::CPPType, S::Block)) => .List) L::List) ~> K:K
+                    TryStmt(_, (ListItem(CatchOp(_::CPPType, S::Block)) => .List) _::List) ~> K:K
                </computation>
                <computation-tail> Tail:K </computation-tail>
                B::Bag
@@ -210,7 +210,7 @@ module CPP-TRANSLATION-PROCESS-LABEL
      rule <k> waitingOnGotoMap ...</k>
           <goto-calc>
                <computation>
-                    TryStmt(_, (ListItem(CatchAnyOp(S::Block)) => .List) L::List) ~> K:K
+                    TryStmt(_, (ListItem(CatchAnyOp(S::Block)) => .List) _::List) ~> K:K
                </computation>
                <computation-tail> Tail:K </computation-tail>
                B::Bag
diff --git a/semantics/cpp/language/translation/stmt/if.k b/semantics/cpp/language/translation/stmt/if.k
index d940b522c..14e964caa 100644
--- a/semantics/cpp/language/translation/stmt/if.k
+++ b/semantics/cpp/language/translation/stmt/if.k
@@ -8,7 +8,7 @@ module CPP-TRANSLATION-STMT-IF
      imports CPP-TRANSLATION-ERROR-SYNTAX
      imports CPP-TYPING-SYNTAX
 
-     rule IfTStmt((C:PRVal => convertType(type(bool), C)), TrueBr:Block, FalseBr:Block)
+     rule IfTStmt((C:PRVal => convertType(type(bool), C)), _TrueBr:Block, _FalseBr:Block)
           requires notBool isCPPBoolType(type(C))
 
      rule (.K => elaborate(TrueBr, FalseBr))
diff --git a/semantics/cpp/language/translation/stmt/loop.k b/semantics/cpp/language/translation/stmt/loop.k
index 74909d15a..2df00ebde 100644
--- a/semantics/cpp/language/translation/stmt/loop.k
+++ b/semantics/cpp/language/translation/stmt/loop.k
@@ -13,7 +13,7 @@ module CPP-TRANSLATION-STMT-LOOP
 
      context ForTStmt((HOLE:Expr => reval(HOLE)), _, _) [result(PRVal)]
 
-     rule ForTStmt((Condition:PRVal => convertType(type(bool), Condition)), Inc::Stmt, Blk::Stmt)
+     rule ForTStmt((Condition:PRVal => convertType(type(bool), Condition)), _Inc::Stmt, _Blk::Stmt)
           requires notBool isCPPBoolType(type(Condition))
 
      rule (.K => elaborate(Inc, Blk)) ~> ForTStmt(Condition:PRVal, Inc::Stmt, Blk::Stmt)
@@ -27,7 +27,7 @@ module CPP-TRANSLATION-STMT-LOOP
 
      context WhileTStmt((HOLE:Expr => reval(HOLE)), _) [result(PRVal)]
 
-     rule WhileTStmt((Condition:PRVal => convertType(type(bool), Condition)), Blk::Stmt)
+     rule WhileTStmt((Condition:PRVal => convertType(type(bool), Condition)), _::Stmt)
           requires notBool isCPPBoolType(type(Condition))
 
      rule (.K => elaborate(Blk)) ~> WhileTStmt(Condition:PRVal, Blk::Stmt)
diff --git a/semantics/cpp/language/translation/typing/canonicalization.k b/semantics/cpp/language/translation/typing/canonicalization.k
index ad3b610b2..4c5f68f27 100644
--- a/semantics/cpp/language/translation/typing/canonicalization.k
+++ b/semantics/cpp/language/translation/typing/canonicalization.k
@@ -139,16 +139,16 @@ module CPP-TRANSLATION-TYPING-CANONICALIZATION
 
      rule (.K => typeof(E)) ~> Decltype(E::Expr)
 
-     rule (.K => catof(E)) ~> typeof(T:CPPType) ~> Decltype(E::Expr)
+     rule (.K => catof(E)) ~> typeof(_:CPPType) ~> Decltype(E::Expr)
           requires Name(_, _) :/=K E
 
      rule typeof(T:CPPType) ~> Decltype(Name(_, _)) => T
 
-     rule catof(xvalue) ~> typeof(T:CPPType) ~> Decltype(E::Expr) => type(rvRefType(T))
+     rule catof(xvalue) ~> typeof(T:CPPType) ~> Decltype(_::Expr) => type(rvRefType(T))
 
-     rule catof(lvalue) ~> typeof(T:CPPType) ~> Decltype(E::Expr) => type(lvRefType(T))
+     rule catof(lvalue) ~> typeof(T:CPPType) ~> Decltype(_::Expr) => type(lvRefType(T))
 
-     rule catof(prvalue) ~> typeof(T:CPPType) ~> Decltype(E::Expr) => T
+     rule catof(prvalue) ~> typeof(T:CPPType) ~> Decltype(_::Expr) => T
 
      syntax KItem ::= elabResult(K)
 
diff --git a/semantics/cpp/language/translation/typing/expr.k b/semantics/cpp/language/translation/typing/expr.k
index 6da06b354..0db9f5f8c 100644
--- a/semantics/cpp/language/translation/typing/expr.k
+++ b/semantics/cpp/language/translation/typing/expr.k
@@ -75,7 +75,7 @@ module CPP-TRANSLATION-TYPING-EXPR
      context (HOLE:TypeExpr => typeof(HOLE)) types:: _
           requires notBool isSpuriousExpr(HOLE) [result(CPPDType)]
 
-     context K:KResult types:: HOLE:STypeList
+     context _:KResult types:: HOLE:STypeList
 
      // ----------------------------------
 
@@ -292,7 +292,7 @@ module CPP-TRANSLATION-TYPING-EXPR
 
      rule #typeofBuiltinOperator(operator[], _, _, t(... st: pointerType(...)) #as T::CPPType) => typeof(innerType(T))
 
-     rule #typeofBuiltinOperator(operator->, t(... st: pointerType(...)) #as T::CPPType, E1::Expr, E2::Name)
+     rule #typeofBuiltinOperator(operator->, t(... st: pointerType(...)) #as _::CPPType, E1::Expr, E2::Name)
           => typeof((* E1) . no-template E2)
 
      rule #typeofBuiltinOperator(operator+, T1::CPPType, _, T2::CPPType)
diff --git a/semantics/cpp/language/translation/value-category.k b/semantics/cpp/language/translation/value-category.k
index c4f495886..955a7c66f 100644
--- a/semantics/cpp/language/translation/value-category.k
+++ b/semantics/cpp/language/translation/value-category.k
@@ -68,7 +68,7 @@ module CPP-TRANSLATION-VALUE-CATEGORY
      context (HOLE:CatExpr => catof(HOLE)) cats:: _
           requires notBool isSpuriousExpr(HOLE) [result(ValueCategory)]
 
-     context K:KResult cats:: HOLE:SCatList
+     context _:KResult cats:: HOLE:SCatList
 
      // --------------------------------
 
@@ -91,11 +91,11 @@ module CPP-TRANSLATION-VALUE-CATEGORY
                   orBool CallExpr(_, _, _) :=K HOLE
                   orBool _ . _ _ :=K HOLE
 
-     rule catof(L:LVal => lvalue)
+     rule catof(_:LVal => lvalue)
 
-     rule catof(X:XVal => xvalue)
+     rule catof(_:XVal => xvalue)
 
-     rule catof(PR:PRVal => prvalue)
+     rule catof(_:PRVal => prvalue)
 
      rule catof(AlignofExpr(_) => prvalue)
 
diff --git a/semantics/linking/c-resolution.k b/semantics/linking/c-resolution.k
index 5a968a52d..7ed0b6e98 100644
--- a/semantics/linking/c-resolution.k
+++ b/semantics/linking/c-resolution.k
@@ -59,7 +59,7 @@ module LINKING-C-RESOLUTION
           ...</external-decls>
           <external-defs>... X |-> _ ...</external-defs>
           <tu-id> Tu </tu-id>
-          <genv>... X |-> Base:DirectBase ...</genv>
+          <genv>... X |-> _:DirectBase ...</genv>
           [structural]
      rule <k> resolveCReference(X:CId, _) => .K  ...</k>
           <external-decls>...
diff --git a/semantics/linking/cpp-builtin.k b/semantics/linking/cpp-builtin.k
index 965e0ad25..e188e94b2 100644
--- a/semantics/linking/cpp-builtin.k
+++ b/semantics/linking/cpp-builtin.k
@@ -60,7 +60,7 @@ module LINKING-CPP-BUILTIN
      syntax List ::= getDummyParams(CPPType) [function]
      syntax List ::= #getDummyParams(CPPTypes, Int) [function]
      rule getDummyParams(t(_, _, functionType(... paramTypes: Ts::CPPTypes))) => #getDummyParams(Ts, 0)
-     rule #getDummyParams(T::CPPType, Ts::CPPTypes, I::Int) => ListItem(Identifier("_" +String showInt(I))) #getDummyParams(Ts, I +Int 1)
+     rule #getDummyParams(_::CPPType, Ts::CPPTypes, I::Int) => ListItem(Identifier("_" +String showInt(I))) #getDummyParams(Ts, I +Int 1)
      rule #getDummyParams(.CPPTypes, _) => .List
 
 endmodule
diff --git a/semantics/linking/cpp-resolution.k b/semantics/linking/cpp-resolution.k
index b898e27ab..123e1e034 100644
--- a/semantics/linking/cpp-resolution.k
+++ b/semantics/linking/cpp-resolution.k
@@ -28,7 +28,7 @@ module LINKING-CPP-RESOLUTION
      syntax KItem ::= resolveCPPReference(SymBase)
      rule <k> resolveCPPReference(OdrBase:DirectBase) ...</k>
           <odr-decls>...
-               OdrBase |-> (SetItem(odrDecl(Tu::String, QX::QualId, _, _, T::CPPType)) => .Set) _::Set
+               OdrBase |-> (SetItem(odrDecl(_Tu::String, QX::QualId, _, _, T::CPPType)) => .Set) _::Set
           ...</odr-decls>
           <odr-defs>... QX |-> (stripType(T) |-> _ _::Map) ...</odr-defs>
 
@@ -54,7 +54,7 @@ module LINKING-CPP-RESOLUTION
           <odr-defs>... N :: X |-> (stripType(T) |-> _ _::Map) ...</odr-defs>
           <tu-id> Tu </tu-id>
           <ns-id> N </ns-id>
-          <nenv>... X |-> (stripType(T) |-> (_, envEntry(... base: Base:DirectBase)) _::Map) ...</nenv>
+          <nenv>... X |-> (stripType(T) |-> (_, envEntry(... base: _:DirectBase)) _::Map) ...</nenv>
 
      rule <k> resolveCPPReference(OdrBase::SymBase) ...</k>
           <odr-decls>...
@@ -75,7 +75,7 @@ module LINKING-CPP-RESOLUTION
           <external-defs>... Mangled |-> _ ...</external-defs>
           <tu-id> Tu </tu-id>
           <ns-id> N </ns-id>
-          <nenv>... X |-> (stripType(T) |-> (_, envEntry(... base: Base:DirectBase)) _::Map) ...</nenv>
+          <nenv>... X |-> (stripType(T) |-> (_, envEntry(... base: _:DirectBase)) _::Map) ...</nenv>
 
      rule <k> (.K => ILL("TDR3",
                     "No definition for function or variable which was odr-used: "
@@ -143,6 +143,6 @@ module LINKING-CPP-RESOLUTION
           <odr-defs>... C :: X |-> (stripType(T) |-> _ _::Map) ...</odr-defs>
           <tu-id> Tu </tu-id>
           <class-id> C </class-id>
-          <cenv>... X |-> (stripType(T) |-> (_, envEntry(... base: Base:DirectBase)) _::Map) ...</cenv>
+          <cenv>... X |-> (stripType(T) |-> (_, envEntry(... base: _:DirectBase)) _::Map) ...</cenv>
 
 endmodule
diff --git a/semantics/linking/init.k b/semantics/linking/init.k
index c368138cb..1060e1561 100644
--- a/semantics/linking/init.k
+++ b/semantics/linking/init.k
@@ -56,7 +56,7 @@ module LINKING-INIT
                ~> removeUnusedIdentifiers(Tu)
           ...</k>
           <external-types> Types:Map </external-types>
-          <external-decls-loc> DeclLocs:Map </external-decls-loc>
+          <external-decls-loc> _:Map </external-decls-loc>
           <external-defs> Defs:Map </external-defs>
           <external-defs-loc> Locs:Map </external-defs-loc>
 
@@ -147,7 +147,7 @@ module LINKING-INIT
           ...</k>
           <odr-uses> OdrUses::Set => .Set </odr-uses>
           <external-uses> Uses::Map => .Map </external-uses>
-          <linking-deps> Deps </linking-deps>
+          <linking-deps> _ </linking-deps>
 
      syntax KItem ::= clearLinkingState()
      rule <k> clearLinkingState() => .K ...</k>
@@ -211,7 +211,7 @@ module LINKING-INIT
                _, X |-> T':Type _,
                Locs::Map)
           requires notBool (X in_keys(Locs))
-     rule (checkExtType(true) => .K) ~> checkExtTypes(X:KItem => .K, _, _, _, _, _)
+     rule (checkExtType(true) => .K) ~> checkExtTypes(_:KItem => .K, _, _, _, _, _)
      rule (.K => setTranslationLoc(L) ~> EXT-UNDEF("TIN1",
                "Identifier " +String showCId({X}:>CId) +String " declared with incompatible types in different translation units."))
                ~> checkExtType(false) ~> checkExtTypes(X:KItem, _, _, _, _, X |-> L::CabsLoc _)
@@ -223,7 +223,7 @@ module LINKING-INIT
      rule checkExtDefs(X:KItem => .K, _, _, Defs':Set, _, _)
           requires notBool (X in Defs')
      rule checkExtDefs(.K, .Set, _, _, _, _) => .K
-     rule checkExtDefs(X:CId, Ids::Set, X |-> T::Type Types::Map, SetItem(X) Ids'::Set, X |-> T'::Type Types'::Map, X |-> L::CabsLoc Locs::Map)
+     rule checkExtDefs(X:CId, Ids::Set, X |-> _::Type Types::Map, SetItem(X) Ids'::Set, X |-> _::Type Types'::Map, X |-> L::CabsLoc Locs::Map)
           => setTranslationLoc(L)
           ~> EXT-UNDEF("TIN2", "Multiple external definitions for " +String showCId({X}:>CId) +String ".")
           ~> errorMultipleDefs(X)