max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/equations_compiler/structural_rec): update comment

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-05 11:03:36 -08:00
parent 832246c06b
commit 931820c06d
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/equations_compiler/structural_rec.h
View file

@ -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<expr> try_structural_rec(environment & env, options const & opts,