diff --git a/app/GlobalOptions.hs b/app/GlobalOptions.hs
index 471717c691..23fa62c0f9 100644
--- a/app/GlobalOptions.hs
+++ b/app/GlobalOptions.hs
@@ -24,6 +24,7 @@ data GlobalOptions = GlobalOptions
     _globalNoPositivity :: Bool,
     _globalNoCoverage :: Bool,
     _globalNoStdlib :: Bool,
+    _globalNoCheck :: Bool,
     _globalUnrollLimit :: Int,
     _globalNumThreads :: NumThreads,
     _globalFieldSize :: Maybe Natural,
@@ -72,6 +73,7 @@ defaultGlobalOptions =
       _globalLogLevel = LogLevelProgress,
       _globalNoCoverage = False,
       _globalNoStdlib = False,
+      _globalNoCheck = False,
       _globalUnrollLimit = defaultUnrollLimit,
       _globalFieldSize = Nothing,
       _globalDevShowThreadIds = False,
@@ -162,6 +164,11 @@ parseGlobalFlags = do
                 <> intercalate " < " [show l | l <- allElements @LogLevel]
             )
       )
+  _globalNoCheck <-
+    switch
+      ( long "dev-no-check"
+          <> help "[DEV] Disable input sanity check in Core"
+      )
   _globalShowNameIds <-
     switch
       ( long "show-name-ids"
@@ -211,6 +218,7 @@ entryPointFromGlobalOptions root mainFile opts = do
         _entryPointNoPositivity = opts ^. globalNoPositivity,
         _entryPointNoCoverage = opts ^. globalNoCoverage,
         _entryPointNoStdlib = opts ^. globalNoStdlib,
+        _entryPointNoCheck = opts ^. globalNoCheck,
         _entryPointUnrollLimit = opts ^. globalUnrollLimit,
         _entryPointGenericOptions = project opts,
         _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir,
@@ -232,6 +240,7 @@ entryPointFromGlobalOptionsNoFile root opts = do
         _entryPointNoPositivity = opts ^. globalNoPositivity,
         _entryPointNoCoverage = opts ^. globalNoCoverage,
         _entryPointNoStdlib = opts ^. globalNoStdlib,
+        _entryPointNoCheck = opts ^. globalNoCheck,
         _entryPointUnrollLimit = opts ^. globalUnrollLimit,
         _entryPointGenericOptions = project opts,
         _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir,
diff --git a/examples/demo/Package.juvix b/examples/demo/Package.juvix
index 95fc82192b..39e428effd 100644
--- a/examples/demo/Package.juvix
+++ b/examples/demo/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "Demo";
     version := mkVersion 0 1 0
   };
diff --git a/examples/midsquare/Package.juvix b/examples/midsquare/Package.juvix
index 564be67861..191f097606 100644
--- a/examples/midsquare/Package.juvix
+++ b/examples/midsquare/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "midsquare";
     version := mkVersion 0 1 0
   };
diff --git a/examples/milestone/Bank/Package.juvix b/examples/milestone/Bank/Package.juvix
index f0b0d1db0f..83819477c1 100644
--- a/examples/milestone/Bank/Package.juvix
+++ b/examples/milestone/Bank/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "bank"
   };
diff --git a/examples/milestone/Collatz/Package.juvix b/examples/milestone/Collatz/Package.juvix
index 87fe97ccb4..10d24fc716 100644
--- a/examples/milestone/Collatz/Package.juvix
+++ b/examples/milestone/Collatz/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "Collatz";
     version := mkVersion 0 1 0;
     main := just "Collatz.juvix"
diff --git a/examples/milestone/Fibonacci/Package.juvix b/examples/milestone/Fibonacci/Package.juvix
index eb009b9675..7624e50fb5 100644
--- a/examples/milestone/Fibonacci/Package.juvix
+++ b/examples/milestone/Fibonacci/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "Fibonacci";
     version := mkVersion 0 1 0;
     main := just "Fibonacci.juvix"
diff --git a/examples/milestone/Hanoi/Package.juvix b/examples/milestone/Hanoi/Package.juvix
index 4588aeb0f1..9bb7f6f53e 100644
--- a/examples/milestone/Hanoi/Package.juvix
+++ b/examples/milestone/Hanoi/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "Hanoi";
     version := mkVersion 0 1 0;
     main := just "Hanoi.juvix"
diff --git a/examples/milestone/HelloWorld/Package.juvix b/examples/milestone/HelloWorld/Package.juvix
index 7960036eaf..ec3f84f5c8 100644
--- a/examples/milestone/HelloWorld/Package.juvix
+++ b/examples/milestone/HelloWorld/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "HelloWorld";
     version := mkVersion 0 1 0;
     main := just "HelloWorld.juvix"
diff --git a/examples/milestone/PascalsTriangle/Package.juvix b/examples/milestone/PascalsTriangle/Package.juvix
index a740b3e86b..c6370e1474 100644
--- a/examples/milestone/PascalsTriangle/Package.juvix
+++ b/examples/milestone/PascalsTriangle/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "PascalsTriangle";
     version := mkVersion 0 1 0;
     main := just "PascalsTriangle.juvix"
diff --git a/examples/milestone/TicTacToe/Package.juvix b/examples/milestone/TicTacToe/Package.juvix
index ff3cda7035..edbcb64f7f 100644
--- a/examples/milestone/TicTacToe/Package.juvix
+++ b/examples/milestone/TicTacToe/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "TicTacToe";
     version := mkVersion 0 1 0;
     main := just "CLI/TicTacToe.juvix"
diff --git a/examples/milestone/Tutorial/Package.juvix b/examples/milestone/Tutorial/Package.juvix
index 3c4a4a3ec4..e670c512c8 100644
--- a/examples/milestone/Tutorial/Package.juvix
+++ b/examples/milestone/Tutorial/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "Tutorial";
     version := mkVersion 0 1 0
   };
diff --git a/include/package/PackageDescription/V1.juvix b/include/package/PackageDescription/V1.juvix
index 179e2f6dcf..440e7c81c5 100644
--- a/include/package/PackageDescription/V1.juvix
+++ b/include/package/PackageDescription/V1.juvix
@@ -62,7 +62,7 @@ mkVersion
   {release : Maybe String := nothing}
   {meta : Maybe String := nothing}
   : SemVer :=
-  mkSemVer@?{
+  mkSemVer@{
     major;
     minor;
     patch;
diff --git a/include/package/PackageDescription/V2.juvix b/include/package/PackageDescription/V2.juvix
index dc043f1bc8..bfaf771899 100644
--- a/include/package/PackageDescription/V2.juvix
+++ b/include/package/PackageDescription/V2.juvix
@@ -49,7 +49,7 @@ mkVersion
   {release : Maybe String := nothing}
   {meta : Maybe String := nothing}
   : SemVer :=
-  mkSemVer@?{
+  mkSemVer@{
     major;
     minor;
     patch;
diff --git a/juvix-stdlib b/juvix-stdlib
index 0c456725a2..ff6d964320 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit 0c456725a23648606f97aebf8f74a9e2a73e90b6
+Subproject commit ff6d964320d24e3e8010733afcd886a62a56dd70
diff --git a/src/Juvix/Compiler/Concrete/Gen.hs b/src/Juvix/Compiler/Concrete/Gen.hs
index 828f67bfeb..0c145247cb 100644
--- a/src/Juvix/Compiler/Concrete/Gen.hs
+++ b/src/Juvix/Compiler/Concrete/Gen.hs
@@ -67,16 +67,6 @@ smallUniverseExpression = do
           _expressionAtoms = pure (AtomUniverse (smallUniverse loc))
         }
 
-isExhaustive :: (Member (Reader Interval) r) => Bool -> Sem r IsExhaustive
-isExhaustive _isExhaustive = do
-  _isExhaustiveKw <-
-    Irrelevant
-      <$> if
-          | _isExhaustive -> kw kwAt
-          | otherwise -> kw kwAtQuestion
-
-  return IsExhaustive {..}
-
 symbol :: (Member (Reader Interval) r) => Text -> Sem r Symbol
 symbol t = do
   l <- ask
@@ -107,25 +97,13 @@ braced a = do
   l <- ask
   AtomBraces . WithLoc l <$> expressionAtoms' a
 
-mkIsExhaustive :: (Member (Reader Interval) r) => Bool -> Sem r IsExhaustive
-mkIsExhaustive _isExhaustive = do
-  keyw <-
-    if
-        | _isExhaustive -> kw kwAt
-        | otherwise -> kw kwAtQuestion
-  return
-    IsExhaustive
-      { _isExhaustiveKw = Irrelevant keyw,
-        _isExhaustive
-      }
-
-namedApplication :: Name -> IsExhaustive -> [NamedArgumentNew 'Parsed] -> ExpressionAtom 'Parsed
-namedApplication n exh as =
-  AtomNamedApplicationNew
-    NamedApplicationNew
-      { _namedApplicationNewName = n,
-        _namedApplicationNewExhaustive = exh,
-        _namedApplicationNewArguments = as
+namedApplication :: Name -> Irrelevant KeywordRef -> [NamedArgument 'Parsed] -> ExpressionAtom 'Parsed
+namedApplication n kwd as =
+  AtomNamedApplication
+    NamedApplication
+      { _namedApplicationName = n,
+        _namedApplicationAtKw = kwd,
+        _namedApplicationArguments = as
       }
 
 literalInteger :: (Member (Reader Interval) r, Integral a) => a -> Sem r (ExpressionAtom 'Parsed)
diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs
index 13bbc43089..d5ac822396 100644
--- a/src/Juvix/Compiler/Concrete/Keywords.hs
+++ b/src/Juvix/Compiler/Concrete/Keywords.hs
@@ -28,7 +28,6 @@ import Juvix.Data.Keyword.All
     kwAssign,
     kwAssoc,
     kwAt,
-    kwAtQuestion,
     kwAxiom,
     kwBelow,
     kwBinary,
@@ -88,7 +87,6 @@ reservedKeywords =
     kwAssign,
     kwDeriving,
     kwAt,
-    kwAtQuestion,
     kwAxiom,
     kwCase,
     kwColon,
diff --git a/src/Juvix/Compiler/Concrete/Language/Base.hs b/src/Juvix/Compiler/Concrete/Language/Base.hs
index 357d393bc9..c61e9c583a 100644
--- a/src/Juvix/Compiler/Concrete/Language/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Language/Base.hs
@@ -1635,7 +1635,7 @@ data Expression
   | ExpressionBraces (WithLoc Expression)
   | ExpressionDoubleBraces (DoubleBracesExpression 'Scoped)
   | ExpressionIterator (Iterator 'Scoped)
-  | ExpressionNamedApplicationNew (NamedApplicationNew 'Scoped)
+  | ExpressionNamedApplication (NamedApplication 'Scoped)
   deriving stock (Show, Eq, Ord, Generic)
 
 instance Serialize Expression
@@ -2537,67 +2537,57 @@ deriving stock instance Ord (NamedArgumentPun 'Parsed)
 
 deriving stock instance Ord (NamedArgumentPun 'Scoped)
 
-data NamedArgumentNew (s :: Stage)
-  = NamedArgumentNewFunction (NamedArgumentFunctionDef s)
+data NamedArgument (s :: Stage)
+  = NamedArgumentFunction (NamedArgumentFunctionDef s)
   | NamedArgumentItemPun (NamedArgumentPun s)
   deriving stock (Generic)
 
-instance Serialize (NamedArgumentNew 'Scoped)
+instance Serialize (NamedArgument 'Scoped)
 
-instance NFData (NamedArgumentNew 'Scoped)
+instance NFData (NamedArgument 'Scoped)
 
-instance Serialize (NamedArgumentNew 'Parsed)
+instance Serialize (NamedArgument 'Parsed)
 
-instance NFData (NamedArgumentNew 'Parsed)
+instance NFData (NamedArgument 'Parsed)
 
-deriving stock instance Show (NamedArgumentNew 'Parsed)
+deriving stock instance Show (NamedArgument 'Parsed)
 
-deriving stock instance Show (NamedArgumentNew 'Scoped)
+deriving stock instance Show (NamedArgument 'Scoped)
 
-deriving stock instance Eq (NamedArgumentNew 'Parsed)
+deriving stock instance Eq (NamedArgument 'Parsed)
 
-deriving stock instance Eq (NamedArgumentNew 'Scoped)
+deriving stock instance Eq (NamedArgument 'Scoped)
 
-deriving stock instance Ord (NamedArgumentNew 'Parsed)
+deriving stock instance Ord (NamedArgument 'Parsed)
 
-deriving stock instance Ord (NamedArgumentNew 'Scoped)
+deriving stock instance Ord (NamedArgument 'Scoped)
 
-data IsExhaustive = IsExhaustive
-  { _isExhaustive :: Bool,
-    _isExhaustiveKw :: Irrelevant KeywordRef
-  }
-  deriving stock (Eq, Show, Ord, Generic)
-
-instance Serialize IsExhaustive
-
-instance NFData IsExhaustive
-
-data NamedApplicationNew (s :: Stage) = NamedApplicationNew
-  { _namedApplicationNewName :: IdentifierType s,
-    _namedApplicationNewExhaustive :: IsExhaustive,
-    _namedApplicationNewArguments :: [NamedArgumentNew s]
+data NamedApplication (s :: Stage) = NamedApplication
+  { _namedApplicationName :: IdentifierType s,
+    _namedApplicationAtKw :: Irrelevant KeywordRef,
+    _namedApplicationArguments :: [NamedArgument s]
   }
   deriving stock (Generic)
 
-instance Serialize (NamedApplicationNew 'Scoped)
+instance Serialize (NamedApplication 'Scoped)
 
-instance NFData (NamedApplicationNew 'Scoped)
+instance NFData (NamedApplication 'Scoped)
 
-instance Serialize (NamedApplicationNew 'Parsed)
+instance Serialize (NamedApplication 'Parsed)
 
-instance NFData (NamedApplicationNew 'Parsed)
+instance NFData (NamedApplication 'Parsed)
 
-deriving stock instance Show (NamedApplicationNew 'Parsed)
+deriving stock instance Show (NamedApplication 'Parsed)
 
-deriving stock instance Show (NamedApplicationNew 'Scoped)
+deriving stock instance Show (NamedApplication 'Scoped)
 
-deriving stock instance Eq (NamedApplicationNew 'Parsed)
+deriving stock instance Eq (NamedApplication 'Parsed)
 
-deriving stock instance Eq (NamedApplicationNew 'Scoped)
+deriving stock instance Eq (NamedApplication 'Scoped)
 
-deriving stock instance Ord (NamedApplicationNew 'Parsed)
+deriving stock instance Ord (NamedApplication 'Parsed)
 
-deriving stock instance Ord (NamedApplicationNew 'Scoped)
+deriving stock instance Ord (NamedApplication 'Scoped)
 
 data RecordSyntaxDef (s :: Stage)
   = RecordSyntaxOperator (OperatorSyntaxDef s)
@@ -2741,7 +2731,7 @@ data ExpressionAtom (s :: Stage)
   | AtomLiteral LiteralLoc
   | AtomParens (ExpressionType s)
   | AtomIterator (Iterator s)
-  | AtomNamedApplicationNew (NamedApplicationNew s)
+  | AtomNamedApplication (NamedApplication s)
   deriving stock (Generic)
 
 instance Serialize (ExpressionAtom 'Parsed)
@@ -3000,7 +2990,6 @@ makeLenses ''FunctionLhs
 makeLenses ''Statements
 makeLenses ''NamedArgumentFunctionDef
 makeLenses ''NamedArgumentPun
-makeLenses ''IsExhaustive
 makeLenses ''SideIfBranch
 makeLenses ''RhsExpression
 makeLenses ''PatternArg
@@ -3069,8 +3058,8 @@ makeLenses ''Initializer
 makeLenses ''Range
 makeLenses ''ArgumentBlock
 makeLenses ''NamedArgumentAssign
-makeLenses ''NamedArgumentNew
-makeLenses ''NamedApplicationNew
+makeLenses ''NamedArgument
+makeLenses ''NamedApplication
 makeLenses ''AliasDef
 makeLenses ''FixitySyntaxDef
 makeLenses ''ParsedFixityInfo
@@ -3083,7 +3072,7 @@ makeLenses ''RecordInfo
 makeLenses ''MarkdownInfo
 makeLenses ''Deriving
 
-makePrisms ''NamedArgumentNew
+makePrisms ''NamedArgument
 makePrisms ''ConstructorRhs
 makePrisms ''FunctionDefNameParsed
 
@@ -3176,7 +3165,7 @@ instance (SingI s) => HasLoc (ArgumentBlock s) where
 instance HasAtomicity (ArgumentBlock s) where
   atomicity = const Atom
 
-instance HasAtomicity (NamedApplicationNew s) where
+instance HasAtomicity (NamedApplication s) where
   atomicity = const (Aggregate updateFixity)
 
 instance HasAtomicity (Do s) where
@@ -3203,7 +3192,7 @@ instance HasAtomicity Expression where
     ExpressionCase c -> atomicity c
     ExpressionIf x -> atomicity x
     ExpressionIterator i -> atomicity i
-    ExpressionNamedApplicationNew i -> atomicity i
+    ExpressionNamedApplication i -> atomicity i
     ExpressionRecordUpdate {} -> Aggregate updateFixity
     ExpressionParensRecordUpdate {} -> Atom
 
@@ -3414,9 +3403,9 @@ instance HasLoc (List s) where
 instance (SingI s) => HasLoc (NamedArgumentFunctionDef s) where
   getLoc (NamedArgumentFunctionDef f) = getLoc f
 
-instance (SingI s) => HasLoc (NamedArgumentNew s) where
+instance (SingI s) => HasLoc (NamedArgument s) where
   getLoc = \case
-    NamedArgumentNewFunction f -> getLoc f
+    NamedArgumentFunction f -> getLoc f
     NamedArgumentItemPun f -> getLoc f
 
 instance HasLoc (RecordUpdatePun s) where
@@ -3425,8 +3414,8 @@ instance HasLoc (RecordUpdatePun s) where
 instance HasLoc (NamedArgumentPun s) where
   getLoc NamedArgumentPun {..} = getLocSymbolType _namedArgumentPunSymbol
 
-instance (SingI s) => HasLoc (NamedApplicationNew s) where
-  getLoc NamedApplicationNew {..} = getLocIdentifierType _namedApplicationNewName
+instance (SingI s) => HasLoc (NamedApplication s) where
+  getLoc NamedApplication {..} = getLocIdentifierType _namedApplicationName
 
 instance (SingI s) => HasLoc (RecordUpdateField s) where
   getLoc = \case
@@ -3478,7 +3467,7 @@ instance HasLoc Expression where
     ExpressionBraces i -> getLoc i
     ExpressionDoubleBraces i -> getLoc i
     ExpressionIterator i -> getLoc i
-    ExpressionNamedApplicationNew i -> getLoc i
+    ExpressionNamedApplication i -> getLoc i
     ExpressionRecordUpdate i -> getLoc i
     ExpressionParensRecordUpdate i -> getLoc i
 
@@ -3707,7 +3696,7 @@ instance (SingI s) => HasLoc (ExpressionAtom s) where
     AtomLiteral x -> getLoc x
     AtomParens x -> getLocExpressionType x
     AtomIterator x -> getLoc x
-    AtomNamedApplicationNew x -> getLoc x
+    AtomNamedApplication x -> getLoc x
 
 instance HasLoc (ExpressionAtoms s) where
   getLoc = getLoc . (^. expressionAtomsLoc)
@@ -3769,17 +3758,17 @@ withFunctionSymbol a f sym = case sing :: SStage s of
   SParsed -> maybe a f (sym ^? _FunctionDefName)
   SScoped -> f (sym ^. functionDefNameScoped)
 
-namedArgumentNewSymbolParsed :: (SingI s) => SimpleGetter (NamedArgumentNew s) Symbol
-namedArgumentNewSymbolParsed = to $ \case
+namedArgumentSymbolParsed :: (SingI s) => SimpleGetter (NamedArgument s) Symbol
+namedArgumentSymbolParsed = to $ \case
   NamedArgumentItemPun a -> a ^. namedArgumentPunSymbol
-  NamedArgumentNewFunction a -> symbolParsed (getFunctionSymbol (a ^. namedArgumentFunctionDef . functionDefName))
+  NamedArgumentFunction a -> symbolParsed (getFunctionSymbol (a ^. namedArgumentFunctionDef . functionDefName))
 
-namedArgumentNewSymbol :: Lens' (NamedArgumentNew 'Parsed) Symbol
-namedArgumentNewSymbol f = \case
+namedArgumentSymbol :: Lens' (NamedArgument 'Parsed) Symbol
+namedArgumentSymbol f = \case
   NamedArgumentItemPun a -> NamedArgumentItemPun <$> (namedArgumentPunSymbol f a)
-  NamedArgumentNewFunction a -> do
+  NamedArgumentFunction a -> do
     a' <- f (a ^?! namedArgumentFunctionDef . functionDefName . _FunctionDefName)
-    return $ NamedArgumentNewFunction (over namedArgumentFunctionDef (set functionDefName (FunctionDefName a')) a)
+    return $ NamedArgumentFunction (over namedArgumentFunctionDef (set functionDefName (FunctionDefName a')) a)
 
 scopedIdenSrcName :: Lens' ScopedIden S.Name
 scopedIdenSrcName f n = case n ^. scopedIdenAlias of
diff --git a/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs b/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs
index 064754798f..2f253b6b23 100644
--- a/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs
+++ b/src/Juvix/Compiler/Concrete/Language/IsApeInstances.hs
@@ -81,12 +81,12 @@ instance IsApe Name ApeLeaf where
           _leafExpr = ApeLeafAtom (sing :&: AtomIdentifier n)
         }
 
-instance (SingI s) => IsApe (NamedApplicationNew s) ApeLeaf where
+instance (SingI s) => IsApe (NamedApplication s) ApeLeaf where
   toApe a =
     ApeLeaf $
       Leaf
         { _leafAtomicity = atomicity a,
-          _leafExpr = ApeLeafAtom (sing :&: AtomNamedApplicationNew a)
+          _leafExpr = ApeLeafAtom (sing :&: AtomNamedApplication a)
         }
 
 instance IsApe Application ApeLeaf where
@@ -144,7 +144,7 @@ instance IsApe Expression ApeLeaf where
     ExpressionInfixApplication a -> toApe a
     ExpressionPostfixApplication a -> toApe a
     ExpressionFunction a -> toApe a
-    ExpressionNamedApplicationNew a -> toApe a
+    ExpressionNamedApplication a -> toApe a
     ExpressionRecordUpdate a -> toApe a
     ExpressionParensRecordUpdate {} -> leaf
     ExpressionParensIdentifier {} -> leaf
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index ebe2624012..7ea873494c 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -347,18 +347,15 @@ instance (SingI s) => PrettyPrint (ArgumentBlock s) where
     where
       Irrelevant d = _argBlockDelims
 
-instance PrettyPrint IsExhaustive where
-  ppCode IsExhaustive {..} = ppCode _isExhaustiveKw
-
-instance (SingI s) => PrettyPrint (NamedApplicationNew s) where
-  ppCode NamedApplicationNew {..} = do
+instance (SingI s) => PrettyPrint (NamedApplication s) where
+  ppCode NamedApplication {..} = do
     let args'
-          | null _namedApplicationNewArguments = mempty
-          | otherwise = ppBlock _namedApplicationNewArguments
+          | null _namedApplicationArguments = mempty
+          | otherwise = ppBlock _namedApplicationArguments
     grouped
       ( align
-          ( ppIdentifierType _namedApplicationNewName
-              <> ppCode _namedApplicationNewExhaustive
+          ( ppIdentifierType _namedApplicationName
+              <> ppCode _namedApplicationAtKw
               <> braces args'
           )
       )
@@ -372,9 +369,9 @@ instance PrettyPrint (RecordUpdatePun s) where
 instance PrettyPrint (NamedArgumentPun s) where
   ppCode = ppCode . (^. namedArgumentPunSymbol)
 
-instance (SingI s) => PrettyPrint (NamedArgumentNew s) where
+instance (SingI s) => PrettyPrint (NamedArgument s) where
   ppCode = \case
-    NamedArgumentNewFunction f -> ppCode f
+    NamedArgumentFunction f -> ppCode f
     NamedArgumentItemPun f -> ppCode f
 
 instance (SingI s) => PrettyPrint (RecordSyntaxDef s) where
@@ -472,7 +469,7 @@ instance (SingI s) => PrettyPrint (ExpressionAtom s) where
     AtomHole w -> ppHoleType w
     AtomInstanceHole w -> ppHoleType w
     AtomIterator i -> ppIterator NotTop i
-    AtomNamedApplicationNew i -> ppCode i
+    AtomNamedApplication i -> ppCode i
 
 instance PrettyPrint PatternScopedIden where
   ppCode = \case
@@ -1006,7 +1003,7 @@ instance PrettyPrint Expression where
     ExpressionCase c -> ppCase NotTop c
     ExpressionIf c -> ppIf NotTop c
     ExpressionIterator i -> ppIterator NotTop i
-    ExpressionNamedApplicationNew i -> ppCode i
+    ExpressionNamedApplication i -> ppCode i
     ExpressionRecordUpdate i -> ppCode i
     ExpressionParensRecordUpdate i -> ppCode i
 
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 37d87ea42b..a0eed183eb 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -2909,22 +2909,22 @@ checkExpressionAtom e = case e of
   AtomLiteral l -> return (pure (AtomLiteral l))
   AtomList l -> pure . AtomList <$> checkList l
   AtomIterator i -> pure . AtomIterator <$> checkIterator i
-  AtomNamedApplicationNew i -> pure . AtomNamedApplicationNew <$> checkNamedApplicationNew i
+  AtomNamedApplication i -> pure . AtomNamedApplication <$> checkNamedApplication i
   AtomRecordUpdate i -> pure . AtomRecordUpdate <$> checkRecordUpdate i
 
-reserveNamedArgumentName :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => NamedArgumentNew 'Parsed -> Sem r ()
+reserveNamedArgumentName :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => NamedArgument 'Parsed -> Sem r ()
 reserveNamedArgumentName a = case a of
-  NamedArgumentNewFunction f -> reserveFunctionLikeSymbol (f ^. namedArgumentFunctionDef)
+  NamedArgumentFunction f -> reserveFunctionLikeSymbol (f ^. namedArgumentFunctionDef)
   NamedArgumentItemPun {} -> return ()
 
-checkNamedApplicationNew ::
+checkNamedApplication ::
   forall r.
   (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId] r) =>
-  NamedApplicationNew 'Parsed ->
-  Sem r (NamedApplicationNew 'Scoped)
-checkNamedApplicationNew napp = do
-  let nargs = napp ^. namedApplicationNewArguments
-  aname <- checkScopedIden (napp ^. namedApplicationNewName)
+  NamedApplication 'Parsed ->
+  Sem r (NamedApplication 'Scoped)
+checkNamedApplication napp = do
+  let nargs = napp ^. namedApplicationArguments
+  aname <- checkScopedIden (napp ^. namedApplicationName)
   sig :: NameSignature 'Parsed <-
     if
         | null nargs -> return (NameSignature [])
@@ -2935,25 +2935,25 @@ checkNamedApplicationNew napp = do
             ^.. nameSignatureArgs
               . each
               . nameBlockSymbols
-  forM_ nargs (checkNameInSignature namesInSignature . (^. namedArgumentNewSymbol))
-  puns <- scopePuns (napp ^.. namedApplicationNewArguments . each . _NamedArgumentItemPun)
+  forM_ nargs (checkNameInSignature namesInSignature . (^. namedArgumentSymbol))
+  puns <- scopePuns (napp ^.. namedApplicationArguments . each . _NamedArgumentItemPun)
   args' <- withLocalScope . localBindings . ignoreSyntax $ do
     mapM_ reserveNamedArgumentName nargs
-    mapM (checkNamedArgumentNew puns) nargs
+    mapM (checkNamedArgument puns) nargs
   let signatureExplicitNames =
         hashSet
           . concatMap (^.. nameBlockSymbols)
           . filter (not . isImplicitOrInstance . (^. nameBlockImplicit))
           $ sig ^. nameSignatureArgs
-      givenNames :: HashSet Symbol = hashSet (map (^. namedArgumentNewSymbol) nargs)
+      givenNames :: HashSet Symbol = hashSet (map (^. namedArgumentSymbol) nargs)
       missingArgs = HashSet.difference signatureExplicitNames givenNames
-  unless (null missingArgs || not (napp ^. namedApplicationNewExhaustive . isExhaustive)) $
+  unless (null missingArgs) $
     throw (ErrMissingArgs (MissingArgs (aname ^. scopedIdenFinal . nameConcrete) missingArgs))
   return
-    NamedApplicationNew
-      { _namedApplicationNewName = aname,
-        _namedApplicationNewArguments = args',
-        _namedApplicationNewExhaustive = napp ^. namedApplicationNewExhaustive
+    NamedApplication
+      { _namedApplicationName = aname,
+        _namedApplicationArguments = args',
+        _namedApplicationAtKw = napp ^. namedApplicationAtKw
       }
   where
     checkNameInSignature :: HashSet Symbol -> Symbol -> Sem r ()
@@ -2967,13 +2967,13 @@ checkNamedApplicationNew napp = do
         scopePun :: Symbol -> Sem r ScopedIden
         scopePun = checkScopedIden . NameUnqualified
 
-checkNamedArgumentNew ::
+checkNamedArgument ::
   (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId] r) =>
   HashMap Symbol ScopedIden ->
-  NamedArgumentNew 'Parsed ->
-  Sem r (NamedArgumentNew 'Scoped)
-checkNamedArgumentNew puns = \case
-  NamedArgumentNewFunction f -> NamedArgumentNewFunction <$> checkNamedArgumentFunctionDef f
+  NamedArgument 'Parsed ->
+  Sem r (NamedArgument 'Scoped)
+checkNamedArgument puns = \case
+  NamedArgumentFunction f -> NamedArgumentFunction <$> checkNamedArgumentFunctionDef f
   NamedArgumentItemPun f -> return (NamedArgumentItemPun (checkNamedArgumentItemPun puns f))
 
 checkNamedArgumentItemPun ::
@@ -3597,11 +3597,11 @@ parseTerm =
           _ -> Nothing
 
     parseNamedApplicationNew :: Parse Expression
-    parseNamedApplicationNew = ExpressionNamedApplicationNew <$> P.token namedApp mempty
+    parseNamedApplicationNew = ExpressionNamedApplication <$> P.token namedApp mempty
       where
-        namedApp :: ExpressionAtom 'Scoped -> Maybe (NamedApplicationNew 'Scoped)
+        namedApp :: ExpressionAtom 'Scoped -> Maybe (NamedApplication 'Scoped)
         namedApp s = case s of
-          AtomNamedApplicationNew u -> Just u
+          AtomNamedApplication u -> Just u
           _ -> Nothing
 
     parseLet :: Parse Expression
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index 19a5003b26..47d485b522 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
@@ -882,7 +882,7 @@ expressionAtom =
   P.label "<expression>" $
     AtomLiteral <$> P.try literal
       <|> AtomIterator <$> iterator
-      <|> AtomNamedApplicationNew <$> namedApplicationNew
+      <|> AtomNamedApplication <$> namedApplication
       <|> AtomList <$> parseList
       <|> AtomIf <$> multiwayIf
       <|> AtomIdentifier <$> name
@@ -1041,19 +1041,19 @@ pnamedArgumentItemPun = do
 
 -- | Parses zero or more named arguments. This function is necessary to avoid
 -- using excessive backtracking.
-manyNamedArgumentNewRBrace ::
+manyNamedArgumentRBrace ::
   forall r.
   (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
-  ParsecS r [NamedArgumentNew 'Parsed]
-manyNamedArgumentNewRBrace = reverse <$> go []
+  ParsecS r [NamedArgument 'Parsed]
+manyNamedArgumentRBrace = reverse <$> go []
   where
-    go :: [NamedArgumentNew 'Parsed] -> ParsecS r [NamedArgumentNew 'Parsed]
+    go :: [NamedArgument 'Parsed] -> ParsecS r [NamedArgument 'Parsed]
     go acc =
       rbrace $> acc
         <|> itemHelper (P.try (withIsLast (NamedArgumentItemPun <$> pnamedArgumentItemPun)))
-        <|> itemHelper (withIsLast (NamedArgumentNewFunction <$> pnamedArgumentFunctionDef))
+        <|> itemHelper (withIsLast (NamedArgumentFunction <$> pnamedArgumentFunctionDef))
       where
-        itemHelper :: ParsecS r (Bool, NamedArgumentNew 'Parsed) -> ParsecS r [NamedArgumentNew 'Parsed]
+        itemHelper :: ParsecS r (Bool, NamedArgument 'Parsed) -> ParsecS r [NamedArgument 'Parsed]
         itemHelper p = do
           (isLast, item) <- p
           let acc' = item : acc
@@ -1072,34 +1072,20 @@ manyNamedArgumentNewRBrace = reverse <$> go []
       isLast <- pIsLast
       return (isLast, res)
 
-pisExhaustive ::
-  forall r.
-  (Members '[ParserResultBuilder] r) =>
-  ParsecS r IsExhaustive
-pisExhaustive = do
-  (keyword, exh) <-
-    (,False) <$> kw kwAtQuestion
-      <|> (,True) <$> kw kwAt
-  return
-    IsExhaustive
-      { _isExhaustiveKw = Irrelevant keyword,
-        _isExhaustive = exh
-      }
-
-namedApplicationNew ::
+namedApplication ::
   forall r.
   (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
-  ParsecS r (NamedApplicationNew 'Parsed)
-namedApplicationNew = P.label "<named application>" $ do
+  ParsecS r (NamedApplication 'Parsed)
+namedApplication = P.label "<named application>" $ do
   checkNoNamedApplicationMissingAt
-  (_namedApplicationNewName, _namedApplicationNewExhaustive) <- P.try $ do
+  (_namedApplicationName, _namedApplicationAtKw) <- P.try $ do
     n <- name
-    exhaustive <- pisExhaustive
+    kwd <- Irrelevant <$> kw kwAt
     lbrace
-    return (n, exhaustive)
-  _namedApplicationNewArguments <- manyNamedArgumentNewRBrace
-  let _namedApplicationNewExtra = Irrelevant ()
-  return NamedApplicationNew {..}
+    return (n, kwd)
+  _namedApplicationArguments <- manyNamedArgumentRBrace
+  let _namedApplicationExtra = Irrelevant ()
+  return NamedApplication {..}
 
 hole :: (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (HoleType 'Parsed)
 hole = kw kwHole
diff --git a/src/Juvix/Compiler/Core/Pipeline.hs b/src/Juvix/Compiler/Core/Pipeline.hs
index 51d4d50658..f762bc7278 100644
--- a/src/Juvix/Compiler/Core/Pipeline.hs
+++ b/src/Juvix/Compiler/Core/Pipeline.hs
@@ -7,7 +7,7 @@ where
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation
-import Juvix.Compiler.Pipeline.EntryPoint (EntryPoint)
+import Juvix.Compiler.Pipeline.EntryPoint (EntryPoint, entryPointNoCheck)
 
 toTypechecked :: (Members '[Error JuvixError, Reader EntryPoint] r) => Module -> Sem r Module
 toTypechecked = mapReader fromEntryPoint . applyTransformations toTypecheckTransformations
@@ -19,7 +19,11 @@ toStored = mapReader fromEntryPoint . applyTransformations toStoredTransformatio
 -- | Perform transformations on stored Core necessary before the translation to
 -- Core.Stripped
 toStripped :: (Members '[Error JuvixError, Reader EntryPoint] r) => TransformationId -> Module -> Sem r Module
-toStripped checkId = mapReader fromEntryPoint . applyTransformations (toStrippedTransformations checkId)
+toStripped checkId md = do
+  noCheck <- asks (^. entryPointNoCheck)
+  let checkId' = if noCheck then IdentityTrans else checkId
+  mapReader fromEntryPoint $
+    applyTransformations (toStrippedTransformations checkId') md
 
 -- | Perform transformations on stored Core necessary before the translation to VampIR
 toVampIR :: (Members '[Error JuvixError, Reader EntryPoint] r) => Module -> Sem r Module
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 505f9678b1..a88d4116af 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -1309,7 +1309,7 @@ goListPattern l = localBuiltins $ do
   where
     loc = getLoc l
 
-createArgumentBlocks :: NonEmpty (NamedArgumentNew 'Scoped) -> [NameBlock 'Scoped] -> NonEmpty (ArgumentBlock 'Scoped)
+createArgumentBlocks :: NonEmpty (NamedArgument 'Scoped) -> [NameBlock 'Scoped] -> NonEmpty (ArgumentBlock 'Scoped)
 createArgumentBlocks appargs =
   nonEmpty'
     . run
@@ -1317,9 +1317,9 @@ createArgumentBlocks appargs =
     . evalState args0
     . mapM_ goBlock
   where
-    namedArgumentRefSymbol :: NamedArgumentNew 'Scoped -> S.Symbol
+    namedArgumentRefSymbol :: NamedArgument 'Scoped -> S.Symbol
     namedArgumentRefSymbol = \case
-      NamedArgumentNewFunction p -> p ^. namedArgumentFunctionDef . functionDefName . functionDefNameScoped
+      NamedArgumentFunction p -> p ^. namedArgumentFunctionDef . functionDefName . functionDefNameScoped
       NamedArgumentItemPun p -> over S.nameConcrete fromUnqualified' (p ^. namedArgumentReferencedSymbol . scopedIdenFinal)
     args0 :: HashSet S.Symbol = hashSet (namedArgumentRefSymbol <$> appargs)
     goBlock ::
@@ -1387,7 +1387,7 @@ goExpression = \case
   ExpressionHole h -> return (Internal.ExpressionHole h)
   ExpressionInstanceHole h -> return (Internal.ExpressionInstanceHole (fromHole h))
   ExpressionIterator i -> goIterator i
-  ExpressionNamedApplicationNew i -> goNamedApplicationNew i []
+  ExpressionNamedApplication i -> goNamedApplication i []
   ExpressionRecordUpdate i -> goRecordUpdateApp i
   ExpressionParensRecordUpdate i -> Internal.ExpressionLambda <$> goRecordUpdate (i ^. parensRecordUpdate)
   where
@@ -1396,19 +1396,19 @@ goExpression = \case
       s <- asks (^. S.infoNameSigs)
       runReader s (runNamedArguments fun blocks extraArgs) >>= goDesugaredNamedApplication
 
-    goNamedApplicationNew ::
-      Concrete.NamedApplicationNew 'Scoped ->
+    goNamedApplication ::
+      Concrete.NamedApplication 'Scoped ->
       [Internal.ApplicationArg] ->
       Sem r Internal.Expression
-    goNamedApplicationNew napp extraArgs = case nonEmpty (napp ^. namedApplicationNewArguments) of
-      Nothing -> return (goIden (napp ^. namedApplicationNewName))
+    goNamedApplication napp extraArgs = case nonEmpty (napp ^. namedApplicationArguments) of
+      Nothing -> return (goIden (napp ^. namedApplicationName))
       Just appargs -> do
-        let name = napp ^. namedApplicationNewName . scopedIdenFinal
+        let name = napp ^. namedApplicationName . scopedIdenFinal
         sig <- fromJust <$> asks (^. S.infoNameSigs . at (name ^. S.nameId))
-        let fun = napp ^. namedApplicationNewName
+        let fun = napp ^. namedApplicationName
             blocks = createArgumentBlocks appargs (sig ^. nameSignatureArgs)
         compiledNameApp <- goNamedApplication' fun blocks extraArgs
-        case nonEmpty (appargs ^.. each . _NamedArgumentNewFunction) of
+        case nonEmpty (appargs ^.. each . _NamedArgumentFunction) of
           Nothing -> return compiledNameApp
           Just funs -> do
             cls <- funDefsToClauses funs
@@ -1650,7 +1650,7 @@ goExpression = \case
       let (f, args) = unfoldApp a
       args' <- toList <$> mapM goApplicationArg args
       case f of
-        ExpressionNamedApplicationNew n -> goNamedApplicationNew n args'
+        ExpressionNamedApplication n -> goNamedApplication n args'
         _ -> do
           f' <- goExpression f
           return (Internal.foldApplication f' args')
diff --git a/src/Juvix/Compiler/Pipeline/EntryPoint.hs b/src/Juvix/Compiler/Pipeline/EntryPoint.hs
index cf23d9892b..df487703b4 100644
--- a/src/Juvix/Compiler/Pipeline/EntryPoint.hs
+++ b/src/Juvix/Compiler/Pipeline/EntryPoint.hs
@@ -33,6 +33,8 @@ data EntryPoint = EntryPoint
     _entryPointTarget :: Maybe Target,
     _entryPointDebug :: Bool,
     _entryPointUnsafe :: Bool,
+    -- | Skip the correctness check in the Core pipeline part.
+    _entryPointNoCheck :: Bool,
     _entryPointUnrollLimit :: Int,
     _entryPointOptimizationLevel :: Int,
     _entryPointInliningDepth :: Int,
@@ -76,6 +78,7 @@ defaultEntryPointNoFile pkg root =
       _entryPointTarget = Nothing,
       _entryPointDebug = False,
       _entryPointUnsafe = False,
+      _entryPointNoCheck = False,
       _entryPointUnrollLimit = defaultUnrollLimit,
       _entryPointOptimizationLevel = defaultOptimizationLevel,
       _entryPointInliningDepth = defaultInliningDepth,
diff --git a/src/Juvix/Compiler/Pipeline/Package/Loader/Versions.hs b/src/Juvix/Compiler/Pipeline/Package/Loader/Versions.hs
index 6f70e8e374..9f63205073 100644
--- a/src/Juvix/Compiler/Pipeline/Package/Loader/Versions.hs
+++ b/src/Juvix/Compiler/Pipeline/Package/Loader/Versions.hs
@@ -116,9 +116,9 @@ v1v2FromPackage p = run . runReader l $ do
       Sem r (NonEmpty (ExpressionAtom 'Parsed))
     defaultPackageWithArgs as = do
       defaultPackageName' <- NameUnqualified <$> symbol defaultPackageStr
-      exhaustive <- mkIsExhaustive False
-      let args = fmap (NamedArgumentNewFunction . NamedArgumentFunctionDef) as
-          defaultPackageArg = namedApplication defaultPackageName' exhaustive (toList args)
+      kwd <- kw kwAt
+      let args = fmap (NamedArgumentFunction . NamedArgumentFunctionDef) as
+          defaultPackageArg = namedApplication defaultPackageName' (Irrelevant kwd) (toList args)
       return (defaultPackageArg :| [])
 
     l :: Interval
diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs
index cb5541eab3..cfac78a381 100644
--- a/src/Juvix/Data/Keyword/All.hs
+++ b/src/Juvix/Data/Keyword/All.hs
@@ -61,9 +61,6 @@ kwExclamation = asciiKw Str.exclamation
 kwAt :: Keyword
 kwAt = asciiKw Str.at_
 
-kwAtQuestion :: Keyword
-kwAtQuestion = asciiKw Str.atQuestion
-
 kwAxiom :: Keyword
 kwAxiom = asciiKw Str.axiom
 
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index a3ca02cbb2..36df2a8be6 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -653,9 +653,6 @@ underscore = "_"
 at_ :: (IsString s) => s
 at_ = "@"
 
-atQuestion :: (IsString s) => s
-atQuestion = "@?"
-
 dot :: (IsString s) => s
 dot = "."
 
diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs
index b87950a646..4703377126 100644
--- a/test/Scope/Negative.hs
+++ b/test/Scope/Negative.hs
@@ -223,7 +223,7 @@ scoperErrorTests =
       "Missing argument"
       $(mkRelDir ".")
       $(mkRelFile "MissingArgument.juvix")
-      $ wantsError ErrNamedArgumentsError,
+      $ wantsError ErrMissingArgs,
     negTest
       "Repeated name in name signature"
       $(mkRelDir ".")
diff --git a/tests/Anoma/Compilation/positive/Package.juvix b/tests/Anoma/Compilation/positive/Package.juvix
index 39b0d6b001..b1b787384a 100644
--- a/tests/Anoma/Compilation/positive/Package.juvix
+++ b/tests/Anoma/Compilation/positive/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "positive";
   };
diff --git a/tests/Anoma/Compilation/positive/test067.juvix b/tests/Anoma/Compilation/positive/test067.juvix
index 5c1b90d87d..2c72c42842 100644
--- a/tests/Anoma/Compilation/positive/test067.juvix
+++ b/tests/Anoma/Compilation/positive/test067.juvix
@@ -6,6 +6,6 @@ import Stdlib.Data.Nat open;
 f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c;
 
 main : Nat :=
-  f@?{
+  f@{
     c := 5
   };
diff --git a/tests/Anoma/Compilation/positive/test069.juvix b/tests/Anoma/Compilation/positive/test069.juvix
index 3500b88af9..0fce3fcef3 100644
--- a/tests/Anoma/Compilation/positive/test069.juvix
+++ b/tests/Anoma/Compilation/positive/test069.juvix
@@ -23,7 +23,7 @@ mkOrdHelper
   : Ord A := mkOrd cmp lt gt;
 
 ordNatNamed : Ord Nat :=
-  mkOrdHelper@?{
+  mkOrdHelper@{
     cmp := Ord.compare
   };
 
diff --git a/tests/Anoma/Compilation/positive/test070.juvix b/tests/Anoma/Compilation/positive/test070.juvix
index 9a9b0f653e..a969a12453 100644
--- a/tests/Anoma/Compilation/positive/test070.juvix
+++ b/tests/Anoma/Compilation/positive/test070.juvix
@@ -6,13 +6,13 @@ import Stdlib.Data.Nat open;
 fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c;
 
 main : Nat :=
-  fun@?{
+  fun@{
     a := fun;
     b :=
-      fun@?{
+      fun@{
           b := 3
         }
-        * fun@?{
+        * fun@{
           b := fun {2}
         }
   };
diff --git a/tests/Anoma/Compilation/positive/test071.juvix b/tests/Anoma/Compilation/positive/test071.juvix
index e24bf1ec60..a3f6207795 100644
--- a/tests/Anoma/Compilation/positive/test071.juvix
+++ b/tests/Anoma/Compilation/positive/test071.juvix
@@ -39,5 +39,5 @@ h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d;
 
 main : Nat :=
   fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} +
-  f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 +
-  h@?{b := 4} 1;
+  f@{c := 5} + \{c := g@{b := 4; c}} 3 + ite (Ord.lt 1 0) 1 0 +
+  \{c := h@{b := 4; c}} 1;
diff --git a/tests/Anoma/Compilation/positive/test072/Package.juvix b/tests/Anoma/Compilation/positive/test072/Package.juvix
index 16589dc288..398af60eb6 100644
--- a/tests/Anoma/Compilation/positive/test072/Package.juvix
+++ b/tests/Anoma/Compilation/positive/test072/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "monads"
   };
diff --git a/tests/Anoma/Compilation/positive/test073/Package.juvix b/tests/Anoma/Compilation/positive/test073/Package.juvix
index eec3c8b6d8..2957205c2f 100644
--- a/tests/Anoma/Compilation/positive/test073/Package.juvix
+++ b/tests/Anoma/Compilation/positive/test073/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "test073"
   };
diff --git a/tests/Anoma/Compilation/positive/test085/Package.juvix b/tests/Anoma/Compilation/positive/test085/Package.juvix
index 613da5f3b1..5cb6655c31 100644
--- a/tests/Anoma/Compilation/positive/test085/Package.juvix
+++ b/tests/Anoma/Compilation/positive/test085/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "test085";
     dependencies := [defaultStdlib; path "client/"];
   };
diff --git a/tests/Anoma/Compilation/positive/test085/client/Package.juvix b/tests/Anoma/Compilation/positive/test085/client/Package.juvix
index 7a1c28caf9..8a384a4fdd 100644
--- a/tests/Anoma/Compilation/positive/test085/client/Package.juvix
+++ b/tests/Anoma/Compilation/positive/test085/client/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "addtransaction";
   };
diff --git a/tests/Casm/Compilation/positive/test067.juvix b/tests/Casm/Compilation/positive/test067.juvix
index 5c1b90d87d..2c72c42842 100644
--- a/tests/Casm/Compilation/positive/test067.juvix
+++ b/tests/Casm/Compilation/positive/test067.juvix
@@ -6,6 +6,6 @@ import Stdlib.Data.Nat open;
 f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c;
 
 main : Nat :=
-  f@?{
+  f@{
     c := 5
   };
diff --git a/tests/Casm/Compilation/positive/test069.juvix b/tests/Casm/Compilation/positive/test069.juvix
index 3ed821fd77..965abebcfa 100644
--- a/tests/Casm/Compilation/positive/test069.juvix
+++ b/tests/Casm/Compilation/positive/test069.juvix
@@ -23,7 +23,7 @@ mkOrdHelper
   : Ord A := mkOrd cmp lt gt;
 
 ordNatNamed : Ord Nat :=
-  mkOrdHelper@?{
+  mkOrdHelper@{
     cmp := Ord.compare
   };
 
diff --git a/tests/Casm/Compilation/positive/test070.juvix b/tests/Casm/Compilation/positive/test070.juvix
index 9a9b0f653e..a969a12453 100644
--- a/tests/Casm/Compilation/positive/test070.juvix
+++ b/tests/Casm/Compilation/positive/test070.juvix
@@ -6,13 +6,13 @@ import Stdlib.Data.Nat open;
 fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c;
 
 main : Nat :=
-  fun@?{
+  fun@{
     a := fun;
     b :=
-      fun@?{
+      fun@{
           b := 3
         }
-        * fun@?{
+        * fun@{
           b := fun {2}
         }
   };
diff --git a/tests/Casm/Compilation/positive/test071.juvix b/tests/Casm/Compilation/positive/test071.juvix
index e24bf1ec60..a3f6207795 100644
--- a/tests/Casm/Compilation/positive/test071.juvix
+++ b/tests/Casm/Compilation/positive/test071.juvix
@@ -39,5 +39,5 @@ h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d;
 
 main : Nat :=
   fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} +
-  f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 +
-  h@?{b := 4} 1;
+  f@{c := 5} + \{c := g@{b := 4; c}} 3 + ite (Ord.lt 1 0) 1 0 +
+  \{c := h@{b := 4; c}} 1;
diff --git a/tests/Casm/Compilation/positive/test072/Package.juvix b/tests/Casm/Compilation/positive/test072/Package.juvix
index 16589dc288..398af60eb6 100644
--- a/tests/Casm/Compilation/positive/test072/Package.juvix
+++ b/tests/Casm/Compilation/positive/test072/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "monads"
   };
diff --git a/tests/Casm/Compilation/positive/test073/Package.juvix b/tests/Casm/Compilation/positive/test073/Package.juvix
index eec3c8b6d8..2957205c2f 100644
--- a/tests/Casm/Compilation/positive/test073/Package.juvix
+++ b/tests/Casm/Compilation/positive/test073/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "test073"
   };
diff --git a/tests/Compilation/positive/test061.juvix b/tests/Compilation/positive/test061.juvix
index 4aa0406cd0..0fc77ee840 100644
--- a/tests/Compilation/positive/test061.juvix
+++ b/tests/Compilation/positive/test061.juvix
@@ -12,7 +12,7 @@ Bool' : Type := Bool;
 
 instance
 showStringI : Show String :=
-  mkShow@?{
+  mkShow@{
     show := id
   };
 
@@ -24,7 +24,7 @@ showBoolI : Show' Bool' :=
 
 instance
 showNatI : Show Nat :=
-  mkShow@?{
+  mkShow@{
     show := natToString
   };
 
@@ -97,7 +97,7 @@ main : IO :=
     >>> printStringLn (f'4 [just [1]; nothing; just [2; 3]])
     >>> printStringLn (f'3 "abba")
     >>> printStringLn
-      (f'3@?{
+      (f'3@{
           M := mkShow λ {x := x ++str "!"}
         }
         "abba")
diff --git a/tests/Compilation/positive/test067.juvix b/tests/Compilation/positive/test067.juvix
index de3721c21d..f761d569cf 100644
--- a/tests/Compilation/positive/test067.juvix
+++ b/tests/Compilation/positive/test067.juvix
@@ -7,6 +7,6 @@ f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat :=
   a * b * c;
 
 main : Nat :=
-  f@?{
+  f@{
     c := 5
   };
diff --git a/tests/Compilation/positive/test069.juvix b/tests/Compilation/positive/test069.juvix
index 3500b88af9..0fce3fcef3 100644
--- a/tests/Compilation/positive/test069.juvix
+++ b/tests/Compilation/positive/test069.juvix
@@ -23,7 +23,7 @@ mkOrdHelper
   : Ord A := mkOrd cmp lt gt;
 
 ordNatNamed : Ord Nat :=
-  mkOrdHelper@?{
+  mkOrdHelper@{
     cmp := Ord.compare
   };
 
diff --git a/tests/Compilation/positive/test070.juvix b/tests/Compilation/positive/test070.juvix
index a7fe2c428d..76fcf68ba3 100644
--- a/tests/Compilation/positive/test070.juvix
+++ b/tests/Compilation/positive/test070.juvix
@@ -6,13 +6,13 @@ import Stdlib.Data.Nat open;
 fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c;
 
 main : Nat :=
-  fun@?{
+  fun@{
     a := fun;
     b :=
-      fun@?{
+      fun@{
         b := 3;
       }
-        * fun@?{
+        * fun@{
             b := fun {2};
           };
   };
diff --git a/tests/Compilation/positive/test071.juvix b/tests/Compilation/positive/test071.juvix
index 0cbb9e7dbf..caddcbbdc5 100644
--- a/tests/Compilation/positive/test071.juvix
+++ b/tests/Compilation/positive/test071.juvix
@@ -57,12 +57,16 @@ main : Nat :=
     + f@{
         c := 5;
       }
-    + g@?{
-        b := 4;
-      }
+    + \{c :=
+        g@{
+          b := 4;
+          c;
+        }}
       3
     + ite (Ord.lt 1 0) 1 0
-    + h@?{
-        b := 4;
-      }
+    + \{c :=
+        h@{
+          b := 4;
+          c;
+        }}
       1;
diff --git a/tests/Compilation/positive/test072/Package.juvix b/tests/Compilation/positive/test072/Package.juvix
index 16589dc288..398af60eb6 100644
--- a/tests/Compilation/positive/test072/Package.juvix
+++ b/tests/Compilation/positive/test072/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "monads"
   };
diff --git a/tests/Compilation/positive/test073/Package.juvix b/tests/Compilation/positive/test073/Package.juvix
index eec3c8b6d8..2957205c2f 100644
--- a/tests/Compilation/positive/test073/Package.juvix
+++ b/tests/Compilation/positive/test073/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "test073"
   };
diff --git a/tests/Internal/positive/Dependencies/Dep1/Package.juvix b/tests/Internal/positive/Dependencies/Dep1/Package.juvix
index bd6138a7a3..a8be479651 100644
--- a/tests/Internal/positive/Dependencies/Dep1/Package.juvix
+++ b/tests/Internal/positive/Dependencies/Dep1/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "dep1";
     dependencies := []
   };
diff --git a/tests/Internal/positive/Dependencies/Dep2/Package.juvix b/tests/Internal/positive/Dependencies/Dep2/Package.juvix
index a32d05f4db..99c5086184 100644
--- a/tests/Internal/positive/Dependencies/Dep2/Package.juvix
+++ b/tests/Internal/positive/Dependencies/Dep2/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "dep2";
     dependencies := []
   };
diff --git a/tests/Rust/Compilation/positive/test067.juvix b/tests/Rust/Compilation/positive/test067.juvix
index 5c1b90d87d..2c72c42842 100644
--- a/tests/Rust/Compilation/positive/test067.juvix
+++ b/tests/Rust/Compilation/positive/test067.juvix
@@ -6,6 +6,6 @@ import Stdlib.Data.Nat open;
 f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c;
 
 main : Nat :=
-  f@?{
+  f@{
     c := 5
   };
diff --git a/tests/Rust/Compilation/positive/test069.juvix b/tests/Rust/Compilation/positive/test069.juvix
index 3ed821fd77..965abebcfa 100644
--- a/tests/Rust/Compilation/positive/test069.juvix
+++ b/tests/Rust/Compilation/positive/test069.juvix
@@ -23,7 +23,7 @@ mkOrdHelper
   : Ord A := mkOrd cmp lt gt;
 
 ordNatNamed : Ord Nat :=
-  mkOrdHelper@?{
+  mkOrdHelper@{
     cmp := Ord.compare
   };
 
diff --git a/tests/Rust/Compilation/positive/test070.juvix b/tests/Rust/Compilation/positive/test070.juvix
index 9a9b0f653e..a969a12453 100644
--- a/tests/Rust/Compilation/positive/test070.juvix
+++ b/tests/Rust/Compilation/positive/test070.juvix
@@ -6,13 +6,13 @@ import Stdlib.Data.Nat open;
 fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} : Nat := a * b + c;
 
 main : Nat :=
-  fun@?{
+  fun@{
     a := fun;
     b :=
-      fun@?{
+      fun@{
           b := 3
         }
-        * fun@?{
+        * fun@{
           b := fun {2}
         }
   };
diff --git a/tests/Rust/Compilation/positive/test071.juvix b/tests/Rust/Compilation/positive/test071.juvix
index e24bf1ec60..a3f6207795 100644
--- a/tests/Rust/Compilation/positive/test071.juvix
+++ b/tests/Rust/Compilation/positive/test071.juvix
@@ -39,5 +39,5 @@ h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d;
 
 main : Nat :=
   fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} +
-  f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 +
-  h@?{b := 4} 1;
+  f@{c := 5} + \{c := g@{b := 4; c}} 3 + ite (Ord.lt 1 0) 1 0 +
+  \{c := h@{b := 4; c}} 1;
diff --git a/tests/Rust/Compilation/positive/test072/Package.juvix b/tests/Rust/Compilation/positive/test072/Package.juvix
index 16589dc288..398af60eb6 100644
--- a/tests/Rust/Compilation/positive/test072/Package.juvix
+++ b/tests/Rust/Compilation/positive/test072/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "monads"
   };
diff --git a/tests/Rust/Compilation/positive/test073/Package.juvix b/tests/Rust/Compilation/positive/test073/Package.juvix
index eec3c8b6d8..2957205c2f 100644
--- a/tests/Rust/Compilation/positive/test073/Package.juvix
+++ b/tests/Rust/Compilation/positive/test073/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "test073"
   };
diff --git a/tests/negative/DuplicateArgument.juvix b/tests/negative/DuplicateArgument.juvix
index 362ce08e77..2a0fa6ed83 100644
--- a/tests/negative/DuplicateArgument.juvix
+++ b/tests/negative/DuplicateArgument.juvix
@@ -5,7 +5,7 @@ type T := t : T;
 f (a : T) : T := t;
 
 x : T :=
-  f@?{
+  f@{
     a := t;
     a := t
   };
diff --git a/tests/negative/MissingArgument.juvix b/tests/negative/MissingArgument.juvix
index b31fe67e18..5228425089 100644
--- a/tests/negative/MissingArgument.juvix
+++ b/tests/negative/MissingArgument.juvix
@@ -5,6 +5,6 @@ type T := t : T;
 f (a : T) (b : T) : T := t;
 
 x : T :=
-  f@?{
+  f@{
     b := t
   };
diff --git a/tests/negative/NoDependencies/Package.juvix b/tests/negative/NoDependencies/Package.juvix
index a6223b86a4..cfab3cce78 100644
--- a/tests/negative/NoDependencies/Package.juvix
+++ b/tests/negative/NoDependencies/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     dependencies := []
   };
diff --git a/tests/negative/NoNamedArguments.juvix b/tests/negative/NoNamedArguments.juvix
index 367e11e4a3..b895aeb437 100644
--- a/tests/negative/NoNamedArguments.juvix
+++ b/tests/negative/NoNamedArguments.juvix
@@ -2,6 +2,6 @@ module NoNamedArguments;
 
 axiom T : Type;
 
-axiom B : T@?{
+axiom B : T@{
   x := Type
 };
diff --git a/tests/negative/Package/PackageJuvixDuplicateDependencies/Package.juvix b/tests/negative/Package/PackageJuvixDuplicateDependencies/Package.juvix
index 8005e06fd7..2cefd28b35 100644
--- a/tests/negative/Package/PackageJuvixDuplicateDependencies/Package.juvix
+++ b/tests/negative/Package/PackageJuvixDuplicateDependencies/Package.juvix
@@ -2,6 +2,6 @@ module Package;
 
 import PackageDescription.V2 open;
 
-package : Package := defaultPackage@?{name := "abc"; version := mkVersion 0 0 1 ; dependencies := [ github "org" "repo" "ref1" ; github "org" "repo" "ref2" ]};
+package : Package := defaultPackage@{name := "abc"; version := mkVersion 0 0 1 ; dependencies := [ github "org" "repo" "ref1" ; github "org" "repo" "ref2" ]};
 
 main : Package := package;
diff --git a/tests/negative/UnexpectedArgument.juvix b/tests/negative/UnexpectedArgument.juvix
index 4bc72c7ef4..10fb1b7096 100644
--- a/tests/negative/UnexpectedArgument.juvix
+++ b/tests/negative/UnexpectedArgument.juvix
@@ -5,6 +5,6 @@ type T := t : T;
 f (a : T) : T := t;
 
 x : T :=
-  f@?{
+  f@{
     x := t
   };
diff --git a/tests/negative/UnexpectedArgumentWildcard.juvix b/tests/negative/UnexpectedArgumentWildcard.juvix
index 52921d51d1..9487c9a9d8 100644
--- a/tests/negative/UnexpectedArgumentWildcard.juvix
+++ b/tests/negative/UnexpectedArgumentWildcard.juvix
@@ -6,7 +6,7 @@ f (a : T) : {_ : Type} -> (b : T) -> T
   | b := t;
 
 x : T :=
-  f@?{
+  f@{
     a := t;
     b := t
   };
diff --git a/tests/negative/issue2771/Package.juvix b/tests/negative/issue2771/Package.juvix
index a92a023e82..03b434d675 100644
--- a/tests/negative/issue2771/Package.juvix
+++ b/tests/negative/issue2771/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "issue2771"
   };
diff --git a/tests/negative/issue3161/Package.juvix b/tests/negative/issue3161/Package.juvix
index 91d7741540..5df850b097 100644
--- a/tests/negative/issue3161/Package.juvix
+++ b/tests/negative/issue3161/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "stdlib";
     version := mkVersion 0 0 1;
     dependencies := []
diff --git a/tests/positive/ConfluentScoping/Package.juvix b/tests/positive/ConfluentScoping/Package.juvix
index 2bf8b10d1e..84bdf2b93b 100644
--- a/tests/positive/ConfluentScoping/Package.juvix
+++ b/tests/positive/ConfluentScoping/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "confluentscoping"
   };
diff --git a/tests/positive/Dependencies/.libs/Extra/Package.juvix b/tests/positive/Dependencies/.libs/Extra/Package.juvix
index 2bfda863c1..f0d985b351 100644
--- a/tests/positive/Dependencies/.libs/Extra/Package.juvix
+++ b/tests/positive/Dependencies/.libs/Extra/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "extra";
     version := mkVersion 1 0 0;
     dependencies := [defaultStdlib; path "../Base"]
diff --git a/tests/positive/Dependencies/Package.juvix b/tests/positive/Dependencies/Package.juvix
index 338e18b9d8..438c552fc3 100644
--- a/tests/positive/Dependencies/Package.juvix
+++ b/tests/positive/Dependencies/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "main-project";
     version := mkVersion 0 0 1;
     dependencies :=
diff --git a/tests/positive/FancyPaths/Package.juvix b/tests/positive/FancyPaths/Package.juvix
index 8cac8ffad8..6317db5113 100644
--- a/tests/positive/FancyPaths/Package.juvix
+++ b/tests/positive/FancyPaths/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     dependencies :=
       [ path "../FancyPaths/././path with spaces"
       ; path "$(JUVIX_TEST_PATH)/../$(JUVIX_TEST_PATH)/"
diff --git a/tests/positive/FancyPaths/home/Package.juvix b/tests/positive/FancyPaths/home/Package.juvix
index a6223b86a4..cfab3cce78 100644
--- a/tests/positive/FancyPaths/home/Package.juvix
+++ b/tests/positive/FancyPaths/home/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     dependencies := []
   };
diff --git a/tests/positive/FancyPaths/other dep/Package.juvix b/tests/positive/FancyPaths/other dep/Package.juvix
index a6223b86a4..cfab3cce78 100644
--- a/tests/positive/FancyPaths/other dep/Package.juvix	
+++ b/tests/positive/FancyPaths/other dep/Package.juvix	
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     dependencies := []
   };
diff --git a/tests/positive/FancyPaths/path with spaces/Package.juvix b/tests/positive/FancyPaths/path with spaces/Package.juvix
index a6223b86a4..cfab3cce78 100644
--- a/tests/positive/FancyPaths/path with spaces/Package.juvix	
+++ b/tests/positive/FancyPaths/path with spaces/Package.juvix	
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     dependencies := []
   };
diff --git a/tests/positive/ImportNestedLocalModule/Package.juvix b/tests/positive/ImportNestedLocalModule/Package.juvix
index 59641083b1..a74778ee7f 100644
--- a/tests/positive/ImportNestedLocalModule/Package.juvix
+++ b/tests/positive/ImportNestedLocalModule/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "test074"
   };
diff --git a/tests/positive/Internal/Positivity2/Package.juvix b/tests/positive/Internal/Positivity2/Package.juvix
index dc768cdde3..52600bdb7c 100644
--- a/tests/positive/Internal/Positivity2/Package.juvix
+++ b/tests/positive/Internal/Positivity2/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "positivity2";
     dependencies := []
   };
diff --git a/tests/positive/Isabelle/Package.juvix b/tests/positive/Isabelle/Package.juvix
index b692045cc2..1ac1d4bb85 100644
--- a/tests/positive/Isabelle/Package.juvix
+++ b/tests/positive/Isabelle/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "isabelle"
   };
diff --git a/tests/positive/Markdown/markdown/Test.md b/tests/positive/Markdown/markdown/Test.md
index f0c03c84c4..17d4080331 100644
--- a/tests/positive/Markdown/markdown/Test.md
+++ b/tests/positive/Markdown/markdown/Test.md
@@ -23,7 +23,7 @@ You can pass a number to the `extract-module-statements` attribute to drop that
 
 Commands like `typecheck` and `compile` can be used with Juvix Markdown files.
 
-<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="YTest:17"><span class="annot"><a href="X#YTest:17" class="ju-code-link ju-function"><span class="annot"><a href="X#YTest:17" class="ju-code-link ju-function"><span class="ju-function">main</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YStdlib.System.IO.Base:1" class="ju-code-link ju-inductive"><span class="ju-axiom">IO</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YStdlib.System.IO.String:2" class="ju-code-link ju-function"><span class="ju-axiom">readLn</span></a></span> <span class="annot"><a href="X#YStdlib.System.IO.Nat:2" class="ju-code-link ju-function"><span class="ju-function"><span class="ju-delimiter">(</span>printNatLn</span></a></span> <span class="annot"><a href="X#YStdlib.Function:1" class="ju-code-link ju-function"><span class="ju-function">&lt;&lt;</span></a></span> <span class="annot"><a href="X#YTest:2" class="ju-code-link ju-function"><span class="ju-function">fibonacci</span></a></span> <span class="annot"><a href="X#YStdlib.Function:1" class="ju-code-link ju-function"><span class="ju-function">&lt;&lt;</span></a></span> <span class="annot"><a href="X#YStdlib.Data.Nat:2" class="ju-code-link ju-function"><span class="ju-axiom">stringToNat</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span></pre></code></pre>
+<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="YTest:17"><span class="annot"><a href="X#YTest:17" class="ju-code-link ju-function"><span class="annot"><a href="X#YTest:17" class="ju-code-link ju-function"><span class="ju-function">main</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#YStdlib.System.IO.Base:1" class="ju-code-link ju-inductive"><span class="ju-axiom">IO</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#YStdlib.System.IO.String:2" class="ju-code-link ju-function"><span class="ju-axiom">readLn</span></a></span> <span class="annot"><a href="X#YStdlib.System.IO.Nat:2" class="ju-code-link ju-function"><span class="ju-function"><span class="ju-delimiter">(</span>printNatLn</span></a></span> <span class="annot"><a href="X#YStdlib.Function:1" class="ju-code-link ju-function"><span class="ju-function">&lt;&lt;</span></a></span> <span class="annot"><a href="X#YTest:2" class="ju-code-link ju-function"><span class="ju-function">fibonacci</span></a></span> <span class="annot"><a href="X#YStdlib.Function:1" class="ju-code-link ju-function"><span class="ju-function">&lt;&lt;</span></a></span> <span class="annot"><a href="X#YStdlib.Data.Nat:3" class="ju-code-link ju-function"><span class="ju-axiom">stringToNat</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span></pre></code></pre>
 
 Other code blocks are not touched, e.g:
 
diff --git a/tests/positive/MarkdownImport/Package.juvix b/tests/positive/MarkdownImport/Package.juvix
index b1daecbbdc..39e9528bf2 100644
--- a/tests/positive/MarkdownImport/Package.juvix
+++ b/tests/positive/MarkdownImport/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "MarkdownImport"
   };
diff --git a/tests/positive/NamedArguments.juvix b/tests/positive/NamedArguments.juvix
index 2365591bca..f158ae319e 100644
--- a/tests/positive/NamedArguments.juvix
+++ b/tests/positive/NamedArguments.juvix
@@ -22,7 +22,7 @@ axiom fun1 : (a : Type) -> (b : Type) -> {c : Type} -> Type;
 
 -- all provided by name
 t1 : Type :=
-  fun1@?{
+  fun1@{
     a := A;
     b := B;
     c := C
@@ -30,7 +30,7 @@ t1 : Type :=
 
 -- skip implicit at the end
 t1' : {_ : Type} -> Type :=
-  fun1@?{
+  fun1@{
     b := B;
     a := A
   };
@@ -43,7 +43,7 @@ axiom fun2 : (a : Type)
 
 -- skip implicit in implicit group
 t2 : {_ : Type} -> Type :=
-  fun2@?{
+  fun2@{
     a := A;
     b := B;
     c := D
@@ -57,7 +57,7 @@ axiom fun3 : (a : Type)
 
 -- skip implicit in the middle
 t3 : Type :=
-  fun3@?{
+  fun3@{
     a := A;
     b := B;
     d := unit
@@ -71,7 +71,7 @@ axiom fun4 : (a : Type)
 
 -- skip implicit in the middle
 t4 : Type :=
-  fun4@?{
+  fun4@{
     a := A;
     b := B;
     d := unit
@@ -85,7 +85,7 @@ axiom fun5 : (a : Type)
   -> Type;
 
 t5 : Type :=
-  fun5@?{
+  fun5@{
     a := A;
     b := B;
     d' := unit;
@@ -93,7 +93,7 @@ t5 : Type :=
   };
 
 t5' : Type :=
-  fun5@?{
+  fun5@{
     a := A;
     b := B;
     d' := unit;
@@ -109,7 +109,7 @@ axiom fun6 : {a : Type}
   -> Type;
 
 t6 : Type :=
-  fun6@?{
+  fun6@{
     b := B;
     d' := unit;
     d := unit;
@@ -117,7 +117,7 @@ t6 : Type :=
   };
 
 t6' : Type :=
-  fun6@?{
+  fun6@{
     d' := unit;
     d := unit;
     a' := unit;
@@ -129,18 +129,18 @@ module FakeRecord;
     mkPair : (fst : A) -> (snd : B) -> Pair A B;
 
   pp
-    : Pair@?{
+    : Pair@{
       B := Unit;
       A := Type
     } :=
-    mkPair@?{
+    mkPair@{
       snd := unit;
       fst := Type
     };
 
   pp2
-    : Pair@?{
+    : Pair@{
       B := Unit;
       A := Type
-    } := mkPair@?{fst := Type} (unit);
+    } := \{snd := mkPair@{fst := Type; snd}} (unit);
 end;
diff --git a/tests/positive/NoDependencies/Package.juvix b/tests/positive/NoDependencies/Package.juvix
index a6223b86a4..cfab3cce78 100644
--- a/tests/positive/NoDependencies/Package.juvix
+++ b/tests/positive/NoDependencies/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     dependencies := []
   };
diff --git a/tests/positive/PackageLoader/PackageJuvix/Package.juvix b/tests/positive/PackageLoader/PackageJuvix/Package.juvix
index 4560e71afe..99c18816d8 100644
--- a/tests/positive/PackageLoader/PackageJuvix/Package.juvix
+++ b/tests/positive/PackageLoader/PackageJuvix/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V1 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "package-juvix"
   };
diff --git a/tests/positive/PackageLoader/PackageJuvixAndYaml/Package.juvix b/tests/positive/PackageLoader/PackageJuvixAndYaml/Package.juvix
index 4560e71afe..99c18816d8 100644
--- a/tests/positive/PackageLoader/PackageJuvixAndYaml/Package.juvix
+++ b/tests/positive/PackageLoader/PackageJuvixAndYaml/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V1 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "package-juvix"
   };
diff --git a/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix b/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix
index cfc67ae272..8e5ddde7ca 100644
--- a/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix
+++ b/tests/positive/PackageLoader/PackageJuvixEmptyDependencies/Package.juvix
@@ -4,7 +4,7 @@ import Stdlib.Prelude open;
 import PackageDescription.V1 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "package-juvix";
     dependencies := []
   };
diff --git a/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix b/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix
index 52fd1ea559..05d7e7f89d 100644
--- a/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix
+++ b/tests/positive/PackageLoader/PackageJuvixUsesLockfile/Package.juvix
@@ -4,7 +4,7 @@ import Stdlib.Prelude open;
 import PackageDescription.V1 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "abc";
     version := mkVersion 0 0 0;
     dependencies := [git "name" "url" "ref1"]
diff --git a/tests/positive/PackageLoader/YamlEmptyDependencies/Package.juvix b/tests/positive/PackageLoader/YamlEmptyDependencies/Package.juvix
index 8991581597..20d310a375 100644
--- a/tests/positive/PackageLoader/YamlEmptyDependencies/Package.juvix
+++ b/tests/positive/PackageLoader/YamlEmptyDependencies/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V1 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "abc";
     dependencies := []
   };
diff --git a/tests/positive/PackageLoaderV2/PackageJuvix/Package.juvix b/tests/positive/PackageLoaderV2/PackageJuvix/Package.juvix
index efff5ba9b1..c4bc6755a0 100644
--- a/tests/positive/PackageLoaderV2/PackageJuvix/Package.juvix
+++ b/tests/positive/PackageLoaderV2/PackageJuvix/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "package-juvix"
   };
diff --git a/tests/positive/PackageLoaderV2/PackageJuvixAndYaml/Package.juvix b/tests/positive/PackageLoaderV2/PackageJuvixAndYaml/Package.juvix
index efff5ba9b1..c4bc6755a0 100644
--- a/tests/positive/PackageLoaderV2/PackageJuvixAndYaml/Package.juvix
+++ b/tests/positive/PackageLoaderV2/PackageJuvixAndYaml/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "package-juvix"
   };
diff --git a/tests/positive/PackageLoaderV2/PackageJuvixEmptyDependencies/Package.juvix b/tests/positive/PackageLoaderV2/PackageJuvixEmptyDependencies/Package.juvix
index 61853bf96b..4da6bc3104 100644
--- a/tests/positive/PackageLoaderV2/PackageJuvixEmptyDependencies/Package.juvix
+++ b/tests/positive/PackageLoaderV2/PackageJuvixEmptyDependencies/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "package-juvix";
     dependencies := []
   };
diff --git a/tests/positive/PackageLoaderV2/PackageJuvixUsesLockfile/Package.juvix b/tests/positive/PackageLoaderV2/PackageJuvixUsesLockfile/Package.juvix
index 9e53af38cb..461a2c768a 100644
--- a/tests/positive/PackageLoaderV2/PackageJuvixUsesLockfile/Package.juvix
+++ b/tests/positive/PackageLoaderV2/PackageJuvixUsesLockfile/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "abc";
     version := mkVersion 0 0 0;
     dependencies := [git "name" "url" "ref1"]
diff --git a/tests/positive/Records.juvix b/tests/positive/Records.juvix
index 85be188405..b7be735399 100644
--- a/tests/positive/Records.juvix
+++ b/tests/positive/Records.juvix
@@ -31,7 +31,7 @@ type EnumRecord :=
 p2 : Pair EnumRecord EnumRecord :=
   mkPair@{
     fst :=
-      C1@?{
+      C1@{
         c1a := constructT;
         c1b := constructT
       };
diff --git a/tests/positive/StdlibList/Package.juvix b/tests/positive/StdlibList/Package.juvix
index a6223b86a4..cfab3cce78 100644
--- a/tests/positive/StdlibList/Package.juvix
+++ b/tests/positive/StdlibList/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     dependencies := []
   };
diff --git a/tests/positive/VisibilityPrecendence/Package.juvix b/tests/positive/VisibilityPrecendence/Package.juvix
index 0027a3bac2..105e486066 100644
--- a/tests/positive/VisibilityPrecendence/Package.juvix
+++ b/tests/positive/VisibilityPrecendence/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "test075"
   };
diff --git a/tests/positive/issue2737/Package.juvix b/tests/positive/issue2737/Package.juvix
index 6a54fa0cd3..630999cb35 100644
--- a/tests/positive/issue2737/Package.juvix
+++ b/tests/positive/issue2737/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "issue2737"
   };
diff --git a/tests/positive/issue2929/Package.juvix b/tests/positive/issue2929/Package.juvix
index ec550a11f2..817eda193c 100644
--- a/tests/positive/issue2929/Package.juvix
+++ b/tests/positive/issue2929/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "issue2929"
   };
diff --git a/tests/positive/issue3048/Package.juvix b/tests/positive/issue3048/Package.juvix
index f04d2d888f..d5e0e45e71 100644
--- a/tests/positive/issue3048/Package.juvix
+++ b/tests/positive/issue3048/Package.juvix
@@ -3,6 +3,6 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "issue3048"
   };
diff --git a/tests/positive/issue3068/Package.juvix b/tests/positive/issue3068/Package.juvix
index bbc6001160..d5fc44153a 100644
--- a/tests/positive/issue3068/Package.juvix
+++ b/tests/positive/issue3068/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "issue3068";
     dependencies := []
   };
diff --git a/tests/positive/package/Package.juvix b/tests/positive/package/Package.juvix
index 308c185ec7..b44f7fbb45 100644
--- a/tests/positive/package/Package.juvix
+++ b/tests/positive/package/Package.juvix
@@ -3,7 +3,7 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage@?{
+  defaultPackage@{
     name := "foo";
     version := mkVersion 0 1 0;
     dependencies :=
diff --git a/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml b/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml
index c6d26e6852..fc79d447fe 100644
--- a/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml
+++ b/tests/smoke/Commands/compile-dependencies-package-juvix.smoke.yaml
@@ -37,7 +37,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -103,7 +103,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -173,7 +173,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -218,7 +218,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -280,7 +280,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "Dep1";
+          defaultPackage@{name := "Dep1";
             version := mkVersion 0 1 0;
             dependencies :=
                [defaultStdlib;
@@ -303,7 +303,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -420,7 +420,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -515,7 +515,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -546,7 +546,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -623,7 +623,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "Dep1";
+          defaultPackage@{name := "Dep1";
             version := mkVersion 0 1 0;
             dependencies :=
                [defaultStdlib;
@@ -659,7 +659,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -735,7 +735,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -771,7 +771,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -822,7 +822,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -867,7 +867,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -912,7 +912,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -982,7 +982,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -1033,7 +1033,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
@@ -1096,7 +1096,7 @@ tests:
         import PackageDescription.V2 open;
 
         package : Package :=
-          defaultPackage@?{name := "HelloWorld";
+          defaultPackage@{name := "HelloWorld";
             version := mkVersion 0 0 1;
             dependencies :=
                [defaultStdlib;
diff --git a/tests/smoke/Commands/compile-dependencies.smoke.yaml b/tests/smoke/Commands/compile-dependencies.smoke.yaml
index 15e6b4f398..968fb1cd51 100644
--- a/tests/smoke/Commands/compile-dependencies.smoke.yaml
+++ b/tests/smoke/Commands/compile-dependencies.smoke.yaml
@@ -1056,7 +1056,7 @@ tests:
         cat <<-EOF > Package.juvix
         module Package;
         import PackageDescription.V2 open;
-        package : Package := defaultPackage@?{dependencies := [defaultStdlib ; git "dep1" "$temp/dep" "main"]}
+        package : Package := defaultPackage@{dependencies := [defaultStdlib ; git "dep1" "$temp/dep" "main"]}
         EOF
 
         cat <<-EOF > HelloWorld.juvix