| /dports/math/hs-Agda/Agda-2.6.2/src/full/Agda/TypeChecking/ |
| H A D | LevelConstraints.hs | 55 rho = mkSub $ List.sort $ zip ys xs
56 mkSub = go 0 function
|
| H A D | RecordPatterns.hs | 468 mkSub s = s ++# raiseS noNewPatternVars function
472 rhsSubst = mkSub s' -- NB:: Defined but not used
477 rhsSubst' = mkSub $ permute (reverseP perm) s'
|
| H A D | Substitute.hs | 392 rhoP = mkSub dotP n rps rargs
393 rho = mkSub id n rps rargs
409 …mkSub :: EndoSubst a => (Term -> a) -> Nat -> [NamedArg DeBruijnPattern] -> [Term] -> Substitution…
410 mkSub _ _ [] [] = idS function
411 mkSub tm n (p : ps) (v : vs) =
413 … VarP _ (DBPatVar _ i) -> mkSub tm (n - 1) (substP i v' ps) vs `composeS` singletonS i (tm v')
415 DotP{} -> mkSub tm n ps vs
416 ConP c _ ps' -> mkSub tm n (ps' ++ ps) (projections c v ++ vs)
420 …IApplyP _ _ _ (DBPatVar _ i) -> mkSub tm (n - 1) (substP i v' ps) vs `composeS` singletonS i (tm v…
422 mkSub _ _ _ _ = __IMPOSSIBLE__ function
|
| /dports/math/libpgmath/flang-d07daf3/tools/flang1/flang1exe/ |
| H A D | datadep.c | 2163 mkSub(int astliTriples, int sub, int astmpyr, int ast) in mkSub() function
2218 bLinear = mkSub(astliTriples, sub, astmpyr, A_LOPG(ast)); in mkSub()
2223 bLinear = (mkSub(astliTriples, sub, astmpyr, A_LOPG(ast)) && in mkSub()
2224 mkSub(astliTriples, sub, astmpyr, A_ROPG(ast))); in mkSub()
2227 bLinear = mkSub(astliTriples, sub, astmpyr, A_LOPG(ast)); in mkSub()
2231 bLinear = mkSub(astliTriples, sub, astmpyr, A_ROPG(ast)); in mkSub()
2235 bLinear = mkSub(astliTriples, sub, astmpyr, A_ROPG(ast)); in mkSub()
2239 bLinear = mkSub(astliTriples, sub, astmpyr, A_LOPG(ast)); in mkSub()
2333 bLinear = mkSub(astliTriples, subStart + n, astb.bnd.one, astSub); in fill_subscripts()
|
| /dports/math/z3/z3-z3-4.8.13/examples/java/ |
| H A D | JavaExample.java | 1265 ArithExpr gx_gy = ctx.mkSub((IntExpr) gx, (IntExpr) gy); in proveExample2()
2028 Expr t1 = ctx.mkAdd(x, ctx.mkSub(y, ctx.mkAdd(x, z))); in simplifierExample()
|
| H A D | JavaGenericExample.java | 1054 ArithExpr<IntSort> gx_gy = ctx.mkSub(gx, gy); in proveExample2()
1834 ArithExpr<IntSort> t1 = ctx.mkAdd(x, ctx.mkSub(y, ctx.mkAdd(x, z))); in simplifierExample()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/java/ |
| H A D | JavaExample.java | 1265 ArithExpr gx_gy = ctx.mkSub((IntExpr) gx, (IntExpr) gy); in proveExample2()
2028 Expr t1 = ctx.mkAdd(x, ctx.mkSub(y, ctx.mkAdd(x, z))); in simplifierExample()
|
| H A D | JavaGenericExample.java | 1023 ArithExpr<IntSort> gx_gy = ctx.mkSub(gx, gy); in gzlog_write()
1803 ArithExpr<IntSort> t1 = ctx.mkAdd(x, ctx.mkSub(y, ctx.mkAdd(x, z)));
|
| /dports/math/z3/z3-z3-4.8.13/src/api/java/ |
| H A D | Context.java | 860 public final <R extends ArithSort> ArithExpr<R> mkSub(Expr<? extends R>... t) in mkSub() method in Context
864 Native.mkSub(nCtx(), t.length, AST.arrayToNative(t))); in mkSub()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/api/java/ |
| H A D | Context.java | 843 public <R extends ArithSort> ArithExpr<R> mkSub(Expr<R>... t) in mkSub() method in Context
847 Native.mkSub(nCtx(), t.length, AST.arrayToNative(t))); in mkSub()
|