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

Author: <NAME>
*/
#pragma once
#include <memory>
#include <vector>
#include "kernel/environment.h"
#include "library/io_state.h"
#include "library/io_state_stream.h"
#include "library/projection.h"

namespace lean {
bool get_class_trace_instances(options const & o);
unsigned get_class_instance_max_depth(options const & o);
bool get_class_trans_instances(options const & o);

class tmp_local_generator {
    unsigned m_next_local_idx;
    name mk_fresh_name();
public:
    tmp_local_generator();

    /** \brief Create a temporary local constant */
    virtual expr mk_tmp_local(expr const & type, binder_info const & bi);

    /** \brief Create a temporary local constant using the given pretty print name.
        The pretty printing name has not semantic significance. */
    virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi);

    /** \brief Return true if \c e was created using \c mk_tmp_local */
    virtual bool is_tmp_local(expr const & e) const;
};

/** \brief Light-weight type inference, normalization and definitional equality.
    It is simpler and more efficient version of the kernel type checker.
    It does not generate unification constraints.
    Unification problems are eagerly solved. However, only higher-order patterns<commit_msg>fix(library/type_context): compilation warning<commit_after>/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#pragma once
#include <memory>
#include <vector>
#include "kernel/environment.h"
#include "library/io_state.h"
#include "library/io_state_stream.h"
#include "library/projection.h"

namespace lean {
bool get_class_trace_instances(options const & o);
unsigned get_class_instance_max_depth(options const & o);
bool get_class_trans_instances(options const & o);

class tmp_local_generator {
    unsigned m_next_local_idx;
    name mk_fresh_name();
public:
    tmp_local_generator();
    virtual ~tmp_local_generator() {}

    /** \brief Create a temporary local constant */
    virtual expr mk_tmp_local(expr const & type, binder_info const & bi);

    /** \brief Create a temporary local constant using the given pretty print name.
        The pretty printing name has not semantic significance. */
    virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi);

    /** \brief Return true if \c e was created using \c mk_tmp_local */
    virtual bool is_tmp_local(expr const & e) const;
};

/** \brief Light-weight type inference, normalization and definitional equality.
    It is simpler and more efficient version of the kernel type checker.
    It does not generate unification constraints.
    Unification problems are eagerly solved. However, only higher-order patterns
{'fraction_non_alphanumeric': 0.08324907313784968, 'fraction_numerical': 0.004044489383215369, 'mean_word_length': 4.347747747747747, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, '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': '1177056', 'n_tokens_mistral': 841, 'n_tokens_neox': 810, 'n_words': 313}