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