text: /*
  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";
  }
  