lean4-htt/src/library/compiler/lc_util.cpp
2018-09-11 18:11:27 -07:00

12 lines
365 B
C++

/*
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/aux_recursors.h"
namespace lean {
bool is_cases_on_recursor(environment const & env, name const & n) {
return ::lean::is_aux_recursor(env, n) && n.get_string() == "cases_on";
}
}