max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(frontends/lean/choice): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-18 15:29:21 -07:00
parent f948892505
commit 5fa357e887
1 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/lean/choice.cpp
View file

@ -43,6 +43,11 @@ bool is_choice(expr const & e) {
return is_mdata(e) && get_nat(mdata_data(e), *g_choice);
}
unsigned get_num_choices(expr const & e) {
lean_assert(is_choice(e));
return get_nat(mdata_data(e), *g_choice)->get_small_value();
}
static void get_choices(expr const & e, buffer<expr> & r) {
lean_assert(is_choice(e));
expr it = mdata_expr(e);
@ -56,12 +61,6 @@ static void get_choices(expr const & e, buffer<expr> & r) {
r.push_back(it);
}
unsigned get_num_choices(expr const & e) {
buffer<expr> choices;
get_choices(e, choices);
return choices.size();
}
expr get_choice(expr const & e, unsigned i) {
buffer<expr> choices;
get_choices(e, choices);