From 931820c06d908caaee5dbe08ac2b58581a48bedc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Mar 2017 11:03:36 -0800 Subject: [PATCH] chore(library/equations_compiler/structural_rec): update comment --- src/library/equations_compiler/structural_rec.h | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/library/equations_compiler/structural_rec.h b/src/library/equations_compiler/structural_rec.h index 0dfce0106e..33dbea05a3 100644 --- a/src/library/equations_compiler/structural_rec.h +++ b/src/library/equations_compiler/structural_rec.h @@ -7,12 +7,11 @@ Author: Leonardo de Moura #pragma once #include "library/type_context.h" namespace lean { -/** \brief Try to eliminate "recursive calls" in the equations \c e by using brec_on's below. - If successful, a new set of (non-recursive) equations is produced. The new equations - have a new argument of type `I.below` and all "recursive calls" are replaced with it. +/** \brief Try to eliminate "recursive calls" in the equations \c eqns by using brec_on's below. + If successful, elim_match is used to compile pattern matching. The procedure fails when: - 1- \c e is defining more than one function + 1- \c eqns is defining more than one function 2- None of the arguments is a primitive inductive datatype with support for brec_on construction, where every recursive call is structurally smaller. */ optional try_structural_rec(environment & env, options const & opts,