/dports/lang/maude/maude-2.7.1/tests/Meta/ |
H A D | metaSearch.expected | 3 '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 D | metaUnify.expected | 6 '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 D | metaSearch.maude | 6 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 D | metaUpModExp.expected | 59 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 D | metaUnify.maude | 7 '_+_['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 D | metaMatch.expected | 3 '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 D | metaSort.maude | 10 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 D | metaMatch.maude | 6 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 D | metaSort.expected | 5 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 D | unification.expected | 21 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 D | parameterization.expected | 3475 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 D | dataStructures.maude | 6 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 D | meseguerFiniteVariant.expected | 72 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 D | commands.expected | 85 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 D | sreduce.maude | 15 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 D | isaplanner-goal20.smt2 | 5 (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 D | InfNat.hs | 43 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 D | fta0210.smt2 | 5 (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 D | hoa0008.smt2 | 7 (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 D | fta0409.smt2 | 5 (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 D | fta0144-alpha-eq.smt2 | 4 (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 D | TypeNats.hs | 26 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 D | SecP521R1Field.java | 7 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 D | SecP521R1FieldElement.java | 6 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 D | rat.expected | 205 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 …]
|