From 60434b348792968bb515b87b883899d536538f71 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 15 Nov 2015 15:06:05 -0800 Subject: [PATCH] fix(tests/lean/urec): adjust test to recent changes --- tests/lean/urec.lean.expected.out | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tests/lean/urec.lean.expected.out b/tests/lean/urec.lean.expected.out index e95bb410a..58e83c33b 100644 --- a/tests/lean/urec.lean.expected.out +++ b/tests/lean/urec.lean.expected.out @@ -7,6 +7,8 @@ myrec.{l_1 l_2} : recursor information num. parameters: 1 num. indices: 0 + num. minors: 3 + recursive: 0 universe param pos.: 0 [motive univ] motive pos.: 2 major premise pos.: 3 @@ -15,6 +17,8 @@ recursor information recursor information num. parameters: 0 num. indices: 0 + num. minors: 2 + recursive: 1 universe param pos.: motive pos.: 1 major premise pos.: 2 @@ -27,6 +31,8 @@ vector.induction_on.{l_1} : recursor information num. parameters: 1 num. indices: 1 + num. minors: 2 + recursive: 1 universe param pos.: 0 motive pos.: 2 major premise pos.: 4 @@ -39,6 +45,8 @@ Exists.rec.{l_1} : recursor information num. parameters: 2 num. indices: 0 + num. minors: 1 + recursive: 0 universe param pos.: 0 motive pos.: 3 major premise pos.: 5