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

Author: Leonardo de Moura
*/
#pragma once

namespace lean {
constexpr char const * g_rec               = "rec";
constexpr char const * g_rec_on            = "recOn";
constexpr char const * g_brec_on           = "brecOn";
constexpr char const * g_binduction_on     = "binductionOn";
constexpr char const * g_cases_on          = "casesOn";
constexpr char const * g_no_confusion      = "noConfusion";
constexpr char const * g_no_confusion_type = "noConfusionType";
}
