Home
last modified time | relevance | path

Searched refs:liftS (Results 1 – 25 of 37) sorted by relevance

12

/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Substitute/
H A DClass.hs97 substUnder n u = applySubst (liftS n (singletonS 0 u))
126 n + 1 == m = wkS (m - 1) (liftS 1 rho)
146 inplaceS k u = singletonS k u `composeS` liftS (k + 1) (raiseS 1)
149 liftS :: Int -> Substitution' a -> Substitution' a
150 liftS 0 rho = rho function
151 liftS k IdS = IdS function
152 liftS k (Lift n rho) = Lift (n + k) rho function
153 liftS k rho = Lift k rho function
167 dropS n (Lift m rho) = wkS 1 $ dropS (n - 1) $ liftS (m - 1) rho
192 splitS n (Lift m rho) = wkS 1 *** liftS 1 $ splitS (n - 1) (liftS (m - 1) rho)
[all …]
/dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/Tools/
H A DPolynomial.hs90 instance Polynomial SWord8 where {showPolynomial b = liftS (sp b); pMult = polyMult; pDivMod …
91 instance Polynomial SWord16 where {showPolynomial b = liftS (sp b); pMult = polyMult; pDivMod …
92 instance Polynomial SWord32 where {showPolynomial b = liftS (sp b); pMult = polyMult; pDivMod …
93 instance Polynomial SWord64 where {showPolynomial b = liftS (sp b); pMult = polyMult; pDivMod …
95 instance (KnownNat n, BVIsNonZero n) => Polynomial (SWord n) where {showPolynomial b = liftS (sp b)…
101 liftS :: SymVal a => (a -> String) -> SBV a -> String
102 liftS f s function
/dports/multimedia/handbrake/ffmpeg-4.4/libavcodec/
H A Dsnow_dwt.h71 #define liftS lift macro
76 #undef liftS
H A Dsnow_dwt.c145 static av_always_inline void liftS(DWTELEM *dst, DWTELEM *src, DWTELEM *ref, in liftS() function
243 liftS(temp, b, temp + w2, 1, 2, 1, width, W_BM, W_BO, W_BS, 0, 0); in horizontal_decompose97i()
/dports/emulators/vice/vice-3.5/src/lib/libffmpeg/libavcodec/
H A Dsnow_dwt.h68 #define liftS lift macro
73 #undef liftS
H A Dsnow_dwt.c150 static av_always_inline void liftS(DWTELEM *dst, DWTELEM *src, DWTELEM *ref, in liftS() function
248 liftS(temp, b, temp + w2, 1, 2, 1, width, W_BM, W_BO, W_BS, 0, 0); in horizontal_decompose97i()
/dports/multimedia/ffmpeg/ffmpeg-4.4.1/libavcodec/
H A Dsnow_dwt.h71 #define liftS lift macro
76 #undef liftS
H A Dsnow_dwt.c145 static av_always_inline void liftS(DWTELEM *dst, DWTELEM *src, DWTELEM *ref, in liftS() function
243 liftS(temp, b, temp + w2, 1, 2, 1, width, W_BM, W_BO, W_BS, 0, 0); in horizontal_decompose97i()
/dports/multimedia/gstreamer1-libav/gst-libav-1.16.2/gst-libs/ext/libav/libavcodec/
H A Dsnow_dwt.h71 #define liftS lift macro
76 #undef liftS
H A Dsnow_dwt.c145 static av_always_inline void liftS(DWTELEM *dst, DWTELEM *src, DWTELEM *ref, in liftS() function
243 liftS(temp, b, temp + w2, 1, 2, 1, width, W_BM, W_BO, W_BS, 0, 0); in horizontal_decompose97i()
/dports/www/qt5-webengine/qtwebengine-everywhere-src-5.15.2/src/3rdparty/chromium/third_party/ffmpeg/libavcodec/
H A Dsnow_dwt.h71 #define liftS lift macro
76 #undef liftS
H A Dsnow_dwt.c145 static av_always_inline void liftS(DWTELEM *dst, DWTELEM *src, DWTELEM *ref, in liftS() function
243 liftS(temp, b, temp + w2, 1, 2, 1, width, W_BM, W_BO, W_BS, 0, 0); in horizontal_decompose97i()
/dports/emulators/libretro-vice/vice-libretro-5725415/vice/src/lib/libffmpeg/libavcodec/
H A Dsnow_dwt.h68 #define liftS lift macro
73 #undef liftS
H A Dsnow_dwt.c150 static av_always_inline void liftS(DWTELEM *dst, DWTELEM *src, DWTELEM *ref, in liftS() function
248 liftS(temp, b, temp + w2, 1, 2, 1, width, W_BM, W_BO, W_BS, 0, 0); in horizontal_decompose97i()
/dports/www/chromium-legacy/chromium-88.0.4324.182/third_party/ffmpeg/libavcodec/
H A Dsnow_dwt.h71 #define liftS lift macro
76 #undef liftS
/dports/sysutils/xvidcap/xvidcap-1.1.7/ffmpeg/libavcodec/
H A Dsnow.h54 #define liftS lift macro
60 #undef liftS
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Compiler/Treeless/
H A DSubst.hs35 TLam b -> TLam (applySubst (liftS 1 rho) b)
36 TLet e b -> TLet (applySubst rho e) (applySubst (liftS 1 rho) b)
49 applySubst rho (TACon c i b) = TACon c i (applySubst (liftS i rho) b)
H A DUnused.hs92 computeSubst (ArgUsed : bs) = liftS 1 $ computeSubst bs
H A DSimplify.hs43 underLams i = onRewrite (raiseS i) . onSubst (liftS i)
130 rho = liftS (x + n + 1) (raiseS 1) `composeS`
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/
H A DData.hs411 the_u = liftS (size fsT) d0 `applySubst` u
449 …ty <- open (Abs "i" $ (liftS 1 (raiseS (size gamma - size params)) `composeS` sub params) `applySu…
514 telePatterns (d0 `applySubst` fsT) (liftS (size fsT) d0 `applySubst` boundary)
760 …delta_i = (liftS 1 (raiseS (size gamma - size deltaI)) `composeS` sub params) -- Defined but not u…
763 fsT' = (liftS 1 (raiseS (size gamma - size deltaI)) `composeS` sub params) `applySubst`
788 , (liftS (size fsT) d0 `applySubst` u) `consS` raiseS (size fsT)
790 , (liftS (size fsT) d0 `applySubst` u)
794 fsT_tel = (liftS 1 (raiseS (size tel - size deltaI)) `composeS` sub params) `applySubst` fsT
847 …theSubst = reverse (tau `applySubst` bodys) ++# (liftS 1 (raiseS (size tel - size deltaI)) `compos…
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/
H A DCoverage.hs429 …let ty = (fmap . fmap) ((parallelS (reverse $ map namedArg extra) `composeS` liftS n_extra s `appl…
741 return $ liftS (size delta) $ hc `consS` raiseS 3
1067 rho = liftS (size delta2) rho3 -- Δ' ⊢ ρ : Δ₁(x:D)Δ₂
1206 rho = liftS (size delta2) rho3 -- Δ' ⊢ ρ : Δ₁(x:D)Δ₂
1424 rho = liftS x $ consS (litP lit) idS
1435 rho = liftS x $ consS varp $ raiseS 1
1471 rho = liftS x $ consS absurdp $ raiseS 1
H A DSubstitute.hs240 sub = liftS (size newContext) $ parallelS $
495 sigma = liftS (ntel - nargs) (parallelS (reverse $ map unArg args))
947 f (applySubst (liftS n rho) ps)
948 (applyNLPatSubst (liftS n rho) rhs)
949 (applyNLPatSubst (liftS n rho) t)
960 Display n (applySubst (liftS n rho) ps)
961 (applySubst (liftS n rho) v)
1015 applySubst rho (Abs x a) = Abs x $ applySubst (liftS 1 rho) a
H A DGeneralize.hs100 letbinds' <- applySubst (liftS (size tel) sub) <$> instantiateFull letbinds
483 let ρ = liftS i σ
485 …ρ' = liftS i $ [ Var 0 [Proj ProjSystem fld] | fld <- reverse $ take (size _Θ) $ genRecFields ] ++…
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rules/LHS/
H A DUnify.hs449 sigma = liftS (n-k-1) $ consS (dotP u') idS
972 rho = liftS (size eqTel2) rho3
1007 rho = liftS (size eqTel2) rho3
1108 sub = liftS (n-k-1) $ consS sizeSu $ raiseS 1
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Rewriting/
H A DConfluence.hs261 b0 = applySubst (liftS k sub1) $ ohType hole0
263 es0 = applySubst (liftS k sub1) $ ohElims hole0
289 let es1 = applySubst (liftS (size bvTel) sub1) es'

12