| 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 | (1484 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) |
| Variable 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 | (38 entries) |
| 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 | (57 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 | (381 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 | (173 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 | (39 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 | (136 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 | (104 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 | (12 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 | (511 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 | (31 entries) |
Global Index
A
analyze_list_from_end [definition, in Minuska.prelude]another_helper_lemma' [lemma, in Minuska.substitution_parseq_conv]
another_helper_lemma [lemma, in Minuska.substitution_parseq_conv]
AO'_getOperator [definition, in Minuska.lowlang]
apply_TermSymbol'' [definition, in Minuska.lowlang]
apply_TermSymbol' [definition, in Minuska.lowlang]
argument_sequence [definition, in Minuska.frontend]
argument_name [definition, in Minuska.frontend]
arity [projection, in Minuska.dt]
asIfWithEq [definition, in Minuska.symex]
ats_edc [definition, in Minuska.hidden.hidden_unit]
attribute_interpretation [projection, in Minuska.spec]
AttrSymbol [projection, in Minuska.spec]
AttrSymbol_morph_inj [projection, in Minuska.signature_morphism]
AttrSymbol_morph [projection, in Minuska.signature_morphism]
AttrSymbol_edc [projection, in Minuska.spec]
B
BackgroundModel [record, in Minuska.spec]BackgroundModelOver [record, in Minuska.spec]
background_model_over [projection, in Minuska.spec]
BasicEffect0 [definition, in Minuska.spec]
BasicEffect0_eqdec [instance, in Minuska.basic_properties]
BasicEffect0_evaluate [definition, in Minuska.spec]
BasicEffect0_evaluate'_frame [lemma, in Minuska.properties]
BasicEffect0_evaluate'_extensive [lemma, in Minuska.properties]
BasicEffect0' [inductive, in Minuska.spec]
BasicTypes [record, in Minuska.spec]
BasicTypesInjMorphism [record, in Minuska.signature_morphism]
BasicTypesMorphism [definition, in Minuska.signature_morphism]
BasicTypesMorphism' [record, in Minuska.signature_morphism]
BasicTypesProperties [record, in Minuska.spec]
BasicValue [projection, in Minuska.spec]
BasicValue_morph_inj [projection, in Minuska.signature_morphism]
BasicValue_morph [projection, in Minuska.signature_morphism]
BasicValue_edc [projection, in Minuska.spec]
basic_rule [definition, in Minuska.default_everything]
basic_types_properties [projection, in Minuska.spec]
basic_types [projection, in Minuska.spec]
basic_properties [library]
bb_function_names [projection, in Minuska.spec]
be_remember [constructor, in Minuska.spec]
be_method [constructor, 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]
bindFresher [definition, in Minuska.fresher]
bindings [definition, in Minuska.pi.trivial]
bindings [definition, in Minuska.builtin.klike]
bindings [definition, in Minuska.builtin.empty]
bindings [definition, in Minuska.hidden.hidden_unit]
bind_None_T_1 [lemma, in Minuska.prelude]
bind_Some_T_2 [lemma, in Minuska.prelude]
bind_Some_T_1 [lemma, in Minuska.prelude]
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_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_va [definition, in Minuska.builtin.bool_model]
bool_relaxed_va [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_signature [library]
bool_model [library]
BoV_to_Expr2 [definition, in Minuska.basic_properties]
bov_Variabl [constructor, in Minuska.spec]
bov_builtin [constructor, in Minuska.spec]
br_value [projection, in Minuska.frontend]
br_kind [projection, in Minuska.frontend]
BuiltinOrVar [definition, in Minuska.spec]
BuiltinOrVar_eqdec [instance, in Minuska.basic_properties]
BuiltinOrVar' [inductive, in Minuska.spec]
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]
BuiltinValue [library]
BuiltinValue0_countable [instance, in Minuska.builtin.klike]
BuiltinValue0_eqdec [instance, in Minuska.builtin.klike]
BuiltinValue0_eqdec_helper_0 [lemma, in Minuska.builtin.klike]
builtin_predicate_interp [projection, in Minuska.spec]
builtin_function_interp [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_EDC [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]
BV_EDC [definition, in Minuska.builtin.empty]
b_have_different_TermSymbols [constructor, in Minuska.builtin.klike]
b_have_same_TermSymbol [constructor, in Minuska.builtin.klike]
b_is_not_applied_TermSymbol [constructor, in Minuska.builtin.klike]
b_is_applied_TermSymbol [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.basic_properties]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]
collapses_to_sind [definition, in Minuska.hilang]
collapses_to_rec [definition, in Minuska.hilang]
collapses_to_ind [definition, in Minuska.hilang]
collapses_to_rect [definition, in Minuska.hilang]
collapses_to [inductive, in Minuska.hilang]
combine_symbol_classifiers [definition, in Minuska.ocaml_interface]
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.dt]
compose_uglify_prettify [lemma, in Minuska.lowlang]
compose_prettify_uglify [lemma, in Minuska.lowlang]
compose_renaming_inverse_restrict [lemma, in Minuska.substitution_parseq_conv]
concat_list_option_str [definition, in Minuska.interp_loop]
concrete_is_larger_than_TermSymbolic [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]
Context__sind [definition, in Minuska.hilang]
Context__rec [definition, in Minuska.hilang]
Context__ind [definition, in Minuska.hilang]
Context__rect [definition, in Minuska.hilang]
Context_ [inductive, in Minuska.hilang]
contract_extend_term [lemma, in Minuska.hilang]
contract_term [definition, in Minuska.hilang]
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]
cto_base [constructor, in Minuska.hilang]
ctx_seq [constructor, in Minuska.hilang]
ctx_subst [definition, in Minuska.hilang]
ctx_term [constructor, in Minuska.hilang]
ctx_hole [constructor, in Minuska.hilang]
custom_induction_principle_2.Σ [variable, in Minuska.basic_properties]
custom_induction_principle_2 [section, in Minuska.basic_properties]
custom_induction_principle_2._edA [variable, in Minuska.basic_properties]
custom_induction_principle_2.A [variable, in Minuska.basic_properties]
custom_induction_principle_2._edB [variable, in Minuska.basic_properties]
custom_induction_principle_2.B [variable, in Minuska.basic_properties]
custom_induction_principle_2.Σ [variable, in Minuska.basic_properties]
custom_induction_principle_2 [section, in Minuska.basic_properties]
custom_induction_principle.preserved_by_attribute [variable, in Minuska.spec]
custom_induction_principle.preserved_by_query [variable, in Minuska.spec]
custom_induction_principle.preserved_by_fun [variable, in Minuska.spec]
custom_induction_principle.true_for_var [variable, in Minuska.spec]
custom_induction_principle.true_for_ground [variable, in Minuska.spec]
custom_induction_principle.P [variable, in Minuska.spec]
custom_induction_principle.As [variable, in Minuska.spec]
custom_induction_principle.Qs [variable, in Minuska.spec]
custom_induction_principle.Fs [variable, in Minuska.spec]
custom_induction_principle.Ts [variable, in Minuska.spec]
custom_induction_principle.Va [variable, in Minuska.spec]
custom_induction_principle.Bv [variable, in Minuska.spec]
custom_induction_principle [section, in Minuska.spec]
custom_induction_principle.preserved_by_term [variable, in Minuska.spec]
custom_induction_principle.true_for_over [variable, in Minuska.spec]
custom_induction_principle.P [variable, in Minuska.spec]
custom_induction_principle.A [variable, in Minuska.spec]
custom_induction_principle.T [variable, in Minuska.spec]
custom_induction_principle [section, in Minuska.spec]
custom_induction_principle.preserved_by_cval [variable, in Minuska.dt]
custom_induction_principle.P [variable, in Minuska.dt]
custom_induction_principle.Σ [variable, in Minuska.dt]
custom_induction_principle [section, in Minuska.dt]
custom_induction_principle.preserved_by_cpat [variable, in Minuska.dt]
custom_induction_principle.true_for_wildcard [variable, in Minuska.dt]
custom_induction_principle.P [variable, in Minuska.dt]
custom_induction_principle.Σ [variable, 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_label [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_correct [lemma, in Minuska.dt]
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]
denot_ss [definition, in Minuska.symex]
denot_sss [definition, in Minuska.symex]
dom_merge_use_left [lemma, in Minuska.valuation_merge]
dom_make_parallel [lemma, in Minuska.substitution_parseq_conv]
dom_make_parallel0 [lemma, in Minuska.substitution_parseq_conv]
dom_rinverse [lemma, in Minuska.substitution_parseq_conv]
dom_rlift_inverse [lemma, in Minuska.substitution_parseq_conv]
dom_renaming_for [lemma, in Minuska.substitution_parseq_conv]
dom_subp_compose_subseteq [lemma, in Minuska.substitution_parseq_conv]
double_satisfies_contradiction [lemma, in Minuska.properties]
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]
EDC [record, in Minuska.spec]
edc_count [projection, in Minuska.spec]
edc_eqdec [projection, in Minuska.spec]
Effect0 [definition, in Minuska.spec]
Effect0_evaluate [definition, in Minuska.spec]
Effect0_evaluate' [definition, in Minuska.spec]
Effect0_evaluate_extensive [lemma, in Minuska.properties]
Effect0_evaluate_strip [lemma, in Minuska.properties]
Effect0_evaluate'_strip_1 [lemma, in Minuska.properties]
Effect0_evaluate'_vars_of [lemma, in Minuska.properties]
Effect0_evaluate'_notin_remembered_2' [lemma, in Minuska.properties]
Effect0_evaluate'_notin_remembered_2 [lemma, in Minuska.properties]
Effect0_evaluate'_notin_remembered_1 [lemma, in Minuska.properties]
Effect0_evaluate'_frame [lemma, in Minuska.properties]
Effect0' [definition, in Minuska.spec]
elem_of_next [lemma, in Minuska.prelude]
elem_of_list_fmap_T_1 [lemma, in Minuska.prelude]
elem_of_fresh_var_seq [lemma, in Minuska.substitution_parseq_conv]
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]
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.unification_interface]
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_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]
example_models [library]
ExprAndBoV [record, in Minuska.notations]
Expression2 [definition, 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_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]
Expression2' [inductive, in Minuska.spec]
Expression2'_ind [definition, in Minuska.spec]
ExtendedBM [definition, in Minuska.hilang]
ExtendedSymbols [inductive, in Minuska.hilang]
ExtendedSymbols_countable [instance, in Minuska.hilang]
ExtendedSymbols_eqdec [instance, in Minuska.hilang]
ExtendedSymbols_sind [definition, in Minuska.hilang]
ExtendedSymbols_rec [definition, in Minuska.hilang]
ExtendedSymbols_ind [definition, in Minuska.hilang]
ExtendedSymbols_rect [definition, in Minuska.hilang]
extend_term [definition, in Minuska.hilang]
extensions [library]
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_attr [constructor, in Minuska.spec]
e_query [constructor, in Minuska.spec]
e_fun [constructor, in Minuska.spec]
e_Variabl [constructor, in Minuska.spec]
e_ground [constructor, in Minuska.spec]
F
FalseState [definition, in Minuska.symex]fewer_arrows_lower_degree [lemma, in Minuska.textbook_unification_alg]
filter_fmap [lemma, in Minuska.prelude]
flat_map_lookup_Some [lemma, in Minuska.prelude]
fmapFresher [definition, in Minuska.fresher]
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]
fold_left_BasicEffect0_evaluate_None [lemma, in Minuska.properties]
forallbin [definition, in Minuska.specb]
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]
fresher [library]
FresherM [definition, in Minuska.fresher]
FresherR [record, in Minuska.fresher]
fresher_avoid [projection, in Minuska.fresher]
freshFresher [definition, in Minuska.fresher]
fresh_nth_iff [lemma, in Minuska.substitution_parseq_conv]
fresh_var_seq_mono [lemma, in Minuska.substitution_parseq_conv]
fresh_nth [definition, in Minuska.substitution_parseq_conv]
fresh_var_seq [definition, in Minuska.substitution_parseq_conv]
from_to_tree [lemma, in Minuska.builtin.klike]
frontend [library]
fst_make_serial1 [lemma, in Minuska.substitution_parseq_conv]
FS_EDC [definition, in Minuska.builtin.klike]
FS_EDC [definition, in Minuska.builtin.empty]
FunSymbol [projection, in Minuska.spec]
FunSymbol_morph_inj [projection, in Minuska.signature_morphism]
FunSymbol_morph [projection, in Minuska.signature_morphism]
FunSymbol_edc [projection, in Minuska.spec]
FunSymbol_fin [instance, in Minuska.builtin.klike]
FunSymbol_eqDec [instance, in Minuska.builtin.klike]
G
genBuiltin [definition, in Minuska.quickchick_setup]genBuiltinOrVar [definition, in Minuska.quickchick_setup]
genExprSized [definition, in Minuska.quickchick_setup]
genFunction [definition, in Minuska.quickchick_setup]
genPatternSized [definition, in Minuska.quickchick_setup]
genSubstitutionSized [definition, in Minuska.playground]
genSymbol [definition, in Minuska.quickchick_setup]
genTermOverExprSized [definition, in Minuska.quickchick_setup]
genTermSized [definition, in Minuska.quickchick_setup]
genTermSized' [definition, in Minuska.quickchick_setup]
genValuationSized [definition, in Minuska.quickchick_setup]
genVariable [definition, in Minuska.quickchick_setup]
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]
H
hd [projection, in Minuska.spec]heating_rule_seq [definition, in Minuska.frontend]
helper [definition, in Minuska.lowlang]
helper_lemma_2 [lemma, in Minuska.textbook_unification]
helper_lemma [lemma, in Minuska.substitution_parallel_properties]
helper_lemma_3 [lemma, in Minuska.substitution_sequential_properties]
helper_lemma_1 [lemma, in Minuska.substitution_sequential_properties]
helper_lemma' [lemma, in Minuska.substitution_parseq_conv]
helper_filter_2 [lemma, in Minuska.properties]
helper_filter [lemma, in Minuska.properties]
helper'' [definition, in Minuska.lowlang]
HiddenAlgebra [record, in Minuska.spec]
HiddenValue [projection, in Minuska.spec]
HiddenValue_morph_inj [projection, in Minuska.signature_morphism]
HiddenValue_morph [projection, in Minuska.signature_morphism]
HiddenValue_edc [projection, in Minuska.spec]
hidden_algebra [projection, in Minuska.spec]
hidden_init [projection, in Minuska.spec]
hidden_predicate_interpretation [projection, in Minuska.spec]
hidden_unit [library]
hilang [library]
HPredSymbol [projection, in Minuska.spec]
HPredSymbol_morph_inj [projection, in Minuska.signature_morphism]
HPredSymbol_morph [projection, in Minuska.signature_morphism]
HPredSymbol_edc [projection, in Minuska.spec]
hps_edc [definition, in Minuska.hidden.hidden_unit]
hv_edc [definition, in Minuska.hidden.hidden_unit]
h_in_l_impl_length_filter_l_gt_1 [lemma, in Minuska.prelude]
I
idren [definition, in Minuska.substitution_parseq_conv]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 [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.prelude]
Injection [record, in Minuska.prelude]
inject_inj [projection, in Minuska.prelude]
inj_id [definition, in Minuska.prelude]
inj_compose [definition, in Minuska.prelude]
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_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_va [definition, in Minuska.builtin.int_model]
int_relaxed_va [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_signature [library]
int_model [library]
inverse_of_renaming_is_normal [lemma, in Minuska.substitution_parseq_conv]
invisible_label [constructor, in Minuska.default_everything]
in_sub_impl_not_in_dom_rlift_inverse_renaming [lemma, in Minuska.substitution_parseq_conv]
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_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]
is_unifier_of [definition, in Minuska.unification_interface]
K
klike [library]KlikeBuiltinValue [definition, in Minuska.builtin.klike]
KlikeBuiltinValue0 [inductive, in Minuska.builtin.klike]
KlikeBuiltinValue0_sind [definition, in Minuska.builtin.klike]
KlikeBuiltinValue0_rec [definition, in Minuska.builtin.klike]
KlikeBuiltinValue0_ind [definition, in Minuska.builtin.klike]
KlikeBuiltinValue0_rect [definition, in Minuska.builtin.klike]
KlikeFunSymbol [inductive, in Minuska.builtin.klike]
KlikeFunSymbol_sind [definition, in Minuska.builtin.klike]
KlikeFunSymbol_rec [definition, in Minuska.builtin.klike]
KlikeFunSymbol_ind [definition, in Minuska.builtin.klike]
KlikeFunSymbol_rect [definition, in Minuska.builtin.klike]
KlikePredSymbol [inductive, in Minuska.builtin.klike]
KlikePredSymbol_sind [definition, in Minuska.builtin.klike]
KlikePredSymbol_rec [definition, in Minuska.builtin.klike]
KlikePredSymbol_ind [definition, in Minuska.builtin.klike]
KlikePredSymbol_rect [definition, in Minuska.builtin.klike]
klike_predicate_interp [definition, in Minuska.builtin.klike]
klike_function_interp [definition, in Minuska.builtin.klike]
L
Label [inductive, in Minuska.default_everything]Label_eqDec [instance, in Minuska.default_everything]
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]
length_fresh_var_seq [lemma, in Minuska.substitution_parseq_conv]
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_to_set_reverse_var [lemma, in Minuska.substitution_parseq_conv]
list_filter_comm [lemma, in Minuska.substitution_parseq_conv]
list_collect_Expression2_evaluate_strip [lemma, in Minuska.properties]
list_collect_Expression2_evaluate_extensive_Some [lemma, in Minuska.properties]
list_collect_e [definition, in Minuska.frontend]
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_wrapper [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]
lookup_of_zip_both_2 [lemma, in Minuska.prelude]
lookup_of_zip_both [lemma, in Minuska.prelude]
lowlang [library]
ls_to_bor_dec [instance, in Minuska.martelli_montanari]
M
make_serial1_correct [lemma, in Minuska.substitution_parseq_conv]make_serial1 [definition, in Minuska.substitution_parseq_conv]
make_parallel_map_to_list [lemma, in Minuska.substitution_parseq_conv]
make_parallel0_map_to_list [lemma, in Minuska.substitution_parseq_conv]
make_parallel_correct [lemma, in Minuska.substitution_parseq_conv]
make_parallel_perm [lemma, in Minuska.substitution_parseq_conv]
make_parallel_app [lemma, in Minuska.substitution_parseq_conv]
make_parallel_normal [lemma, in Minuska.substitution_parseq_conv]
make_parallel [definition, in Minuska.substitution_parseq_conv]
make_parallel0_compose [lemma, in Minuska.substitution_parseq_conv]
make_parallel0_normal [lemma, in Minuska.substitution_parseq_conv]
make_parallel0 [definition, in Minuska.substitution_parseq_conv]
make_serial [definition, in Minuska.substitution_parseq_conv]
make_serial0 [definition, in Minuska.substitution_parseq_conv]
map_uglify'_inj [lemma, in Minuska.lowlang]
map_lookup_Some [lemma, in Minuska.prelude]
map_to_list_precompose [lemma, in Minuska.substitution_parseq_conv]
map_img_subp_compose [lemma, in Minuska.substitution_parseq_conv]
map_to_list_union [lemma, in Minuska.substitution_parseq_conv]
map_disjoint_compose_inverse [lemma, in Minuska.substitution_parseq_conv]
map_img_renaming_for_codom [lemma, in Minuska.substitution_parseq_conv]
map_img_renaming_for_dom [lemma, in Minuska.substitution_parseq_conv]
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]
method_interpretation [projection, in Minuska.spec]
MethSymbol [projection, in Minuska.spec]
MethSymbol_morph_inj [projection, in Minuska.signature_morphism]
MethSymbol_morph [projection, in Minuska.signature_morphism]
MethSymbol_edc [projection, in Minuska.spec]
mgu_res [definition, in Minuska.martelli_montanari_tests]
minuska [library]
mkSwitchCaseList [constructor, in Minuska.dt]
model_algebra [library]
model_functor [library]
ms_edc [definition, in Minuska.hidden.hidden_unit]
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]
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_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]
NoDup_reverse [lemma, in Minuska.substitution_parseq_conv]
NoDup_fresh_var_seq [lemma, in Minuska.substitution_parseq_conv]
NondetValue [projection, in Minuska.spec]
NondetValue_morph_inj [projection, in Minuska.signature_morphism]
NondetValue_morph [projection, in Minuska.signature_morphism]
NondetValue_edc [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
ocaml_interface [library]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
pair_swap_zip [lemma, in Minuska.substitution_parseq_conv]pair_swap_perm [instance, in Minuska.substitution_parseq_conv]
pair_swap [definition, in Minuska.substitution_parseq_conv]
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_TermSymbol_interp [projection, in Minuska.spec]
playground [library]
poly_interpreter_ext [definition, in Minuska.default_everything]
poly_interpreter [definition, in Minuska.default_everything]
PredSymbol [projection, in Minuska.spec]
PredSymbol_morph_inj [projection, in Minuska.signature_morphism]
PredSymbol_morph [projection, in Minuska.signature_morphism]
PredSymbol_edc [projection, in Minuska.spec]
PredSymbol_fin [instance, in Minuska.builtin.klike]
PredSymbol_eqDec [instance, in Minuska.builtin.klike]
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_TermSymbol [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]
properties [library]
PS_EDC [definition, in Minuska.builtin.klike]
PS_EDC [definition, in Minuska.builtin.empty]
pt_app_ao [constructor, in Minuska.lowlang]
pt_app_operand [constructor, in Minuska.lowlang]
pt_operator [constructor, in Minuska.lowlang]
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_edc [definition, in Minuska.pi.trivial]qs_program [constructor, in Minuska.pi.trivial]
QuerySymbol [projection, in Minuska.spec]
QuerySymbol_morph_inj [projection, in Minuska.signature_morphism]
QuerySymbol_morph [projection, in Minuska.signature_morphism]
QuerySymbol_edc [projection, in Minuska.spec]
quickchick_setup [library]
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]
RelaxedValueAlgebra [record, in Minuska.model_algebra]
remembered_vars_of_effect [definition, in Minuska.properties]
renaming_for_contra [lemma, in Minuska.substitution_parseq_conv]
renaming_for_avoid [lemma, in Minuska.substitution_parseq_conv]
renaming_is_normal [lemma, in Minuska.substitution_parseq_conv]
renaming_for_ok [lemma, in Minuska.substitution_parseq_conv]
renaming_for [definition, in Minuska.substitution_parseq_conv]
renaming_ok_nodup [lemma, in Minuska.substitution_parseq_conv]
renaming_ok_insert_inv [lemma, in Minuska.substitution_parseq_conv]
renaming_ok_empty [lemma, in Minuska.substitution_parseq_conv]
renaming_ok [definition, in Minuska.substitution_parseq_conv]
replace_and_collect [definition, in Minuska.symex]
replace_and_collect1 [definition, in Minuska.symex]
replace_and_collect0 [definition, in Minuska.symex]
RestrictP [definition, in Minuska.substitution_parallel]
restrictp_decision [instance, in Minuska.substitution_parallel]
restrict_equiv_1 [lemma, in Minuska.substitution_parseq_conv]
restrict_id [lemma, in Minuska.substitution_parseq_conv]
restrict_equiv_2 [lemma, in Minuska.substitution_parseq_conv]
restrict_filter [lemma, in Minuska.substitution_parseq_conv]
restrict_more [lemma, in Minuska.substitution_parseq_conv]
REST_SEQ [definition, in Minuska.frontend]
returnFresher [definition, in Minuska.fresher]
ReversibleInjection [record, in Minuska.prelude]
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 [definition, in Minuska.spec]
RewritingRule2_eqdec [instance, in Minuska.basic_properties]
RewritingRule2_wf [definition, in Minuska.spec_interpreter]
RewritingRule2' [record, in Minuska.spec]
RewritingRule2'_wf [definition, in Minuska.spec_interpreter]
RewritingTheory2 [definition, in Minuska.spec]
RewritingTheory2_wf [definition, in Minuska.spec_interpreter]
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.prelude]
rinj_inl [definition, in Minuska.prelude]
rinj_id [definition, in Minuska.prelude]
rinj_compose [definition, in Minuska.prelude]
ri_reverse_pf [projection, in Minuska.prelude]
ri_reverse [projection, in Minuska.prelude]
ri_injection [projection, in Minuska.prelude]
rlift [definition, in Minuska.substitution_parseq_conv]
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]
rva_over [projection, in Minuska.model_algebra]
r_label [projection, in Minuska.spec]
r_eff [projection, in Minuska.spec]
r_scs [projection, in Minuska.spec]
r_to [projection, in Minuska.spec]
r_from [projection, in Minuska.spec]
r_inverse_inverse [lemma, in Minuska.substitution_parseq_conv]
r_inverse_ok [lemma, in Minuska.substitution_parseq_conv]
r_inverse_insert [lemma, in Minuska.substitution_parseq_conv]
r_inverse [definition, in Minuska.substitution_parseq_conv]
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
SA [definition, in Minuska.playground]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]
Satisfies_Valuation2_TermOverBuiltinValue_BuiltinOrVar_reflect [lemma, in Minuska.specb]
Satisfies_Valuation2_TermOverBuiltinValue_BuiltinOrVar_b [definition, in Minuska.specb]
sat2B [definition, in Minuska.spec]
sat2Bb [definition, in Minuska.specb]
sat2B_refl [lemma, in Minuska.specb]
sat2E [definition, in Minuska.spec]
sat2Eb [definition, in Minuska.specb]
sat2E_refl [lemma, in Minuska.specb]
SB [definition, in Minuska.playground]
sbov_to_e_bov [definition, in Minuska.frontend]
sbov_var [constructor, in Minuska.frontend]
sbov_builtin [constructor, in Minuska.frontend]
SC [definition, in Minuska.playground]
sce_or [constructor, in Minuska.symex]
sce_and [constructor, in Minuska.symex]
sce_hatom [constructor, in Minuska.symex]
sce_natom [constructor, in Minuska.symex]
sce_atom [constructor, in Minuska.symex]
sce_eq [constructor, in Minuska.symex]
sce_false [constructor, in Minuska.symex]
sce_true [constructor, in Minuska.symex]
ScList [definition, in Minuska.symex]
sclist_to_sceq [definition, in Minuska.symex]
sc_or [constructor, in Minuska.spec]
sc_and [constructor, in Minuska.spec]
sc_hpred [constructor, in Minuska.spec]
sc_npred [constructor, in Minuska.spec]
sc_pred [constructor, in Minuska.spec]
sc_false [constructor, in Minuska.spec]
sc_true [constructor, in Minuska.spec]
sc_satisfies_insensitive [lemma, in Minuska.properties]
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.TermSymbol [variable, in Minuska.builtin.klike]
sec._sc [variable, in Minuska.builtin.klike]
sec._se [variable, in Minuska.builtin.klike]
sec2 [section, in Minuska.builtin.klike]
sec2.NondetValue [variable, in Minuska.builtin.klike]
sec2.TermSymbol [variable, in Minuska.builtin.klike]
sec2._ET [variable, in Minuska.builtin.klike]
set_filter_pred_impl [lemma, in Minuska.prelude]
se_to_Expression [definition, in Minuska.frontend]
se_apply [constructor, in Minuska.frontend]
se_variable [constructor, in Minuska.frontend]
se_ground [constructor, in Minuska.frontend]
showAttribute [instance, in Minuska.quickchick_setup]
showBuiltinOrVar [instance, in Minuska.quickchick_setup]
showExpr [instance, in Minuska.quickchick_setup]
showFun [instance, in Minuska.quickchick_setup]
showQery [instance, in Minuska.quickchick_setup]
showSubP [instance, in Minuska.quickchick_setup]
showSubP_ [definition, in Minuska.quickchick_setup]
showTerm [instance, in Minuska.quickchick_setup]
showVal [instance, in Minuska.quickchick_setup]
showVal_ [definition, in Minuska.quickchick_setup]
show_e [definition, in Minuska.quickchick_setup]
show_to [definition, in Minuska.quickchick_setup]
show_TermSymbol [instance, in Minuska.quickchick_setup]
show_builtin [instance, in Minuska.quickchick_setup]
SideCondition [definition, in Minuska.spec]
SideConditionEq [inductive, in Minuska.symex]
SideConditionEq_evaluate_asIfWithEq [lemma, in Minuska.symex]
SideConditionEq_evaluate [definition, in Minuska.symex]
SideConditionEq_sind [definition, in Minuska.symex]
SideConditionEq_rec [definition, in Minuska.symex]
SideConditionEq_ind [definition, in Minuska.symex]
SideConditionEq_rect [definition, in Minuska.symex]
SideCondition_subst [definition, in Minuska.basic_properties]
SideCondition_eqdec [instance, in Minuska.basic_properties]
SideCondition_evaluate [definition, in Minuska.spec]
SideCondition_satisfies_strip [lemma, in Minuska.properties]
SideCondition_satisfies_extensive [lemma, in Minuska.properties]
SideCondition' [inductive, 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]
Signature [record, in Minuska.dt]
signature_morphism [library]
simpleStepByRule [definition, in Minuska.symex]
SimpleSymbolicState [record, in Minuska.symex]
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_of_var_in_val [definition, in Minuska.properties]
size_subst_2 [lemma, in Minuska.termoverbov_subst_properties]
size_subst_1 [lemma, in Minuska.termoverbov_subst_properties]
si_method [constructor, in Minuska.ocaml_interface]
si_query [constructor, in Minuska.ocaml_interface]
si_attribute [constructor, in Minuska.ocaml_interface]
si_function [constructor, in Minuska.ocaml_interface]
si_hidden_predicate [constructor, in Minuska.ocaml_interface]
si_predicate [constructor, in Minuska.ocaml_interface]
si_none [constructor, in Minuska.ocaml_interface]
si2m [definition, in Minuska.ocaml_interface]
si2p [definition, in Minuska.ocaml_interface]
si2qfa [definition, in Minuska.ocaml_interface]
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]
small_model_of_relaxed [definition, in Minuska.model_algebra]
snd_make_serial1 [lemma, in Minuska.substitution_parseq_conv]
spec [library]
specb [library]
spec_interpreter [library]
spec_syntax [library]
srenaming_ok [definition, in Minuska.substitution_parseq_conv]
srlift [definition, in Minuska.substitution_parseq_conv]
srlift_map_to_list [lemma, in Minuska.substitution_parseq_conv]
srr_to_rr [definition, in Minuska.frontend]
sr_inverse [definition, in Minuska.substitution_parseq_conv]
sr_label [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_npred [constructor, in Minuska.frontend]
ssc_pred [constructor, in Minuska.frontend]
ssc_false [constructor, in Minuska.frontend]
ssc_true [constructor, in Minuska.frontend]
sss_sc [projection, in Minuska.symex]
sss_term [projection, in Minuska.symex]
sSymbolicTerm_to_ExprTerm [definition, in Minuska.frontend]
State [record, in Minuska.frontend]
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]
string_infinite [instance, in Minuska.prelude]
string_countable [instance, in Minuska.prelude]
string_eq_dec [instance, in Minuska.prelude]
string_countable0 [definition, in Minuska.prelude]
string_eq_dec0 [definition, in Minuska.prelude]
string2m [projection, in Minuska.frontend]
string2p [projection, in Minuska.frontend]
string2qfa [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]
SubP [definition, in Minuska.substitution_parallel]
subp_eqdec [instance, in Minuska.playground]
subp_compose_assoc [lemma, in Minuska.substitution_parallel_properties]
subp_compose_correct [lemma, in Minuska.substitution_parallel_properties]
subp_union_is_compose__sometimes_1 [lemma, in Minuska.substitution_parallel_properties]
subp_app_union [lemma, in Minuska.substitution_parallel_properties]
subp_compose_helper_1 [lemma, in Minuska.substitution_parallel_properties]
subp_app_union_comm [lemma, in Minuska.substitution_parallel_properties]
subp_app_singleton [lemma, in Minuska.substitution_parallel_properties]
subp_compose_id [lemma, in Minuska.substitution_parallel_properties]
subp_id_compose [lemma, in Minuska.substitution_parallel_properties]
subp_normalize_normal [lemma, in Minuska.substitution_parallel_properties]
subp_normalize_normalize [lemma, in Minuska.substitution_parallel_properties]
subp_app_insert0 [lemma, in Minuska.substitution_parallel_properties]
subp_app_empty' [lemma, in Minuska.substitution_parallel_properties]
subp_app_almost_closed [lemma, in Minuska.substitution_parallel_properties]
subp_app_closed [lemma, in Minuska.substitution_parallel_properties]
subp_app_empty [lemma, in Minuska.substitution_parallel_properties]
subp_precompose [definition, in Minuska.substitution_parallel]
subp_restrict [definition, in Minuska.substitution_parallel]
subp_id [definition, in Minuska.substitution_parallel]
subp_compose [definition, in Minuska.substitution_parallel]
subp_is_normal [definition, in Minuska.substitution_parallel]
subp_normalize [definition, in Minuska.substitution_parallel]
subp_codom [definition, in Minuska.substitution_parallel]
subp_dom [definition, in Minuska.substitution_parallel]
subp_app [definition, in Minuska.substitution_parallel]
subp_app_restrict_eq [lemma, in Minuska.substitution_parseq_conv]
subp_app_compose_precompose [lemma, in Minuska.substitution_parseq_conv]
subp_precomposes [definition, in Minuska.substitution_parseq_conv]
subp_app_insert [lemma, in Minuska.substitution_parseq_conv]
subp_codom_inverse [lemma, in Minuska.substitution_parseq_conv]
subp_dom_inverse [lemma, in Minuska.substitution_parseq_conv]
subp_codom_make_parallel0 [lemma, in Minuska.substitution_parseq_conv]
subp_codom_renaming_for_disjoint_dom_m [lemma, in Minuska.substitution_parseq_conv]
subp_codom_insert [lemma, in Minuska.substitution_parseq_conv]
subp_codom_subp_compose_2 [lemma, in Minuska.substitution_parseq_conv]
subp_codom_subp_compose [lemma, in Minuska.substitution_parseq_conv]
subp_is_normal_normalize [lemma, in Minuska.substitution_parseq_conv]
subp_compose_empty_l [lemma, in Minuska.substitution_parseq_conv]
subp_compose_com [lemma, in Minuska.substitution_parseq_conv]
subp_compose_empty_r [lemma, in Minuska.substitution_parseq_conv]
subp_app_insert_2 [lemma, in Minuska.substitution_parseq_conv]
subp_restrict_id_2 [lemma, in Minuska.substitution_parseq_conv]
subp_app_restrict [lemma, in Minuska.substitution_parseq_conv]
subp_is_normal_spec [lemma, in Minuska.substitution_parseq_conv]
subp_is_normal_restrict [lemma, in Minuska.substitution_parseq_conv]
subp_restrict_compose [lemma, in Minuska.substitution_parseq_conv]
SubS [definition, in Minuska.substitution_sequential]
Subseteq_Valuation2 [instance, in Minuska.spec]
substitution_sequential_properties [library]
substitution_parallel [library]
substitution_sequential [library]
substitution_parallel_properties [library]
substitution_parseq_conv [library]
subst_preserves_subterm [lemma, in Minuska.textbook_unification]
subst_id [lemma, in Minuska.termoverbov_subst_properties]
subst_notin2 [lemma, in Minuska.termoverbov_subst_properties]
subst_notin [lemma, in Minuska.termoverbov_subst_properties]
subs_app_preserves_subterm [lemma, in Minuska.textbook_unification]
subs_app_unbound_var_2 [lemma, in Minuska.textbook_unification]
subs_app_unbound_var_1 [lemma, in Minuska.textbook_unification]
subs_app_untouched [lemma, in Minuska.substitution_sequential_properties]
subs_app_nodup_2 [lemma, in Minuska.substitution_sequential_properties]
subs_app_nodup_1 [lemma, in Minuska.substitution_sequential_properties]
subs_no_twice_approx [definition, in Minuska.substitution_sequential_properties]
subs_app_term [lemma, in Minuska.substitution_sequential_properties]
subs_app_builtin [lemma, in Minuska.substitution_sequential_properties]
subs_app_cons [lemma, in Minuska.substitution_sequential_properties]
subs_app_app [lemma, in Minuska.substitution_sequential_properties]
subs_is_normal_make_serial1 [lemma, in Minuska.substitution_parseq_conv]
subs_app_nodup_3 [lemma, in Minuska.substitution_parseq_conv]
subs_app_renaming_inverse_0 [lemma, in Minuska.substitution_parseq_conv]
subs_app_app' [lemma, in Minuska.substitution_parseq_conv]
subs_precomposes [definition, in Minuska.substitution_parseq_conv]
subs_precomposep [definition, in Minuska.substitution_parseq_conv]
subs_is_normal [definition, in Minuska.substitution_parseq_conv]
subs_app [definition, in Minuska.substitution_sequential]
subtmm_closed [definition, in Minuska.substitution_parallel_properties]
subt_codom [definition, in Minuska.substitution_sequential_properties]
subt_dom [definition, in Minuska.substitution_sequential_properties]
subt_codom_renaming [lemma, in Minuska.substitution_parseq_conv]
subt_codom_map_to_list [lemma, in Minuska.substitution_parseq_conv]
subt_closed [definition, in Minuska.substitution_sequential]
sub_decreases_degree [lemma, in Minuska.textbook_unification_alg]
sub_notin [lemma, in Minuska.textbook_unification_alg]
sub_ext_cons [lemma, in Minuska.textbook_unification]
sub_ext_nil [lemma, in Minuska.textbook_unification]
sub_ext [definition, 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]
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]
SymbolicState [definition, in Minuska.symex]
SymbolicTerm_to_ExprTerm [definition, in Minuska.frontend]
SymbolInfo [inductive, in Minuska.ocaml_interface]
symex [library]
symex_spec [library]
sym_heatedAt [constructor, in Minuska.hilang]
sym_hole [constructor, in Minuska.hilang]
sym_top [constructor, in Minuska.hilang]
sym_emptyCseq [constructor, in Minuska.hilang]
sym_cseq [constructor, in Minuska.hilang]
sym_original [constructor, in Minuska.hilang]
T
T [definition, in Minuska.martelli_montanari]take_any [definition, in Minuska.martelli_montanari]
TermOverBoV_to_TermOverExpr2 [definition, in Minuska.basic_properties]
TermOverBoV_subst_cancel [lemma, in Minuska.substitution_parseq_conv]
TermOverBoV_eval [definition, in Minuska.properties]
TermOverBoV_satisfies_strip [lemma, in Minuska.properties]
TermOverBoV_satisfies_extensive [lemma, in Minuska.properties]
TermOverBoV_subst_once_size [lemma, in Minuska.termoverbov_subst_properties]
TermOverBoV_subst [definition, in Minuska.termoverbov_subst]
TermOverBoV_subst_expr2 [definition, in Minuska.termoverbov_subst]
TermOverBoV_subst_gen [definition, in Minuska.termoverbov_subst]
termoverbov_subst_properties [library]
termoverbov_subst [library]
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_size [definition, in Minuska.spec]
TermOver_collect [definition, in Minuska.properties]
TermOver' [inductive, in Minuska.spec]
TermOver'_map [definition, in Minuska.spec]
TermOver'_ind [definition, in Minuska.spec]
TermOver'_join [definition, in Minuska.properties]
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'_e_map [definition, in Minuska.frontend]
TermOver'_option_map__Expression2_evaluate__extensive [lemma, in Minuska.naive_interpreter]
TermSymbol [projection, in Minuska.spec]
TermSymbol_morph_inj [projection, in Minuska.signature_morphism]
TermSymbol_morph [projection, in Minuska.signature_morphism]
TermSymbol_edc [projection, in Minuska.spec]
Term_TermSymbol_fmap [instance, in Minuska.lowlang]
term_operand [constructor, in Minuska.lowlang]
term_preterm [constructor, in Minuska.lowlang]
term_has_same_TermSymbol [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]
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]
TS_EDC [definition, in Minuska.builtin.klike]
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_Variabl_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]
unit_hidden_model [definition, in Minuska.hidden.hidden_unit]
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_delete_union [lemma, in Minuska.properties]valuation_restrict_vars_of_self [lemma, in Minuska.naive_interpreter]
valuation_merge [library]
Valuation' [definition, in Minuska.spec]
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.properties]
Valuation2_restrict [definition, in Minuska.properties]
Value [inductive, in Minuska.dt]
ValueAlgebra [record, in Minuska.spec]
ValueVector [definition, in Minuska.dt]
value_algebra [projection, in Minuska.spec]
Value_ind [definition, in Minuska.dt]
Variabl [projection, in Minuska.spec]
Variable_inf [projection, in Minuska.spec]
Variabl_morph_inj [projection, in Minuska.signature_morphism]
Variabl_morph [projection, in Minuska.signature_morphism]
Variabl_edc [projection, in Minuska.spec]
VarsOf [record, in Minuska.spec]
VarsOf_Term' [instance, in Minuska.lowlang]
VarsOf_aosB [instance, in Minuska.lowlang]
VarsOf_sce [instance, in Minuska.symex]
VarsOf_Valuation2 [instance, in Minuska.spec]
VarsOf_Valuation2_ [instance, in Minuska.spec]
VarsOf_BoV [instance, in Minuska.spec]
VarsOf_Effect0 [instance, in Minuska.spec]
VarsOf_sc [instance, in Minuska.spec]
VarsOf_Expression2 [instance, in Minuska.spec]
VarsOf_list_something [instance, in Minuska.spec]
VarsOf_TermOver [instance, in Minuska.spec]
VarsOf_builtin [instance, in Minuska.spec]
VarsOf_TermSymbol [instance, in Minuska.spec]
vars_of_sub [definition, in Minuska.textbook_unification]
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_sce [definition, in Minuska.symex]
vars_of_BoV [definition, in Minuska.spec]
vars_of_Effect0' [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_subs_app [lemma, in Minuska.substitution_sequential_properties]
vars_of_sat_tobov [lemma, in Minuska.interpreter_results]
vars_of_subp_app [lemma, in Minuska.substitution_parseq_conv]
vars_of_Variabl [lemma, in Minuska.properties]
vars_of_builtin [lemma, in Minuska.properties]
vars_of_t_over_expr [lemma, in Minuska.properties]
vars_of_to_l2r_of_tob [lemma, in Minuska.properties]
vars_of_to_l2r_subst [lemma, in Minuska.termoverbov_subst_properties]
vars_of_TermOverBoV_subst [lemma, in Minuska.termoverbov_subst_properties]
vars_of__TermOverBoV_subst__varless [lemma, in Minuska.termoverbov_subst_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]
va_reduction [definition, in Minuska.model_algebra]
vector_of_wildcards_dec [instance, in Minuska.dt]
vector_of_wildcards [definition, in Minuska.dt]
void_value_algebra [definition, in Minuska.builtin.empty]
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]
wsm.default_label [variable, in Minuska.frontend]
wsm.Label [variable, in Minuska.frontend]
Z
zipWith [definition, in Minuska.martelli_montanari]other
_ ~up _ [notation, in Minuska.martelli_montanari]Σ [instance, in Minuska.quickchick_setup]
Σ1 [definition, in Minuska.example_models]
β [definition, in Minuska.builtin.klike]
Notation Index
other
_ ~up _ [in Minuska.martelli_montanari]Module Index
I
Implementation [in Minuska.symex]Variable Index
C
custom_induction_principle_2.Σ [in Minuska.basic_properties]custom_induction_principle_2._edA [in Minuska.basic_properties]
custom_induction_principle_2.A [in Minuska.basic_properties]
custom_induction_principle_2._edB [in Minuska.basic_properties]
custom_induction_principle_2.B [in Minuska.basic_properties]
custom_induction_principle_2.Σ [in Minuska.basic_properties]
custom_induction_principle.preserved_by_attribute [in Minuska.spec]
custom_induction_principle.preserved_by_query [in Minuska.spec]
custom_induction_principle.preserved_by_fun [in Minuska.spec]
custom_induction_principle.true_for_var [in Minuska.spec]
custom_induction_principle.true_for_ground [in Minuska.spec]
custom_induction_principle.P [in Minuska.spec]
custom_induction_principle.As [in Minuska.spec]
custom_induction_principle.Qs [in Minuska.spec]
custom_induction_principle.Fs [in Minuska.spec]
custom_induction_principle.Ts [in Minuska.spec]
custom_induction_principle.Va [in Minuska.spec]
custom_induction_principle.Bv [in Minuska.spec]
custom_induction_principle.preserved_by_term [in Minuska.spec]
custom_induction_principle.true_for_over [in Minuska.spec]
custom_induction_principle.P [in Minuska.spec]
custom_induction_principle.A [in Minuska.spec]
custom_induction_principle.T [in Minuska.spec]
custom_induction_principle.preserved_by_cval [in Minuska.dt]
custom_induction_principle.P [in Minuska.dt]
custom_induction_principle.Σ [in Minuska.dt]
custom_induction_principle.preserved_by_cpat [in Minuska.dt]
custom_induction_principle.true_for_wildcard [in Minuska.dt]
custom_induction_principle.P [in Minuska.dt]
custom_induction_principle.Σ [in Minuska.dt]
S
sec.TermSymbol [in Minuska.builtin.klike]sec._sc [in Minuska.builtin.klike]
sec._se [in Minuska.builtin.klike]
sec2.NondetValue [in Minuska.builtin.klike]
sec2.TermSymbol [in Minuska.builtin.klike]
sec2._ET [in Minuska.builtin.klike]
W
wsm.default_label [in Minuska.frontend]wsm.Label [in Minuska.frontend]
Library Index
B
basic_propertiesbool_signature
bool_model
builtins
BuiltinValue
C
conservative_mergeD
default_everythingdt
E
emptyexample_list_int_model
example_models
extensions
F
fresherfrontend
H
hidden_unithilang
I
information_flow_functorinterpreter_results
interp_loop
int_signature
int_model
K
klikeL
list_modellist_signature
lowlang
M
martelli_montanari_testsmartelli_montanari
minuska
model_algebra
model_functor
N
naive_interpreternat_builtin
notations
O
ocaml_interfaceP
playgroundprelude
properties
Q
quickchick_setupS
signature_morphismspec
specb
spec_interpreter
spec_syntax
substitution_sequential_properties
substitution_parallel
substitution_sequential
substitution_parallel_properties
substitution_parseq_conv
symex
symex_spec
T
termoverbov_subst_propertiestermoverbov_subst
textbook_unification
textbook_unification_alg
trivial
U
unification_interfaceV
valuation_mergeLemma Index
A
another_helper_lemma' [in Minuska.substitution_parseq_conv]another_helper_lemma [in Minuska.substitution_parseq_conv]
B
BasicEffect0_evaluate'_frame [in Minuska.properties]BasicEffect0_evaluate'_extensive [in Minuska.properties]
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]
compose_renaming_inverse_restrict [in Minuska.substitution_parseq_conv]
concrete_is_larger_than_TermSymbolic [in Minuska.properties]
contract_extend_term [in Minuska.hilang]
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]
dom_make_parallel [in Minuska.substitution_parseq_conv]
dom_make_parallel0 [in Minuska.substitution_parseq_conv]
dom_rinverse [in Minuska.substitution_parseq_conv]
dom_rlift_inverse [in Minuska.substitution_parseq_conv]
dom_renaming_for [in Minuska.substitution_parseq_conv]
dom_subp_compose_subseteq [in Minuska.substitution_parseq_conv]
double_satisfies_contradiction [in Minuska.properties]
E
Effect0_evaluate_extensive [in Minuska.properties]Effect0_evaluate_strip [in Minuska.properties]
Effect0_evaluate'_strip_1 [in Minuska.properties]
Effect0_evaluate'_vars_of [in Minuska.properties]
Effect0_evaluate'_notin_remembered_2' [in Minuska.properties]
Effect0_evaluate'_notin_remembered_2 [in Minuska.properties]
Effect0_evaluate'_notin_remembered_1 [in Minuska.properties]
Effect0_evaluate'_frame [in Minuska.properties]
elem_of_next [in Minuska.prelude]
elem_of_list_fmap_T_1 [in Minuska.prelude]
elem_of_fresh_var_seq [in Minuska.substitution_parseq_conv]
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]
fold_left_BasicEffect0_evaluate_None [in Minuska.properties]
forall_satisfies_inv [in Minuska.properties]
forall_satisfies_inv' [in Minuska.properties]
fresh_nth_iff [in Minuska.substitution_parseq_conv]
fresh_var_seq_mono [in Minuska.substitution_parseq_conv]
from_to_tree [in Minuska.builtin.klike]
fst_make_serial1 [in Minuska.substitution_parseq_conv]
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_2 [in Minuska.textbook_unification]helper_lemma [in Minuska.substitution_parallel_properties]
helper_lemma_3 [in Minuska.substitution_sequential_properties]
helper_lemma_1 [in Minuska.substitution_sequential_properties]
helper_lemma' [in Minuska.substitution_parseq_conv]
helper_filter_2 [in Minuska.properties]
helper_filter [in Minuska.properties]
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]
inverse_of_renaming_is_normal [in Minuska.substitution_parseq_conv]
in_sub_impl_not_in_dom_rlift_inverse_renaming [in Minuska.substitution_parseq_conv]
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]
length_fresh_var_seq [in Minuska.substitution_parseq_conv]
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_to_set_reverse_var [in Minuska.substitution_parseq_conv]
list_filter_comm [in Minuska.substitution_parseq_conv]
list_collect_Expression2_evaluate_strip [in Minuska.properties]
list_collect_Expression2_evaluate_extensive_Some [in Minuska.properties]
list_swap_head_involutive [in Minuska.dt]
lookup_of_zip_both_2 [in Minuska.prelude]
lookup_of_zip_both [in Minuska.prelude]
M
make_serial1_correct [in Minuska.substitution_parseq_conv]make_parallel_map_to_list [in Minuska.substitution_parseq_conv]
make_parallel0_map_to_list [in Minuska.substitution_parseq_conv]
make_parallel_correct [in Minuska.substitution_parseq_conv]
make_parallel_perm [in Minuska.substitution_parseq_conv]
make_parallel_app [in Minuska.substitution_parseq_conv]
make_parallel_normal [in Minuska.substitution_parseq_conv]
make_parallel0_compose [in Minuska.substitution_parseq_conv]
make_parallel0_normal [in Minuska.substitution_parseq_conv]
map_uglify'_inj [in Minuska.lowlang]
map_lookup_Some [in Minuska.prelude]
map_to_list_precompose [in Minuska.substitution_parseq_conv]
map_img_subp_compose [in Minuska.substitution_parseq_conv]
map_to_list_union [in Minuska.substitution_parseq_conv]
map_disjoint_compose_inverse [in Minuska.substitution_parseq_conv]
map_img_renaming_for_codom [in Minuska.substitution_parseq_conv]
map_img_renaming_for_dom [in Minuska.substitution_parseq_conv]
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]
N
naive_interpreter_sound [in Minuska.naive_interpreter]NoDup_reverse [in Minuska.substitution_parseq_conv]
NoDup_fresh_var_seq [in Minuska.substitution_parseq_conv]
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
pair_swap_zip [in Minuska.substitution_parseq_conv]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
renaming_for_contra [in Minuska.substitution_parseq_conv]renaming_for_avoid [in Minuska.substitution_parseq_conv]
renaming_is_normal [in Minuska.substitution_parseq_conv]
renaming_for_ok [in Minuska.substitution_parseq_conv]
renaming_ok_nodup [in Minuska.substitution_parseq_conv]
renaming_ok_insert_inv [in Minuska.substitution_parseq_conv]
renaming_ok_empty [in Minuska.substitution_parseq_conv]
restrict_equiv_1 [in Minuska.substitution_parseq_conv]
restrict_id [in Minuska.substitution_parseq_conv]
restrict_equiv_2 [in Minuska.substitution_parseq_conv]
restrict_filter [in Minuska.substitution_parseq_conv]
restrict_more [in Minuska.substitution_parseq_conv]
rev_ind_T [in Minuska.prelude]
rev_list_ind_T [in Minuska.prelude]
RST_list_closure_elem_of [in Minuska.martelli_montanari]
r_inverse_inverse [in Minuska.substitution_parseq_conv]
r_inverse_ok [in Minuska.substitution_parseq_conv]
r_inverse_insert [in Minuska.substitution_parseq_conv]
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]
Satisfies_Valuation2_TermOverBuiltinValue_BuiltinOrVar_reflect [in Minuska.specb]
sat2B_refl [in Minuska.specb]
sat2E_refl [in Minuska.specb]
sc_satisfies_insensitive [in Minuska.properties]
set_filter_pred_impl [in Minuska.prelude]
SideConditionEq_evaluate_asIfWithEq [in Minuska.symex]
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.termoverbov_subst_properties]
size_subst_1 [in Minuska.termoverbov_subst_properties]
snd_make_serial1 [in Minuska.substitution_parseq_conv]
srlift_map_to_list [in Minuska.substitution_parseq_conv]
subp_compose_assoc [in Minuska.substitution_parallel_properties]
subp_compose_correct [in Minuska.substitution_parallel_properties]
subp_union_is_compose__sometimes_1 [in Minuska.substitution_parallel_properties]
subp_app_union [in Minuska.substitution_parallel_properties]
subp_compose_helper_1 [in Minuska.substitution_parallel_properties]
subp_app_union_comm [in Minuska.substitution_parallel_properties]
subp_app_singleton [in Minuska.substitution_parallel_properties]
subp_compose_id [in Minuska.substitution_parallel_properties]
subp_id_compose [in Minuska.substitution_parallel_properties]
subp_normalize_normal [in Minuska.substitution_parallel_properties]
subp_normalize_normalize [in Minuska.substitution_parallel_properties]
subp_app_insert0 [in Minuska.substitution_parallel_properties]
subp_app_empty' [in Minuska.substitution_parallel_properties]
subp_app_almost_closed [in Minuska.substitution_parallel_properties]
subp_app_closed [in Minuska.substitution_parallel_properties]
subp_app_empty [in Minuska.substitution_parallel_properties]
subp_app_restrict_eq [in Minuska.substitution_parseq_conv]
subp_app_compose_precompose [in Minuska.substitution_parseq_conv]
subp_app_insert [in Minuska.substitution_parseq_conv]
subp_codom_inverse [in Minuska.substitution_parseq_conv]
subp_dom_inverse [in Minuska.substitution_parseq_conv]
subp_codom_make_parallel0 [in Minuska.substitution_parseq_conv]
subp_codom_renaming_for_disjoint_dom_m [in Minuska.substitution_parseq_conv]
subp_codom_insert [in Minuska.substitution_parseq_conv]
subp_codom_subp_compose_2 [in Minuska.substitution_parseq_conv]
subp_codom_subp_compose [in Minuska.substitution_parseq_conv]
subp_is_normal_normalize [in Minuska.substitution_parseq_conv]
subp_compose_empty_l [in Minuska.substitution_parseq_conv]
subp_compose_com [in Minuska.substitution_parseq_conv]
subp_compose_empty_r [in Minuska.substitution_parseq_conv]
subp_app_insert_2 [in Minuska.substitution_parseq_conv]
subp_restrict_id_2 [in Minuska.substitution_parseq_conv]
subp_app_restrict [in Minuska.substitution_parseq_conv]
subp_is_normal_spec [in Minuska.substitution_parseq_conv]
subp_is_normal_restrict [in Minuska.substitution_parseq_conv]
subp_restrict_compose [in Minuska.substitution_parseq_conv]
subst_preserves_subterm [in Minuska.textbook_unification]
subst_id [in Minuska.termoverbov_subst_properties]
subst_notin2 [in Minuska.termoverbov_subst_properties]
subst_notin [in Minuska.termoverbov_subst_properties]
subs_app_preserves_subterm [in Minuska.textbook_unification]
subs_app_unbound_var_2 [in Minuska.textbook_unification]
subs_app_unbound_var_1 [in Minuska.textbook_unification]
subs_app_untouched [in Minuska.substitution_sequential_properties]
subs_app_nodup_2 [in Minuska.substitution_sequential_properties]
subs_app_nodup_1 [in Minuska.substitution_sequential_properties]
subs_app_term [in Minuska.substitution_sequential_properties]
subs_app_builtin [in Minuska.substitution_sequential_properties]
subs_app_cons [in Minuska.substitution_sequential_properties]
subs_app_app [in Minuska.substitution_sequential_properties]
subs_is_normal_make_serial1 [in Minuska.substitution_parseq_conv]
subs_app_nodup_3 [in Minuska.substitution_parseq_conv]
subs_app_renaming_inverse_0 [in Minuska.substitution_parseq_conv]
subs_app_app' [in Minuska.substitution_parseq_conv]
subt_codom_renaming [in Minuska.substitution_parseq_conv]
subt_codom_map_to_list [in Minuska.substitution_parseq_conv]
sub_decreases_degree [in Minuska.textbook_unification_alg]
sub_notin [in Minuska.textbook_unification_alg]
sub_ext_cons [in Minuska.textbook_unification]
sub_ext_nil [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_cancel [in Minuska.substitution_parseq_conv]TermOverBoV_satisfies_strip [in Minuska.properties]
TermOverBoV_satisfies_extensive [in Minuska.properties]
TermOverBoV_subst_once_size [in Minuska.termoverbov_subst_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_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_Variabl_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_delete_union [in Minuska.properties]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.properties]
vars_of_t_term [in Minuska.basic_properties]
vars_of_uglify [in Minuska.lowlang]
vars_of_uglify' [in Minuska.lowlang]
vars_of_subs_app [in Minuska.substitution_sequential_properties]
vars_of_sat_tobov [in Minuska.interpreter_results]
vars_of_subp_app [in Minuska.substitution_parseq_conv]
vars_of_Variabl [in Minuska.properties]
vars_of_builtin [in Minuska.properties]
vars_of_t_over_expr [in Minuska.properties]
vars_of_to_l2r_of_tob [in Minuska.properties]
vars_of_to_l2r_subst [in Minuska.termoverbov_subst_properties]
vars_of_TermOverBoV_subst [in Minuska.termoverbov_subst_properties]
vars_of__TermOverBoV_subst__varless [in Minuska.termoverbov_subst_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
be_remember [in Minuska.spec]be_method [in Minuska.spec]
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_Variabl [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_TermSymbols [in Minuska.builtin.klike]
b_have_same_TermSymbol [in Minuska.builtin.klike]
b_is_not_applied_TermSymbol [in Minuska.builtin.klike]
b_is_applied_TermSymbol [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]
C
cto_base [in Minuska.hilang]ctx_seq [in Minuska.hilang]
ctx_term [in Minuska.hilang]
ctx_hole [in Minuska.hilang]
D
decl_strict [in Minuska.frontend]decl_ctx [in Minuska.frontend]
decl_rule [in Minuska.frontend]
default_label [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_attr [in Minuska.spec]e_query [in Minuska.spec]
e_fun [in Minuska.spec]
e_Variabl [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_label [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]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]
sce_or [in Minuska.symex]
sce_and [in Minuska.symex]
sce_hatom [in Minuska.symex]
sce_natom [in Minuska.symex]
sce_atom [in Minuska.symex]
sce_eq [in Minuska.symex]
sce_false [in Minuska.symex]
sce_true [in Minuska.symex]
sc_or [in Minuska.spec]
sc_and [in Minuska.spec]
sc_hpred [in Minuska.spec]
sc_npred [in Minuska.spec]
sc_pred [in Minuska.spec]
sc_false [in Minuska.spec]
sc_true [in Minuska.spec]
se_apply [in Minuska.frontend]
se_variable [in Minuska.frontend]
se_ground [in Minuska.frontend]
si_method [in Minuska.ocaml_interface]
si_query [in Minuska.ocaml_interface]
si_attribute [in Minuska.ocaml_interface]
si_function [in Minuska.ocaml_interface]
si_hidden_predicate [in Minuska.ocaml_interface]
si_predicate [in Minuska.ocaml_interface]
si_none [in Minuska.ocaml_interface]
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_npred [in Minuska.frontend]
ssc_pred [in Minuska.frontend]
ssc_false [in Minuska.frontend]
ssc_true [in Minuska.frontend]
sym_heatedAt [in Minuska.hilang]
sym_hole [in Minuska.hilang]
sym_top [in Minuska.hilang]
sym_emptyCseq [in Minuska.hilang]
sym_cseq [in Minuska.hilang]
sym_original [in Minuska.hilang]
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
B
BasicEffect0' [in Minuska.spec]BoolFunSymbol [in Minuska.builtin.bool_signature]
BoolPredSymbol [in Minuska.builtin.bool_signature]
BuiltinOrVar' [in Minuska.spec]
BVLeaf [in Minuska.builtin.klike]
C
collapses_to [in Minuska.hilang]Context_ [in Minuska.hilang]
D
DecisionTree [in Minuska.dt]Declaration [in Minuska.frontend]
dt_sem_aux [in Minuska.dt]
dt_sem [in Minuska.dt]
E
Expression2' [in Minuska.spec]ExtendedSymbols [in Minuska.hilang]
I
IntFunSymbol [in Minuska.builtin.int_signature]IntPredSymbol [in Minuska.builtin.int_signature]
K
KlikeBuiltinValue0 [in Minuska.builtin.klike]KlikeFunSymbol [in Minuska.builtin.klike]
KlikePredSymbol [in Minuska.builtin.klike]
L
Label [in Minuska.default_everything]ListFunSymbol [in Minuska.builtin.list_signature]
ListPredSymbol [in Minuska.builtin.list_signature]
M
MyQuerySymbol [in Minuska.pi.trivial]MyUnit [in Minuska.prelude]
N
notinstance [in Minuska.dt]P
Pattern [in Minuska.dt]PreTerm' [in Minuska.lowlang]
pvmatch [in Minuska.dt]
S
SideConditionEq [in Minuska.symex]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.ocaml_interface]
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]attribute_interpretation [in Minuska.spec]
AttrSymbol [in Minuska.spec]
AttrSymbol_morph_inj [in Minuska.signature_morphism]
AttrSymbol_morph [in Minuska.signature_morphism]
AttrSymbol_edc [in Minuska.spec]
B
background_model_over [in Minuska.spec]BasicValue [in Minuska.spec]
BasicValue_morph_inj [in Minuska.signature_morphism]
BasicValue_morph [in Minuska.signature_morphism]
BasicValue_edc [in Minuska.spec]
basic_types_properties [in Minuska.spec]
basic_types [in Minuska.spec]
bb_function_names [in Minuska.spec]
br_value [in Minuska.frontend]
br_kind [in Minuska.frontend]
builtin_predicate_interp [in Minuska.spec]
builtin_function_interp [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]
edc_count [in Minuska.spec]
edc_eqdec [in Minuska.spec]
F
fresher_avoid [in Minuska.fresher]FunSymbol [in Minuska.spec]
FunSymbol_morph_inj [in Minuska.signature_morphism]
FunSymbol_morph [in Minuska.signature_morphism]
FunSymbol_edc [in Minuska.spec]
H
hd [in Minuska.spec]HiddenValue [in Minuska.spec]
HiddenValue_morph_inj [in Minuska.signature_morphism]
HiddenValue_morph [in Minuska.signature_morphism]
HiddenValue_edc [in Minuska.spec]
hidden_algebra [in Minuska.spec]
hidden_init [in Minuska.spec]
hidden_predicate_interpretation [in Minuska.spec]
HPredSymbol [in Minuska.spec]
HPredSymbol_morph_inj [in Minuska.signature_morphism]
HPredSymbol_morph [in Minuska.signature_morphism]
HPredSymbol_edc [in Minuska.spec]
I
inject [in Minuska.prelude]inject_inj [in Minuska.prelude]
M
method_interpretation [in Minuska.spec]MethSymbol [in Minuska.spec]
MethSymbol_morph_inj [in Minuska.signature_morphism]
MethSymbol_morph [in Minuska.signature_morphism]
MethSymbol_edc [in Minuska.spec]
N
NondetValue [in Minuska.spec]NondetValue_morph_inj [in Minuska.signature_morphism]
NondetValue_morph [in Minuska.signature_morphism]
NondetValue_edc [in Minuska.spec]
nondet_gen [in Minuska.spec]
P
pi_TermSymbol_interp [in Minuska.spec]PredSymbol [in Minuska.spec]
PredSymbol_morph_inj [in Minuska.signature_morphism]
PredSymbol_morph [in Minuska.signature_morphism]
PredSymbol_edc [in Minuska.spec]
ProgramT [in Minuska.spec]
program_info [in Minuska.spec]
Q
QuerySymbol [in Minuska.spec]QuerySymbol_morph_inj [in Minuska.signature_morphism]
QuerySymbol_morph [in Minuska.signature_morphism]
QuerySymbol_edc [in Minuska.spec]
R
rd_rule [in Minuska.frontend]rd_label [in Minuska.frontend]
realize_br [in Minuska.frontend]
ri_reverse_pf [in Minuska.prelude]
ri_reverse [in Minuska.prelude]
ri_injection [in Minuska.prelude]
rva_over [in Minuska.model_algebra]
r_label [in Minuska.spec]
r_eff [in Minuska.spec]
r_scs [in Minuska.spec]
r_to [in Minuska.spec]
r_from [in Minuska.spec]
S
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]
sr_label [in Minuska.frontend]
sr_scs [in Minuska.frontend]
sr_to [in Minuska.frontend]
sr_from [in Minuska.frontend]
sss_sc [in Minuska.symex]
sss_term [in Minuska.symex]
string2m [in Minuska.frontend]
string2p [in Minuska.frontend]
string2qfa [in Minuska.frontend]
string2sym [in Minuska.frontend]
string2var [in Minuska.frontend]
st_rules [in Minuska.frontend]
T
TermSymbol [in Minuska.spec]TermSymbol_morph_inj [in Minuska.signature_morphism]
TermSymbol_morph [in Minuska.signature_morphism]
TermSymbol_edc [in Minuska.spec]
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
value_algebra [in Minuska.spec]Variabl [in Minuska.spec]
Variable_inf [in Minuska.spec]
Variabl_morph_inj [in Minuska.signature_morphism]
Variabl_morph [in Minuska.signature_morphism]
Variabl_edc [in Minuska.spec]
vars_of [in Minuska.spec]
Instance Index
B
BasicEffect0_eqdec [in Minuska.basic_properties]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.basic_properties]cancel_uglify_prettify [in Minuska.lowlang]
cancel_prettify_uglify [in Minuska.lowlang]
E
Expression2_countable [in Minuska.basic_properties]ExtendedSymbols_countable [in Minuska.hilang]
ExtendedSymbols_eqdec [in Minuska.hilang]
F
FunSymbol_fin [in Minuska.builtin.klike]FunSymbol_eqDec [in Minuska.builtin.klike]
I
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]
is_WildcardPattern_dec [in Minuska.dt]
is_ConstructorPattern_dec [in Minuska.dt]
L
Label_eqDec [in Minuska.default_everything]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]
MyProgramInfo [in Minuska.pi.trivial]
MyQuerySymbol_fin [in Minuska.pi.trivial]
MyQuerySymbol_eqdec [in Minuska.pi.trivial]
O
option_Valuation2_vars_of [in Minuska.valuation_merge]P
pair_swap_perm [in Minuska.substitution_parseq_conv]PredSymbol_fin [in Minuska.builtin.klike]
PredSymbol_eqDec [in Minuska.builtin.klike]
PreTerm'_A_B_fmap [in Minuska.lowlang]
PreTerm'_countable [in Minuska.lowlang]
PreTerm'_eqdec [in Minuska.lowlang]
R
restrictp_decision [in Minuska.substitution_parallel]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
showAttribute [in Minuska.quickchick_setup]showBuiltinOrVar [in Minuska.quickchick_setup]
showExpr [in Minuska.quickchick_setup]
showFun [in Minuska.quickchick_setup]
showQery [in Minuska.quickchick_setup]
showSubP [in Minuska.quickchick_setup]
showTerm [in Minuska.quickchick_setup]
showVal [in Minuska.quickchick_setup]
show_TermSymbol [in Minuska.quickchick_setup]
show_builtin [in Minuska.quickchick_setup]
SideCondition_eqdec [in Minuska.basic_properties]
simple_list_carrier__countable [in Minuska.builtin.list_model]
simple_list_carrier__eqdec [in Minuska.builtin.list_model]
sm [in Minuska.martelli_montanari_tests]
string_infinite [in Minuska.prelude]
string_countable [in Minuska.prelude]
string_eq_dec [in Minuska.prelude]
subp_eqdec [in Minuska.playground]
Subseteq_Valuation2 [in Minuska.spec]
T
TermOver_countable [in Minuska.basic_properties]Term_TermSymbol_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_sce [in Minuska.symex]
VarsOf_Valuation2 [in Minuska.spec]
VarsOf_Valuation2_ [in Minuska.spec]
VarsOf_BoV [in Minuska.spec]
VarsOf_Effect0 [in Minuska.spec]
VarsOf_sc [in Minuska.spec]
VarsOf_Expression2 [in Minuska.spec]
VarsOf_list_something [in Minuska.spec]
VarsOf_TermOver [in Minuska.spec]
VarsOf_builtin [in Minuska.spec]
VarsOf_TermSymbol [in Minuska.spec]
vector_of_wildcards_dec [in Minuska.dt]
other
Σ [in Minuska.quickchick_setup]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]
E
eqdec [in Minuska.lowlang]S
sec [in Minuska.builtin.klike]sec2 [in Minuska.builtin.klike]
sum [in Minuska.model_algebra]
W
wsm [in Minuska.frontend]Definition Index
A
analyze_list_from_end [in Minuska.prelude]AO'_getOperator [in Minuska.lowlang]
apply_TermSymbol'' [in Minuska.lowlang]
apply_TermSymbol' [in Minuska.lowlang]
argument_sequence [in Minuska.frontend]
argument_name [in Minuska.frontend]
asIfWithEq [in Minuska.symex]
ats_edc [in Minuska.hidden.hidden_unit]
B
BasicEffect0 [in Minuska.spec]BasicEffect0_evaluate [in Minuska.spec]
BasicTypesMorphism [in Minuska.signature_morphism]
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]
bindFresher [in Minuska.fresher]
bindings [in Minuska.pi.trivial]
bindings [in Minuska.builtin.klike]
bindings [in Minuska.builtin.empty]
bindings [in Minuska.hidden.hidden_unit]
bool_va [in Minuska.builtin.bool_model]
bool_relaxed_va [in Minuska.builtin.bool_model]
bool_predicate_interp [in Minuska.builtin.bool_model]
bool_function_interp [in Minuska.builtin.bool_model]
BoV_to_Expr2 [in Minuska.basic_properties]
BuiltinOrVar [in Minuska.spec]
BuiltinOrVar'_sind [in Minuska.spec]
BuiltinOrVar'_rec [in Minuska.spec]
BuiltinOrVar'_ind [in Minuska.spec]
BuiltinOrVar'_rect [in Minuska.spec]
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_EDC [in Minuska.builtin.klike]
bv_to_tree [in Minuska.builtin.klike]
BV_EDC [in Minuska.builtin.empty]
C
ClauseMatrix [in Minuska.dt]ClauseMatrix_size [in Minuska.dt]
cmmatch [in Minuska.dt]
collapses_to_sind [in Minuska.hilang]
collapses_to_rec [in Minuska.hilang]
collapses_to_ind [in Minuska.hilang]
collapses_to_rect [in Minuska.hilang]
combine_symbol_classifiers [in Minuska.ocaml_interface]
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.dt]
concat_list_option_str [in Minuska.interp_loop]
ContextTemplate [in Minuska.frontend]
Context__sind [in Minuska.hilang]
Context__rec [in Minuska.hilang]
Context__ind [in Minuska.hilang]
Context__rect [in Minuska.hilang]
contract_term [in Minuska.hilang]
cooling_rule [in Minuska.frontend]
create_eqn [in Minuska.martelli_montanari]
cseq [in Minuska.frontend]
ctx_subst [in Minuska.hilang]
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]
deg [in Minuska.textbook_unification_alg]
delta_in_val [in Minuska.properties]
denot_ss [in Minuska.symex]
denot_sss [in Minuska.symex]
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
Effect0 [in Minuska.spec]Effect0_evaluate [in Minuska.spec]
Effect0_evaluate' [in Minuska.spec]
Effect0' [in Minuska.spec]
emptyCseq [in Minuska.frontend]
eqn [in Minuska.textbook_unification_alg]
eqn [in Minuska.unification_interface]
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_et [in Minuska.naive_interpreter]
example_list_int_model_1 [in Minuska.builtin.example_list_int_model]
Expression2 [in Minuska.spec]
Expression2_subst [in Minuska.basic_properties]
Expression2_rect [in Minuska.basic_properties]
Expression2_evaluate [in Minuska.spec]
Expression2_evaluate_nv [in Minuska.naive_interpreter]
Expression2'_ind [in Minuska.spec]
ExtendedBM [in Minuska.hilang]
ExtendedSymbols_sind [in Minuska.hilang]
ExtendedSymbols_rec [in Minuska.hilang]
ExtendedSymbols_ind [in Minuska.hilang]
ExtendedSymbols_rect [in Minuska.hilang]
extend_term [in Minuska.hilang]
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
FalseState [in Minuska.symex]fmapFresher [in Minuska.fresher]
forallbin [in Minuska.specb]
format_string_list [in Minuska.prelude]
framed_rule [in Minuska.default_everything]
freezer [in Minuska.frontend]
FresherM [in Minuska.fresher]
freshFresher [in Minuska.fresher]
fresh_nth [in Minuska.substitution_parseq_conv]
fresh_var_seq [in Minuska.substitution_parseq_conv]
FS_EDC [in Minuska.builtin.klike]
FS_EDC [in Minuska.builtin.empty]
G
genBuiltin [in Minuska.quickchick_setup]genBuiltinOrVar [in Minuska.quickchick_setup]
genExprSized [in Minuska.quickchick_setup]
genFunction [in Minuska.quickchick_setup]
genPatternSized [in Minuska.quickchick_setup]
genSubstitutionSized [in Minuska.playground]
genSymbol [in Minuska.quickchick_setup]
genTermOverExprSized [in Minuska.quickchick_setup]
genTermSized [in Minuska.quickchick_setup]
genTermSized' [in Minuska.quickchick_setup]
genValuationSized [in Minuska.quickchick_setup]
genVariable [in Minuska.quickchick_setup]
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]
H
heating_rule_seq [in Minuska.frontend]helper [in Minuska.lowlang]
helper'' [in Minuska.lowlang]
hps_edc [in Minuska.hidden.hidden_unit]
hv_edc [in Minuska.hidden.hidden_unit]
I
idren [in Minuska.substitution_parseq_conv]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]
initialState [in Minuska.frontend]
init_r [in Minuska.martelli_montanari]
init_r' [in Minuska.martelli_montanari]
init_meqn [in Minuska.martelli_montanari]
inj_id [in Minuska.prelude]
inj_compose [in Minuska.prelude]
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_va [in Minuska.builtin.int_model]
int_relaxed_va [in Minuska.builtin.int_model]
int_predicate_interp [in Minuska.builtin.int_model]
int_function_interp [in Minuska.builtin.int_model]
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_WildcardPattern [in Minuska.dt]
is_ConstructorPattern [in Minuska.dt]
is_unifier_of [in Minuska.unification_interface]
K
KlikeBuiltinValue [in Minuska.builtin.klike]KlikeBuiltinValue0_sind [in Minuska.builtin.klike]
KlikeBuiltinValue0_rec [in Minuska.builtin.klike]
KlikeBuiltinValue0_ind [in Minuska.builtin.klike]
KlikeBuiltinValue0_rect [in Minuska.builtin.klike]
KlikeFunSymbol_sind [in Minuska.builtin.klike]
KlikeFunSymbol_rec [in Minuska.builtin.klike]
KlikeFunSymbol_ind [in Minuska.builtin.klike]
KlikeFunSymbol_rect [in Minuska.builtin.klike]
KlikePredSymbol_sind [in Minuska.builtin.klike]
KlikePredSymbol_rec [in Minuska.builtin.klike]
KlikePredSymbol_ind [in Minuska.builtin.klike]
KlikePredSymbol_rect [in Minuska.builtin.klike]
klike_predicate_interp [in Minuska.builtin.klike]
klike_function_interp [in Minuska.builtin.klike]
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_swap_head [in Minuska.dt]
list_wrapper [in Minuska.builtin.list_model]
list_predicate_interp [in Minuska.builtin.list_model]
list_function_interp [in Minuska.builtin.list_model]
M
make_serial1 [in Minuska.substitution_parseq_conv]make_parallel [in Minuska.substitution_parseq_conv]
make_parallel0 [in Minuska.substitution_parseq_conv]
make_serial [in Minuska.substitution_parseq_conv]
make_serial0 [in Minuska.substitution_parseq_conv]
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]
ms_edc [in Minuska.hidden.hidden_unit]
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_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
pair_swap [in Minuska.substitution_parseq_conv]PatternMatrice [in Minuska.dt]
PatternVector [in Minuska.dt]
Pattern_ind [in Minuska.dt]
pflookup [in Minuska.prelude]
pfmap [in Minuska.prelude]
poly_interpreter_ext [in Minuska.default_everything]
poly_interpreter [in Minuska.default_everything]
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_TermSymbol [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]
PS_EDC [in Minuska.builtin.klike]
PS_EDC [in Minuska.builtin.empty]
pvmatch_sind [in Minuska.dt]
pvmatch_ind [in Minuska.dt]
pvvecmatch [in Minuska.dt]
Q
qs_edc [in Minuska.pi.trivial]R
R [in Minuska.martelli_montanari]realize_thy [in Minuska.frontend]
remembered_vars_of_effect [in Minuska.properties]
renaming_for [in Minuska.substitution_parseq_conv]
renaming_ok [in Minuska.substitution_parseq_conv]
replace_and_collect [in Minuska.symex]
replace_and_collect1 [in Minuska.symex]
replace_and_collect0 [in Minuska.symex]
RestrictP [in Minuska.substitution_parallel]
REST_SEQ [in Minuska.frontend]
returnFresher [in Minuska.fresher]
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 [in Minuska.spec]
RewritingRule2_wf [in Minuska.spec_interpreter]
RewritingRule2'_wf [in Minuska.spec_interpreter]
RewritingTheory2 [in Minuska.spec]
RewritingTheory2_wf [in Minuska.spec_interpreter]
RewritingTheory2'_wf [in Minuska.spec_interpreter]
rewriting_relation [in Minuska.spec]
rinj_inr [in Minuska.prelude]
rinj_inl [in Minuska.prelude]
rinj_id [in Minuska.prelude]
rinj_compose [in Minuska.prelude]
rlift [in Minuska.substitution_parseq_conv]
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_inverse [in Minuska.substitution_parseq_conv]
r_valid [in Minuska.martelli_montanari]
r_has_all_vars [in Minuska.martelli_montanari]
r_vars_disjoint [in Minuska.martelli_montanari]
S
SA [in Minuska.playground]Satisfies_Valuation2_TermOverBuiltinValue_BuiltinOrVar [in Minuska.spec]
Satisfies_Valuation2_TermOverBuiltinValue_BuiltinOrVar_b [in Minuska.specb]
sat2B [in Minuska.spec]
sat2Bb [in Minuska.specb]
sat2E [in Minuska.spec]
sat2Eb [in Minuska.specb]
SB [in Minuska.playground]
sbov_to_e_bov [in Minuska.frontend]
SC [in Minuska.playground]
ScList [in Minuska.symex]
sclist_to_sceq [in Minuska.symex]
se_to_Expression [in Minuska.frontend]
showSubP_ [in Minuska.quickchick_setup]
showVal_ [in Minuska.quickchick_setup]
show_e [in Minuska.quickchick_setup]
show_to [in Minuska.quickchick_setup]
SideCondition [in Minuska.spec]
SideConditionEq_evaluate [in Minuska.symex]
SideConditionEq_sind [in Minuska.symex]
SideConditionEq_rec [in Minuska.symex]
SideConditionEq_ind [in Minuska.symex]
SideConditionEq_rect [in Minuska.symex]
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]
simpleStepByRule [in Minuska.symex]
Simplify [in Minuska.dt]
Simplify_step [in Minuska.dt]
size_of_var_in_val [in Minuska.properties]
si2m [in Minuska.ocaml_interface]
si2p [in Minuska.ocaml_interface]
si2qfa [in Minuska.ocaml_interface]
slice [in Minuska.prelude]
small_model_of_relaxed [in Minuska.model_algebra]
srenaming_ok [in Minuska.substitution_parseq_conv]
srlift [in Minuska.substitution_parseq_conv]
srr_to_rr [in Minuska.frontend]
sr_inverse [in Minuska.substitution_parseq_conv]
ssc_to_sc [in Minuska.frontend]
sSymbolicTerm_to_ExprTerm [in Minuska.frontend]
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]
string_countable0 [in Minuska.prelude]
string_eq_dec0 [in Minuska.prelude]
stuck [in Minuska.spec_interpreter]
sub [in Minuska.textbook_unification_alg]
SubP [in Minuska.substitution_parallel]
subp_precompose [in Minuska.substitution_parallel]
subp_restrict [in Minuska.substitution_parallel]
subp_id [in Minuska.substitution_parallel]
subp_compose [in Minuska.substitution_parallel]
subp_is_normal [in Minuska.substitution_parallel]
subp_normalize [in Minuska.substitution_parallel]
subp_codom [in Minuska.substitution_parallel]
subp_dom [in Minuska.substitution_parallel]
subp_app [in Minuska.substitution_parallel]
subp_precomposes [in Minuska.substitution_parseq_conv]
SubS [in Minuska.substitution_sequential]
subs_no_twice_approx [in Minuska.substitution_sequential_properties]
subs_precomposes [in Minuska.substitution_parseq_conv]
subs_precomposep [in Minuska.substitution_parseq_conv]
subs_is_normal [in Minuska.substitution_parseq_conv]
subs_app [in Minuska.substitution_sequential]
subtmm_closed [in Minuska.substitution_parallel_properties]
subt_codom [in Minuska.substitution_sequential_properties]
subt_dom [in Minuska.substitution_sequential_properties]
subt_closed [in Minuska.substitution_sequential]
sub_ext [in Minuska.textbook_unification]
sub_lt [in Minuska.textbook_unification]
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]
SymbolicState [in Minuska.symex]
SymbolicTerm_to_ExprTerm [in Minuska.frontend]
T
T [in Minuska.martelli_montanari]take_any [in Minuska.martelli_montanari]
TermOverBoV_to_TermOverExpr2 [in Minuska.basic_properties]
TermOverBoV_eval [in Minuska.properties]
TermOverBoV_subst [in Minuska.termoverbov_subst]
TermOverBoV_subst_expr2 [in Minuska.termoverbov_subst]
TermOverBoV_subst_gen [in Minuska.termoverbov_subst]
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_size [in Minuska.spec]
TermOver_collect [in Minuska.properties]
TermOver'_map [in Minuska.spec]
TermOver'_ind [in Minuska.spec]
TermOver'_join [in Minuska.properties]
TermOver'_leaves [in Minuska.properties]
TermOver'_option_map [in Minuska.properties]
TermOver'_e_map [in Minuska.frontend]
term_has_same_TermSymbol [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]
try_neg_s [in Minuska.frontend]
try_match_lhs_with_sc [in Minuska.naive_interpreter]
try_match_new [in Minuska.naive_interpreter]
TS_EDC [in Minuska.builtin.klike]
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]
unit_hidden_model [in Minuska.hidden.hidden_unit]
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
Valuation' [in Minuska.spec]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.properties]
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_sce [in Minuska.symex]
vars_of_BoV [in Minuska.spec]
vars_of_Effect0' [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]
va_reduction [in Minuska.model_algebra]
vector_of_wildcards [in Minuska.dt]
void_value_algebra [in Minuska.builtin.empty]
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
Σ1 [in Minuska.example_models]β [in Minuska.builtin.klike]
Record Index
B
BackgroundModel [in Minuska.spec]BackgroundModelOver [in Minuska.spec]
BasicTypes [in Minuska.spec]
BasicTypesInjMorphism [in Minuska.signature_morphism]
BasicTypesMorphism' [in Minuska.signature_morphism]
BasicTypesProperties [in Minuska.spec]
BuiltinRepr [in Minuska.frontend]
BuiltinsBinding [in Minuska.spec]
C
ContextDeclaration [in Minuska.frontend]D
Defaults [in Minuska.frontend]E
EDC [in Minuska.spec]ExprAndBoV [in Minuska.notations]
F
FresherR [in Minuska.fresher]H
HiddenAlgebra [in Minuska.spec]I
Injection [in Minuska.prelude]P
ProgramInfo [in Minuska.spec]R
Realization [in Minuska.frontend]RelaxedValueAlgebra [in Minuska.model_algebra]
ReversibleInjection [in Minuska.prelude]
RewritingRule2' [in Minuska.spec]
RuleDeclaration [in Minuska.frontend]
S
Signature [in Minuska.dt]SimpleSymbolicState [in Minuska.symex]
State [in Minuska.frontend]
Stream [in Minuska.spec]
StrictnessDeclaration [in Minuska.frontend]
StringRewritingRule [in Minuska.frontend]
U
UnificationAlgorithm [in Minuska.unification_interface]U_ops [in Minuska.martelli_montanari]
V
ValueAlgebra [in Minuska.spec]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 | (1484 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) |
| Variable 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 | (38 entries) |
| 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 | (57 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 | (381 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 | (173 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 | (39 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 | (136 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 | (104 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 | (12 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 | (511 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 | (31 entries) |