@@ -417,13 +417,12 @@ irTerm top vs env tm@(App _ f a) = do
417417 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]
418418
419419 -- compile Nat-likes as bigints
420− -- not sure if prim applications must be saturated
421− -- let's wrap it in a lambda just to be sure
420+ -- it seems that prim applications needn't be saturated
422421 | Just LikeS <- isLikeNat ist n
423− -> LLam [sMN 0 "nh"] <$>
424− (irTerm top vs env $
425− mkApp (P Ref (sUN "prim__addBigInt") Erased)
426− [Constant $ BI 1, P Ref (sMN 0 "nh") Erased])
422+ -> irTerm top vs env $
423+ App Complete
424+ (P Ref (sUN "prim__addBigInt") Erased)
425+ (Constant $ BI 1)
427426
428427 -- not a newtype, just apply to a constructor
429428 | otherwise