michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/inductive): add getters for inductive decls

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-16 17:47:37 -07:00
parent 6dedb480ec
commit ace5dee63d
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/kernel/inductive/inductive.h
View file

@ -23,12 +23,20 @@ typedef std::tuple<name, // introduction rule name
expr // result type expr // result type
> intro_rule; > 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 */ /** \brief Inductive datatype */
typedef std::tuple<name, // datatype name typedef std::tuple<name, // datatype name
telescope, // indices telescope, // indices
list<intro_rule> // introduction rules for this datatype list<intro_rule> // introduction rules for this datatype
> inductive_decl; > 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<intro_rule> const & inductive_decl_intros(inductive_decl const & d) { return std::get<2>(d); }
/** \brief Declare a finite set of mutually dependent inductive datatypes. */ /** \brief Declare a finite set of mutually dependent inductive datatypes. */
environment add_inductive(environment const & env, environment add_inductive(environment const & env,
level_param_names const & level_params, level_param_names const & level_params,