<commit_before>/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include <string>
#include "util/flet.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/instantiate.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "kernel/inductive/inductive.h"
#include "library/trace.h"
#include "library/num.h"
#include "library/constants.h"
#include "library/idx_metavar.h"
#include "library/string.h"
#include "library/pp_options.h"
#include "library/exception.h"
#include "library/util.h"
#include "library/locals.h"
#include "library/annotation.h"
#include "library/private.h"
#include "library/inverse.h"
#include "library/aux_definition.h"
#include "library/app_builder.h"
#include "library/delayed_abstraction.h"
#include "library/tactic/tactic_state.h"
#include "library/tactic/revert_tactic.h"
#include "library/tactic/clear_tactic.h"
#include "library/tactic/cases_tactic.h"
#include "library/tactic/intro_tactic.h"
#include "library/equations_compiler/equations.h"
#include "library/equations_compiler/util.h"
#include "library/equations_compiler/elim_match.h"

#ifndef LEAN_DEFAULT_EQN_COMPILER_ITE
#define LEAN_DEFAULT_EQN_COMPILER_ITE true
#endif

#ifndef LEAN_DEFAULT_EQN_COMPILER_MAX_STEPS
#define LEAN_DEFAULT_EQN_COMPILER_MAX_STEPS 128
#endif

namespace lean {
static name * g_eqn_compiler_ite       = nullptr;
static name * g_eqn_compiler_max_steps = nullptr;
<commit_msg>feat(library/equations_compiler/elim_match): change default max number of steps to 2048<commit_after>/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#include <string>
#include "util/flet.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/instantiate.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "kernel/inductive/inductive.h"
#include "library/trace.h"
#include "library/num.h"
#include "library/constants.h"
#include "library/idx_metavar.h"
#include "library/string.h"
#include "library/pp_options.h"
#include "library/exception.h"
#include "library/util.h"
#include "library/locals.h"
#include "library/annotation.h"
#include "library/private.h"
#include "library/inverse.h"
#include "library/aux_definition.h"
#include "library/app_builder.h"
#include "library/delayed_abstraction.h"
#include "library/tactic/tactic_state.h"
#include "library/tactic/revert_tactic.h"
#include "library/tactic/clear_tactic.h"
#include "library/tactic/cases_tactic.h"
#include "library/tactic/intro_tactic.h"
#include "library/equations_compiler/equations.h"
#include "library/equations_compiler/util.h"
#include "library/equations_compiler/elim_match.h"

#ifndef LEAN_DEFAULT_EQN_COMPILER_ITE
#define LEAN_DEFAULT_EQN_COMPILER_ITE true
#endif

#ifndef LEAN_DEFAULT_EQN_COMPILER_MAX_STEPS
#define LEAN_DEFAULT_EQN_COMPILER_MAX_STEPS 2048
#endif

namespace lean {
static name * g_eqn_compiler_ite       = nullptr;
static name * g_eqn_compiler_max_steps = nullptr;

{'fraction_non_alphanumeric': 0.12166934189406099, 'fraction_numerical': 0.007383627608346709, 'mean_word_length': 6.809523809523809, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6806731', 'n_tokens_mistral': 1147, 'n_tokens_neox': 1119, 'n_words': 216}