| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1250 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (260 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (152 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (146 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (103 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (451 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
Global Index
A
Act [inductive, in Minuska.default_everything]actions_of_ldef [definition, in Minuska.minusl_syntax]
actions_of_decl [definition, in Minuska.minusl_syntax]
Act_eqDec [instance, in Minuska.default_everything]
analyze_list_from_end [definition, in Minuska.prelude]
AO'_getOperator [definition, in Minuska.lowlang]
apply_symbol'' [definition, in Minuska.lowlang]
apply_symbol' [definition, in Minuska.lowlang]
argument_sequence [definition, in Minuska.frontend]
argument_name [definition, in Minuska.frontend]
arity [projection, in Minuska.dt]
B
basic_rule [definition, in Minuska.default_everything]basic_properties [library]
bb_function_names [projection, in Minuska.spec]
bfmap_Z_Z__bool [definition, in Minuska.builtin.klike]
bfmap_Z_Z__Prop [definition, in Minuska.builtin.klike]
bfmap_Z_Z__Z [definition, in Minuska.builtin.klike]
bfmap1 [definition, in Minuska.builtin.klike]
bfmap2 [definition, in Minuska.builtin.klike]
bfmap2P [definition, in Minuska.builtin.klike]
bind_None_T_1 [lemma, in Minuska.prelude]
bind_Some_T_2 [lemma, in Minuska.prelude]
bind_Some_T_1 [lemma, in Minuska.prelude]
bi_sym_info [projection, in Minuska.pval_ocaml_binding]
bi_beta [projection, in Minuska.pval_ocaml_binding]
bi_signature [projection, in Minuska.pval_ocaml_binding]
BoolFunSymbol [inductive, in Minuska.builtin.bool_signature]
BoolFunSymbol_fin [instance, in Minuska.builtin.bool_signature]
BoolFunSymbol_eqdec [instance, in Minuska.builtin.bool_signature]
BoolPredSymbol [inductive, in Minuska.builtin.bool_signature]
BoolPredSymbol_fin [instance, in Minuska.builtin.bool_signature]
BoolPredSymbol_eqdec [instance, in Minuska.builtin.bool_signature]
bool_signature [definition, in Minuska.builtin.bool_signature]
bool_pred_is_true [constructor, in Minuska.builtin.bool_signature]
bool_pred_is_false [constructor, in Minuska.builtin.bool_signature]
bool_pred_is [constructor, in Minuska.builtin.bool_signature]
bool_fun_xor [constructor, in Minuska.builtin.bool_signature]
bool_fun_iff [constructor, in Minuska.builtin.bool_signature]
bool_fun_or [constructor, in Minuska.builtin.bool_signature]
bool_fun_and [constructor, in Minuska.builtin.bool_signature]
bool_fun_neg [constructor, in Minuska.builtin.bool_signature]
bool_fun_false [constructor, in Minuska.builtin.bool_signature]
bool_fun_true [constructor, in Minuska.builtin.bool_signature]
bool_model [definition, in Minuska.builtin.bool_model]
bool_relaxed_model [definition, in Minuska.builtin.bool_model]
bool_model_over [definition, in Minuska.builtin.bool_model]
bool_predicate_interp [definition, in Minuska.builtin.bool_model]
bool_function_interp [definition, in Minuska.builtin.bool_model]
bool_carrier [definition, in Minuska.builtin.bool_model]
bool_signature [library]
bool_model [library]
BoV_to_Expr2 [definition, in Minuska.default_everything]
BoV_to_Expr2 [definition, in Minuska.basic_properties]
bov_variable [constructor, in Minuska.spec]
bov_builtin [constructor, in Minuska.spec]
bps_neg_correct [projection, in Minuska.spec]
bps_neg__sym [projection, in Minuska.spec]
bps_neg_ar [projection, in Minuska.spec]
bps_neg [projection, in Minuska.spec]
bps_ar [projection, in Minuska.spec]
br_value [projection, in Minuska.frontend]
br_kind [projection, in Minuska.frontend]
builtin [projection, in Minuska.spec]
BuiltinInterface [record, in Minuska.pval_ocaml_binding]
BuiltinOrVar [inductive, in Minuska.spec]
BuiltinOrVar_eqdec [instance, in Minuska.basic_properties]
BuiltinOrVar_sind [definition, in Minuska.spec]
BuiltinOrVar_rec [definition, in Minuska.spec]
BuiltinOrVar_ind [definition, in Minuska.spec]
BuiltinOrVar_rect [definition, in Minuska.spec]
BuiltinRepr [record, in Minuska.frontend]
builtins [library]
BuiltinsBinding [record, in Minuska.spec]
builtins_binding [definition, in Minuska.builtin.empty]
builtins_klike [definition, in Minuska.pval_ocaml_binding]
builtins_empty [definition, in Minuska.pval_ocaml_binding]
BuiltinValue [definition, in Minuska.builtin.klike]
BuiltinValue [library]
BuiltinValue0 [inductive, in Minuska.builtin.klike]
BuiltinValue0_countable [instance, in Minuska.builtin.klike]
BuiltinValue0_eqdec [instance, in Minuska.builtin.klike]
BuiltinValue0_eqdec_helper_0 [lemma, in Minuska.builtin.klike]
BuiltinValue0_sind [definition, in Minuska.builtin.klike]
BuiltinValue0_rec [definition, in Minuska.builtin.klike]
BuiltinValue0_ind [definition, in Minuska.builtin.klike]
BuiltinValue0_rect [definition, in Minuska.builtin.klike]
builtin_model_over [projection, in Minuska.spec]
builtin_value_countable [projection, in Minuska.spec]
builtin_value_eqdec [projection, in Minuska.spec]
builtin_value [projection, in Minuska.spec]
builtin_predicate_interp [projection, in Minuska.spec]
builtin_function_interp [projection, in Minuska.spec]
builtin_predicate_symbol_countable [projection, in Minuska.spec]
builtin_predicate_symbol_eqdec [projection, in Minuska.spec]
builtin_predicate_symbol [projection, in Minuska.spec]
builtin_function_symbol_countable [projection, in Minuska.spec]
builtin_function_symbol_eqdec [projection, in Minuska.spec]
builtin_function_symbol [projection, in Minuska.spec]
BVLeaf [inductive, in Minuska.builtin.klike]
BVLeaf_eqdec [instance, in Minuska.builtin.klike]
BVLeaf_sind [definition, in Minuska.builtin.klike]
BVLeaf_rec [definition, in Minuska.builtin.klike]
BVLeaf_ind [definition, in Minuska.builtin.klike]
BVLeaf_rect [definition, in Minuska.builtin.klike]
bvl_sym [constructor, in Minuska.builtin.klike]
bvl_str [constructor, in Minuska.builtin.klike]
bvl_Z [constructor, in Minuska.builtin.klike]
bvl_bool [constructor, in Minuska.builtin.klike]
BVsize [definition, in Minuska.builtin.klike]
bv_to_tree [definition, in Minuska.builtin.klike]
bv_pmap [constructor, in Minuska.builtin.klike]
bv_list [constructor, in Minuska.builtin.klike]
bv_str [constructor, in Minuska.builtin.klike]
bv_sym [constructor, in Minuska.builtin.klike]
bv_Z [constructor, in Minuska.builtin.klike]
bv_bool [constructor, in Minuska.builtin.klike]
b_have_different_symbols [constructor, in Minuska.builtin.klike]
b_have_same_symbol [constructor, in Minuska.builtin.klike]
b_is_not_applied_symbol [constructor, in Minuska.builtin.klike]
b_is_applied_symbol [constructor, in Minuska.builtin.klike]
b_map_hasKey [constructor, in Minuska.builtin.klike]
b_term_eq [constructor, in Minuska.builtin.klike]
b_bool_is_false [constructor, in Minuska.builtin.klike]
b_bool_is_true [constructor, in Minuska.builtin.klike]
b_isNotMap [constructor, in Minuska.builtin.klike]
b_isMap [constructor, in Minuska.builtin.klike]
b_isNotList [constructor, in Minuska.builtin.klike]
b_isList [constructor, in Minuska.builtin.klike]
b_isNotString [constructor, in Minuska.builtin.klike]
b_isString [constructor, in Minuska.builtin.klike]
b_isNotBool [constructor, in Minuska.builtin.klike]
b_isBool [constructor, in Minuska.builtin.klike]
b_isNotZ [constructor, in Minuska.builtin.klike]
b_isZ [constructor, in Minuska.builtin.klike]
b_isNotSymbol [constructor, in Minuska.builtin.klike]
b_isSymbol [constructor, in Minuska.builtin.klike]
b_isNotBuiltin [constructor, in Minuska.builtin.klike]
b_isBuiltin [constructor, in Minuska.builtin.klike]
b_map_update [constructor, in Minuska.builtin.klike]
b_map_lookup [constructor, in Minuska.builtin.klike]
b_bool_neg [constructor, in Minuska.builtin.klike]
b_Z_neq [constructor, in Minuska.builtin.klike]
b_Z_eq [constructor, in Minuska.builtin.klike]
b_Z_isGt [constructor, in Minuska.builtin.klike]
b_Z_isGe [constructor, in Minuska.builtin.klike]
b_Z_isLt [constructor, in Minuska.builtin.klike]
b_Z_isLe [constructor, in Minuska.builtin.klike]
b_Z_div [constructor, in Minuska.builtin.klike]
b_Z_times [constructor, in Minuska.builtin.klike]
b_Z_minus [constructor, in Minuska.builtin.klike]
b_Z_plus [constructor, in Minuska.builtin.klike]
b_map_size [constructor, in Minuska.builtin.klike]
b_map_empty [constructor, in Minuska.builtin.klike]
b_list_empty [constructor, in Minuska.builtin.klike]
b_zero [constructor, in Minuska.builtin.klike]
C
cancel_TermOver_map [instance, in Minuska.lowlang]cancel_uglify_prettify [instance, in Minuska.lowlang]
cancel_prettify_uglify [instance, in Minuska.lowlang]
cd_cseq_context [projection, in Minuska.frontend]
cd_isValue [projection, in Minuska.frontend]
cd_positions_to_wait_for [projection, in Minuska.frontend]
cd_position [projection, in Minuska.frontend]
cd_arity [projection, in Minuska.frontend]
cd_sym [projection, in Minuska.frontend]
cd_label [projection, in Minuska.frontend]
ClauseMatrix [definition, in Minuska.dt]
ClauseMatrix_size [definition, in Minuska.dt]
cmmatch [definition, in Minuska.dt]
compactify [definition, in Minuska.martelli_montanari]
compactify_keeps_equiv_UP [lemma, in Minuska.martelli_montanari]
compactify_keeps_valid_u [lemma, in Minuska.martelli_montanari]
compactify_is_compact [lemma, in Minuska.martelli_montanari]
compactify_by_vars_keeps_equiv_UP [lemma, in Minuska.martelli_montanari]
compactify_by_vars_keeps_u_valid [lemma, in Minuska.martelli_montanari]
compactify_by_vars_keeps_get_vars [lemma, in Minuska.martelli_montanari]
compactify_by_vars_is_compact_up_to_vars [lemma, in Minuska.martelli_montanari]
compactify_by_vars_keeps_compactness [lemma, in Minuska.martelli_montanari]
compactify_by_vars_inv_fold [lemma, in Minuska.martelli_montanari]
compactify_by_var_keeps_unifier_of [lemma, in Minuska.martelli_montanari]
compactify_by_var_keeps_up_of_u [lemma, in Minuska.martelli_montanari]
compactify_by_var_keeps_u_valid [lemma, in Minuska.martelli_montanari]
compactify_by_var_keeps_previous_compactness [lemma, in Minuska.martelli_montanari]
compactify_by_var_meqn_only_in_u' [lemma, in Minuska.martelli_montanari]
compactify_by_var_meqn_in_v_in [lemma, in Minuska.martelli_montanari]
compactify_by_var_keeps_get_vars [lemma, in Minuska.martelli_montanari]
compactify_by_var_is_compact_up_to_var [lemma, in Minuska.martelli_montanari]
compactify_by_var_v_in_meqn [lemma, in Minuska.martelli_montanari]
compactify_by_var_v_not_in_meqn [lemma, in Minuska.martelli_montanari]
compactify_by_var_meqn_inv_rg [lemma, in Minuska.martelli_montanari]
compactify_by_vars [definition, in Minuska.martelli_montanari]
compactify_by_var [definition, in Minuska.martelli_montanari]
compactify_by_var_extract_and_comp [definition, in Minuska.martelli_montanari]
compile [definition, in Minuska.minusl_compile]
compile [definition, in Minuska.dt]
CompileT [definition, in Minuska.minusl_compile]
compile' [definition, in Minuska.minusl_compile]
compose_uglify_prettify [lemma, in Minuska.lowlang]
compose_prettify_uglify [lemma, in Minuska.lowlang]
concat_list_option_str [definition, in Minuska.interp_loop]
concrete_is_larger_than_symbolic [lemma, in Minuska.properties]
conservative_merge [library]
Constructor [projection, in Minuska.dt]
Constructor_eqdec [projection, in Minuska.dt]
ContextDeclaration [record, in Minuska.frontend]
ContextTemplate [definition, in Minuska.frontend]
cooling_rule [definition, in Minuska.frontend]
countable [section, in Minuska.lowlang]
count_one_split [lemma, in Minuska.prelude]
create_eqn [definition, in Minuska.martelli_montanari]
cseq [definition, in Minuska.frontend]
ctx_cool [definition, in Minuska.minusl_compile]
ctx_heat [definition, in Minuska.minusl_compile]
custom_induction_principle_2 [section, in Minuska.basic_properties]
custom_induction_principle_2 [section, in Minuska.basic_properties]
custom_induction_principle [section, in Minuska.spec]
custom_induction_principle [section, in Minuska.spec]
custom_induction_principle [section, in Minuska.dt]
custom_induction_principle [section, in Minuska.dt]
D
dec [definition, in Minuska.martelli_montanari]DecisionTree [inductive, in Minuska.dt]
DecisionTree_sind [definition, in Minuska.dt]
DecisionTree_rec [definition, in Minuska.dt]
DecisionTree_ind [definition, in Minuska.dt]
DecisionTree_rect [definition, in Minuska.dt]
Declaration [inductive, in Minuska.frontend]
Declaration_sind [definition, in Minuska.frontend]
Declaration_rec [definition, in Minuska.frontend]
Declaration_ind [definition, in Minuska.frontend]
Declaration_rect [definition, in Minuska.frontend]
decl_strict [constructor, in Minuska.frontend]
decl_ctx [constructor, in Minuska.frontend]
decl_rule [constructor, in Minuska.frontend]
dec_paper_input1 [definition, in Minuska.martelli_montanari_tests]
dec_keeps_equiv_UP [lemma, in Minuska.martelli_montanari]
dec_exists [lemma, in Minuska.martelli_montanari]
dec_aux_TermOver_size_enough [lemma, in Minuska.martelli_montanari]
dec_aux [definition, in Minuska.martelli_montanari]
dec_make_multeq [definition, in Minuska.martelli_montanari]
Default [definition, in Minuska.dt]
Defaults [record, in Minuska.frontend]
default_act [constructor, in Minuska.default_everything]
default_isValue [projection, in Minuska.frontend]
default_context_template [projection, in Minuska.frontend]
default_empty_cseq_name [projection, in Minuska.frontend]
default_cseq_name [projection, in Minuska.frontend]
default_model [definition, in Minuska.default_static_model]
default_model [section, in Minuska.default_static_model]
Default_correct [lemma, in Minuska.dt]
default_static_model [library]
default_everything [library]
deg [definition, in Minuska.textbook_unification_alg]
deg_cons_lt [lemma, in Minuska.textbook_unification_alg]
deg_swap_head [lemma, in Minuska.textbook_unification_alg]
delta_in_val [definition, in Minuska.properties]
dom_merge_use_left [lemma, in Minuska.valuation_merge]
double_satisfies_contradiction [lemma, in Minuska.properties]
downC [definition, in Minuska.minusl_compile]
down2 [definition, in Minuska.minusl_compile]
down2E [definition, in Minuska.minusl_compile]
DSM [instance, in Minuska.default_everything]
dt [library]
dtsem_switch_default [constructor, in Minuska.dt]
dtsem_switch_constr [constructor, in Minuska.dt]
dtsem_swap [constructor, in Minuska.dt]
dtsem_yield_continue [constructor, in Minuska.dt]
dtsem_yield_now [constructor, in Minuska.dt]
dt_sem_aux_sind [definition, in Minuska.dt]
dt_sem_aux_ind [definition, in Minuska.dt]
dt_sem_sind [definition, in Minuska.dt]
dt_sem_ind [definition, in Minuska.dt]
dt_sem_aux_cont [constructor, in Minuska.dt]
dt_sem_aux_default [constructor, in Minuska.dt]
dt_sem_aux_found [constructor, in Minuska.dt]
dt_sem_aux [inductive, in Minuska.dt]
dt_sem [inductive, in Minuska.dt]
dt_swap [constructor, in Minuska.dt]
dt_switch [constructor, in Minuska.dt]
dt_yield [constructor, in Minuska.dt]
dt_fail [constructor, in Minuska.dt]
E
eab_bov [projection, in Minuska.notations]eab_expr [projection, in Minuska.notations]
eject [definition, in Minuska.builtin.empty]
elem_of_next [lemma, in Minuska.basic_properties]
elem_of_list_fmap_T_1 [lemma, in Minuska.prelude]
elem_of_union_meqn [lemma, in Minuska.martelli_montanari]
elem_of_singleton_meqn [lemma, in Minuska.martelli_montanari]
empty [library]
emptyCseq [definition, in Minuska.frontend]
Emptyset [inductive, in Minuska.builtin.empty]
emptyset_fin [instance, in Minuska.builtin.empty]
emptyset_eqdec [instance, in Minuska.builtin.empty]
Emptyset_sind [definition, in Minuska.builtin.empty]
Emptyset_rec [definition, in Minuska.builtin.empty]
Emptyset_ind [definition, in Minuska.builtin.empty]
Emptyset_rect [definition, in Minuska.builtin.empty]
enveloping_preserves_or_increases_delta [lemma, in Minuska.properties]
eqdec [section, in Minuska.lowlang]
eqn [definition, in Minuska.textbook_unification_alg]
eqn [definition, in Minuska.martelli_montanari]
eqns_vars_zip [lemma, in Minuska.textbook_unification_alg]
eqns_vars_app [lemma, in Minuska.textbook_unification_alg]
eqns_vars_sub [lemma, in Minuska.textbook_unification_alg]
eqns_vars_cons [lemma, in Minuska.textbook_unification_alg]
eqns_vars [definition, in Minuska.textbook_unification_alg]
eqns_size [definition, in Minuska.textbook_unification_alg]
eqns_vars_hd_comm [lemma, in Minuska.textbook_unification]
eqn_vars [definition, in Minuska.textbook_unification_alg]
eqn_size [definition, in Minuska.textbook_unification_alg]
equiv_UP [definition, in Minuska.martelli_montanari]
eval_function_in_iflow [definition, in Minuska.builtin.information_flow_functor]
eval_function_in_orig [definition, in Minuska.builtin.information_flow_functor]
eval_predicate_in_iflow [definition, in Minuska.builtin.information_flow_functor]
eval_predicate_in_orig [definition, in Minuska.builtin.information_flow_functor]
eval_et_extensive_Some [lemma, in Minuska.naive_interpreter]
eval_et_evaluate_None_relative [lemma, in Minuska.naive_interpreter]
eval_et_correct_2 [lemma, in Minuska.naive_interpreter]
eval_et_correct [lemma, in Minuska.naive_interpreter]
eval_et_strip [lemma, in Minuska.naive_interpreter]
eval_et_strip_helper [lemma, in Minuska.naive_interpreter]
eval_et_Some_val [lemma, in Minuska.naive_interpreter]
eval_et [definition, in Minuska.naive_interpreter]
example_list_int_model_1 [definition, in Minuska.builtin.example_list_int_model]
example_list_int_model [library]
ExprAndBoV [record, in Minuska.notations]
Expression2 [inductive, in Minuska.spec]
Expression2Term_matches_enough [lemma, in Minuska.properties]
Expression2_countable [instance, in Minuska.basic_properties]
Expression2_subst [definition, in Minuska.basic_properties]
Expression2_rect [definition, in Minuska.basic_properties]
Expression2_eqdec [lemma, in Minuska.basic_properties]
Expression2_evaluate [definition, in Minuska.spec]
Expression2_ind [definition, in Minuska.spec]
Expression2_evalute_strip [lemma, in Minuska.properties]
Expression2_evaluate_None_relative [lemma, in Minuska.properties]
Expression2_evaluate_total_1 [lemma, in Minuska.properties]
Expression2_evaluate_extensive_Some [lemma, in Minuska.properties]
Expression2_evaluate_nv [definition, in Minuska.naive_interpreter]
extract_mgu_contains_var [lemma, in Minuska.martelli_montanari]
extract_mgu [definition, in Minuska.martelli_montanari]
extract_mgu_aux [definition, in Minuska.martelli_montanari]
E_from_to_tree [lemma, in Minuska.basic_properties]
E_of_tree [definition, in Minuska.basic_properties]
E_to_tree [definition, in Minuska.basic_properties]
e_query [constructor, in Minuska.spec]
e_fun [constructor, in Minuska.spec]
e_variable [constructor, in Minuska.spec]
e_ground [constructor, in Minuska.spec]
F
fewer_arrows_lower_degree [lemma, in Minuska.textbook_unification_alg]filter_fmap [lemma, in Minuska.prelude]
flat_map_lookup_Some [lemma, in Minuska.prelude]
fmap_uglify_prettify_option [lemma, in Minuska.lowlang]
fmap_prettify_uglify_option [lemma, in Minuska.lowlang]
fmap_uglify_prettify_list [lemma, in Minuska.lowlang]
fmap_prettify_uglify_list [lemma, in Minuska.lowlang]
fmap_Some_T_1 [lemma, in Minuska.prelude]
forall_satisfies_inv [lemma, in Minuska.properties]
forall_satisfies_inv' [lemma, in Minuska.properties]
format_string_list [definition, in Minuska.prelude]
framed_rule [definition, in Minuska.default_everything]
freezer [definition, in Minuska.frontend]
from_to_tree [lemma, in Minuska.builtin.klike]
frontend [library]
FunctionSymbol [inductive, in Minuska.builtin.klike]
FunctionSymbol_fin [instance, in Minuska.builtin.klike]
FunctionSymbol_eqDec [instance, in Minuska.builtin.klike]
FunctionSymbol_sind [definition, in Minuska.builtin.klike]
FunctionSymbol_rec [definition, in Minuska.builtin.klike]
FunctionSymbol_ind [definition, in Minuska.builtin.klike]
FunctionSymbol_rect [definition, in Minuska.builtin.klike]
function_interp_sum [definition, in Minuska.model_algebra]
function_symbol_morphism [projection, in Minuska.signature_morphism]
G
getSubterm [definition, in Minuska.dt]get_vars_of_M_listset_meqns [definition, in Minuska.martelli_montanari]
get_vars_of_S_listset_meqns_equiv [lemma, in Minuska.martelli_montanari]
get_vars_of_S_listset_meqns [definition, in Minuska.martelli_montanari]
get_vars_of_M_meqns [definition, in Minuska.martelli_montanari]
get_vars_of_S_list_meqns_equiv [lemma, in Minuska.martelli_montanari]
get_vars_of_S_list_meqns [definition, in Minuska.martelli_montanari]
get_nonvar_part [definition, in Minuska.martelli_montanari]
get_var_part [definition, in Minuska.martelli_montanari]
global_naive_interpreter_sound [definition, in Minuska.default_everything]
global_naive_interpreter_ext [definition, in Minuska.default_everything]
global_naive_interpreter [definition, in Minuska.default_everything]
GT [definition, in Minuska.default_everything]
gt_term [definition, in Minuska.default_everything]
gt_over [definition, in Minuska.default_everything]
H
hasDepthExactly [definition, in Minuska.minusl_compile_properties]hd [projection, in Minuska.spec]
heating_rule_seq [definition, in Minuska.frontend]
helper [definition, in Minuska.lowlang]
helper_lemma_3 [lemma, in Minuska.textbook_unification]
helper_lemma_2 [lemma, in Minuska.textbook_unification]
helper_lemma_1 [lemma, in Minuska.textbook_unification]
helper'' [definition, in Minuska.lowlang]
h_in_l_impl_length_filter_l_gt_1 [lemma, in Minuska.prelude]
I
IFCRelaxedModelTrait0 [record, in Minuska.builtin.information_flow_functor]IFCRelaxedModelTrait1 [record, in Minuska.builtin.information_flow_functor]
ifc_pure_function [projection, in Minuska.builtin.information_flow_functor]
ifc_pure_predicate [projection, in Minuska.builtin.information_flow_functor]
ifc_0 [projection, in Minuska.builtin.information_flow_functor]
ifc_get_pure_of_tagged [projection, in Minuska.builtin.information_flow_functor]
ifc_get_tags_of_tagged [projection, in Minuska.builtin.information_flow_functor]
ifc_get_pure [projection, in Minuska.builtin.information_flow_functor]
ifc_get_tags [projection, in Minuska.builtin.information_flow_functor]
ifc_tagged [projection, in Minuska.builtin.information_flow_functor]
IFLattice [record, in Minuska.builtin.information_flow_functor]
ifl_meet_top [projection, in Minuska.builtin.information_flow_functor]
ifl_top [projection, in Minuska.builtin.information_flow_functor]
ifl_join_bot [projection, in Minuska.builtin.information_flow_functor]
ifl_bot [projection, in Minuska.builtin.information_flow_functor]
ifl_absorb_2 [projection, in Minuska.builtin.information_flow_functor]
ifl_absorb_1 [projection, in Minuska.builtin.information_flow_functor]
ifl_join_comm [projection, in Minuska.builtin.information_flow_functor]
ifl_join_assoc [projection, in Minuska.builtin.information_flow_functor]
ifl_join [projection, in Minuska.builtin.information_flow_functor]
ifl_meet_comm [projection, in Minuska.builtin.information_flow_functor]
ifl_meet_assoc [projection, in Minuska.builtin.information_flow_functor]
ifl_meet [projection, in Minuska.builtin.information_flow_functor]
Implementation [module, in Minuska.symex]
impl_isMap [definition, in Minuska.builtin.klike]
impl_isList [definition, in Minuska.builtin.klike]
impl_isBool [definition, in Minuska.builtin.klike]
impl_isString [definition, in Minuska.builtin.klike]
impl_isZ [definition, in Minuska.builtin.klike]
information_flow_functor_trait [instance, in Minuska.builtin.information_flow_functor]
information_flow_functor_get_pure [definition, in Minuska.builtin.information_flow_functor]
information_flow_functor_get_tags [definition, in Minuska.builtin.information_flow_functor]
information_flow_functor_tagged [definition, in Minuska.builtin.information_flow_functor]
information_flow_functor [definition, in Minuska.builtin.information_flow_functor]
information_flow_functor [library]
initialState [definition, in Minuska.frontend]
init_r_keeps_UP [lemma, in Minuska.martelli_montanari]
init_r_valid [lemma, in Minuska.martelli_montanari]
init_r [definition, in Minuska.martelli_montanari]
init_r' [definition, in Minuska.martelli_montanari]
init_meqn [definition, in Minuska.martelli_montanari]
inject [projection, in Minuska.model_algebra]
Injection [record, in Minuska.model_algebra]
inject_inj [projection, in Minuska.model_algebra]
inject_string [definition, in Minuska.builtin.empty]
inject_Z [definition, in Minuska.builtin.empty]
inject_bool [definition, in Minuska.builtin.empty]
inj_id [definition, in Minuska.model_algebra]
inj_compose [definition, in Minuska.model_algebra]
inspect [definition, in Minuska.prelude]
Interpreter [definition, in Minuska.spec_interpreter]
Interpreter_sound [definition, in Minuska.spec_interpreter]
Interpreter_sound' [definition, in Minuska.spec_interpreter]
Interpreter_ext [definition, in Minuska.spec_interpreter]
interpreter_results [library]
interp_in_from [definition, in Minuska.interp_loop]
interp_in_from' [definition, in Minuska.interp_loop]
interp_loop_ext [definition, in Minuska.interp_loop]
interp_loop [definition, in Minuska.interp_loop]
interp_loop [library]
IntFunSymbol [inductive, in Minuska.builtin.int_signature]
IntFunSymbol_fin [instance, in Minuska.builtin.int_signature]
IntFunSymbol_eqdec [instance, in Minuska.builtin.int_signature]
IntPredSymbol [inductive, in Minuska.builtin.int_signature]
IntPredSymbol_fin [instance, in Minuska.builtin.int_signature]
IntPredSymbol_eqdec [instance, in Minuska.builtin.int_signature]
int_signature [definition, in Minuska.builtin.int_signature]
int_is [constructor, in Minuska.builtin.int_signature]
int_lt [constructor, in Minuska.builtin.int_signature]
int_le [constructor, in Minuska.builtin.int_signature]
int_eq [constructor, in Minuska.builtin.int_signature]
int_one [constructor, in Minuska.builtin.int_signature]
int_zero [constructor, in Minuska.builtin.int_signature]
int_uminus [constructor, in Minuska.builtin.int_signature]
int_minus [constructor, in Minuska.builtin.int_signature]
int_plus [constructor, in Minuska.builtin.int_signature]
int_model [definition, in Minuska.builtin.int_model]
int_relaxed_model [definition, in Minuska.builtin.int_model]
int_model_over [definition, in Minuska.builtin.int_model]
int_predicate_interp [definition, in Minuska.builtin.int_model]
int_function_interp [definition, in Minuska.builtin.int_model]
int_carrier [definition, in Minuska.builtin.int_model]
int_signature [library]
int_model [library]
invisible_act [constructor, in Minuska.default_everything]
in_compile_inv [lemma, in Minuska.minusl_compile_properties]
isDownC [definition, in Minuska.minusl_compile_properties]
IsDownC_dec [instance, in Minuska.minusl_compile_properties]
isHeadInFirstColumn [definition, in Minuska.dt]
is_unifier_of_extensive [lemma, in Minuska.textbook_unification]
is_subterm_antisym [lemma, in Minuska.textbook_unification]
is_subterm_size [lemma, in Minuska.textbook_unification]
is_unifier_of_app [lemma, in Minuska.textbook_unification]
is_unifier_of_cons [lemma, in Minuska.textbook_unification]
is_unifier_of [definition, in Minuska.textbook_unification]
is_subterm_sizes [lemma, in Minuska.basic_properties]
is_subterm_b [definition, in Minuska.basic_properties]
is_compact_up_to_vars_is_compact [lemma, in Minuska.martelli_montanari]
is_compact_up_to_var_at_most_one_meqn_with_var [lemma, in Minuska.martelli_montanari]
is_compact [definition, in Minuska.martelli_montanari]
is_compact_up_to_vars [definition, in Minuska.martelli_montanari]
is_compact_up_to_var [definition, in Minuska.martelli_montanari]
is_unifier_of [definition, in Minuska.martelli_montanari]
is_WildcardPattern_dec [instance, in Minuska.dt]
is_WildcardPattern [definition, in Minuska.dt]
is_ConstructorPattern_dec [instance, in Minuska.dt]
is_ConstructorPattern [definition, in Minuska.dt]
K
klike [library]L
least_of_nil_nil [lemma, in Minuska.textbook_unification]least_of [definition, in Minuska.textbook_unification]
length_filter_eq__eq__length_filter_in__one [lemma, in Minuska.prelude]
length_filter_eq__eq__length_filter_in__zero [lemma, in Minuska.prelude]
length_filter_l_1_impl_h_in_l' [lemma, in Minuska.prelude]
length_filter_l_1_impl_h_in_l [lemma, in Minuska.prelude]
length_list_collect_Some [lemma, in Minuska.prelude]
length_pfmap [lemma, in Minuska.prelude]
liftBinary [definition, in Minuska.builtin.klike]
liftBinaryP [definition, in Minuska.builtin.klike]
liftNulary [definition, in Minuska.builtin.klike]
liftNularyP [definition, in Minuska.builtin.klike]
liftTernary [definition, in Minuska.builtin.klike]
liftUnary [definition, in Minuska.builtin.klike]
liftUnaryP [definition, in Minuska.builtin.klike]
ListFunSymbol [inductive, in Minuska.builtin.list_signature]
ListFunSymbol_fin [instance, in Minuska.builtin.list_signature]
ListFunSymbol_eqdec [instance, in Minuska.builtin.list_signature]
ListPredSymbol [inductive, in Minuska.builtin.list_signature]
ListPredSymbol_fin [instance, in Minuska.builtin.list_signature]
ListPredSymbol_eqdec [instance, in Minuska.builtin.list_signature]
listset_eqdec [instance, in Minuska.martelli_montanari]
list_filter_Forall_all [lemma, in Minuska.prelude]
list_filter_Forall_not [lemma, in Minuska.prelude]
list_collect_Forall_T [lemma, in Minuska.prelude]
list_collect_Exists_1 [lemma, in Minuska.prelude]
list_collect_Forall [lemma, in Minuska.prelude]
list_collect_Exists [lemma, in Minuska.prelude]
list_collect_inv [lemma, in Minuska.prelude]
list_collect [definition, in Minuska.prelude]
list_find_elem_of_isSome [lemma, in Minuska.prelude]
list_collect_Expression2_evaluate_extensive_Some [lemma, in Minuska.properties]
list_collect_e [definition, in Minuska.frontend]
list_signature [definition, in Minuska.builtin.list_signature]
list_is [constructor, in Minuska.builtin.list_signature]
list_is_nil [constructor, in Minuska.builtin.list_signature]
list_tail [constructor, in Minuska.builtin.list_signature]
list_head [constructor, in Minuska.builtin.list_signature]
list_cons [constructor, in Minuska.builtin.list_signature]
list_nil [constructor, in Minuska.builtin.list_signature]
list_swap_head_involutive [lemma, in Minuska.dt]
list_swap_head [definition, in Minuska.dt]
list_relaxed_functor [definition, in Minuska.builtin.list_model]
list_predicate_interp [definition, in Minuska.builtin.list_model]
list_function_interp [definition, in Minuska.builtin.list_model]
list_model [library]
list_signature [library]
lowlang [library]
ls_to_bor_dec [instance, in Minuska.martelli_montanari]
M
map_uglify'_inj [lemma, in Minuska.lowlang]map_lookup_Some [lemma, in Minuska.prelude]
martelli_montanari_tests [library]
martelli_montanari [library]
Meqn [definition, in Minuska.martelli_montanari]
meqns_s_intersect [definition, in Minuska.martelli_montanari]
meqn_union_list_elem_of_get_nonvar_part [lemma, in Minuska.martelli_montanari]
meqn_get_nonvar_part_mjoin_union_list [lemma, in Minuska.martelli_montanari]
meqn_valid_elem_of_in [lemma, in Minuska.martelli_montanari]
meqn_valid [definition, in Minuska.martelli_montanari]
meqn_left_valid [definition, in Minuska.martelli_montanari]
meqn_right_valid [definition, in Minuska.martelli_montanari]
meqn_semiset [instance, in Minuska.martelli_montanari]
meqn_singleton [instance, in Minuska.martelli_montanari]
meqn_union [instance, in Minuska.martelli_montanari]
meqn_equivalence [instance, in Minuska.martelli_montanari]
meqn_equivalent_trans [lemma, in Minuska.martelli_montanari]
meqn_equivalent_symm [lemma, in Minuska.martelli_montanari]
meqn_equivalent_refl [lemma, in Minuska.martelli_montanari]
meqn_equiv [instance, in Minuska.martelli_montanari]
meqn_elem_of [instance, in Minuska.martelli_montanari]
meqn_empty [instance, in Minuska.martelli_montanari]
meqn_m_empty [definition, in Minuska.martelli_montanari]
meqn_dec [instance, in Minuska.martelli_montanari]
meqn_subst [definition, in Minuska.martelli_montanari]
merge_use_left_below [lemma, in Minuska.valuation_merge]
merge_valuations_dom [lemma, in Minuska.valuation_merge]
merge_use_left_subseteq [lemma, in Minuska.valuation_merge]
merge_valuations_empty_l [lemma, in Minuska.valuation_merge]
merge_valuations_empty_r [lemma, in Minuska.valuation_merge]
mgu_res [definition, in Minuska.martelli_montanari_tests]
minuska [library]
MinusL_rewrites_sind [definition, in Minuska.minusl_semantics]
MinusL_rewrites_rec [definition, in Minuska.minusl_semantics]
MinusL_rewrites_ind [definition, in Minuska.minusl_semantics]
MinusL_rewrites_rect [definition, in Minuska.minusl_semantics]
MinusL_rewrites [inductive, in Minuska.minusl_semantics]
MinusL_sem [section, in Minuska.minusl_semantics]
MinusL_isNonValue [definition, in Minuska.minusl_syntax]
MinusL_isValue [definition, in Minuska.minusl_syntax]
MinusL_LangDef_wf [definition, in Minuska.minusl_syntax]
MinusL_LangDef [record, in Minuska.minusl_syntax]
MinusL_Decl_eqDec [instance, in Minuska.minusl_syntax]
MinusL_Decl [inductive, in Minuska.minusl_syntax]
minusl_compile [library]
minusl_semantics [library]
minusl_syntax [library]
minusl_compile_properties [library]
mkSwitchCaseList [constructor, in Minuska.dt]
mld_context [constructor, in Minuska.minusl_syntax]
mld_rewrite [constructor, in Minuska.minusl_syntax]
mlld_decls [projection, in Minuska.minusl_syntax]
mlld_isValue_var [projection, in Minuska.minusl_syntax]
mlld_isNonValue_c [projection, in Minuska.minusl_syntax]
mlld_isValue_c [projection, in Minuska.minusl_syntax]
mlr_context [constructor, in Minuska.minusl_semantics]
mlr_trans [constructor, in Minuska.minusl_semantics]
mlr_rule [constructor, in Minuska.minusl_semantics]
mlr_refl [constructor, in Minuska.minusl_semantics]
Model [record, in Minuska.spec]
ModelOver [record, in Minuska.spec]
modelover_nv_lift [definition, in Minuska.model_algebra]
modelover_sum_reduce_2 [lemma, in Minuska.model_algebra]
modelover_sum_reduce_1 [lemma, in Minuska.model_algebra]
modelover_sum [definition, in Minuska.model_algebra]
model_reduction [definition, in Minuska.model_algebra]
model_of_relaxed [definition, in Minuska.model_algebra]
model_algebra [library]
model_traits [library]
model_functor [library]
MVariables [record, in Minuska.spec]
MyProgramInfo [instance, in Minuska.pi.trivial]
MyQuerySymbol [inductive, in Minuska.pi.trivial]
MyQuerySymbol_fin [instance, in Minuska.pi.trivial]
MyQuerySymbol_eqdec [instance, in Minuska.pi.trivial]
MyQuerySymbol_sind [definition, in Minuska.pi.trivial]
MyQuerySymbol_rec [definition, in Minuska.pi.trivial]
MyQuerySymbol_ind [definition, in Minuska.pi.trivial]
MyQuerySymbol_rect [definition, in Minuska.pi.trivial]
mysignature [instance, in Minuska.builtin.klike]
mysignature [instance, in Minuska.builtin.empty]
MySymbols [instance, in Minuska.default_static_model]
mytt [constructor, in Minuska.prelude]
MyUnit [inductive, in Minuska.prelude]
MyUnit_sind [definition, in Minuska.prelude]
MyUnit_rec [definition, in Minuska.prelude]
MyUnit_ind [definition, in Minuska.prelude]
MyUnit_rect [definition, in Minuska.prelude]
my_binding [definition, in Minuska.pi.trivial]
my_decode [definition, in Minuska.builtin.klike]
my_encode [definition, in Minuska.builtin.klike]
N
naive_interpreter_sound [lemma, in Minuska.naive_interpreter]naive_interpreter [definition, in Minuska.naive_interpreter]
naive_interpreter_ext [definition, in Minuska.naive_interpreter]
naive_interpreter [library]
nat_builtin [library]
ni_list_different [constructor, in Minuska.dt]
ni_ctor_diferent [constructor, in Minuska.dt]
NondetValue [projection, in Minuska.spec]
nondet_gen [projection, in Minuska.spec]
notations [library]
notinstance [inductive, in Minuska.dt]
notinstance_sind [definition, in Minuska.dt]
notinstance_ind [definition, in Minuska.dt]
not_subterm_subst [lemma, in Minuska.basic_properties]
not_stuck [definition, in Minuska.spec_interpreter]
not_elem_of_empty_meqn [lemma, in Minuska.martelli_montanari]
O
Occurrence [definition, in Minuska.dt]on_distinct_vars [lemma, in Minuska.textbook_unification]
on_a_shared_prefix [lemma, in Minuska.prelude]
option_Valuation2_vars_of [instance, in Minuska.valuation_merge]
P
partition_fl_false_equiv [lemma, in Minuska.martelli_montanari]partition_tl_true_equiv [lemma, in Minuska.martelli_montanari]
partition_tl_fl_disjunct [lemma, in Minuska.martelli_montanari]
partition_fl_means_false [lemma, in Minuska.martelli_montanari]
partition_tl_means_true [lemma, in Minuska.martelli_montanari]
partition_true_in_tl [lemma, in Minuska.martelli_montanari]
Pattern [inductive, in Minuska.dt]
PatternMatrice [definition, in Minuska.dt]
PatternVector [definition, in Minuska.dt]
Pattern_ind [definition, in Minuska.dt]
pflookup [definition, in Minuska.prelude]
pflookup_spec [lemma, in Minuska.prelude]
pfmap [definition, in Minuska.prelude]
pfmap_lookup_Some_1 [lemma, in Minuska.prelude]
pfmap_lookup_Some_lt [lemma, in Minuska.prelude]
pi_symbol_interp [projection, in Minuska.spec]
pi_trivial [definition, in Minuska.pval_ocaml_binding]
PredicateSymbol [inductive, in Minuska.builtin.klike]
PredicateSymbol_fin [instance, in Minuska.builtin.klike]
PredicateSymbol_eqDec [instance, in Minuska.builtin.klike]
PredicateSymbol_sind [definition, in Minuska.builtin.klike]
PredicateSymbol_rec [definition, in Minuska.builtin.klike]
PredicateSymbol_ind [definition, in Minuska.builtin.klike]
PredicateSymbol_rect [definition, in Minuska.builtin.klike]
predicate_interp_sum [definition, in Minuska.model_algebra]
predicate_symbol_morphism [projection, in Minuska.signature_morphism]
prelude [library]
PreTerm' [inductive, in Minuska.lowlang]
PreTerm'_zipWith [definition, in Minuska.lowlang]
PreTerm'_collapse_option [definition, in Minuska.lowlang]
PreTerm'_A_B_fmap [instance, in Minuska.lowlang]
PreTerm'_fmap [definition, in Minuska.lowlang]
PreTerm'_countable [instance, in Minuska.lowlang]
PreTerm'_of_to_gen_tree [lemma, in Minuska.lowlang]
PreTerm'_of_gen_tree [definition, in Minuska.lowlang]
PreTerm'_to_gen_tree [definition, in Minuska.lowlang]
PreTerm'_eqdec [instance, in Minuska.lowlang]
PreTerm'_get_symbol [definition, in Minuska.lowlang]
PreTerm'_sind [definition, in Minuska.lowlang]
PreTerm'_rec [definition, in Minuska.lowlang]
PreTerm'_ind [definition, in Minuska.lowlang]
PreTerm'_rect [definition, in Minuska.lowlang]
prettify [definition, in Minuska.lowlang]
prettify' [definition, in Minuska.lowlang]
process_declarations [definition, in Minuska.frontend]
process_declaration [definition, in Minuska.frontend]
process_strictness_declaration [definition, in Minuska.frontend]
process_context_declaration [definition, in Minuska.frontend]
process_rule_declaration [definition, in Minuska.frontend]
ProgramInfo [record, in Minuska.spec]
ProgramT [projection, in Minuska.spec]
program_info [projection, in Minuska.spec]
projTopCont [definition, in Minuska.minusl_compile_properties]
projTopCtrl [definition, in Minuska.minusl_compile_properties]
projTopData [definition, in Minuska.minusl_compile_properties]
properties [library]
pt_app_ao [constructor, in Minuska.lowlang]
pt_app_operand [constructor, in Minuska.lowlang]
pt_operator [constructor, in Minuska.lowlang]
pval_ocaml_binding [library]
pvmatch [inductive, in Minuska.dt]
pvmatch_sind [definition, in Minuska.dt]
pvmatch_ind [definition, in Minuska.dt]
pvm_ctor [constructor, in Minuska.dt]
pvm_wildcard [constructor, in Minuska.dt]
pvvecmatch [definition, in Minuska.dt]
p_cpat [constructor, in Minuska.dt]
p_wildcard [constructor, in Minuska.dt]
Q
qs_program [constructor, in Minuska.pi.trivial]QuerySymbol [projection, in Minuska.spec]
QuerySymbol_countable [projection, in Minuska.spec]
QuerySymbol_eqdec [projection, in Minuska.spec]
R
R [definition, in Minuska.martelli_montanari]rd_rule [projection, in Minuska.frontend]
rd_label [projection, in Minuska.frontend]
Realization [record, in Minuska.frontend]
realize_thy [definition, in Minuska.frontend]
realize_br [projection, in Minuska.frontend]
RelaxedModel [record, in Minuska.model_algebra]
RelaxedModelFunctorT [record, in Minuska.model_algebra]
REST_SEQ [definition, in Minuska.frontend]
ReversibleInjection [record, in Minuska.model_algebra]
rev_ind_T [lemma, in Minuska.prelude]
rev_list_ind_T [lemma, in Minuska.prelude]
rewrites_to_thy [definition, in Minuska.spec]
rewrites_to_nondet [definition, in Minuska.spec]
rewrites_to [definition, in Minuska.spec]
rewrites_in_valuation_under_to [definition, in Minuska.spec]
RewritingRule2 [record, in Minuska.spec]
RewritingRule2_eqdec [instance, in Minuska.basic_properties]
RewritingRule2_wf [definition, in Minuska.spec_interpreter]
RewritingTheory2 [definition, in Minuska.spec]
RewritingTheory2_wf_dec [instance, in Minuska.interpreter_results]
RewritingTheory2_wf [definition, in Minuska.spec_interpreter]
rewriting_relation [definition, in Minuska.spec]
rinj_inr [definition, in Minuska.model_algebra]
rinj_inl [definition, in Minuska.model_algebra]
rinj_id [definition, in Minuska.model_algebra]
rinj_compose [definition, in Minuska.model_algebra]
ri_reverse_pf [projection, in Minuska.model_algebra]
ri_reverse [projection, in Minuska.model_algebra]
ri_injection [projection, in Minuska.model_algebra]
rmf_apply [definition, in Minuska.model_algebra]
rmf_model [projection, in Minuska.model_algebra]
rmf_nondet [projection, in Minuska.model_algebra]
rmf_signature [projection, in Minuska.model_algebra]
rm_model_over [projection, in Minuska.model_algebra]
rm_carrier_countable [projection, in Minuska.model_algebra]
rm_carrier_eqdec [projection, in Minuska.model_algebra]
rm_carrier [projection, in Minuska.model_algebra]
row_of_wildcards_dec [instance, in Minuska.dt]
row_of_wildcards [definition, in Minuska.dt]
row_startswith_ctor_dec [instance, in Minuska.dt]
row_startswith_ctor [definition, in Minuska.dt]
row_startswith_wildcard_dec [instance, in Minuska.dt]
row_startswith_wildcard [definition, in Minuska.dt]
row_matches_ctor_dec [instance, in Minuska.dt]
row_matches_ctor [definition, in Minuska.dt]
RST_list_closure_elem_of [lemma, in Minuska.martelli_montanari]
RST_list_closure [definition, in Minuska.martelli_montanari]
RuleDeclaration [record, in Minuska.frontend]
r_act [projection, in Minuska.spec]
r_scs [projection, in Minuska.spec]
r_to [projection, in Minuska.spec]
r_from [projection, in Minuska.spec]
r_valid [definition, in Minuska.martelli_montanari]
r_has_all_vars [definition, in Minuska.martelli_montanari]
r_vars_disjoint [definition, in Minuska.martelli_montanari]
r_elem_of [instance, in Minuska.martelli_montanari]
r_elements [instance, in Minuska.martelli_montanari]
S
satisfies [projection, in Minuska.spec]Satisfies [record, in Minuska.spec]
Satisfies_Valuation2_TermOverBuiltin_TermOverBoV [instance, in Minuska.spec]
Satisfies_SideCondition [instance, in Minuska.spec]
Satisfies_TermOverBuiltin_TermOverExpression2 [instance, in Minuska.spec]
Satisfies_Valuation2_TermOverBuiltinValue_BuiltinOrVar_instnace [instance, in Minuska.spec]
Satisfies_Valuation2_TermOverBuiltinValue_BuiltinOrVar [definition, in Minuska.spec]
satisfies_TermOverBoV__impl__vars_subseteq [lemma, in Minuska.properties]
satisfies_TermOverBoV_to_TermOverExpr [lemma, in Minuska.properties]
satisfies_in_size [lemma, in Minuska.properties]
satisfies_inv [lemma, in Minuska.properties]
satisfies_inv' [lemma, in Minuska.properties]
satisfies_var_expr_inv [lemma, in Minuska.properties]
satisfies_var_inv [lemma, in Minuska.properties]
satisfies_var_expr [lemma, in Minuska.properties]
satisfies_var [lemma, in Minuska.properties]
satisfies_TermOverBuiltin_to_TermOverBoV [lemma, in Minuska.properties]
satisfies_term_expr_inv [lemma, in Minuska.properties]
satisfies_term_bov_inv [lemma, in Minuska.properties]
sat2B [definition, in Minuska.spec]
sat2E [definition, in Minuska.spec]
sbov_to_e_bov [definition, in Minuska.frontend]
sbov_var [constructor, in Minuska.frontend]
sbov_builtin [constructor, in Minuska.frontend]
sc_or [constructor, in Minuska.spec]
sc_and [constructor, in Minuska.spec]
sc_atom [constructor, in Minuska.spec]
sc_false [constructor, in Minuska.spec]
sc_true [constructor, in Minuska.spec]
sc_satisfies_insensitive [lemma, in Minuska.naive_interpreter]
sd_cseq_context [projection, in Minuska.frontend]
sd_isValue [projection, in Minuska.frontend]
sd_positions [projection, in Minuska.frontend]
sd_arity [projection, in Minuska.frontend]
sd_sym [projection, in Minuska.frontend]
sec [section, in Minuska.builtin.klike]
sec [section, in Minuska.builtin.empty]
sec2 [section, in Minuska.builtin.klike]
set_filter_pred_impl [lemma, in Minuska.prelude]
se_to_Expression [definition, in Minuska.frontend]
se_applyq [constructor, in Minuska.frontend]
se_applyf [constructor, in Minuska.frontend]
se_variable [constructor, in Minuska.frontend]
se_ground [constructor, in Minuska.frontend]
SideCondition [inductive, in Minuska.spec]
SideCondition_subst [definition, in Minuska.basic_properties]
SideCondition_eqdec [instance, in Minuska.basic_properties]
SideCondition_evaluate [definition, in Minuska.spec]
SideCondition_sind [definition, in Minuska.spec]
SideCondition_rec [definition, in Minuska.spec]
SideCondition_ind [definition, in Minuska.spec]
SideCondition_rect [definition, in Minuska.spec]
SideCondition_satisfies_strip [lemma, in Minuska.properties]
SideCondition_satisfies_extensive [lemma, in Minuska.properties]
signature [projection, in Minuska.spec]
Signature [record, in Minuska.spec]
Signature [record, in Minuska.dt]
SignatureMorphism [record, in Minuska.signature_morphism]
signature_sum_morph_2_inj [instance, in Minuska.model_algebra]
signature_sum_morph_1_inj [instance, in Minuska.model_algebra]
signature_sum_morphism_2 [definition, in Minuska.model_algebra]
signature_sum_morphism_2_predicate [definition, in Minuska.model_algebra]
signature_sum_morphism_2_function [definition, in Minuska.model_algebra]
signature_sum_morphism_1 [definition, in Minuska.model_algebra]
signature_sum_morphism_1_predicate [definition, in Minuska.model_algebra]
signature_sum_morphism_1_function [definition, in Minuska.model_algebra]
signature_sum [definition, in Minuska.model_algebra]
signature_morphism [library]
simple_list_carrier__countable [instance, in Minuska.builtin.list_model]
simple_list_carrier__eqdec [instance, in Minuska.builtin.list_model]
simple_list_carrier [inductive, in Minuska.builtin.list_model]
Simplify [definition, in Minuska.dt]
simplify_correct [lemma, in Minuska.dt]
simplify_correct_helper_1 [lemma, in Minuska.dt]
Simplify_step [definition, in Minuska.dt]
size_subst_2 [lemma, in Minuska.basic_properties]
size_subst_1 [lemma, in Minuska.basic_properties]
size_of_var_in_val [definition, in Minuska.properties]
si_function [constructor, in Minuska.spec]
si_predicate [constructor, in Minuska.spec]
si_none [constructor, in Minuska.spec]
slc_list [constructor, in Minuska.builtin.list_model]
slc_inner [constructor, in Minuska.builtin.list_model]
slice [definition, in Minuska.prelude]
sm [instance, in Minuska.martelli_montanari_tests]
smif [projection, in Minuska.signature_morphism]
SMInj [record, in Minuska.signature_morphism]
smip [projection, in Minuska.signature_morphism]
sm_pred_neg [projection, in Minuska.signature_morphism]
sm_pred_ar [projection, in Minuska.signature_morphism]
spec [library]
spec_interpreter [library]
spec_syntax [library]
srr_to_rr [definition, in Minuska.frontend]
sr_act [projection, in Minuska.frontend]
sr_scs [projection, in Minuska.frontend]
sr_to [projection, in Minuska.frontend]
sr_from [projection, in Minuska.frontend]
ssc_to_sc [definition, in Minuska.frontend]
ssc_or [constructor, in Minuska.frontend]
ssc_and [constructor, in Minuska.frontend]
ssc_atom [constructor, in Minuska.frontend]
ssc_false [constructor, in Minuska.frontend]
ssc_true [constructor, in Minuska.frontend]
sSymbolicTerm_to_ExprTerm [definition, in Minuska.frontend]
State [record, in Minuska.frontend]
StaticModel [record, in Minuska.spec]
StepT [definition, in Minuska.default_everything]
StepT_ext [definition, in Minuska.default_everything]
sTermOverBoV_subst [definition, in Minuska.default_everything]
sTermOverBoV_subst_expr2 [definition, in Minuska.default_everything]
sTermOverBoV_subst_gen [definition, in Minuska.default_everything]
Stream [record, in Minuska.spec]
StrictnessDeclaration [record, in Minuska.frontend]
strictness_to_contexts [definition, in Minuska.frontend]
StringBuiltinOrVar [inductive, in Minuska.frontend]
StringExpression [inductive, in Minuska.frontend]
StringExpression_sind [definition, in Minuska.frontend]
StringExpression_rec [definition, in Minuska.frontend]
StringExpression_ind [definition, in Minuska.frontend]
StringExpression_rect [definition, in Minuska.frontend]
StringRewritingRule [record, in Minuska.frontend]
StringSideCondition [inductive, in Minuska.frontend]
StringSideCondition_sind [definition, in Minuska.frontend]
StringSideCondition_rec [definition, in Minuska.frontend]
StringSideCondition_ind [definition, in Minuska.frontend]
StringSideCondition_rect [definition, in Minuska.frontend]
StringVariables [definition, in Minuska.string_variables]
string_variables [library]
string2f [projection, in Minuska.frontend]
string2p [projection, in Minuska.frontend]
string2q [projection, in Minuska.frontend]
string2sym [projection, in Minuska.frontend]
string2var [projection, in Minuska.frontend]
stuck [definition, in Minuska.spec_interpreter]
st_rules [projection, in Minuska.frontend]
sub [definition, in Minuska.textbook_unification_alg]
Subseteq_Valuation2 [instance, in Minuska.spec]
subst_preserves_subterm [lemma, in Minuska.textbook_unification]
subst_id [lemma, in Minuska.textbook_unification]
subst_notin2 [lemma, in Minuska.basic_properties]
subst_notin [lemma, in Minuska.basic_properties]
SubT [definition, in Minuska.unification_interface]
SubTMM [definition, in Minuska.martelli_montanari]
sub_decreases_degree [lemma, in Minuska.textbook_unification_alg]
sub_notin [lemma, in Minuska.textbook_unification_alg]
sub_app_preserves_subterm [lemma, in Minuska.textbook_unification]
sub_app_unbound_var_2 [lemma, in Minuska.textbook_unification]
sub_app_unbound_var_1 [lemma, in Minuska.textbook_unification]
sub_app_builtin [lemma, in Minuska.textbook_unification]
sub_app_app [lemma, in Minuska.textbook_unification]
sub_ext_cons [lemma, in Minuska.textbook_unification]
sub_ext_nil [lemma, in Minuska.textbook_unification]
sub_ext [definition, in Minuska.textbook_unification]
sub_app_term [lemma, in Minuska.textbook_unification]
sub_lt [definition, in Minuska.textbook_unification]
sub_no_unifier [lemma, in Minuska.martelli_montanari]
sub_is_unifier [lemma, in Minuska.martelli_montanari]
sub_app_mm [definition, in Minuska.martelli_montanari]
sub_app [definition, in Minuska.unification_interface]
sum [section, in Minuska.model_algebra]
sum_list_with_perm [lemma, in Minuska.prelude]
sum_list_with_eq_plus_pairwise [lemma, in Minuska.prelude]
sum_list_with_eq_pairwise [lemma, in Minuska.prelude]
sum_list_with_pairwise [lemma, in Minuska.prelude]
sum_list_with_sum_list_with [lemma, in Minuska.prelude]
sum_list_fmap [lemma, in Minuska.prelude]
sum_list_with_S [lemma, in Minuska.prelude]
sum_list_with_compose [lemma, in Minuska.prelude]
swap_column_in_clause_matrix [definition, in Minuska.dt]
swap_column_in_list [definition, in Minuska.dt]
SwitchCaseList [inductive, in Minuska.dt]
SwitchCaseList_sind [definition, in Minuska.dt]
SwitchCaseList_rec [definition, in Minuska.dt]
SwitchCaseList_ind [definition, in Minuska.dt]
SwitchCaseList_rect [definition, in Minuska.dt]
symbol [projection, in Minuska.spec]
SymbolicTerm_to_ExprTerm [definition, in Minuska.frontend]
SymbolInfo [inductive, in Minuska.spec]
symbols [projection, in Minuska.spec]
Symbols [record, in Minuska.spec]
symbol_countable [projection, in Minuska.spec]
symbol_eqdec [projection, in Minuska.spec]
symex [library]
symex_spec [library]
sym_info [definition, in Minuska.builtin.klike]
T
T [definition, in Minuska.martelli_montanari]take_any [definition, in Minuska.martelli_montanari]
TermOver [definition, in Minuska.spec]
TermOverBoV_to_TermOverExpr2 [definition, in Minuska.basic_properties]
TermOverBoV_subst [definition, in Minuska.basic_properties]
TermOverBoV_subst_expr2 [definition, in Minuska.basic_properties]
TermOverBoV_subst_gen [definition, in Minuska.basic_properties]
TermOverBoV_eval [definition, in Minuska.properties]
TermOverBoV_subst_once_size [lemma, in Minuska.properties]
TermOverBoV_satisfies_strip [lemma, in Minuska.properties]
TermOverBoV_satisfies_extensive [lemma, in Minuska.properties]
TermOverBuiltin_subst [definition, in Minuska.basic_properties]
TermOverBuiltin_to_TermOverBoV [definition, in Minuska.spec]
TermOverExpression2_satisfies_strip [lemma, in Minuska.properties]
TermOverExpression2_satisfies_injective [lemma, in Minuska.properties]
TermOverExpression2_satisfies_extensive [lemma, in Minuska.properties]
TermOver_size_not_zero [lemma, in Minuska.basic_properties]
TermOver_countable [instance, in Minuska.basic_properties]
TermOver_size_with [definition, in Minuska.basic_properties]
TermOver_rect [definition, in Minuska.basic_properties]
TermOver_eqdec [lemma, in Minuska.basic_properties]
TermOver_map [definition, in Minuska.spec]
TermOver_size [definition, in Minuska.spec]
TermOver_collect [definition, in Minuska.naive_interpreter]
TermOver' [inductive, in Minuska.spec]
TermOver'_map [definition, in Minuska.spec]
TermOver'_ind [definition, in Minuska.spec]
TermOver'_option_map__extensional [lemma, in Minuska.properties]
TermOver'_option_map__extension [lemma, in Minuska.properties]
TermOver'_option_map__Some_1 [lemma, in Minuska.properties]
TermOver'_leaves [definition, in Minuska.properties]
TermOver'_option_map [definition, in Minuska.properties]
TermOver'_rinj [definition, in Minuska.builtin.information_flow_functor]
TermOver'_e_map [definition, in Minuska.frontend]
TermOver'_option_map__Expression2_evaluate__extensive [lemma, in Minuska.naive_interpreter]
TermOver'_join [definition, in Minuska.naive_interpreter]
Term_symbol_fmap [instance, in Minuska.lowlang]
term_operand [constructor, in Minuska.lowlang]
term_preterm [constructor, in Minuska.lowlang]
term_has_same_symbol [definition, in Minuska.martelli_montanari]
term_params [definition, in Minuska.martelli_montanari]
term_is_constant [definition, in Minuska.martelli_montanari]
term_is_nonvar [definition, in Minuska.martelli_montanari]
term_is_var [definition, in Minuska.martelli_montanari]
Term' [inductive, in Minuska.lowlang]
Term'_collapse_option [definition, in Minuska.lowlang]
Term'_A_B_fmap [instance, in Minuska.lowlang]
Term'_fmap [definition, in Minuska.lowlang]
Term'_countable [instance, in Minuska.lowlang]
Term'_to_from_gen_tree [lemma, in Minuska.lowlang]
Term'_from_gen_tree [definition, in Minuska.lowlang]
Term'_to_gen_tree [definition, in Minuska.lowlang]
Term'_eqdec [instance, in Minuska.lowlang]
textbook_unification_algorithm [definition, in Minuska.textbook_unification]
textbook_unification [library]
textbook_unification_alg [library]
thy_lhs_match_one_Some [lemma, in Minuska.naive_interpreter]
thy_lhs_match_one_None [lemma, in Minuska.naive_interpreter]
thy_lhs_match_one [definition, in Minuska.naive_interpreter]
tl [projection, in Minuska.spec]
tosse_to_e_tose [definition, in Minuska.frontend]
toss_to_e_tosb [definition, in Minuska.frontend]
TO_from_to_tree [lemma, in Minuska.basic_properties]
TO_of_tree [definition, in Minuska.basic_properties]
TO_to_tree [definition, in Minuska.basic_properties]
to_PreTerm''_app [lemma, in Minuska.lowlang]
to_PreTerm'' [definition, in Minuska.lowlang]
to_Term'' [definition, in Minuska.lowlang]
to_PreTerm'_app [lemma, in Minuska.lowlang]
to_PreTerm' [definition, in Minuska.lowlang]
to_Term' [definition, in Minuska.lowlang]
to_theory [definition, in Minuska.frontend]
to_transform_sym [definition, in Minuska.frontend]
transl_string_pattern [definition, in Minuska.frontend]
transpose [definition, in Minuska.martelli_montanari]
tree_to_bv [definition, in Minuska.builtin.klike]
trivial [library]
trivial_stream [definition, in Minuska.default_static_model]
try_neg_sym [lemma, in Minuska.properties]
try_neg [definition, in Minuska.properties]
try_neg_s [definition, in Minuska.frontend]
try_match_lhs_with_sc_complete [lemma, in Minuska.naive_interpreter]
try_match_new_correct [lemma, in Minuska.naive_interpreter]
try_match_new_complete [lemma, in Minuska.naive_interpreter]
try_match_lhs_with_sc [definition, in Minuska.naive_interpreter]
try_match_new [definition, in Minuska.naive_interpreter]
t_term [constructor, in Minuska.spec]
t_over [constructor, in Minuska.spec]
t_valid [definition, in Minuska.martelli_montanari]
t_meqn_v_prec [definition, in Minuska.martelli_montanari]
t_meqn_m_valid [definition, in Minuska.martelli_montanari]
U
U [projection, in Minuska.martelli_montanari]ua_unify_complete [projection, in Minuska.unification_interface]
ua_unify_sound [projection, in Minuska.unification_interface]
ua_unify [projection, in Minuska.unification_interface]
uf_rec_sub2_r [constructor, in Minuska.textbook_unification]
uf_rec_sub2_l [constructor, in Minuska.textbook_unification]
uf_rec [constructor, in Minuska.textbook_unification]
uf_subterm [constructor, in Minuska.textbook_unification]
uf_term_len [constructor, in Minuska.textbook_unification]
uf_term_sym [constructor, in Minuska.textbook_unification]
uf_term_over [constructor, in Minuska.textbook_unification]
uf_over_term [constructor, in Minuska.textbook_unification]
uf_diff_builtin [constructor, in Minuska.textbook_unification]
uf_varin_fail_2 [constructor, in Minuska.textbook_unification]
uf_varin_fail_1 [constructor, in Minuska.textbook_unification]
uglify' [definition, in Minuska.lowlang]
uglify'_prettify' [lemma, in Minuska.lowlang]
under_rel_subrel [instance, in Minuska.prelude]
under_rel_equiv [instance, in Minuska.prelude]
under_rel_symm [instance, in Minuska.prelude]
under_rel_trans [instance, in Minuska.prelude]
under_rel_refl [instance, in Minuska.prelude]
under_proper [instance, in Minuska.prelude]
under_flip_mono [instance, in Minuska.prelude]
under_mono [instance, in Minuska.prelude]
UnificationAlgorithm [record, in Minuska.unification_interface]
unification_interface [library]
unify [definition, in Minuska.textbook_unification_alg]
unify_paper1_input2 [definition, in Minuska.martelli_montanari_tests]
unify_paper1_input1 [definition, in Minuska.martelli_montanari_tests]
unify_sound2 [lemma, in Minuska.textbook_unification]
unify_failure_is_severe [lemma, in Minuska.textbook_unification]
unify_sound [lemma, in Minuska.textbook_unification]
unify_failure_sind [definition, in Minuska.textbook_unification]
unify_failure_ind [definition, in Minuska.textbook_unification]
unify_failure [inductive, in Minuska.textbook_unification]
unify_no_variable_out_of_thin_air [lemma, in Minuska.textbook_unification]
unify_terms [definition, in Minuska.martelli_montanari]
unify_r [definition, in Minuska.martelli_montanari]
unify_r_aux_valid_t [lemma, in Minuska.martelli_montanari]
unify_r_aux_n_enough [lemma, in Minuska.martelli_montanari]
unify_r_aux [definition, in Minuska.martelli_montanari]
unify_r_keeps_equiv_UP [lemma, in Minuska.martelli_montanari]
unify_r_valid_r [lemma, in Minuska.martelli_montanari]
unify_r_step [definition, in Minuska.martelli_montanari]
union_list_valid_meqn_keeps_valid [lemma, in Minuska.martelli_montanari]
UP [definition, in Minuska.martelli_montanari]
up_of_r [definition, in Minuska.martelli_montanari]
up_of_t [definition, in Minuska.martelli_montanari]
up_of_valid_u_elem_of [lemma, in Minuska.martelli_montanari]
up_of_valid_u_meqn_all_terms_in_UP [lemma, in Minuska.martelli_montanari]
up_of_u [definition, in Minuska.martelli_montanari]
up_of_meqns_elem_of [lemma, in Minuska.martelli_montanari]
up_of_meqns_all_terms_in_UP [lemma, in Minuska.martelli_montanari]
up_of_meqns [definition, in Minuska.martelli_montanari]
up_of_meqn_elem_of [lemma, in Minuska.martelli_montanari]
up_of_meqn [definition, in Minuska.martelli_montanari]
up_of_terms [definition, in Minuska.martelli_montanari]
u_subst_keeps_equiv_UP [lemma, in Minuska.martelli_montanari]
u_subst_keeps_u_valid [lemma, in Minuska.martelli_montanari]
u_subst [definition, in Minuska.martelli_montanari]
u_insert_many [definition, in Minuska.martelli_montanari]
U_listset_ops [definition, in Minuska.martelli_montanari]
u_extract_overlapping_meqns_insert_equiv_listset [lemma, in Minuska.martelli_montanari]
u_extract_overlapping_meqns_in_u'_listset [lemma, in Minuska.martelli_montanari]
u_extract_overlapping_meqns_in_ls_meqn_listset [lemma, in Minuska.martelli_montanari]
u_extract_nonempty_m_meqn_is_nonempty_listset [lemma, in Minuska.martelli_montanari]
u_extract_overlapping_meqns_listset [definition, in Minuska.martelli_montanari]
u_extract_nonempty_m_insert_equiv_listset [lemma, in Minuska.martelli_montanari]
u_extract_nonempty_m_removes_element_listset [lemma, in Minuska.martelli_montanari]
U_NoDup_listset [lemma, in Minuska.martelli_montanari]
u_extract_nonempty_m_meqn_listset [definition, in Minuska.martelli_montanari]
u_insert_listset [definition, in Minuska.martelli_montanari]
u_extract_overlapping_meqns_keeps_get_vars [lemma, in Minuska.martelli_montanari]
u_insert_keeps_u_get_vars [lemma, in Minuska.martelli_montanari]
u_insert_keeps_u_get_vars_rg [lemma, in Minuska.martelli_montanari]
u_insert_keeps_u_get_vars_lf [lemma, in Minuska.martelli_montanari]
u_insert_elem_of [lemma, in Minuska.martelli_montanari]
u_get_vars_exists_meqn [lemma, in Minuska.martelli_montanari]
u_extract_overlapping_meqns_disjunct [lemma, in Minuska.martelli_montanari]
u_get_vars [definition, in Minuska.martelli_montanari]
u_valid [definition, in Minuska.martelli_montanari]
u_extract_overlapping_meqns_insert_equiv [projection, in Minuska.martelli_montanari]
u_extract_overlapping_meqns_in_u' [projection, in Minuska.martelli_montanari]
u_extract_overlapping_meqns_in_ls_meqn [projection, in Minuska.martelli_montanari]
u_extract_overlapping_meqns [projection, in Minuska.martelli_montanari]
u_extract_nonempty_m_meqn_is_nonempty [projection, in Minuska.martelli_montanari]
u_extract_nonempty_m_insert_equiv [projection, in Minuska.martelli_montanari]
u_extract_nonempty_m_removes_element [projection, in Minuska.martelli_montanari]
u_extract_nonempty_m_meqn [projection, in Minuska.martelli_montanari]
u_insert_add [projection, in Minuska.martelli_montanari]
u_insert_id [projection, in Minuska.martelli_montanari]
u_insert [projection, in Minuska.martelli_montanari]
u_map_elem_of [projection, in Minuska.martelli_montanari]
u_map [projection, in Minuska.martelli_montanari]
U_NoDup [projection, in Minuska.martelli_montanari]
U_elements [projection, in Minuska.martelli_montanari]
U_empty [projection, in Minuska.martelli_montanari]
U_ops [record, in Minuska.martelli_montanari]
V
valuation_restrict_vars_of_self [lemma, in Minuska.naive_interpreter]valuation_merge [library]
Valuation2 [definition, in Minuska.spec]
Valuation2_merge_olist_correct [lemma, in Minuska.valuation_merge]
Valuation2_merge_olist_inv [lemma, in Minuska.valuation_merge]
Valuation2_merge_olist_vars_of [lemma, in Minuska.valuation_merge]
Valuation2_merge_with_correct_2 [lemma, in Minuska.valuation_merge]
Valuation2_merge_with_correct [lemma, in Minuska.valuation_merge]
Valuation2_merge_olist [definition, in Minuska.valuation_merge]
Valuation2_merge_list [definition, in Minuska.valuation_merge]
Valuation2_merge_with [definition, in Minuska.valuation_merge]
Valuation2_compatible_with_bound [definition, in Minuska.valuation_merge]
Valuation2_compatible_with [definition, in Minuska.valuation_merge]
Valuation2_use_left [definition, in Minuska.valuation_merge]
Valuation2_restrict_eq_subseteq [lemma, in Minuska.naive_interpreter]
Valuation2_restrict [definition, in Minuska.naive_interpreter]
Value [inductive, in Minuska.dt]
ValueVector [definition, in Minuska.dt]
Value_ind [definition, in Minuska.dt]
variable [projection, in Minuska.spec]
variables [projection, in Minuska.spec]
variable_infinite [projection, in Minuska.spec]
variable_countable [projection, in Minuska.spec]
variable_eqdec [projection, in Minuska.spec]
VarsOf [record, in Minuska.spec]
VarsOf_Term' [instance, in Minuska.lowlang]
VarsOf_aosB [instance, in Minuska.lowlang]
VarsOf_Valuation2 [instance, in Minuska.spec]
VarsOf_Valuation2_ [instance, in Minuska.spec]
VarsOf_TermOver_Expression2 [instance, in Minuska.spec]
VarsOf_TermOver_BuiltinOrVar [instance, in Minuska.spec]
VarsOf_BoV [instance, in Minuska.spec]
VarsOf_sc [instance, in Minuska.spec]
VarsOf_list_something [instance, in Minuska.spec]
VarsOf_Expression2 [instance, in Minuska.spec]
VarsOf_TermOver [instance, in Minuska.spec]
VarsOf_builtin [instance, in Minuska.spec]
VarsOf_symbol [instance, in Minuska.spec]
VarsOf_MinusL_LangDef [instance, in Minuska.minusl_syntax]
VarsOf_MinusL_Decl [instance, in Minuska.minusl_syntax]
vars_of_TermOverBoV_subst [lemma, in Minuska.textbook_unification_alg]
vars_of_to_l2r_subst [lemma, in Minuska.minusl_compile_properties]
vars_of_variable [lemma, in Minuska.textbook_unification]
vars_of_builtin [lemma, in Minuska.textbook_unification]
vars_of_sub [definition, in Minuska.textbook_unification]
vars_of_t_term_e [lemma, in Minuska.basic_properties]
vars_of_t_term [lemma, in Minuska.basic_properties]
vars_of_to_l2r [definition, in Minuska.basic_properties]
vars_of_uglify [lemma, in Minuska.lowlang]
vars_of_uglify' [lemma, in Minuska.lowlang]
vars_of_Term'B [definition, in Minuska.lowlang]
vars_of_aosB [definition, in Minuska.lowlang]
vars_of_BoV [definition, in Minuska.spec]
vars_of_sc [definition, in Minuska.spec]
vars_of_Expression2 [definition, in Minuska.spec]
vars_of [projection, in Minuska.spec]
vars_of_sat_tobov [lemma, in Minuska.interpreter_results]
vars_of__TermOverBoV_subst__varless [lemma, in Minuska.properties]
vars_of_t_over_expr [lemma, in Minuska.properties]
vars_of_to_l2r_of_tob [lemma, in Minuska.properties]
var_is_subterm [lemma, in Minuska.textbook_unification]
var_elem_of_meqn [lemma, in Minuska.martelli_montanari]
var_term_to_var_some [lemma, in Minuska.martelli_montanari]
var_term_to_var [definition, in Minuska.martelli_montanari]
var_to_term [definition, in Minuska.martelli_montanari]
vector_of_wildcards_dec [instance, in Minuska.dt]
vector_of_wildcards [definition, in Minuska.dt]
v_cval [constructor, in Minuska.dt]
W
wfeqn [definition, in Minuska.textbook_unification]wfeqns [definition, in Minuska.textbook_unification]
wfsub [definition, in Minuska.textbook_unification]
wft [definition, in Minuska.textbook_unification]
wft_minus [lemma, in Minuska.textbook_unification]
wf_concat [lemma, in Minuska.textbook_unification]
wsm [section, in Minuska.frontend]
Z
zipWith [definition, in Minuska.martelli_montanari]other
_ ~up _ [notation, in Minuska.martelli_montanari]β [instance, in Minuska.builtin.klike]
β [instance, in Minuska.builtin.empty]
βover [definition, in Minuska.builtin.klike]
βover [definition, in Minuska.builtin.empty]
Notation Index
other
_ ~up _ [in Minuska.martelli_montanari]Module Index
I
Implementation [in Minuska.symex]Library Index
B
basic_propertiesbool_signature
bool_model
builtins
BuiltinValue
C
conservative_mergeD
default_static_modeldefault_everything
dt
E
emptyexample_list_int_model
F
frontendI
information_flow_functorinterpreter_results
interp_loop
int_signature
int_model
K
klikeL
list_modellist_signature
lowlang
M
martelli_montanari_testsmartelli_montanari
minuska
minusl_compile
minusl_semantics
minusl_syntax
minusl_compile_properties
model_algebra
model_traits
model_functor
N
naive_interpreternat_builtin
notations
P
preludeproperties
pval_ocaml_binding
S
signature_morphismspec
spec_interpreter
spec_syntax
string_variables
symex
symex_spec
T
textbook_unificationtextbook_unification_alg
trivial
U
unification_interfaceV
valuation_mergeLemma Index
B
bind_None_T_1 [in Minuska.prelude]bind_Some_T_2 [in Minuska.prelude]
bind_Some_T_1 [in Minuska.prelude]
BuiltinValue0_eqdec_helper_0 [in Minuska.builtin.klike]
C
compactify_keeps_equiv_UP [in Minuska.martelli_montanari]compactify_keeps_valid_u [in Minuska.martelli_montanari]
compactify_is_compact [in Minuska.martelli_montanari]
compactify_by_vars_keeps_equiv_UP [in Minuska.martelli_montanari]
compactify_by_vars_keeps_u_valid [in Minuska.martelli_montanari]
compactify_by_vars_keeps_get_vars [in Minuska.martelli_montanari]
compactify_by_vars_is_compact_up_to_vars [in Minuska.martelli_montanari]
compactify_by_vars_keeps_compactness [in Minuska.martelli_montanari]
compactify_by_vars_inv_fold [in Minuska.martelli_montanari]
compactify_by_var_keeps_unifier_of [in Minuska.martelli_montanari]
compactify_by_var_keeps_up_of_u [in Minuska.martelli_montanari]
compactify_by_var_keeps_u_valid [in Minuska.martelli_montanari]
compactify_by_var_keeps_previous_compactness [in Minuska.martelli_montanari]
compactify_by_var_meqn_only_in_u' [in Minuska.martelli_montanari]
compactify_by_var_meqn_in_v_in [in Minuska.martelli_montanari]
compactify_by_var_keeps_get_vars [in Minuska.martelli_montanari]
compactify_by_var_is_compact_up_to_var [in Minuska.martelli_montanari]
compactify_by_var_v_in_meqn [in Minuska.martelli_montanari]
compactify_by_var_v_not_in_meqn [in Minuska.martelli_montanari]
compactify_by_var_meqn_inv_rg [in Minuska.martelli_montanari]
compose_uglify_prettify [in Minuska.lowlang]
compose_prettify_uglify [in Minuska.lowlang]
concrete_is_larger_than_symbolic [in Minuska.properties]
count_one_split [in Minuska.prelude]
D
dec_keeps_equiv_UP [in Minuska.martelli_montanari]dec_exists [in Minuska.martelli_montanari]
dec_aux_TermOver_size_enough [in Minuska.martelli_montanari]
Default_correct [in Minuska.dt]
deg_cons_lt [in Minuska.textbook_unification_alg]
deg_swap_head [in Minuska.textbook_unification_alg]
dom_merge_use_left [in Minuska.valuation_merge]
double_satisfies_contradiction [in Minuska.properties]
E
elem_of_next [in Minuska.basic_properties]elem_of_list_fmap_T_1 [in Minuska.prelude]
elem_of_union_meqn [in Minuska.martelli_montanari]
elem_of_singleton_meqn [in Minuska.martelli_montanari]
enveloping_preserves_or_increases_delta [in Minuska.properties]
eqns_vars_zip [in Minuska.textbook_unification_alg]
eqns_vars_app [in Minuska.textbook_unification_alg]
eqns_vars_sub [in Minuska.textbook_unification_alg]
eqns_vars_cons [in Minuska.textbook_unification_alg]
eqns_vars_hd_comm [in Minuska.textbook_unification]
eval_et_extensive_Some [in Minuska.naive_interpreter]
eval_et_evaluate_None_relative [in Minuska.naive_interpreter]
eval_et_correct_2 [in Minuska.naive_interpreter]
eval_et_correct [in Minuska.naive_interpreter]
eval_et_strip [in Minuska.naive_interpreter]
eval_et_strip_helper [in Minuska.naive_interpreter]
eval_et_Some_val [in Minuska.naive_interpreter]
Expression2Term_matches_enough [in Minuska.properties]
Expression2_eqdec [in Minuska.basic_properties]
Expression2_evalute_strip [in Minuska.properties]
Expression2_evaluate_None_relative [in Minuska.properties]
Expression2_evaluate_total_1 [in Minuska.properties]
Expression2_evaluate_extensive_Some [in Minuska.properties]
extract_mgu_contains_var [in Minuska.martelli_montanari]
E_from_to_tree [in Minuska.basic_properties]
F
fewer_arrows_lower_degree [in Minuska.textbook_unification_alg]filter_fmap [in Minuska.prelude]
flat_map_lookup_Some [in Minuska.prelude]
fmap_uglify_prettify_option [in Minuska.lowlang]
fmap_prettify_uglify_option [in Minuska.lowlang]
fmap_uglify_prettify_list [in Minuska.lowlang]
fmap_prettify_uglify_list [in Minuska.lowlang]
fmap_Some_T_1 [in Minuska.prelude]
forall_satisfies_inv [in Minuska.properties]
forall_satisfies_inv' [in Minuska.properties]
from_to_tree [in Minuska.builtin.klike]
G
get_vars_of_S_listset_meqns_equiv [in Minuska.martelli_montanari]get_vars_of_S_list_meqns_equiv [in Minuska.martelli_montanari]
H
helper_lemma_3 [in Minuska.textbook_unification]helper_lemma_2 [in Minuska.textbook_unification]
helper_lemma_1 [in Minuska.textbook_unification]
h_in_l_impl_length_filter_l_gt_1 [in Minuska.prelude]
I
init_r_keeps_UP [in Minuska.martelli_montanari]init_r_valid [in Minuska.martelli_montanari]
in_compile_inv [in Minuska.minusl_compile_properties]
is_unifier_of_extensive [in Minuska.textbook_unification]
is_subterm_antisym [in Minuska.textbook_unification]
is_subterm_size [in Minuska.textbook_unification]
is_unifier_of_app [in Minuska.textbook_unification]
is_unifier_of_cons [in Minuska.textbook_unification]
is_subterm_sizes [in Minuska.basic_properties]
is_compact_up_to_vars_is_compact [in Minuska.martelli_montanari]
is_compact_up_to_var_at_most_one_meqn_with_var [in Minuska.martelli_montanari]
L
least_of_nil_nil [in Minuska.textbook_unification]length_filter_eq__eq__length_filter_in__one [in Minuska.prelude]
length_filter_eq__eq__length_filter_in__zero [in Minuska.prelude]
length_filter_l_1_impl_h_in_l' [in Minuska.prelude]
length_filter_l_1_impl_h_in_l [in Minuska.prelude]
length_list_collect_Some [in Minuska.prelude]
length_pfmap [in Minuska.prelude]
list_filter_Forall_all [in Minuska.prelude]
list_filter_Forall_not [in Minuska.prelude]
list_collect_Forall_T [in Minuska.prelude]
list_collect_Exists_1 [in Minuska.prelude]
list_collect_Forall [in Minuska.prelude]
list_collect_Exists [in Minuska.prelude]
list_collect_inv [in Minuska.prelude]
list_find_elem_of_isSome [in Minuska.prelude]
list_collect_Expression2_evaluate_extensive_Some [in Minuska.properties]
list_swap_head_involutive [in Minuska.dt]
M
map_uglify'_inj [in Minuska.lowlang]map_lookup_Some [in Minuska.prelude]
meqn_union_list_elem_of_get_nonvar_part [in Minuska.martelli_montanari]
meqn_get_nonvar_part_mjoin_union_list [in Minuska.martelli_montanari]
meqn_valid_elem_of_in [in Minuska.martelli_montanari]
meqn_equivalent_trans [in Minuska.martelli_montanari]
meqn_equivalent_symm [in Minuska.martelli_montanari]
meqn_equivalent_refl [in Minuska.martelli_montanari]
merge_use_left_below [in Minuska.valuation_merge]
merge_valuations_dom [in Minuska.valuation_merge]
merge_use_left_subseteq [in Minuska.valuation_merge]
merge_valuations_empty_l [in Minuska.valuation_merge]
merge_valuations_empty_r [in Minuska.valuation_merge]
modelover_sum_reduce_2 [in Minuska.model_algebra]
modelover_sum_reduce_1 [in Minuska.model_algebra]
N
naive_interpreter_sound [in Minuska.naive_interpreter]not_subterm_subst [in Minuska.basic_properties]
not_elem_of_empty_meqn [in Minuska.martelli_montanari]
O
on_distinct_vars [in Minuska.textbook_unification]on_a_shared_prefix [in Minuska.prelude]
P
partition_fl_false_equiv [in Minuska.martelli_montanari]partition_tl_true_equiv [in Minuska.martelli_montanari]
partition_tl_fl_disjunct [in Minuska.martelli_montanari]
partition_fl_means_false [in Minuska.martelli_montanari]
partition_tl_means_true [in Minuska.martelli_montanari]
partition_true_in_tl [in Minuska.martelli_montanari]
pflookup_spec [in Minuska.prelude]
pfmap_lookup_Some_1 [in Minuska.prelude]
pfmap_lookup_Some_lt [in Minuska.prelude]
PreTerm'_of_to_gen_tree [in Minuska.lowlang]
R
rev_ind_T [in Minuska.prelude]rev_list_ind_T [in Minuska.prelude]
RST_list_closure_elem_of [in Minuska.martelli_montanari]
S
satisfies_TermOverBoV__impl__vars_subseteq [in Minuska.properties]satisfies_TermOverBoV_to_TermOverExpr [in Minuska.properties]
satisfies_in_size [in Minuska.properties]
satisfies_inv [in Minuska.properties]
satisfies_inv' [in Minuska.properties]
satisfies_var_expr_inv [in Minuska.properties]
satisfies_var_inv [in Minuska.properties]
satisfies_var_expr [in Minuska.properties]
satisfies_var [in Minuska.properties]
satisfies_TermOverBuiltin_to_TermOverBoV [in Minuska.properties]
satisfies_term_expr_inv [in Minuska.properties]
satisfies_term_bov_inv [in Minuska.properties]
sc_satisfies_insensitive [in Minuska.naive_interpreter]
set_filter_pred_impl [in Minuska.prelude]
SideCondition_satisfies_strip [in Minuska.properties]
SideCondition_satisfies_extensive [in Minuska.properties]
simplify_correct [in Minuska.dt]
simplify_correct_helper_1 [in Minuska.dt]
size_subst_2 [in Minuska.basic_properties]
size_subst_1 [in Minuska.basic_properties]
subst_preserves_subterm [in Minuska.textbook_unification]
subst_id [in Minuska.textbook_unification]
subst_notin2 [in Minuska.basic_properties]
subst_notin [in Minuska.basic_properties]
sub_decreases_degree [in Minuska.textbook_unification_alg]
sub_notin [in Minuska.textbook_unification_alg]
sub_app_preserves_subterm [in Minuska.textbook_unification]
sub_app_unbound_var_2 [in Minuska.textbook_unification]
sub_app_unbound_var_1 [in Minuska.textbook_unification]
sub_app_builtin [in Minuska.textbook_unification]
sub_app_app [in Minuska.textbook_unification]
sub_ext_cons [in Minuska.textbook_unification]
sub_ext_nil [in Minuska.textbook_unification]
sub_app_term [in Minuska.textbook_unification]
sub_no_unifier [in Minuska.martelli_montanari]
sub_is_unifier [in Minuska.martelli_montanari]
sum_list_with_perm [in Minuska.prelude]
sum_list_with_eq_plus_pairwise [in Minuska.prelude]
sum_list_with_eq_pairwise [in Minuska.prelude]
sum_list_with_pairwise [in Minuska.prelude]
sum_list_with_sum_list_with [in Minuska.prelude]
sum_list_fmap [in Minuska.prelude]
sum_list_with_S [in Minuska.prelude]
sum_list_with_compose [in Minuska.prelude]
T
TermOverBoV_subst_once_size [in Minuska.properties]TermOverBoV_satisfies_strip [in Minuska.properties]
TermOverBoV_satisfies_extensive [in Minuska.properties]
TermOverExpression2_satisfies_strip [in Minuska.properties]
TermOverExpression2_satisfies_injective [in Minuska.properties]
TermOverExpression2_satisfies_extensive [in Minuska.properties]
TermOver_size_not_zero [in Minuska.basic_properties]
TermOver_eqdec [in Minuska.basic_properties]
TermOver'_option_map__extensional [in Minuska.properties]
TermOver'_option_map__extension [in Minuska.properties]
TermOver'_option_map__Some_1 [in Minuska.properties]
TermOver'_option_map__Expression2_evaluate__extensive [in Minuska.naive_interpreter]
Term'_to_from_gen_tree [in Minuska.lowlang]
thy_lhs_match_one_Some [in Minuska.naive_interpreter]
thy_lhs_match_one_None [in Minuska.naive_interpreter]
TO_from_to_tree [in Minuska.basic_properties]
to_PreTerm''_app [in Minuska.lowlang]
to_PreTerm'_app [in Minuska.lowlang]
try_neg_sym [in Minuska.properties]
try_match_lhs_with_sc_complete [in Minuska.naive_interpreter]
try_match_new_correct [in Minuska.naive_interpreter]
try_match_new_complete [in Minuska.naive_interpreter]
U
uglify'_prettify' [in Minuska.lowlang]unify_sound2 [in Minuska.textbook_unification]
unify_failure_is_severe [in Minuska.textbook_unification]
unify_sound [in Minuska.textbook_unification]
unify_no_variable_out_of_thin_air [in Minuska.textbook_unification]
unify_r_aux_valid_t [in Minuska.martelli_montanari]
unify_r_aux_n_enough [in Minuska.martelli_montanari]
unify_r_keeps_equiv_UP [in Minuska.martelli_montanari]
unify_r_valid_r [in Minuska.martelli_montanari]
union_list_valid_meqn_keeps_valid [in Minuska.martelli_montanari]
up_of_valid_u_elem_of [in Minuska.martelli_montanari]
up_of_valid_u_meqn_all_terms_in_UP [in Minuska.martelli_montanari]
up_of_meqns_elem_of [in Minuska.martelli_montanari]
up_of_meqns_all_terms_in_UP [in Minuska.martelli_montanari]
up_of_meqn_elem_of [in Minuska.martelli_montanari]
u_subst_keeps_equiv_UP [in Minuska.martelli_montanari]
u_subst_keeps_u_valid [in Minuska.martelli_montanari]
u_extract_overlapping_meqns_insert_equiv_listset [in Minuska.martelli_montanari]
u_extract_overlapping_meqns_in_u'_listset [in Minuska.martelli_montanari]
u_extract_overlapping_meqns_in_ls_meqn_listset [in Minuska.martelli_montanari]
u_extract_nonempty_m_meqn_is_nonempty_listset [in Minuska.martelli_montanari]
u_extract_nonempty_m_insert_equiv_listset [in Minuska.martelli_montanari]
u_extract_nonempty_m_removes_element_listset [in Minuska.martelli_montanari]
U_NoDup_listset [in Minuska.martelli_montanari]
u_extract_overlapping_meqns_keeps_get_vars [in Minuska.martelli_montanari]
u_insert_keeps_u_get_vars [in Minuska.martelli_montanari]
u_insert_keeps_u_get_vars_rg [in Minuska.martelli_montanari]
u_insert_keeps_u_get_vars_lf [in Minuska.martelli_montanari]
u_insert_elem_of [in Minuska.martelli_montanari]
u_get_vars_exists_meqn [in Minuska.martelli_montanari]
u_extract_overlapping_meqns_disjunct [in Minuska.martelli_montanari]
V
valuation_restrict_vars_of_self [in Minuska.naive_interpreter]Valuation2_merge_olist_correct [in Minuska.valuation_merge]
Valuation2_merge_olist_inv [in Minuska.valuation_merge]
Valuation2_merge_olist_vars_of [in Minuska.valuation_merge]
Valuation2_merge_with_correct_2 [in Minuska.valuation_merge]
Valuation2_merge_with_correct [in Minuska.valuation_merge]
Valuation2_restrict_eq_subseteq [in Minuska.naive_interpreter]
vars_of_TermOverBoV_subst [in Minuska.textbook_unification_alg]
vars_of_to_l2r_subst [in Minuska.minusl_compile_properties]
vars_of_variable [in Minuska.textbook_unification]
vars_of_builtin [in Minuska.textbook_unification]
vars_of_t_term_e [in Minuska.basic_properties]
vars_of_t_term [in Minuska.basic_properties]
vars_of_uglify [in Minuska.lowlang]
vars_of_uglify' [in Minuska.lowlang]
vars_of_sat_tobov [in Minuska.interpreter_results]
vars_of__TermOverBoV_subst__varless [in Minuska.properties]
vars_of_t_over_expr [in Minuska.properties]
vars_of_to_l2r_of_tob [in Minuska.properties]
var_is_subterm [in Minuska.textbook_unification]
var_elem_of_meqn [in Minuska.martelli_montanari]
var_term_to_var_some [in Minuska.martelli_montanari]
W
wft_minus [in Minuska.textbook_unification]wf_concat [in Minuska.textbook_unification]
Constructor Index
B
bool_pred_is_true [in Minuska.builtin.bool_signature]bool_pred_is_false [in Minuska.builtin.bool_signature]
bool_pred_is [in Minuska.builtin.bool_signature]
bool_fun_xor [in Minuska.builtin.bool_signature]
bool_fun_iff [in Minuska.builtin.bool_signature]
bool_fun_or [in Minuska.builtin.bool_signature]
bool_fun_and [in Minuska.builtin.bool_signature]
bool_fun_neg [in Minuska.builtin.bool_signature]
bool_fun_false [in Minuska.builtin.bool_signature]
bool_fun_true [in Minuska.builtin.bool_signature]
bov_variable [in Minuska.spec]
bov_builtin [in Minuska.spec]
bvl_sym [in Minuska.builtin.klike]
bvl_str [in Minuska.builtin.klike]
bvl_Z [in Minuska.builtin.klike]
bvl_bool [in Minuska.builtin.klike]
bv_pmap [in Minuska.builtin.klike]
bv_list [in Minuska.builtin.klike]
bv_str [in Minuska.builtin.klike]
bv_sym [in Minuska.builtin.klike]
bv_Z [in Minuska.builtin.klike]
bv_bool [in Minuska.builtin.klike]
b_have_different_symbols [in Minuska.builtin.klike]
b_have_same_symbol [in Minuska.builtin.klike]
b_is_not_applied_symbol [in Minuska.builtin.klike]
b_is_applied_symbol [in Minuska.builtin.klike]
b_map_hasKey [in Minuska.builtin.klike]
b_term_eq [in Minuska.builtin.klike]
b_bool_is_false [in Minuska.builtin.klike]
b_bool_is_true [in Minuska.builtin.klike]
b_isNotMap [in Minuska.builtin.klike]
b_isMap [in Minuska.builtin.klike]
b_isNotList [in Minuska.builtin.klike]
b_isList [in Minuska.builtin.klike]
b_isNotString [in Minuska.builtin.klike]
b_isString [in Minuska.builtin.klike]
b_isNotBool [in Minuska.builtin.klike]
b_isBool [in Minuska.builtin.klike]
b_isNotZ [in Minuska.builtin.klike]
b_isZ [in Minuska.builtin.klike]
b_isNotSymbol [in Minuska.builtin.klike]
b_isSymbol [in Minuska.builtin.klike]
b_isNotBuiltin [in Minuska.builtin.klike]
b_isBuiltin [in Minuska.builtin.klike]
b_map_update [in Minuska.builtin.klike]
b_map_lookup [in Minuska.builtin.klike]
b_bool_neg [in Minuska.builtin.klike]
b_Z_neq [in Minuska.builtin.klike]
b_Z_eq [in Minuska.builtin.klike]
b_Z_isGt [in Minuska.builtin.klike]
b_Z_isGe [in Minuska.builtin.klike]
b_Z_isLt [in Minuska.builtin.klike]
b_Z_isLe [in Minuska.builtin.klike]
b_Z_div [in Minuska.builtin.klike]
b_Z_times [in Minuska.builtin.klike]
b_Z_minus [in Minuska.builtin.klike]
b_Z_plus [in Minuska.builtin.klike]
b_map_size [in Minuska.builtin.klike]
b_map_empty [in Minuska.builtin.klike]
b_list_empty [in Minuska.builtin.klike]
b_zero [in Minuska.builtin.klike]
D
decl_strict [in Minuska.frontend]decl_ctx [in Minuska.frontend]
decl_rule [in Minuska.frontend]
default_act [in Minuska.default_everything]
dtsem_switch_default [in Minuska.dt]
dtsem_switch_constr [in Minuska.dt]
dtsem_swap [in Minuska.dt]
dtsem_yield_continue [in Minuska.dt]
dtsem_yield_now [in Minuska.dt]
dt_sem_aux_cont [in Minuska.dt]
dt_sem_aux_default [in Minuska.dt]
dt_sem_aux_found [in Minuska.dt]
dt_swap [in Minuska.dt]
dt_switch [in Minuska.dt]
dt_yield [in Minuska.dt]
dt_fail [in Minuska.dt]
E
e_query [in Minuska.spec]e_fun [in Minuska.spec]
e_variable [in Minuska.spec]
e_ground [in Minuska.spec]
I
int_is [in Minuska.builtin.int_signature]int_lt [in Minuska.builtin.int_signature]
int_le [in Minuska.builtin.int_signature]
int_eq [in Minuska.builtin.int_signature]
int_one [in Minuska.builtin.int_signature]
int_zero [in Minuska.builtin.int_signature]
int_uminus [in Minuska.builtin.int_signature]
int_minus [in Minuska.builtin.int_signature]
int_plus [in Minuska.builtin.int_signature]
invisible_act [in Minuska.default_everything]
L
list_is [in Minuska.builtin.list_signature]list_is_nil [in Minuska.builtin.list_signature]
list_tail [in Minuska.builtin.list_signature]
list_head [in Minuska.builtin.list_signature]
list_cons [in Minuska.builtin.list_signature]
list_nil [in Minuska.builtin.list_signature]
M
mkSwitchCaseList [in Minuska.dt]mld_context [in Minuska.minusl_syntax]
mld_rewrite [in Minuska.minusl_syntax]
mlr_context [in Minuska.minusl_semantics]
mlr_trans [in Minuska.minusl_semantics]
mlr_rule [in Minuska.minusl_semantics]
mlr_refl [in Minuska.minusl_semantics]
mytt [in Minuska.prelude]
N
ni_list_different [in Minuska.dt]ni_ctor_diferent [in Minuska.dt]
P
pt_app_ao [in Minuska.lowlang]pt_app_operand [in Minuska.lowlang]
pt_operator [in Minuska.lowlang]
pvm_ctor [in Minuska.dt]
pvm_wildcard [in Minuska.dt]
p_cpat [in Minuska.dt]
p_wildcard [in Minuska.dt]
Q
qs_program [in Minuska.pi.trivial]S
sbov_var [in Minuska.frontend]sbov_builtin [in Minuska.frontend]
sc_or [in Minuska.spec]
sc_and [in Minuska.spec]
sc_atom [in Minuska.spec]
sc_false [in Minuska.spec]
sc_true [in Minuska.spec]
se_applyq [in Minuska.frontend]
se_applyf [in Minuska.frontend]
se_variable [in Minuska.frontend]
se_ground [in Minuska.frontend]
si_function [in Minuska.spec]
si_predicate [in Minuska.spec]
si_none [in Minuska.spec]
slc_list [in Minuska.builtin.list_model]
slc_inner [in Minuska.builtin.list_model]
ssc_or [in Minuska.frontend]
ssc_and [in Minuska.frontend]
ssc_atom [in Minuska.frontend]
ssc_false [in Minuska.frontend]
ssc_true [in Minuska.frontend]
T
term_operand [in Minuska.lowlang]term_preterm [in Minuska.lowlang]
t_term [in Minuska.spec]
t_over [in Minuska.spec]
U
uf_rec_sub2_r [in Minuska.textbook_unification]uf_rec_sub2_l [in Minuska.textbook_unification]
uf_rec [in Minuska.textbook_unification]
uf_subterm [in Minuska.textbook_unification]
uf_term_len [in Minuska.textbook_unification]
uf_term_sym [in Minuska.textbook_unification]
uf_term_over [in Minuska.textbook_unification]
uf_over_term [in Minuska.textbook_unification]
uf_diff_builtin [in Minuska.textbook_unification]
uf_varin_fail_2 [in Minuska.textbook_unification]
uf_varin_fail_1 [in Minuska.textbook_unification]
V
v_cval [in Minuska.dt]Inductive Index
A
Act [in Minuska.default_everything]B
BoolFunSymbol [in Minuska.builtin.bool_signature]BoolPredSymbol [in Minuska.builtin.bool_signature]
BuiltinOrVar [in Minuska.spec]
BuiltinValue0 [in Minuska.builtin.klike]
BVLeaf [in Minuska.builtin.klike]
D
DecisionTree [in Minuska.dt]Declaration [in Minuska.frontend]
dt_sem_aux [in Minuska.dt]
dt_sem [in Minuska.dt]
E
Emptyset [in Minuska.builtin.empty]Expression2 [in Minuska.spec]
F
FunctionSymbol [in Minuska.builtin.klike]I
IntFunSymbol [in Minuska.builtin.int_signature]IntPredSymbol [in Minuska.builtin.int_signature]
L
ListFunSymbol [in Minuska.builtin.list_signature]ListPredSymbol [in Minuska.builtin.list_signature]
M
MinusL_rewrites [in Minuska.minusl_semantics]MinusL_Decl [in Minuska.minusl_syntax]
MyQuerySymbol [in Minuska.pi.trivial]
MyUnit [in Minuska.prelude]
N
notinstance [in Minuska.dt]P
Pattern [in Minuska.dt]PredicateSymbol [in Minuska.builtin.klike]
PreTerm' [in Minuska.lowlang]
pvmatch [in Minuska.dt]
S
SideCondition [in Minuska.spec]simple_list_carrier [in Minuska.builtin.list_model]
StringBuiltinOrVar [in Minuska.frontend]
StringExpression [in Minuska.frontend]
StringSideCondition [in Minuska.frontend]
SwitchCaseList [in Minuska.dt]
SymbolInfo [in Minuska.spec]
T
TermOver' [in Minuska.spec]Term' [in Minuska.lowlang]
U
unify_failure [in Minuska.textbook_unification]V
Value [in Minuska.dt]Projection Index
A
arity [in Minuska.dt]B
bb_function_names [in Minuska.spec]bi_sym_info [in Minuska.pval_ocaml_binding]
bi_beta [in Minuska.pval_ocaml_binding]
bi_signature [in Minuska.pval_ocaml_binding]
bps_neg_correct [in Minuska.spec]
bps_neg__sym [in Minuska.spec]
bps_neg_ar [in Minuska.spec]
bps_neg [in Minuska.spec]
bps_ar [in Minuska.spec]
br_value [in Minuska.frontend]
br_kind [in Minuska.frontend]
builtin [in Minuska.spec]
builtin_model_over [in Minuska.spec]
builtin_value_countable [in Minuska.spec]
builtin_value_eqdec [in Minuska.spec]
builtin_value [in Minuska.spec]
builtin_predicate_interp [in Minuska.spec]
builtin_function_interp [in Minuska.spec]
builtin_predicate_symbol_countable [in Minuska.spec]
builtin_predicate_symbol_eqdec [in Minuska.spec]
builtin_predicate_symbol [in Minuska.spec]
builtin_function_symbol_countable [in Minuska.spec]
builtin_function_symbol_eqdec [in Minuska.spec]
builtin_function_symbol [in Minuska.spec]
C
cd_cseq_context [in Minuska.frontend]cd_isValue [in Minuska.frontend]
cd_positions_to_wait_for [in Minuska.frontend]
cd_position [in Minuska.frontend]
cd_arity [in Minuska.frontend]
cd_sym [in Minuska.frontend]
cd_label [in Minuska.frontend]
Constructor [in Minuska.dt]
Constructor_eqdec [in Minuska.dt]
D
default_isValue [in Minuska.frontend]default_context_template [in Minuska.frontend]
default_empty_cseq_name [in Minuska.frontend]
default_cseq_name [in Minuska.frontend]
E
eab_bov [in Minuska.notations]eab_expr [in Minuska.notations]
F
function_symbol_morphism [in Minuska.signature_morphism]H
hd [in Minuska.spec]I
ifc_pure_function [in Minuska.builtin.information_flow_functor]ifc_pure_predicate [in Minuska.builtin.information_flow_functor]
ifc_0 [in Minuska.builtin.information_flow_functor]
ifc_get_pure_of_tagged [in Minuska.builtin.information_flow_functor]
ifc_get_tags_of_tagged [in Minuska.builtin.information_flow_functor]
ifc_get_pure [in Minuska.builtin.information_flow_functor]
ifc_get_tags [in Minuska.builtin.information_flow_functor]
ifc_tagged [in Minuska.builtin.information_flow_functor]
ifl_meet_top [in Minuska.builtin.information_flow_functor]
ifl_top [in Minuska.builtin.information_flow_functor]
ifl_join_bot [in Minuska.builtin.information_flow_functor]
ifl_bot [in Minuska.builtin.information_flow_functor]
ifl_absorb_2 [in Minuska.builtin.information_flow_functor]
ifl_absorb_1 [in Minuska.builtin.information_flow_functor]
ifl_join_comm [in Minuska.builtin.information_flow_functor]
ifl_join_assoc [in Minuska.builtin.information_flow_functor]
ifl_join [in Minuska.builtin.information_flow_functor]
ifl_meet_comm [in Minuska.builtin.information_flow_functor]
ifl_meet_assoc [in Minuska.builtin.information_flow_functor]
ifl_meet [in Minuska.builtin.information_flow_functor]
inject [in Minuska.model_algebra]
inject_inj [in Minuska.model_algebra]
M
mlld_decls [in Minuska.minusl_syntax]mlld_isValue_var [in Minuska.minusl_syntax]
mlld_isNonValue_c [in Minuska.minusl_syntax]
mlld_isValue_c [in Minuska.minusl_syntax]
N
NondetValue [in Minuska.spec]nondet_gen [in Minuska.spec]
P
pi_symbol_interp [in Minuska.spec]predicate_symbol_morphism [in Minuska.signature_morphism]
ProgramT [in Minuska.spec]
program_info [in Minuska.spec]
Q
QuerySymbol [in Minuska.spec]QuerySymbol_countable [in Minuska.spec]
QuerySymbol_eqdec [in Minuska.spec]
R
rd_rule [in Minuska.frontend]rd_label [in Minuska.frontend]
realize_br [in Minuska.frontend]
ri_reverse_pf [in Minuska.model_algebra]
ri_reverse [in Minuska.model_algebra]
ri_injection [in Minuska.model_algebra]
rmf_model [in Minuska.model_algebra]
rmf_nondet [in Minuska.model_algebra]
rmf_signature [in Minuska.model_algebra]
rm_model_over [in Minuska.model_algebra]
rm_carrier_countable [in Minuska.model_algebra]
rm_carrier_eqdec [in Minuska.model_algebra]
rm_carrier [in Minuska.model_algebra]
r_act [in Minuska.spec]
r_scs [in Minuska.spec]
r_to [in Minuska.spec]
r_from [in Minuska.spec]
S
satisfies [in Minuska.spec]sd_cseq_context [in Minuska.frontend]
sd_isValue [in Minuska.frontend]
sd_positions [in Minuska.frontend]
sd_arity [in Minuska.frontend]
sd_sym [in Minuska.frontend]
signature [in Minuska.spec]
smif [in Minuska.signature_morphism]
smip [in Minuska.signature_morphism]
sm_pred_neg [in Minuska.signature_morphism]
sm_pred_ar [in Minuska.signature_morphism]
sr_act [in Minuska.frontend]
sr_scs [in Minuska.frontend]
sr_to [in Minuska.frontend]
sr_from [in Minuska.frontend]
string2f [in Minuska.frontend]
string2p [in Minuska.frontend]
string2q [in Minuska.frontend]
string2sym [in Minuska.frontend]
string2var [in Minuska.frontend]
st_rules [in Minuska.frontend]
symbol [in Minuska.spec]
symbols [in Minuska.spec]
symbol_countable [in Minuska.spec]
symbol_eqdec [in Minuska.spec]
T
tl [in Minuska.spec]U
U [in Minuska.martelli_montanari]ua_unify_complete [in Minuska.unification_interface]
ua_unify_sound [in Minuska.unification_interface]
ua_unify [in Minuska.unification_interface]
u_extract_overlapping_meqns_insert_equiv [in Minuska.martelli_montanari]
u_extract_overlapping_meqns_in_u' [in Minuska.martelli_montanari]
u_extract_overlapping_meqns_in_ls_meqn [in Minuska.martelli_montanari]
u_extract_overlapping_meqns [in Minuska.martelli_montanari]
u_extract_nonempty_m_meqn_is_nonempty [in Minuska.martelli_montanari]
u_extract_nonempty_m_insert_equiv [in Minuska.martelli_montanari]
u_extract_nonempty_m_removes_element [in Minuska.martelli_montanari]
u_extract_nonempty_m_meqn [in Minuska.martelli_montanari]
u_insert_add [in Minuska.martelli_montanari]
u_insert_id [in Minuska.martelli_montanari]
u_insert [in Minuska.martelli_montanari]
u_map_elem_of [in Minuska.martelli_montanari]
u_map [in Minuska.martelli_montanari]
U_NoDup [in Minuska.martelli_montanari]
U_elements [in Minuska.martelli_montanari]
U_empty [in Minuska.martelli_montanari]
V
variable [in Minuska.spec]variables [in Minuska.spec]
variable_infinite [in Minuska.spec]
variable_countable [in Minuska.spec]
variable_eqdec [in Minuska.spec]
vars_of [in Minuska.spec]
Instance Index
A
Act_eqDec [in Minuska.default_everything]B
BoolFunSymbol_fin [in Minuska.builtin.bool_signature]BoolFunSymbol_eqdec [in Minuska.builtin.bool_signature]
BoolPredSymbol_fin [in Minuska.builtin.bool_signature]
BoolPredSymbol_eqdec [in Minuska.builtin.bool_signature]
BuiltinOrVar_eqdec [in Minuska.basic_properties]
BuiltinValue0_countable [in Minuska.builtin.klike]
BuiltinValue0_eqdec [in Minuska.builtin.klike]
BVLeaf_eqdec [in Minuska.builtin.klike]
C
cancel_TermOver_map [in Minuska.lowlang]cancel_uglify_prettify [in Minuska.lowlang]
cancel_prettify_uglify [in Minuska.lowlang]
D
DSM [in Minuska.default_everything]E
emptyset_fin [in Minuska.builtin.empty]emptyset_eqdec [in Minuska.builtin.empty]
Expression2_countable [in Minuska.basic_properties]
F
FunctionSymbol_fin [in Minuska.builtin.klike]FunctionSymbol_eqDec [in Minuska.builtin.klike]
I
information_flow_functor_trait [in Minuska.builtin.information_flow_functor]IntFunSymbol_fin [in Minuska.builtin.int_signature]
IntFunSymbol_eqdec [in Minuska.builtin.int_signature]
IntPredSymbol_fin [in Minuska.builtin.int_signature]
IntPredSymbol_eqdec [in Minuska.builtin.int_signature]
IsDownC_dec [in Minuska.minusl_compile_properties]
is_WildcardPattern_dec [in Minuska.dt]
is_ConstructorPattern_dec [in Minuska.dt]
L
ListFunSymbol_fin [in Minuska.builtin.list_signature]ListFunSymbol_eqdec [in Minuska.builtin.list_signature]
ListPredSymbol_fin [in Minuska.builtin.list_signature]
ListPredSymbol_eqdec [in Minuska.builtin.list_signature]
listset_eqdec [in Minuska.martelli_montanari]
ls_to_bor_dec [in Minuska.martelli_montanari]
M
meqn_semiset [in Minuska.martelli_montanari]meqn_singleton [in Minuska.martelli_montanari]
meqn_union [in Minuska.martelli_montanari]
meqn_equivalence [in Minuska.martelli_montanari]
meqn_equiv [in Minuska.martelli_montanari]
meqn_elem_of [in Minuska.martelli_montanari]
meqn_empty [in Minuska.martelli_montanari]
meqn_dec [in Minuska.martelli_montanari]
MinusL_Decl_eqDec [in Minuska.minusl_syntax]
MyProgramInfo [in Minuska.pi.trivial]
MyQuerySymbol_fin [in Minuska.pi.trivial]
MyQuerySymbol_eqdec [in Minuska.pi.trivial]
mysignature [in Minuska.builtin.klike]
mysignature [in Minuska.builtin.empty]
MySymbols [in Minuska.default_static_model]
O
option_Valuation2_vars_of [in Minuska.valuation_merge]P
PredicateSymbol_fin [in Minuska.builtin.klike]PredicateSymbol_eqDec [in Minuska.builtin.klike]
PreTerm'_A_B_fmap [in Minuska.lowlang]
PreTerm'_countable [in Minuska.lowlang]
PreTerm'_eqdec [in Minuska.lowlang]
R
RewritingRule2_eqdec [in Minuska.basic_properties]RewritingTheory2_wf_dec [in Minuska.interpreter_results]
row_of_wildcards_dec [in Minuska.dt]
row_startswith_ctor_dec [in Minuska.dt]
row_startswith_wildcard_dec [in Minuska.dt]
row_matches_ctor_dec [in Minuska.dt]
r_elem_of [in Minuska.martelli_montanari]
r_elements [in Minuska.martelli_montanari]
S
Satisfies_Valuation2_TermOverBuiltin_TermOverBoV [in Minuska.spec]Satisfies_SideCondition [in Minuska.spec]
Satisfies_TermOverBuiltin_TermOverExpression2 [in Minuska.spec]
Satisfies_Valuation2_TermOverBuiltinValue_BuiltinOrVar_instnace [in Minuska.spec]
SideCondition_eqdec [in Minuska.basic_properties]
signature_sum_morph_2_inj [in Minuska.model_algebra]
signature_sum_morph_1_inj [in Minuska.model_algebra]
simple_list_carrier__countable [in Minuska.builtin.list_model]
simple_list_carrier__eqdec [in Minuska.builtin.list_model]
sm [in Minuska.martelli_montanari_tests]
Subseteq_Valuation2 [in Minuska.spec]
T
TermOver_countable [in Minuska.basic_properties]Term_symbol_fmap [in Minuska.lowlang]
Term'_A_B_fmap [in Minuska.lowlang]
Term'_countable [in Minuska.lowlang]
Term'_eqdec [in Minuska.lowlang]
U
under_rel_subrel [in Minuska.prelude]under_rel_equiv [in Minuska.prelude]
under_rel_symm [in Minuska.prelude]
under_rel_trans [in Minuska.prelude]
under_rel_refl [in Minuska.prelude]
under_proper [in Minuska.prelude]
under_flip_mono [in Minuska.prelude]
under_mono [in Minuska.prelude]
V
VarsOf_Term' [in Minuska.lowlang]VarsOf_aosB [in Minuska.lowlang]
VarsOf_Valuation2 [in Minuska.spec]
VarsOf_Valuation2_ [in Minuska.spec]
VarsOf_TermOver_Expression2 [in Minuska.spec]
VarsOf_TermOver_BuiltinOrVar [in Minuska.spec]
VarsOf_BoV [in Minuska.spec]
VarsOf_sc [in Minuska.spec]
VarsOf_list_something [in Minuska.spec]
VarsOf_Expression2 [in Minuska.spec]
VarsOf_TermOver [in Minuska.spec]
VarsOf_builtin [in Minuska.spec]
VarsOf_symbol [in Minuska.spec]
VarsOf_MinusL_LangDef [in Minuska.minusl_syntax]
VarsOf_MinusL_Decl [in Minuska.minusl_syntax]
vector_of_wildcards_dec [in Minuska.dt]
other
β [in Minuska.builtin.klike]β [in Minuska.builtin.empty]
Section Index
C
countable [in Minuska.lowlang]custom_induction_principle_2 [in Minuska.basic_properties]
custom_induction_principle_2 [in Minuska.basic_properties]
custom_induction_principle [in Minuska.spec]
custom_induction_principle [in Minuska.spec]
custom_induction_principle [in Minuska.dt]
custom_induction_principle [in Minuska.dt]
D
default_model [in Minuska.default_static_model]E
eqdec [in Minuska.lowlang]M
MinusL_sem [in Minuska.minusl_semantics]S
sec [in Minuska.builtin.klike]sec [in Minuska.builtin.empty]
sec2 [in Minuska.builtin.klike]
sum [in Minuska.model_algebra]
W
wsm [in Minuska.frontend]Definition Index
A
actions_of_ldef [in Minuska.minusl_syntax]actions_of_decl [in Minuska.minusl_syntax]
analyze_list_from_end [in Minuska.prelude]
AO'_getOperator [in Minuska.lowlang]
apply_symbol'' [in Minuska.lowlang]
apply_symbol' [in Minuska.lowlang]
argument_sequence [in Minuska.frontend]
argument_name [in Minuska.frontend]
B
basic_rule [in Minuska.default_everything]bfmap_Z_Z__bool [in Minuska.builtin.klike]
bfmap_Z_Z__Prop [in Minuska.builtin.klike]
bfmap_Z_Z__Z [in Minuska.builtin.klike]
bfmap1 [in Minuska.builtin.klike]
bfmap2 [in Minuska.builtin.klike]
bfmap2P [in Minuska.builtin.klike]
bool_signature [in Minuska.builtin.bool_signature]
bool_model [in Minuska.builtin.bool_model]
bool_relaxed_model [in Minuska.builtin.bool_model]
bool_model_over [in Minuska.builtin.bool_model]
bool_predicate_interp [in Minuska.builtin.bool_model]
bool_function_interp [in Minuska.builtin.bool_model]
bool_carrier [in Minuska.builtin.bool_model]
BoV_to_Expr2 [in Minuska.default_everything]
BoV_to_Expr2 [in Minuska.basic_properties]
BuiltinOrVar_sind [in Minuska.spec]
BuiltinOrVar_rec [in Minuska.spec]
BuiltinOrVar_ind [in Minuska.spec]
BuiltinOrVar_rect [in Minuska.spec]
builtins_binding [in Minuska.builtin.empty]
builtins_klike [in Minuska.pval_ocaml_binding]
builtins_empty [in Minuska.pval_ocaml_binding]
BuiltinValue [in Minuska.builtin.klike]
BuiltinValue0_sind [in Minuska.builtin.klike]
BuiltinValue0_rec [in Minuska.builtin.klike]
BuiltinValue0_ind [in Minuska.builtin.klike]
BuiltinValue0_rect [in Minuska.builtin.klike]
BVLeaf_sind [in Minuska.builtin.klike]
BVLeaf_rec [in Minuska.builtin.klike]
BVLeaf_ind [in Minuska.builtin.klike]
BVLeaf_rect [in Minuska.builtin.klike]
BVsize [in Minuska.builtin.klike]
bv_to_tree [in Minuska.builtin.klike]
C
ClauseMatrix [in Minuska.dt]ClauseMatrix_size [in Minuska.dt]
cmmatch [in Minuska.dt]
compactify [in Minuska.martelli_montanari]
compactify_by_vars [in Minuska.martelli_montanari]
compactify_by_var [in Minuska.martelli_montanari]
compactify_by_var_extract_and_comp [in Minuska.martelli_montanari]
compile [in Minuska.minusl_compile]
compile [in Minuska.dt]
CompileT [in Minuska.minusl_compile]
compile' [in Minuska.minusl_compile]
concat_list_option_str [in Minuska.interp_loop]
ContextTemplate [in Minuska.frontend]
cooling_rule [in Minuska.frontend]
create_eqn [in Minuska.martelli_montanari]
cseq [in Minuska.frontend]
ctx_cool [in Minuska.minusl_compile]
ctx_heat [in Minuska.minusl_compile]
D
dec [in Minuska.martelli_montanari]DecisionTree_sind [in Minuska.dt]
DecisionTree_rec [in Minuska.dt]
DecisionTree_ind [in Minuska.dt]
DecisionTree_rect [in Minuska.dt]
Declaration_sind [in Minuska.frontend]
Declaration_rec [in Minuska.frontend]
Declaration_ind [in Minuska.frontend]
Declaration_rect [in Minuska.frontend]
dec_paper_input1 [in Minuska.martelli_montanari_tests]
dec_aux [in Minuska.martelli_montanari]
dec_make_multeq [in Minuska.martelli_montanari]
Default [in Minuska.dt]
default_model [in Minuska.default_static_model]
deg [in Minuska.textbook_unification_alg]
delta_in_val [in Minuska.properties]
downC [in Minuska.minusl_compile]
down2 [in Minuska.minusl_compile]
down2E [in Minuska.minusl_compile]
dt_sem_aux_sind [in Minuska.dt]
dt_sem_aux_ind [in Minuska.dt]
dt_sem_sind [in Minuska.dt]
dt_sem_ind [in Minuska.dt]
E
eject [in Minuska.builtin.empty]emptyCseq [in Minuska.frontend]
Emptyset_sind [in Minuska.builtin.empty]
Emptyset_rec [in Minuska.builtin.empty]
Emptyset_ind [in Minuska.builtin.empty]
Emptyset_rect [in Minuska.builtin.empty]
eqn [in Minuska.textbook_unification_alg]
eqn [in Minuska.martelli_montanari]
eqns_vars [in Minuska.textbook_unification_alg]
eqns_size [in Minuska.textbook_unification_alg]
eqn_vars [in Minuska.textbook_unification_alg]
eqn_size [in Minuska.textbook_unification_alg]
equiv_UP [in Minuska.martelli_montanari]
eval_function_in_iflow [in Minuska.builtin.information_flow_functor]
eval_function_in_orig [in Minuska.builtin.information_flow_functor]
eval_predicate_in_iflow [in Minuska.builtin.information_flow_functor]
eval_predicate_in_orig [in Minuska.builtin.information_flow_functor]
eval_et [in Minuska.naive_interpreter]
example_list_int_model_1 [in Minuska.builtin.example_list_int_model]
Expression2_subst [in Minuska.basic_properties]
Expression2_rect [in Minuska.basic_properties]
Expression2_evaluate [in Minuska.spec]
Expression2_ind [in Minuska.spec]
Expression2_evaluate_nv [in Minuska.naive_interpreter]
extract_mgu [in Minuska.martelli_montanari]
extract_mgu_aux [in Minuska.martelli_montanari]
E_of_tree [in Minuska.basic_properties]
E_to_tree [in Minuska.basic_properties]
F
format_string_list [in Minuska.prelude]framed_rule [in Minuska.default_everything]
freezer [in Minuska.frontend]
FunctionSymbol_sind [in Minuska.builtin.klike]
FunctionSymbol_rec [in Minuska.builtin.klike]
FunctionSymbol_ind [in Minuska.builtin.klike]
FunctionSymbol_rect [in Minuska.builtin.klike]
function_interp_sum [in Minuska.model_algebra]
G
getSubterm [in Minuska.dt]get_vars_of_M_listset_meqns [in Minuska.martelli_montanari]
get_vars_of_S_listset_meqns [in Minuska.martelli_montanari]
get_vars_of_M_meqns [in Minuska.martelli_montanari]
get_vars_of_S_list_meqns [in Minuska.martelli_montanari]
get_nonvar_part [in Minuska.martelli_montanari]
get_var_part [in Minuska.martelli_montanari]
global_naive_interpreter_sound [in Minuska.default_everything]
global_naive_interpreter_ext [in Minuska.default_everything]
global_naive_interpreter [in Minuska.default_everything]
GT [in Minuska.default_everything]
gt_term [in Minuska.default_everything]
gt_over [in Minuska.default_everything]
H
hasDepthExactly [in Minuska.minusl_compile_properties]heating_rule_seq [in Minuska.frontend]
helper [in Minuska.lowlang]
helper'' [in Minuska.lowlang]
I
impl_isMap [in Minuska.builtin.klike]impl_isList [in Minuska.builtin.klike]
impl_isBool [in Minuska.builtin.klike]
impl_isString [in Minuska.builtin.klike]
impl_isZ [in Minuska.builtin.klike]
information_flow_functor_get_pure [in Minuska.builtin.information_flow_functor]
information_flow_functor_get_tags [in Minuska.builtin.information_flow_functor]
information_flow_functor_tagged [in Minuska.builtin.information_flow_functor]
information_flow_functor [in Minuska.builtin.information_flow_functor]
initialState [in Minuska.frontend]
init_r [in Minuska.martelli_montanari]
init_r' [in Minuska.martelli_montanari]
init_meqn [in Minuska.martelli_montanari]
inject_string [in Minuska.builtin.empty]
inject_Z [in Minuska.builtin.empty]
inject_bool [in Minuska.builtin.empty]
inj_id [in Minuska.model_algebra]
inj_compose [in Minuska.model_algebra]
inspect [in Minuska.prelude]
Interpreter [in Minuska.spec_interpreter]
Interpreter_sound [in Minuska.spec_interpreter]
Interpreter_sound' [in Minuska.spec_interpreter]
Interpreter_ext [in Minuska.spec_interpreter]
interp_in_from [in Minuska.interp_loop]
interp_in_from' [in Minuska.interp_loop]
interp_loop_ext [in Minuska.interp_loop]
interp_loop [in Minuska.interp_loop]
int_signature [in Minuska.builtin.int_signature]
int_model [in Minuska.builtin.int_model]
int_relaxed_model [in Minuska.builtin.int_model]
int_model_over [in Minuska.builtin.int_model]
int_predicate_interp [in Minuska.builtin.int_model]
int_function_interp [in Minuska.builtin.int_model]
int_carrier [in Minuska.builtin.int_model]
isDownC [in Minuska.minusl_compile_properties]
isHeadInFirstColumn [in Minuska.dt]
is_unifier_of [in Minuska.textbook_unification]
is_subterm_b [in Minuska.basic_properties]
is_compact [in Minuska.martelli_montanari]
is_compact_up_to_vars [in Minuska.martelli_montanari]
is_compact_up_to_var [in Minuska.martelli_montanari]
is_unifier_of [in Minuska.martelli_montanari]
is_WildcardPattern [in Minuska.dt]
is_ConstructorPattern [in Minuska.dt]
L
least_of [in Minuska.textbook_unification]liftBinary [in Minuska.builtin.klike]
liftBinaryP [in Minuska.builtin.klike]
liftNulary [in Minuska.builtin.klike]
liftNularyP [in Minuska.builtin.klike]
liftTernary [in Minuska.builtin.klike]
liftUnary [in Minuska.builtin.klike]
liftUnaryP [in Minuska.builtin.klike]
list_collect [in Minuska.prelude]
list_collect_e [in Minuska.frontend]
list_signature [in Minuska.builtin.list_signature]
list_swap_head [in Minuska.dt]
list_relaxed_functor [in Minuska.builtin.list_model]
list_predicate_interp [in Minuska.builtin.list_model]
list_function_interp [in Minuska.builtin.list_model]
M
Meqn [in Minuska.martelli_montanari]meqns_s_intersect [in Minuska.martelli_montanari]
meqn_valid [in Minuska.martelli_montanari]
meqn_left_valid [in Minuska.martelli_montanari]
meqn_right_valid [in Minuska.martelli_montanari]
meqn_m_empty [in Minuska.martelli_montanari]
meqn_subst [in Minuska.martelli_montanari]
mgu_res [in Minuska.martelli_montanari_tests]
MinusL_rewrites_sind [in Minuska.minusl_semantics]
MinusL_rewrites_rec [in Minuska.minusl_semantics]
MinusL_rewrites_ind [in Minuska.minusl_semantics]
MinusL_rewrites_rect [in Minuska.minusl_semantics]
MinusL_isNonValue [in Minuska.minusl_syntax]
MinusL_isValue [in Minuska.minusl_syntax]
MinusL_LangDef_wf [in Minuska.minusl_syntax]
modelover_nv_lift [in Minuska.model_algebra]
modelover_sum [in Minuska.model_algebra]
model_reduction [in Minuska.model_algebra]
model_of_relaxed [in Minuska.model_algebra]
MyQuerySymbol_sind [in Minuska.pi.trivial]
MyQuerySymbol_rec [in Minuska.pi.trivial]
MyQuerySymbol_ind [in Minuska.pi.trivial]
MyQuerySymbol_rect [in Minuska.pi.trivial]
MyUnit_sind [in Minuska.prelude]
MyUnit_rec [in Minuska.prelude]
MyUnit_ind [in Minuska.prelude]
MyUnit_rect [in Minuska.prelude]
my_binding [in Minuska.pi.trivial]
my_decode [in Minuska.builtin.klike]
my_encode [in Minuska.builtin.klike]
N
naive_interpreter [in Minuska.naive_interpreter]naive_interpreter_ext [in Minuska.naive_interpreter]
notinstance_sind [in Minuska.dt]
notinstance_ind [in Minuska.dt]
not_stuck [in Minuska.spec_interpreter]
O
Occurrence [in Minuska.dt]P
PatternMatrice [in Minuska.dt]PatternVector [in Minuska.dt]
Pattern_ind [in Minuska.dt]
pflookup [in Minuska.prelude]
pfmap [in Minuska.prelude]
pi_trivial [in Minuska.pval_ocaml_binding]
PredicateSymbol_sind [in Minuska.builtin.klike]
PredicateSymbol_rec [in Minuska.builtin.klike]
PredicateSymbol_ind [in Minuska.builtin.klike]
PredicateSymbol_rect [in Minuska.builtin.klike]
predicate_interp_sum [in Minuska.model_algebra]
PreTerm'_zipWith [in Minuska.lowlang]
PreTerm'_collapse_option [in Minuska.lowlang]
PreTerm'_fmap [in Minuska.lowlang]
PreTerm'_of_gen_tree [in Minuska.lowlang]
PreTerm'_to_gen_tree [in Minuska.lowlang]
PreTerm'_get_symbol [in Minuska.lowlang]
PreTerm'_sind [in Minuska.lowlang]
PreTerm'_rec [in Minuska.lowlang]
PreTerm'_ind [in Minuska.lowlang]
PreTerm'_rect [in Minuska.lowlang]
prettify [in Minuska.lowlang]
prettify' [in Minuska.lowlang]
process_declarations [in Minuska.frontend]
process_declaration [in Minuska.frontend]
process_strictness_declaration [in Minuska.frontend]
process_context_declaration [in Minuska.frontend]
process_rule_declaration [in Minuska.frontend]
projTopCont [in Minuska.minusl_compile_properties]
projTopCtrl [in Minuska.minusl_compile_properties]
projTopData [in Minuska.minusl_compile_properties]
pvmatch_sind [in Minuska.dt]
pvmatch_ind [in Minuska.dt]
pvvecmatch [in Minuska.dt]
R
R [in Minuska.martelli_montanari]realize_thy [in Minuska.frontend]
REST_SEQ [in Minuska.frontend]
rewrites_to_thy [in Minuska.spec]
rewrites_to_nondet [in Minuska.spec]
rewrites_to [in Minuska.spec]
rewrites_in_valuation_under_to [in Minuska.spec]
RewritingRule2_wf [in Minuska.spec_interpreter]
RewritingTheory2 [in Minuska.spec]
RewritingTheory2_wf [in Minuska.spec_interpreter]
rewriting_relation [in Minuska.spec]
rinj_inr [in Minuska.model_algebra]
rinj_inl [in Minuska.model_algebra]
rinj_id [in Minuska.model_algebra]
rinj_compose [in Minuska.model_algebra]
rmf_apply [in Minuska.model_algebra]
row_of_wildcards [in Minuska.dt]
row_startswith_ctor [in Minuska.dt]
row_startswith_wildcard [in Minuska.dt]
row_matches_ctor [in Minuska.dt]
RST_list_closure [in Minuska.martelli_montanari]
r_valid [in Minuska.martelli_montanari]
r_has_all_vars [in Minuska.martelli_montanari]
r_vars_disjoint [in Minuska.martelli_montanari]
S
Satisfies_Valuation2_TermOverBuiltinValue_BuiltinOrVar [in Minuska.spec]sat2B [in Minuska.spec]
sat2E [in Minuska.spec]
sbov_to_e_bov [in Minuska.frontend]
se_to_Expression [in Minuska.frontend]
SideCondition_subst [in Minuska.basic_properties]
SideCondition_evaluate [in Minuska.spec]
SideCondition_sind [in Minuska.spec]
SideCondition_rec [in Minuska.spec]
SideCondition_ind [in Minuska.spec]
SideCondition_rect [in Minuska.spec]
signature_sum_morphism_2 [in Minuska.model_algebra]
signature_sum_morphism_2_predicate [in Minuska.model_algebra]
signature_sum_morphism_2_function [in Minuska.model_algebra]
signature_sum_morphism_1 [in Minuska.model_algebra]
signature_sum_morphism_1_predicate [in Minuska.model_algebra]
signature_sum_morphism_1_function [in Minuska.model_algebra]
signature_sum [in Minuska.model_algebra]
Simplify [in Minuska.dt]
Simplify_step [in Minuska.dt]
size_of_var_in_val [in Minuska.properties]
slice [in Minuska.prelude]
srr_to_rr [in Minuska.frontend]
ssc_to_sc [in Minuska.frontend]
sSymbolicTerm_to_ExprTerm [in Minuska.frontend]
StepT [in Minuska.default_everything]
StepT_ext [in Minuska.default_everything]
sTermOverBoV_subst [in Minuska.default_everything]
sTermOverBoV_subst_expr2 [in Minuska.default_everything]
sTermOverBoV_subst_gen [in Minuska.default_everything]
strictness_to_contexts [in Minuska.frontend]
StringExpression_sind [in Minuska.frontend]
StringExpression_rec [in Minuska.frontend]
StringExpression_ind [in Minuska.frontend]
StringExpression_rect [in Minuska.frontend]
StringSideCondition_sind [in Minuska.frontend]
StringSideCondition_rec [in Minuska.frontend]
StringSideCondition_ind [in Minuska.frontend]
StringSideCondition_rect [in Minuska.frontend]
StringVariables [in Minuska.string_variables]
stuck [in Minuska.spec_interpreter]
sub [in Minuska.textbook_unification_alg]
SubT [in Minuska.unification_interface]
SubTMM [in Minuska.martelli_montanari]
sub_ext [in Minuska.textbook_unification]
sub_lt [in Minuska.textbook_unification]
sub_app_mm [in Minuska.martelli_montanari]
sub_app [in Minuska.unification_interface]
swap_column_in_clause_matrix [in Minuska.dt]
swap_column_in_list [in Minuska.dt]
SwitchCaseList_sind [in Minuska.dt]
SwitchCaseList_rec [in Minuska.dt]
SwitchCaseList_ind [in Minuska.dt]
SwitchCaseList_rect [in Minuska.dt]
SymbolicTerm_to_ExprTerm [in Minuska.frontend]
sym_info [in Minuska.builtin.klike]
T
T [in Minuska.martelli_montanari]take_any [in Minuska.martelli_montanari]
TermOver [in Minuska.spec]
TermOverBoV_to_TermOverExpr2 [in Minuska.basic_properties]
TermOverBoV_subst [in Minuska.basic_properties]
TermOverBoV_subst_expr2 [in Minuska.basic_properties]
TermOverBoV_subst_gen [in Minuska.basic_properties]
TermOverBoV_eval [in Minuska.properties]
TermOverBuiltin_subst [in Minuska.basic_properties]
TermOverBuiltin_to_TermOverBoV [in Minuska.spec]
TermOver_size_with [in Minuska.basic_properties]
TermOver_rect [in Minuska.basic_properties]
TermOver_map [in Minuska.spec]
TermOver_size [in Minuska.spec]
TermOver_collect [in Minuska.naive_interpreter]
TermOver'_map [in Minuska.spec]
TermOver'_ind [in Minuska.spec]
TermOver'_leaves [in Minuska.properties]
TermOver'_option_map [in Minuska.properties]
TermOver'_rinj [in Minuska.builtin.information_flow_functor]
TermOver'_e_map [in Minuska.frontend]
TermOver'_join [in Minuska.naive_interpreter]
term_has_same_symbol [in Minuska.martelli_montanari]
term_params [in Minuska.martelli_montanari]
term_is_constant [in Minuska.martelli_montanari]
term_is_nonvar [in Minuska.martelli_montanari]
term_is_var [in Minuska.martelli_montanari]
Term'_collapse_option [in Minuska.lowlang]
Term'_fmap [in Minuska.lowlang]
Term'_from_gen_tree [in Minuska.lowlang]
Term'_to_gen_tree [in Minuska.lowlang]
textbook_unification_algorithm [in Minuska.textbook_unification]
thy_lhs_match_one [in Minuska.naive_interpreter]
tosse_to_e_tose [in Minuska.frontend]
toss_to_e_tosb [in Minuska.frontend]
TO_of_tree [in Minuska.basic_properties]
TO_to_tree [in Minuska.basic_properties]
to_PreTerm'' [in Minuska.lowlang]
to_Term'' [in Minuska.lowlang]
to_PreTerm' [in Minuska.lowlang]
to_Term' [in Minuska.lowlang]
to_theory [in Minuska.frontend]
to_transform_sym [in Minuska.frontend]
transl_string_pattern [in Minuska.frontend]
transpose [in Minuska.martelli_montanari]
tree_to_bv [in Minuska.builtin.klike]
trivial_stream [in Minuska.default_static_model]
try_neg [in Minuska.properties]
try_neg_s [in Minuska.frontend]
try_match_lhs_with_sc [in Minuska.naive_interpreter]
try_match_new [in Minuska.naive_interpreter]
t_valid [in Minuska.martelli_montanari]
t_meqn_v_prec [in Minuska.martelli_montanari]
t_meqn_m_valid [in Minuska.martelli_montanari]
U
uglify' [in Minuska.lowlang]unify [in Minuska.textbook_unification_alg]
unify_paper1_input2 [in Minuska.martelli_montanari_tests]
unify_paper1_input1 [in Minuska.martelli_montanari_tests]
unify_failure_sind [in Minuska.textbook_unification]
unify_failure_ind [in Minuska.textbook_unification]
unify_terms [in Minuska.martelli_montanari]
unify_r [in Minuska.martelli_montanari]
unify_r_aux [in Minuska.martelli_montanari]
unify_r_step [in Minuska.martelli_montanari]
UP [in Minuska.martelli_montanari]
up_of_r [in Minuska.martelli_montanari]
up_of_t [in Minuska.martelli_montanari]
up_of_u [in Minuska.martelli_montanari]
up_of_meqns [in Minuska.martelli_montanari]
up_of_meqn [in Minuska.martelli_montanari]
up_of_terms [in Minuska.martelli_montanari]
u_subst [in Minuska.martelli_montanari]
u_insert_many [in Minuska.martelli_montanari]
U_listset_ops [in Minuska.martelli_montanari]
u_extract_overlapping_meqns_listset [in Minuska.martelli_montanari]
u_extract_nonempty_m_meqn_listset [in Minuska.martelli_montanari]
u_insert_listset [in Minuska.martelli_montanari]
u_get_vars [in Minuska.martelli_montanari]
u_valid [in Minuska.martelli_montanari]
V
Valuation2 [in Minuska.spec]Valuation2_merge_olist [in Minuska.valuation_merge]
Valuation2_merge_list [in Minuska.valuation_merge]
Valuation2_merge_with [in Minuska.valuation_merge]
Valuation2_compatible_with_bound [in Minuska.valuation_merge]
Valuation2_compatible_with [in Minuska.valuation_merge]
Valuation2_use_left [in Minuska.valuation_merge]
Valuation2_restrict [in Minuska.naive_interpreter]
ValueVector [in Minuska.dt]
Value_ind [in Minuska.dt]
vars_of_sub [in Minuska.textbook_unification]
vars_of_to_l2r [in Minuska.basic_properties]
vars_of_Term'B [in Minuska.lowlang]
vars_of_aosB [in Minuska.lowlang]
vars_of_BoV [in Minuska.spec]
vars_of_sc [in Minuska.spec]
vars_of_Expression2 [in Minuska.spec]
var_term_to_var [in Minuska.martelli_montanari]
var_to_term [in Minuska.martelli_montanari]
vector_of_wildcards [in Minuska.dt]
W
wfeqn [in Minuska.textbook_unification]wfeqns [in Minuska.textbook_unification]
wfsub [in Minuska.textbook_unification]
wft [in Minuska.textbook_unification]
Z
zipWith [in Minuska.martelli_montanari]other
βover [in Minuska.builtin.klike]βover [in Minuska.builtin.empty]
Record Index
B
BuiltinInterface [in Minuska.pval_ocaml_binding]BuiltinRepr [in Minuska.frontend]
BuiltinsBinding [in Minuska.spec]
C
ContextDeclaration [in Minuska.frontend]D
Defaults [in Minuska.frontend]E
ExprAndBoV [in Minuska.notations]I
IFCRelaxedModelTrait0 [in Minuska.builtin.information_flow_functor]IFCRelaxedModelTrait1 [in Minuska.builtin.information_flow_functor]
IFLattice [in Minuska.builtin.information_flow_functor]
Injection [in Minuska.model_algebra]
M
MinusL_LangDef [in Minuska.minusl_syntax]Model [in Minuska.spec]
ModelOver [in Minuska.spec]
MVariables [in Minuska.spec]
P
ProgramInfo [in Minuska.spec]R
Realization [in Minuska.frontend]RelaxedModel [in Minuska.model_algebra]
RelaxedModelFunctorT [in Minuska.model_algebra]
ReversibleInjection [in Minuska.model_algebra]
RewritingRule2 [in Minuska.spec]
RuleDeclaration [in Minuska.frontend]
S
Satisfies [in Minuska.spec]Signature [in Minuska.spec]
Signature [in Minuska.dt]
SignatureMorphism [in Minuska.signature_morphism]
SMInj [in Minuska.signature_morphism]
State [in Minuska.frontend]
StaticModel [in Minuska.spec]
Stream [in Minuska.spec]
StrictnessDeclaration [in Minuska.frontend]
StringRewritingRule [in Minuska.frontend]
Symbols [in Minuska.spec]
U
UnificationAlgorithm [in Minuska.unification_interface]U_ops [in Minuska.martelli_montanari]
V
VarsOf [in Minuska.spec]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1250 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (49 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (260 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (152 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (146 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (103 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (451 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |