Lines Matching refs:PrimImpl

448   return $ PrimImpl ty $ primFun __IMPOSSIBLE__ 3 $ \ ts -> do
541   return $ PrimImpl t $ primFun __IMPOSSIBLE__ (1 + size eqTel) $ \ ts -> do
590   return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \ ts ->
643   return $ PrimImpl t $ primFun __IMPOSSIBLE__ 0 $ \_ -> redReturn $ Level $ ClosedLevel 0
648   return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ ~[a] -> do
655   return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \ ~[a, b] -> do
663   return $ PrimImpl t $ primFun __IMPOSSIBLE__ 0 $ \_ -> redReturn $ Sort $ Inf f 0
668   return $ PrimImpl t $ primFun __IMPOSSIBLE__ 0 $ \_ -> redReturn $ Sort LockUniv
683     return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ts ->
700     return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ts ->
717     return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \ts ->
739     return $ PrimImpl t $ primFun __IMPOSSIBLE__ 3 $ \ts ->
766     return $ PrimImpl t $ primFun __IMPOSSIBLE__ 4 $ \ts ->