summaryrefslogtreecommitdiff
path: root/test-suite/output/SearchPattern.out
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/SearchPattern.out')
-rw-r--r--test-suite/output/SearchPattern.out101
1 files changed, 55 insertions, 46 deletions
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index f3c12eff..b0ac9ea2 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -1,77 +1,86 @@
-true: bool
false: bool
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+true: bool
+negb: bool -> bool
implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
xorb: bool -> bool -> bool
-negb: bool -> bool
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
Nat.even: nat -> bool
Nat.odd: nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
Nat.testbit: nat -> nat -> bool
-O: nat
-S: nat -> nat
-length: forall A : Type, list A -> nat
-Nat.zero: nat
-Nat.one: nat
+Nat.eqb: nat -> nat -> bool
Nat.two: nat
+Nat.one: nat
+Nat.zero: nat
+O: nat
+Nat.div2: nat -> nat
+Nat.log2: nat -> nat
Nat.succ: nat -> nat
+Nat.sqrt: nat -> nat
Nat.pred: nat -> nat
-Nat.add: nat -> nat -> nat
Nat.double: nat -> nat
-Nat.mul: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
+Nat.square: nat -> nat
+S: nat -> nat
+Nat.ldiff: nat -> nat -> nat
+Nat.tail_add: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
+Nat.tail_mul: nat -> nat -> nat
+Nat.div: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.gcd: nat -> nat -> nat
+Nat.modulo: nat -> nat -> nat
Nat.max: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.mul: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
Nat.min: nat -> nat -> nat
Nat.pow: nat -> nat -> nat
-Nat.div: nat -> nat -> nat
-Nat.modulo: nat -> nat -> nat
-Nat.gcd: nat -> nat -> nat
-Nat.square: nat -> nat
+Nat.of_uint: Decimal.uint -> nat
+Nat.tail_addmul: nat -> nat -> nat -> nat
+Nat.of_uint_acc: Decimal.uint -> nat -> nat
+Nat.log2_iter: nat -> nat -> nat -> nat -> nat
Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
+length: forall A : Type, list A -> nat
+Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+Nat.div2: nat -> nat
Nat.sqrt: nat -> nat
-Nat.log2_iter: nat -> nat -> nat -> nat -> nat
Nat.log2: nat -> nat
-Nat.div2: nat -> nat
-Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
-Nat.ldiff: nat -> nat -> nat
-Nat.lxor: nat -> nat -> nat
-S: nat -> nat
-Nat.succ: nat -> nat
-Nat.pred: nat -> nat
-Nat.add: nat -> nat -> nat
Nat.double: nat -> nat
-Nat.mul: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
-Nat.max: nat -> nat -> nat
-Nat.min: nat -> nat -> nat
+Nat.pred: nat -> nat
+Nat.square: nat -> nat
+Nat.succ: nat -> nat
+S: nat -> nat
+Nat.ldiff: nat -> nat -> nat
Nat.pow: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
Nat.div: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.tail_mul: nat -> nat -> nat
Nat.modulo: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.mul: nat -> nat -> nat
Nat.gcd: nat -> nat -> nat
-Nat.square: nat -> nat
-Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
-Nat.sqrt: nat -> nat
+Nat.max: nat -> nat -> nat
+Nat.tail_add: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
+Nat.min: nat -> nat -> nat
+Nat.tail_addmul: nat -> nat -> nat -> nat
+Nat.of_uint_acc: Decimal.uint -> nat -> nat
Nat.log2_iter: nat -> nat -> nat -> nat -> nat
-Nat.log2: nat -> nat
-Nat.div2: nat -> nat
+Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
-Nat.ldiff: nat -> nat -> nat
-Nat.lxor: nat -> nat -> nat
mult_n_Sm: forall n m : nat, n * m + n = n * S m
-identity_refl: forall (A : Type) (a : A), identity a a
iff_refl: forall A : Prop, A <-> A
+le_n: forall n : nat, n <= n
+identity_refl: forall (A : Type) (a : A), identity a a
eq_refl: forall (A : Type) (x : A), x = x
Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-le_n: forall n : nat, n <= n
-pair: forall A B : Type, A -> B -> A * B
conj: forall A B : Prop, A -> B -> A /\ B
+pair: forall A B : Type, A -> B -> A * B
Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
h: n <> newdef n
h: n <> newdef n