Home
last modified time | relevance | path

Searched refs:Nat (Results 1 – 25 of 3700) sorted by relevance

12345678910>>...148

/dports/lang/maude/maude-2.7.1/tests/Meta/
H A DmetaSearch.expected3 'c.Nat]], 'X:Nat, '_*_['Y:Nat,'Z:Nat] := 'X:Nat, '*, 100, 0) .
5 result ResultTriple: {'_*_['a.Nat,'_+_['b.Nat,'c.Nat]],'Nat,
6 'X:Nat <- '_*_['a.Nat,'_+_['b.Nat,'c.Nat]] ;
7 'Y:Nat <- '_+_['b.Nat,'c.Nat] ;
11 'c.Nat]], 'X:Nat, '_*_['Y:Nat,'Z:Nat] := 'X:Nat, '*, 100, 1) .
14 'X:Nat <- '_*_['a.Nat,'_+_['b.Nat,'c.Nat]] ;
19 'c.Nat]], 'X:Nat, '_*_['Y:Nat,'Z:Nat] := 'X:Nat, '*, 100, 2) .
24 'c.Nat]], 'X:Nat, '_*_['Y:Nat,'Z:Nat] := 'X:Nat /\ 'Y:Nat = 'a.Nat, '*,
33 'c.Nat]], 'X:Nat, '_*_['Y:Nat,'Z:Nat] := 'X:Nat /\ 'Y:Nat = 'a.Nat, '*,
48 'X:Nat <- '_+_['_*_['a.Nat,'b.Nat],'_*_['a.Nat,'c.Nat]]}
[all …]
H A DmetaUnify.expected6 'X:Nat <- '_+_['#1:Nat,'#3:Nat] ;
7 'Y:Nat <- '_+_['#2:Nat,'#4:Nat],
8 'X:Nat <- '_+_['#1:Nat,'#2:Nat] ;
9 'Y:Nat <- '_+_['#3:Nat,'#4:Nat],4}
15 'X:Nat <- '_+_['#1:Nat,'#3:Nat] ;
17 'X:Nat <- '_+_['#1:Nat,'#2:Nat] ;
25 'Y:Nat <- '_+_['#2:Nat,'#3:Nat],
26 'X:Nat <- '_+_['#1:Nat,'#2:Nat] ;
33 'X:Nat <- '_+_['#1:Nat,'#2:Nat] ;
36 'Y:Nat <- '_+_['#2:Nat,'#3:Nat],3}
[all …]
H A DmetaSearch.maude6 op _+_ : Nat Nat -> Nat [assoc comm prec 5] .
22 '_*_['Y:Nat, 'Z:Nat] := 'X:Nat,
30 '_*_['Y:Nat, 'Z:Nat] := 'X:Nat,
46 '_*_['Y:Nat, 'Z:Nat] := 'X:Nat /\ 'Y:Nat = 'a.Nat,
54 '_*_['Y:Nat, 'Z:Nat] := 'X:Nat /\ 'Y:Nat = 'a.Nat,
108 '_+_['_*_['a.Nat,'b.Nat],'_*_['a.Nat,'c.Nat]],
116 '_+_['_*_['a.Nat,'b.Nat],'_*_['a.Nat,'c.Nat]],
132 '_+_['_*_['a.Nat,'b.Nat],'_*_['a.Nat,'c.Nat], '_*_['a.Nat,'d.Nat]],
140 '_+_['_*_['a.Nat,'b.Nat],'_*_['a.Nat,'c.Nat], '_*_['a.Nat,'d.Nat]],
148 '_+_['_*_['a.Nat,'b.Nat],'_*_['a.Nat,'c.Nat], '_*_['a.Nat,'d.Nat]],
[all …]
H A DmetaUpModExp.expected59 op '_&_ : 'Nat 'Nat -> 'Nat [assoc comm prec(53) special(
62 op '_*_ : 'Nat 'Nat -> 'Nat [assoc comm prec(31) special(
69 op '_+_ : 'Nat 'Nat -> 'Nat [assoc comm prec(33) special(
76 op '_<<_ : 'Nat 'Nat -> 'Nat [prec(35) gather('E 'e) special(
134 op '_|_ : 'Nat 'Nat -> 'Nat [assoc comm prec(57) special(
143 op 'gcd : 'Nat 'Nat -> 'Nat [assoc comm special(
154 op 'lcm : 'Nat 'Nat -> 'Nat [assoc comm special(
160 op 'max : 'Nat 'Nat -> 'Nat [assoc comm special(
166 op 'min : 'Nat 'Nat -> 'Nat [assoc comm special(
172 op 'modExp : '`[Nat`] '`[Nat`] '`[Nat`] -> '`[Nat`] [special(
[all …]
H A DmetaUnify.maude7 '_+_['X:Nat, 'Y:Nat] =? '_+_['X:Nat, 'Y:Nat],
12 '_+_['X:Nat, 'Y:Nat] =? '_+_['X:Nat, 'Y:Nat],
17 '_+_['X:Nat, 'Y:Nat] =? '_+_['X:Nat, 'Y:Nat],
22 '_+_['X:Nat, 'Y:Nat] =? '_+_['X:Nat, 'Y:Nat],
27 '_+_['X:Nat, 'Y:Nat] =? '_+_['X:Nat, 'Y:Nat],
32 '_+_['X:Nat, 'Y:Nat] =? '_+_['X:Nat, 'Y:Nat],
37 '_+_['X:Nat, 'Y:Nat] =? '_+_['X:Nat, 'Y:Nat],
42 '_+_['X:Nat, 'Y:Nat] =? '_+_['X:Nat, 'Y:Nat],
48 '_+_['X:Nat, 'Y:Nat] =? '_+_['A:Nat, 'B:Nat],
56 '_+_['X:Nat, 'Y:Nat] =? '_+_['#1:Nat, 'Y:Nat],
H A DmetaMatch.expected3 'b.Nat,'c.Nat]], '_*_['Y:Nat,'Z:Nat] := 'X:Nat, 0) .
6 'X:Nat <- '_*_['a.Nat,'_+_['b.Nat,'c.Nat]] ;
7 'Y:Nat <- '_+_['b.Nat,'c.Nat] ;
11 'b.Nat,'c.Nat]], '_*_['Y:Nat,'Z:Nat] := 'X:Nat, 1) .
14 'X:Nat <- '_*_['a.Nat,'_+_['b.Nat,'c.Nat]] ;
16 'Z:Nat <- '_+_['b.Nat,'c.Nat]
19 'b.Nat,'c.Nat]], '_*_['Y:Nat,'Z:Nat] := 'X:Nat, 2) .
24 'b.Nat,'c.Nat]], '_*_['Y:Nat,'Z:Nat] := 'X:Nat /\ 'Y:Nat = 'a.Nat, 0) .
27 'X:Nat <- '_*_['a.Nat,'_+_['b.Nat,'c.Nat]] ;
29 'Z:Nat <- '_+_['b.Nat,'c.Nat]
[all …]
H A DmetaSort.maude10 subsort 'NzNat < 'Nat .
12 subsort 'Nat < 'Int .
23 subsort 'NzNat < 'Nat .
25 subsort 'Nat < 'Int .
38 subsort 'Nat < 'Int .
51 subsort 'Nat < 'Int .
127 endfm, 'Nat) .
153 endfm, 'Nat, 'Int) .
257 red maximalAritySet(['RAT], '_+_, 'Nat 'Nat, 'PosRat) .
258 red maximalAritySet(['RAT], '_+_, 'Nat 'Nat, 'Rat) .
[all …]
H A DmetaMatch.maude6 op _+_ : Nat Nat -> Nat [assoc comm prec 5] .
7 op _*_ : Nat Nat -> Nat [assoc comm prec 3] .
21 '_*_['a.Nat, '_+_['b.Nat, 'c.Nat]],
22 '_*_['Y:Nat, 'Z:Nat] := 'X:Nat,
27 '_*_['a.Nat, '_+_['b.Nat, 'c.Nat]],
28 '_*_['Y:Nat, 'Z:Nat] := 'X:Nat,
33 '_*_['a.Nat, '_+_['b.Nat, 'c.Nat]],
34 '_*_['Y:Nat, 'Z:Nat] := 'X:Nat,
39 '_*_['a.Nat, '_+_['b.Nat, 'c.Nat]],
40 '_*_['Y:Nat, 'Z:Nat] := 'X:Nat /\ 'Y:Nat = 'a.Nat,
[all …]
H A DmetaSort.expected5 subsort 'NzNat < 'Nat .
7 subsort 'Nat < 'Int .
19 subsort 'NzNat < 'Nat .
21 subsort 'Nat < 'Int .
35 subsort 'Nat < 'Int .
49 subsort 'Nat < 'Int .
131 endfm, 'Nat) .
159 endfm, 'Nat, 'Int) .
161 result Sort: 'Nat
312 result TypeListSet: 'Nat 'PosRat ; 'PosRat 'Nat ; 'PosRat 'PosRat
[all …]
/dports/lang/maude/maude-2.7.1/tests/Misc/
H A Dunification.expected21 X:Nat --> #1:Nat + #2:Nat + #3:Nat + #5:Nat + #6:Nat + #8:Nat
23 A:Nat --> #1:Nat + #1:Nat + #2:Nat + #3:Nat + #4:Nat
24 B:Nat --> #2:Nat + #5:Nat + #5:Nat + #6:Nat + #7:Nat
25 C:Nat --> #3:Nat + #6:Nat + #8:Nat + #8:Nat + #9:Nat
28 X:Nat --> #1:Nat + #2:Nat + #3:Nat + #5:Nat + #6:Nat + #8:Nat
30 A:Nat --> #1:Nat + #1:Nat + #2:Nat + #3:Nat + #4:Nat
31 B:Nat --> #2:Nat + #5:Nat + #5:Nat + #6:Nat + #7:Nat
35 X:Nat --> #1:Nat + #2:Nat + #3:Nat + #5:Nat + #6:Nat
37 A:Nat --> #1:Nat + #1:Nat + #2:Nat + #3:Nat + #4:Nat
38 B:Nat --> #2:Nat + #5:Nat + #5:Nat + #6:Nat + #7:Nat
[all …]
H A Dparameterization.expected3475 op g : Nat Nat -> Nat .
3485 eq g(A:Nat, B:Nat) = B:Nat + A:Nat + A:Nat + B:Nat .
4304 op g : Nat Nat -> Nat .
4314 eq g(A:Nat, B:Nat) = B:Nat + B:Nat + A:Nat + A:Nat .
4456 eq g(A:Nat, B:Nat) = _+_(B:Nat, _+_(B:Nat, _+_(A:Nat, A:Nat))) .
5330 eq g(A:Nat, B:Nat) = if if if A:Nat > A:Nat then A:Nat else A:Nat fi > B:Nat
5331 then if A:Nat > A:Nat then A:Nat else A:Nat fi else B:Nat fi > B:Nat then
5332 if if A:Nat > A:Nat then A:Nat else A:Nat fi > B:Nat then if A:Nat > A:Nat
5476 _>_(A:Nat, A:Nat), A:Nat, A:Nat), B:Nat), if_then_else_fi(_>_(A:Nat,
5478 _>_(A:Nat, A:Nat), A:Nat, A:Nat), B:Nat), if_then_else_fi(_>_(A:Nat,
[all …]
H A DdataStructures.maude6 var N : Nat .
9 op gen : Nat -> List{Nat<} .
12 op gen2 : Nat List{Nat<} -> List{Nat<} .
30 op gen : Nat Nat -> Set{Nat} .
33 op gen2 : Nat Nat Set{Nat} -> Set{Nat} .
54 op gen : Nat -> List{Nat} .
57 op gen2 : Nat List{Nat} -> List{Nat} .
73 op gen : Nat -> List{Nat<} .
76 op gen2 : Nat List{Nat<} -> List{Nat<} .
106 op zf : Nat -> Set{Nat} .
[all …]
H A DmeseguerFiniteVariant.expected72 Nat: #1:Nat + #2:Nat
78 Nat: %1:Nat
84 Nat: %1:Nat
95 Nat: #1:Nat - #2:Nat
124 Nat: #1:Nat - #2:Nat
132 m --> %1:Nat + %2:Nat
136 Nat: %2:Nat
137 n --> %1:Nat + %2:Nat
147 Conj: ((#1:Nat - #2:Nat) =/= 0) /\ (#2:Nat - #1:Nat) =/= 0
318 Nat: %1:Nat
[all …]
H A Dcommands.expected85 op sd : Nat Nat -> Nat [comm special (
143 op gcd : Nat Nat -> Nat [assoc comm special (
159 op lcm : Nat Nat -> Nat [assoc comm special (
175 op min : Nat Nat -> Nat [assoc comm special (
191 op max : Nat Nat -> Nat [assoc comm special (
611 op sd : Nat Nat -> Nat [comm special (
669 op gcd : Nat Nat -> Nat [assoc comm special (
685 op lcm : Nat Nat -> Nat [assoc comm special (
701 op min : Nat Nat -> Nat [assoc comm special (
717 op max : Nat Nat -> Nat [assoc comm special (
[all …]
H A Dsreduce.maude15 op _+_ : Nat NzNat -> Nat .
16 op _+_ : Nat Nat -> Nat .
21 op _*_ : Nat Nat -> Nat .
25 op _^_ : Nat Nat -> Nat .
30 op c : Nat Nat -> Nat .
35 op _mod_ : Nat NzNat -> Nat .
38 op i : Nat Nat NzNat -> Nat .
44 op modExp : Nat Nat NzNat ~> Nat .
61 op _+_ : Nat NzNat -> Nat .
62 op _+_ : Nat Nat -> Nat .
[all …]
/dports/math/cvc4/CVC4-1.7/test/regress/regress1/quantifiers/
H A Disaplanner-goal20.smt25 (declare-datatypes ((Nat 0)) (((succ (pred Nat)) (zero))
11 (declare-datatypes ((Pair 0)(ZLst 0)) (((mkpair (first Nat) (second Nat)))
15 (declare-fun f (Nat) Nat)
16 (declare-fun less (Nat Nat) Bool)
17 (declare-fun plus (Nat Nat) Nat)
18 (declare-fun minus (Nat Nat) Nat)
19 (declare-fun mult (Nat Nat) Nat)
20 (declare-fun nmax (Nat Nat) Nat)
21 (declare-fun nmin (Nat Nat) Nat)
27 (declare-fun count (Nat Lst) Nat)
[all …]
/dports/security/hs-cryptol/cryptol-2.11.0/src/Cryptol/TypeCheck/Solver/
H A DInfNat.hs43 nAdd (Nat x) (Nat y) = Nat (x + y)
55 nMul (Nat 0) _ = Nat 0
59 nMul (Nat x) (Nat y) = Nat (x * y)
76 nExp (Nat x) (Nat y) = Nat (x ^ y)
81 nMin (Nat x) (Nat y) = Nat (min x y)
86 nMax (Nat x) (Nat y) = Nat (max x y)
92 nSub (Nat x) (Nat y)
115 nDiv (Nat x) (Nat y) = Just (Nat (div x y))
121 nMod (Nat x) (Nat y) = Just (Nat (mod x y))
148 nLg2 (Nat 0) = Nat 0
[all …]
/dports/math/cvc4/CVC4-1.7/test/regress/regress1/ho/
H A Dfta0210.smt25 (declare-sort Nat$ 0)
11 (declare-fun one$ () Nat$)
12 (declare-fun suc$ (Nat$) Nat$)
16 (declare-fun uud$ (Nat$ (-> Nat$ Nat$) Nat$) Nat$)
17 (declare-fun uue$ (Nat$) Nat$)
25 (declare-fun plus$a (Nat$ Nat$) Nat$)
28 (declare-fun poly$a (Nat_poly$ Nat$) Nat$)
33 (declare-fun zero$a () Nat$)
41 (declare-fun power$c (Nat$ Nat$) Nat$)
43 (declare-fun times$a (Nat$ Nat$) Nat$)
[all …]
H A Dhoa0008.smt27 (declare-sort Nat$ 0)
21 (declare-fun suc$ (Nat$) Nat$)
27 (declare-fun plus$ (Nat$ Nat$) Nat$)
29 (declare-fun size$ (A_triple$) Nat$)
33 (declare-fun zero$ () Nat$)
39 (declare-fun size$a (Com$) Nat$)
41 (declare-fun size$c (Bool) Nat$)
48 (declare-fun rec_bool$ (Nat$ Nat$) (-> Bool Nat$))
49 (declare-fun size_com$ (Com$) Nat$)
52 (declare-fun size_option$ ((-> Com$ Nat$)) (-> Com_option$ Nat$))
[all …]
H A Dfta0409.smt25 (declare-sort Nat$ 0)
15 (declare-fun suc$ (Nat$) Nat$)
17 (declare-fun dvd$b (Nat$ Nat$) Bool)
30 (declare-fun plus$a (Nat$ Nat$) Nat$)
34 (declare-fun poly$b (Nat_poly$ Nat$) Nat$)
37 (declare-fun times$ (Nat$ Nat$) Nat$)
42 (declare-fun coeff$a (Nat_poly$ Nat$) Nat$)
46 (declare-fun monom$b (Nat$ Nat$) Nat_poly$)
52 (declare-fun power$c (Nat$ Nat$) Nat$)
57 (declare-fun less_eq$ (Nat$ Nat$) Bool)
[all …]
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/ho/
H A Dfta0144-alpha-eq.smt24 (declare-sort Nat$ 0)
7 (declare-fun g$ (Nat$) Complex$)
11 (declare-fun less$ (Nat$ Nat$) Bool)
16 (declare-fun zero$a () Nat$)
18 (declare-fun minus$a (Nat$ Nat$) Nat$)
21 (declare-fun less_eq$ (Nat$ Nat$) Bool)
22 (declare-fun strict_mono$ ((-> Nat$ Nat$)) Bool)
24 (declare-fun strict_mono$b ((-> Nat$ Real)) Bool)
25 (declare-fun strict_mono$c ((-> Real Nat$)) Bool)
27 …(! (forall ((?v0 (-> Nat$ Nat$)) (?v1 Complex$)) (=> (and true (forall ((?v2 Real)) (=> true (exis…
[all …]
/dports/lang/ghc/ghc-8.10.7/libraries/base/GHC/
H A DTypeNats.hs26 Nat -- declared in GHC.Types in package ghc-prim
42 import GHC.Types( Nat )
58 class KnownNat (n :: Nat) where
179 type family (m :: Nat) <=? (n :: Nat) :: Bool
184 type family (m :: Nat) + (n :: Nat) :: Nat
189 type family (m :: Nat) * (n :: Nat) :: Nat
194 type family (m :: Nat) ^ (n :: Nat) :: Nat
199 type family (m :: Nat) - (n :: Nat) :: Nat
205 type family Div (m :: Nat) (n :: Nat) :: Nat
211 type family Mod (m :: Nat) (n :: Nat) :: Nat
[all …]
/dports/java/bouncycastle15/crypto-169/core/src/main/java/org/bouncycastle/math/ec/custom/sec/
H A DSecP521R1Field.java7 import org.bouncycastle.math.raw.Nat;
23 c += Nat.inc(16, z); in add()
34 c += Nat.inc(16, z); in addOne()
43 if (Nat.eq(17, z, P)) in fromBigInteger()
45 Nat.zero(17, z); in fromBigInteger()
75 int[] tt = Nat.create(33); in multiply()
84 Nat.sub(17, P, P, z); in negate()
88 Nat.sub(17, P, x, z); in negate()
123 c += Nat.inc(16, z); in reduce()
135 c += Nat.inc(16, z); in reduce23()
[all …]
H A DSecP521R1FieldElement.java6 import org.bouncycastle.math.raw.Nat;
29 this.x = Nat.create(17); in SecP521R1FieldElement()
39 return Nat.isZero(17, x); in isZero()
44 return Nat.isOne(17, x); in isOne()
69 int[] z = Nat.create(17); in add()
76 int[] z = Nat.create(17); in addOne()
83 int[] z = Nat.create(17); in subtract()
90 int[] z = Nat.create(17); in multiply()
98 int[] z = Nat.create(17); in divide()
106 int[] z = Nat.create(17); in negate()
[all …]
/dports/lang/maude/maude-2.7.1/tests/BuiltIn/
H A Drat.expected205 op _+_ : Nat Nat -> Nat [assoc comm prec 33 gather (e E) special (
225 op sd : Nat Nat -> Nat [comm special (
232 op _*_ : Nat Nat -> Nat [assoc comm prec 31 gather (e E) special (
284 op _^_ : Nat Nat -> Nat [prec 29 gather (E e) special (
319 op gcd : Nat Nat -> Nat [assoc comm special (
343 op lcm : Nat Nat -> Nat [assoc comm special (
367 op min : Nat Nat -> Nat [assoc comm special (
395 op max : Nat Nat -> Nat [assoc comm special (
435 op _&_ : Nat Nat -> Nat [assoc comm prec 53 gather (e E) special (
463 op _>>_ : Nat Nat -> Nat [prec 35 gather (E e) special (
[all …]

12345678910>>...148