From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/output/SearchPattern.out | 101 ++++++++++++++++++++---------------- 1 file changed, 55 insertions(+), 46 deletions(-) (limited to 'test-suite/output/SearchPattern.out') 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 -- cgit v1.2.3