From ace5dee63dd925e108578d7ab6501f1186898888 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 16 May 2014 17:47:37 -0700 Subject: [PATCH] feat(kernel/inductive): add getters for inductive decls Signed-off-by: Leonardo de Moura --- src/kernel/inductive/inductive.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h index 1bee374a4..61f0a4690 100644 --- a/src/kernel/inductive/inductive.h +++ b/src/kernel/inductive/inductive.h @@ -23,12 +23,20 @@ typedef std::tuple intro_rule; +inline name const & intro_rule_name(intro_rule const & r) { return std::get<0>(r); } +inline telescope const & intro_rule_args(intro_rule const & r) { return std::get<1>(r); } +inline expr const & intro_rule_type(intro_rule const & r) { return std::get<2>(r); } + /** \brief Inductive datatype */ typedef std::tuple // introduction rules for this datatype > inductive_decl; +inline name const & inductive_decl_name(inductive_decl const & d) { return std::get<0>(d); } +inline telescope const & inductive_decl_indices(inductive_decl const & d) { return std::get<1>(d); } +inline list const & inductive_decl_intros(inductive_decl const & d) { return std::get<2>(d); } + /** \brief Declare a finite set of mutually dependent inductive datatypes. */ environment add_inductive(environment const & env, level_param_names const & level_params,