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

Author: <NAME>
*/
#pragma once
#include <vector>
#include "kernel/pos_info_provider.h"
#include "library/local_context.h"
#include "library/type_context.h"
#include "library/tactic/tactic_state.h"
#include "frontends/lean/elaborator_exception.h"
#include "frontends/lean/info_manager.h"

namespace lean {
enum class elaborator_strategy {
    Simple,
    WithExpectedType,
    AsEliminator
};

class sanitize_param_names_fn;

class elaborator {
public:
    class checkpoint;
private:
    typedef std::vector<pair<expr, expr>> to_check_sorts;
    enum class arg_mask {
        AllExplicit /* @ annotation */,
        InstHoExplicit, /* @@ annotation (i.e., instance implicit and higher-order arguments are explicit  */
        Default /* default behavior */
    };
    environment       m_env;
    options           m_opts;
    type_context      m_ctx;<commit_msg>fix(frontends/lean/elaborator): compilation warning with clang<commit_after>/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: <NAME>
*/
#pragma once
#include <vector>
#include "kernel/pos_info_provider.h"
#include "library/local_context.h"
#include "library/type_context.h"
#include "library/tactic/tactic_state.h"
#include "frontends/lean/elaborator_exception.h"
#include "frontends/lean/info_manager.h"

namespace lean {
enum class elaborator_strategy {
    Simple,
    WithExpectedType,
    AsEliminator
};

struct sanitize_param_names_fn;

class elaborator {
public:
    class checkpoint;
private:
    typedef std::vector<pair<expr, expr>> to_check_sorts;
    enum class arg_mask {
        AllExplicit /* @ annotation */,
        InstHoExplicit, /* @@ annotation (i.e., instance implicit and higher-order arguments are explicit  */
        Default /* default behavior */
    };
    environment       m_env;
    options           m_opts;
    type_context      m_ctx;
{'fraction_non_alphanumeric': 0.09884281581485053, 'fraction_numerical': 0.0057859209257473485, 'mean_word_length': 3.726651480637813, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 11, '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': '2207757', 'n_tokens_mistral': 642, 'n_tokens_neox': 625, 'n_words': 167}