From 1b628930bae409f188ae782ae513bf2bda207332 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Oct 2016 17:13:52 -0700 Subject: [PATCH] feat(kernel/inductive): v_idx ==> ih_idx --- src/kernel/inductive/inductive.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 21a5caab55..2b8753389e 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -610,7 +610,7 @@ struct add_inductive_fn { C_app = mk_app(C_app, u_app); } expr v_i_ty = Pi(xs, C_app); - expr v_i = mk_local(mk_fresh_name(), name("v").append_after(i), v_i_ty, binder_info()); + expr v_i = mk_local(mk_fresh_name(), name("ih").append_after(i+1), v_i_ty, binder_info()); v.push_back(v_i); } expr minor_ty = Pi(b, Pi(u, Pi(v, C_app)));