Home
last modified time | relevance | path

Searched refs:PrimImpl (Results 1 – 7 of 7) sorted by relevance

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/
H A DPrimitive.hs448 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 ->
648 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ ~[a] -> do
655 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \ ~[a, b] -> do
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 ->
[all …]
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Primitive/
H A DCubical.hs52 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ ts -> do
80 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \ ts -> do
102 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \ ts -> do
166 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 8 $ \ ts -> do
221 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 8 $ \ ts -> do
245 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \ ts -> do
1431 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \ts ->
1457 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 5 $ \ts ->
1515 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \ts ->
1537 return $ PrimImpl t $ primFun __IMPOSSIBLE__ 8 $ \ts ->
[all …]
H A DBase.hs181 PrimImpl t pf <- lookupPrimitiveFunction s
182 return (s, PrimImpl t $ pf { primFunName = q })
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A DBuiltin.hs794 PrimImpl t pf <- lookupPrimitiveFunction pfname
948 PrimImpl t pf <- lookupPrimitiveFunction name
H A DDecl.hs676 (name, PrimImpl t' pf) <- lookupPrimitiveFunctionQ x
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Interaction/
H A DImports.hs230 PrimImpl _ pf <- lookupPrimitiveFunction x
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Monad/
H A DBase.hs2437 data PrimitiveImpl = PrimImpl Type PrimFun constructor