Module BuiltinLang

module BuiltinLang: sig .. end

val global_sdefs : SyntaxDef.syntax_def list Pervasives.ref

Basic Types and Syntax Definitions

val string_tp : Term.term

val additional_xslt_name : string

val list_nil_name : string

val list_cons_name : string

val list_nil_sd : SyntaxDef.syntax_def

val list_cons_sd : SyntaxDef.syntax_def

val hlist_empty_name : string

val hlist_one_name : string

val hlist_tp : Term.term

val hlist_name : string

val hlist_cons_name : string

val bit_sd : SyntaxDef.syntax_def

val bit_0_cons_name : string

val bit_tp : Term.term

val bit_name : string

val bit_1_cons_name : string

val char_cons_name : string

val char_name : string

val char_tp : Term.term

val list_tp : Term.term -> Term.term

val list_tp_name : string

val list_sd : SyntaxDef.syntax_def

val list_tp_a : Term.term

val string_name : string

val string_cons_name : string

val boolean_true_name : string

val boolean_name : string

val boolean_tp : Term.term

val boolean_sd : SyntaxDef.syntax_def

val boolean_false_name : string

val boolean_true_sd : SyntaxDef.syntax_def

val boolean_false_sd : SyntaxDef.syntax_def

val term_type_var_name : string

val term_type_var_b_name : string

val term_tp : Term.term

val term_tp_name : string

val term_var_cons_name : string

val term_term_cons_name : string

val rewrite_rule_cons_name : string

val ground_rewrite_rule_cons_name : string

val rewrite_rule_name : string

val rewrite_rule_tp : Term.term

val let_be_name : string

val let_ground_be_name : string

val input_rewrite_rule_tp : Term.term

val input_rewrite_rule_name : string

val let_major_be_name : string

val let_major_ground_be_name : string

val priority_input_rewrite_rule_tp : Term.term

val priority_input_rewrite_rule_name : string

val fun_definition_cons_name : string

val fun_definition_name : string

val fun_definition_tp : Term.term

val syntax_element_str_name : string

val syntax_element_name : string

val syntax_element_tp : Term.term

val syntax_element_tpcons_name : string

val syntax_element_list_elem_name : string

val syntax_element_list_tp : Term.term

val syntax_element_list_name : string

val syntax_element_list_cons_name : string

val syntax_definition_tp : Term.term

val syntax_definition_name : string

val syntax_definition_decl_name : string

val syntax_definition_var_name : string

val syntax_definition_var_op_name : string

val syntax_definition_type_var_name : string

val syntax_definition_type_var_b_name : string

val parsed_tvar_name : string

val parsed_tvar_b_name : string

val parsed_tvar_tp : Term.term

val universal_tvar_name : string

val universal_tvar_b_name : string

val brackets_name : string

val verbatim_name : string

val if_then_else_name : string

val glb_name : string

val assign_name : string

val string_quote_name : string

val close_context_name : string

val path_library_name : string

val path_file_name : string

val load_file_name : string

val set_prop_name : string

val code_as_term_name : string

val get_nonvar_definitions_name : string

val eq_bool_name : string

val ternary_truth_value_tp : Term.term

val ternary_unknown_name : string

val exception_name : string

val is_level_name : string -> bool

val value_level_name : string

val value_pref : Term.term -> Term.term

val level_E_name : string

val level_E_pref : Term.term -> Term.term

val level_D_name : string

val level_D_pref : Term.term -> Term.term

val level_C_name : string

val level_C_pref : Term.term -> Term.term

val level_B_name : string

val level_B_pref : Term.term -> Term.term

val level_A_name : string

val level_A_pref : Term.term -> Term.term

val is_level_ind_name : string -> bool

val value_i_name : string

val level_E_i_name : string

val level_D_i_name : string

val level_C_i_name : string

val level_B_i_name : string

val level_A_i_name : string

val integer_of_level : Term.term -> int

val remove_sharing : Term.term -> Term.term

val needs_brackets : required:Term.term -> provided:Term.term -> bool