/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/Substitute/ |
H A D | Class.hs | 97 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 D | Polynomial.hs | 90 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 D | snow_dwt.h | 71 #define liftS lift macro 76 #undef liftS
|
H A D | snow_dwt.c | 145 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 D | snow_dwt.h | 68 #define liftS lift macro 73 #undef liftS
|
H A D | snow_dwt.c | 150 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 D | snow_dwt.h | 71 #define liftS lift macro 76 #undef liftS
|
H A D | snow_dwt.c | 145 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 D | snow_dwt.h | 71 #define liftS lift macro 76 #undef liftS
|
H A D | snow_dwt.c | 145 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 D | snow_dwt.h | 71 #define liftS lift macro 76 #undef liftS
|
H A D | snow_dwt.c | 145 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 D | snow_dwt.h | 68 #define liftS lift macro 73 #undef liftS
|
H A D | snow_dwt.c | 150 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 D | snow_dwt.h | 71 #define liftS lift macro 76 #undef liftS
|
/dports/sysutils/xvidcap/xvidcap-1.1.7/ffmpeg/libavcodec/ |
H A D | snow.h | 54 #define liftS lift macro 60 #undef liftS
|
/dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/Compiler/Treeless/ |
H A D | Subst.hs | 35 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 D | Unused.hs | 92 computeSubst (ArgUsed : bs) = liftS 1 $ computeSubst bs
|
H A D | Simplify.hs | 43 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 D | Data.hs | 411 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 D | Coverage.hs | 429 …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 D | Substitute.hs | 240 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 D | Generalize.hs | 100 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 D | Unify.hs | 449 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 D | Confluence.hs | 261 b0 = applySubst (liftS k sub1) $ ohType hole0 263 es0 = applySubst (liftS k sub1) $ ohElims hole0 289 let es1 = applySubst (liftS (size bvTel) sub1) es'
|