| 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 | (1562 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 | (10 entries) |
| 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 | (108 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 | (15 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 | (623 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 | (116 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) |
| 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 | (23 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 | (29 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 | (33 entries) |
| Abbreviation 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 | (25 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 | (426 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 | (18 entries) |
Global Index
A
A [abbreviation, in SMTLIB.Theory.Seq]abs_has_sort [lemma, in SMTLIB.Theory.Reals_Ints]
abs_ [definition, in SMTLIB.Theory.Reals_Ints]
adt [definition, in SMTLIB.Signature]
adt_interp_tester_false_off_constructor [lemma, in SMTLIB.Theory]
adt_constructed_of_adt_axioms [lemma, in SMTLIB.Theory]
adt_constructed_signatures_agree_except_sorts [lemma, in SMTLIB.Theory]
adt_constructed_disjoint [projection, in SMTLIB.Theory]
adt_constructed_domain [projection, in SMTLIB.Theory]
adt_constructed [record, in SMTLIB.Theory]
adt_interp_constructor_disjoint [lemma, in SMTLIB.Theory]
adt_interp_tester_at_rank [lemma, in SMTLIB.Theory]
adt_interp_tester [projection, in SMTLIB.Theory]
adt_interp_selector [projection, in SMTLIB.Theory]
adt_interp_constructor [projection, in SMTLIB.Theory]
adt_domain [projection, in SMTLIB.Theory]
adt_axioms [record, in SMTLIB.Theory]
adt_constructor_condition [definition, in SMTLIB.Theory]
adt_tester_condition [definition, in SMTLIB.Theory]
adt_selector_condition [definition, in SMTLIB.Theory]
adt_signatures_agree_except_sorts [lemma, in SMTLIB.Signature]
adt_free_of_embeddable [lemma, in SMTLIB.Signature]
adt_free_app_intro [lemma, in SMTLIB.Signature]
adt_free_param_intro [lemma, in SMTLIB.Signature]
adt_free_not_adt [lemma, in SMTLIB.Signature]
adt_free_param_inv [lemma, in SMTLIB.Signature]
adt_free_app_inv [lemma, in SMTLIB.Signature]
adt_free_app [lemma, in SMTLIB.Signature]
adt_free_param [lemma, in SMTLIB.Signature]
adt_freeb_args_true [lemma, in SMTLIB.Signature]
adt_free_dec [instance, in SMTLIB.Signature]
adt_free_irrelevant [lemma, in SMTLIB.Signature]
adt_free [definition, in SMTLIB.Signature]
adt_freeb_args_unfold [lemma, in SMTLIB.Signature]
adt_freeb_args [definition, in SMTLIB.Signature]
adt_freeb [definition, in SMTLIB.Signature]
adt_intro [lemma, in SMTLIB.Signature]
adt_dec [instance, in SMTLIB.Signature]
adt_irrelevant [lemma, in SMTLIB.Signature]
adt_of_adt_spec [lemma, in SMTLIB.Signature]
adt_spec_of_adt [lemma, in SMTLIB.Signature]
adt_spec_dec [instance, in SMTLIB.Signature]
adt_spec [definition, in SMTLIB.Signature]
adt_constructed_of_seq_adt_axioms [lemma, in SMTLIB.Theory.Seq]
adt_free_domain_witness [definition, in SMTLIB.Domain]
adt_free_domain [definition, in SMTLIB.Domain]
ands_has_sort [lemma, in SMTLIB.Theory.Core]
ands_ [definition, in SMTLIB.Theory.Core]
and_has_sort [lemma, in SMTLIB.Theory.Core]
and_ [definition, in SMTLIB.Theory.Core]
app_slash [lemma, in SMTLIB.Theory.Reals_Ints]
app_empty_l [lemma, in SMTLIB.Theory.Reals_Ints]
app_slash_inj [lemma, in SMTLIB.Theory.Reals_Ints]
app_has_sort [lemma, in SMTLIB.Theory.HO_Core]
app_ [definition, in SMTLIB.Theory.HO_Core]
arities_consistent [projection, in SMTLIB.Signature]
arity [projection, in SMTLIB.Signature]
arity_s_map [projection, in SMTLIB.Signature]
arity_s_bool [projection, in SMTLIB.Signature]
at_most_two_has_sort [lemma, in SMTLIB.Tests.UnitTests]
at_most_two [definition, in SMTLIB.Tests.UnitTests]
at_most_two_body [definition, in SMTLIB.Tests.UnitTests]
A_ho_models [lemma, in SMTLIB.Tests.TestTheory]
A_ho_adt_axioms [lemma, in SMTLIB.Tests.TestTheory]
A_ho_models_ho_core [lemma, in SMTLIB.Tests.TestTheory]
A_ho_models_core [lemma, in SMTLIB.Tests.TestTheory]
A_ho [definition, in SMTLIB.Tests.TestTheory]
A_free_models [lemma, in SMTLIB.Tests.TestTheory]
A_free_adt_axioms [lemma, in SMTLIB.Tests.TestTheory]
A_free_models_reals_ints [lemma, in SMTLIB.Tests.TestTheory]
A_free_models_core [lemma, in SMTLIB.Tests.TestTheory]
A_free [definition, in SMTLIB.Tests.TestTheory]
A0 [abbreviation, in SMTLIB.Theory.Seq]
B
base [abbreviation, in SMTLIB.Theory.Strings]base [abbreviation, in SMTLIB.Theory.Core]
base [abbreviation, in SMTLIB.Theory.Reals_Ints]
base [abbreviation, in SMTLIB.Theory.Seq]
base_interp [definition, in SMTLIB.Tests.TestTheory]
bool_has_sort [lemma, in SMTLIB.Theory.Core]
bool_ [definition, in SMTLIB.Theory.Core]
BuildInterp [section, in SMTLIB.Theory]
BuildInterp.D [variable, in SMTLIB.Theory]
C
cast [definition, in SMTLIB.Utils]cast_to_bool [definition, in SMTLIB.Theory.Strings]
cast_to_Z [definition, in SMTLIB.Theory.Strings]
cast_to_string [definition, in SMTLIB.Theory.Strings]
cast_to_bool [definition, in SMTLIB.Theory.Core]
cast_to_bool [definition, in SMTLIB.Theory.Reals_Ints]
cast_to_R [definition, in SMTLIB.Theory.Reals_Ints]
cast_to_Z [definition, in SMTLIB.Theory.Reals_Ints]
cast_sym_true_neq_false [lemma, in SMTLIB.Utils]
cast_sym_true_or_false [lemma, in SMTLIB.Utils]
cast_cast_sym [lemma, in SMTLIB.Utils]
cast_sym_cast [lemma, in SMTLIB.Utils]
cast_eq_iff_eq_cast_sym [lemma, in SMTLIB.Utils]
cast_sym [definition, in SMTLIB.Utils]
cast_to_map [definition, in SMTLIB.Theory.HO_Core]
cast_to_bool [definition, in SMTLIB.Theory.Seq]
cast_to_map [definition, in SMTLIB.Theory.Seq]
cast_to_Z [definition, in SMTLIB.Theory.Seq]
cast_to_list [definition, in SMTLIB.Theory.Seq]
cast_sym_inj [lemma, in SMTLIB.Tests.TestTheory]
cb_escape [constructor, in SMTLIB.Theory.Strings]
cb_plain [constructor, in SMTLIB.Theory.Strings]
cb_empty [constructor, in SMTLIB.Theory.Strings]
closed [definition, in SMTLIB.Term]
Compose [record, in SMTLIB.Signature]
Compose [inductive, in SMTLIB.Signature]
constant_body_printable [lemma, in SMTLIB.Theory.Strings]
constant_body_sind [definition, in SMTLIB.Theory.Strings]
constant_body_ind [definition, in SMTLIB.Theory.Strings]
constant_body [inductive, in SMTLIB.Theory.Strings]
constructors [projection, in SMTLIB.Signature]
constructors_consistent_right [projection, in SMTLIB.Signature]
constructors_consistent_left [projection, in SMTLIB.Signature]
constructors_for_sort_consistent [projection, in SMTLIB.Signature]
constructors_for_sort_wf [projection, in SMTLIB.Signature]
constructors_for_sort [projection, in SMTLIB.Signature]
constructors_wf [projection, in SMTLIB.Signature]
constructor_for_tester_consistent [projection, in SMTLIB.Signature]
constructor_args_embeddable [definition, in SMTLIB.Signature]
constructor_tester_bijection [projection, in SMTLIB.Signature]
constructor_for_tester_wf [projection, in SMTLIB.Signature]
constructor_for_tester [projection, in SMTLIB.Signature]
constructor_args_seq_embeddable [definition, in SMTLIB.Theory.Seq]
Core [library]
CoreInterpretable [section, in SMTLIB.Theory.Core]
CoreInterpretable.D [variable, in SMTLIB.Theory.Core]
CoreInterpretable.Hbool [variable, in SMTLIB.Theory.Core]
CoreInterpretable.witness [variable, in SMTLIB.Theory.Core]
CoreModels [section, in SMTLIB.Theory.Core]
CoreModels.A [variable, in SMTLIB.Theory.Core]
core_interp_models [lemma, in SMTLIB.Theory.Core]
core_interp_ite [lemma, in SMTLIB.Theory.Core]
core_interp_distinct [lemma, in SMTLIB.Theory.Core]
core_interp_eq [lemma, in SMTLIB.Theory.Core]
core_interp_xor [lemma, in SMTLIB.Theory.Core]
core_interp_or [lemma, in SMTLIB.Theory.Core]
core_interp_and [lemma, in SMTLIB.Theory.Core]
core_interp_impl [lemma, in SMTLIB.Theory.Core]
core_interp_not [lemma, in SMTLIB.Theory.Core]
core_interp_false [lemma, in SMTLIB.Theory.Core]
core_interp_true [lemma, in SMTLIB.Theory.Core]
core_interp [definition, in SMTLIB.Theory.Core]
core_ite [definition, in SMTLIB.Theory.Core]
core_cmp [definition, in SMTLIB.Theory.Core]
core_binop [definition, in SMTLIB.Theory.Core]
core_unop [definition, in SMTLIB.Theory.Core]
core_lit [definition, in SMTLIB.Theory.Core]
core_funcs [definition, in SMTLIB.Theory.Core]
core_funcs_ho_core_funcs_disjoint [lemma, in SMTLIB.Tests.TestTheory]
core_funcs_reals_ints_funcs_disjoint [lemma, in SMTLIB.Tests.TestTheory]
C_ho [definition, in SMTLIB.Tests.TestTheory]
C_test [definition, in SMTLIB.Tests.TestTheory]
C_arith [definition, in SMTLIB.Tests.TestTheory]
D
decimal_of_Z [abbreviation, in SMTLIB.Tests.UnitTests]decimal_literal_has_sort [lemma, in SMTLIB.Theory.Reals_Ints]
decimal_literal_value_eq [lemma, in SMTLIB.Theory.Reals_Ints]
decimal_literal_value [definition, in SMTLIB.Theory.Reals_Ints]
decimal_literal [definition, in SMTLIB.Theory.Reals_Ints]
decimal_literals_dec [instance, in SMTLIB.Theory.Reals_Ints]
decimal_literals [definition, in SMTLIB.Theory.Reals_Ints]
define_fun_eval_inserts [lemma, in SMTLIB.Theory.Core]
define_fun_eval_instantiate_inv [lemma, in SMTLIB.Theory.Core]
define_fun_eval_instantiate [lemma, in SMTLIB.Theory.Core]
define_fun_eval_intro [lemma, in SMTLIB.Theory.Core]
define_fun_intro_forall_telescope [lemma, in SMTLIB.Theory.Core]
define_fun_strip_forall_telescope [lemma, in SMTLIB.Theory.Core]
define_fun_forall_telescope_lc [lemma, in SMTLIB.Theory.Core]
define_fun [definition, in SMTLIB.Theory.Core]
distinct_has_sort [lemma, in SMTLIB.Theory.Core]
distinct_ [definition, in SMTLIB.Theory.Core]
divisible [definition, in SMTLIB.Theory.Reals_Ints]
divisible_has_sort [lemma, in SMTLIB.Theory.Reals_Ints]
divisible_value_eq [lemma, in SMTLIB.Theory.Reals_Ints]
divisible_value [definition, in SMTLIB.Theory.Reals_Ints]
divisible_func_dec [instance, in SMTLIB.Theory.Reals_Ints]
divisible_func [definition, in SMTLIB.Theory.Reals_Ints]
div_has_sort [lemma, in SMTLIB.Theory.Reals_Ints]
div_mod_euclidean [lemma, in SMTLIB.Theory.Reals_Ints]
div_ [definition, in SMTLIB.Theory.Reals_Ints]
div_by_zero [definition, in SMTLIB.Tests.TestTheory]
domain [projection, in SMTLIB.Theory]
Domain [library]
DomainConstruction [section, in SMTLIB.Domain]
DomainConstruction.base [variable, in SMTLIB.Domain]
DomainConstruction.base_witness [variable, in SMTLIB.Domain]
DomainConstruction.Σ [variable, in SMTLIB.Domain]
domain_witness [definition, in SMTLIB.Theory]
domain_gen [definition, in SMTLIB.Theory]
domain_σ_map [projection, in SMTLIB.Theory]
domain_σ_bool [projection, in SMTLIB.Theory]
dom_fun [definition, in SMTLIB.Tests.UnitTests]
D_test_τ_map [lemma, in SMTLIB.Tests.TestTheory]
D_test_σ_real [lemma, in SMTLIB.Tests.TestTheory]
D_test_σ_int [lemma, in SMTLIB.Tests.TestTheory]
D_test_σ_bool [lemma, in SMTLIB.Tests.TestTheory]
D_test [definition, in SMTLIB.Tests.TestTheory]
E
elem_of_fv_term_open_TFVar1 [lemma, in SMTLIB.Term]elem_of_fv_term_open_TFVar [lemma, in SMTLIB.Term]
embeddable_sort_of_ground_term [definition, in SMTLIB.Theory]
embeddable_sort_app_nil [lemma, in SMTLIB.Signature]
embeddable_sort_dec [instance, in SMTLIB.Signature]
embeddable_sort_adt_free [lemma, in SMTLIB.Signature]
embeddable_sort_adt [lemma, in SMTLIB.Signature]
embeddable_sort [definition, in SMTLIB.Signature]
embeddable_sort_of_seq_embeddable [lemma, in SMTLIB.Theory.Seq]
entails [definition, in SMTLIB.Eval]
entails_trichotomy [lemma, in SMTLIB.Eval]
entails_sat [lemma, in SMTLIB.Eval]
entails_iff_monomorphic_entails [lemma, in SMTLIB.Eval]
eq_has_sort [lemma, in SMTLIB.Theory.Core]
eq_ [definition, in SMTLIB.Theory.Core]
eq_of_existT [lemma, in SMTLIB.Utils]
eq_of_heq [lemma, in SMTLIB.Utils]
escape_string_inj [lemma, in SMTLIB.Theory.Strings]
escape_ascii_head [lemma, in SMTLIB.Theory.Strings]
escape_ascii_nonempty [lemma, in SMTLIB.Theory.Strings]
escape_string_wf [lemma, in SMTLIB.Theory.Strings]
escape_ascii_escaped [lemma, in SMTLIB.Theory.Strings]
escape_ascii_plain [lemma, in SMTLIB.Theory.Strings]
escape_string [definition, in SMTLIB.Theory.Strings]
escape_ascii [definition, in SMTLIB.Theory.Strings]
ES_cons [constructor, in SMTLIB.Eval]
ES_nil [constructor, in SMTLIB.Eval]
eval [inductive, in SMTLIB.Eval]
Eval [library]
evals [inductive, in SMTLIB.Eval]
evals_deterministic [lemma, in SMTLIB.Eval]
evals_vals_eq [lemma, in SMTLIB.Eval]
evals_sorts_eq [lemma, in SMTLIB.Eval]
evals_selector_sorts [lemma, in SMTLIB.Eval]
evals_cong_signature [lemma, in SMTLIB.Eval]
evals_cong [lemma, in SMTLIB.Eval]
evals_map_TFVar_deterministic [lemma, in SMTLIB.Eval]
evals_map_TFVar [lemma, in SMTLIB.Eval]
evals_intro [lemma, in SMTLIB.Eval]
evals_lookup [lemma, in SMTLIB.Eval]
evals_nth [lemma, in SMTLIB.Eval]
evals_length [lemma, in SMTLIB.Eval]
evals_cons_inv [lemma, in SMTLIB.Eval]
evals_cons_sigT [lemma, in SMTLIB.Eval]
evals_nil_sorts [lemma, in SMTLIB.Eval]
evals_mind [definition, in SMTLIB.Eval]
evals_sind [definition, in SMTLIB.Eval]
evals_ind [definition, in SMTLIB.Eval]
eval_at_most_two_body [lemma, in SMTLIB.Tests.UnitTests]
eval_app_lambda [lemma, in SMTLIB.Tests.UnitTests]
eval_nn_bool [lemma, in SMTLIB.Tests.UnitTests]
eval_neg_bool [lemma, in SMTLIB.Tests.UnitTests]
eval_id_bool [lemma, in SMTLIB.Tests.UnitTests]
eval_lambda_bool [lemma, in SMTLIB.Tests.UnitTests]
eval_forall_int_is_zero_false [lemma, in SMTLIB.Tests.UnitTests]
eval_total [lemma, in SMTLIB.Eval]
eval_total_signatures_agree_except_sorts [lemma, in SMTLIB.Eval]
eval_TMatch_total [lemma, in SMTLIB.Eval]
eval_term_open_alpha [lemma, in SMTLIB.Eval]
eval_term_open_alpha_disjoint [lemma, in SMTLIB.Eval]
eval_term_open_close_inserts [lemma, in SMTLIB.Eval]
eval_term_subst_TFVar_alpha [lemma, in SMTLIB.Eval]
eval_term_subst_TFVar1_alpha_inv [lemma, in SMTLIB.Eval]
eval_term_subst_TFVar1_alpha [lemma, in SMTLIB.Eval]
eval_term_subst_singleton_insert [lemma, in SMTLIB.Eval]
eval_term_subst_singleton_insert_mut_aux [lemma, in SMTLIB.Eval]
eval_term_open_alpha1 [lemma, in SMTLIB.Eval]
eval_rename [lemma, in SMTLIB.Eval]
eval_rename_mut_aux [lemma, in SMTLIB.Eval]
eval_TApp_args_value [lemma, in SMTLIB.Eval]
eval_deterministic [lemma, in SMTLIB.Eval]
eval_deterministic_TMatch [lemma, in SMTLIB.Eval]
eval_deterministic_TExists_arm [lemma, in SMTLIB.Eval]
eval_deterministic_TLet_arm [lemma, in SMTLIB.Eval]
eval_deterministic_TApp_arm_typed [lemma, in SMTLIB.Eval]
eval_deterministic_TApp_arm [lemma, in SMTLIB.Eval]
eval_deterministic_selector_app_arm [lemma, in SMTLIB.Eval]
eval_sort_of_well_sorted [lemma, in SMTLIB.Eval]
eval_sort_TMatch_PApp [lemma, in SMTLIB.Eval]
eval_sort_TMatch_PVar [lemma, in SMTLIB.Eval]
eval_cong_signature [lemma, in SMTLIB.Eval]
eval_cong_signature_mut_aux [lemma, in SMTLIB.Eval]
eval_strengthen1 [lemma, in SMTLIB.Eval]
eval_strengthen [lemma, in SMTLIB.Eval]
eval_weaken1 [lemma, in SMTLIB.Eval]
eval_weaken [lemma, in SMTLIB.Eval]
eval_closed_cong [lemma, in SMTLIB.Eval]
eval_cong [lemma, in SMTLIB.Eval]
eval_cong_mut_aux [lemma, in SMTLIB.Eval]
eval_term_open_map_TFVar [lemma, in SMTLIB.Eval]
eval_term_open_map_TFVar_mut_aux [lemma, in SMTLIB.Eval]
eval_TLet_NoDup_intro [lemma, in SMTLIB.Eval]
eval_value_heq [lemma, in SMTLIB.Eval]
eval_inserted_TFVar [lemma, in SMTLIB.Eval]
eval_TFVar_has_sort [lemma, in SMTLIB.Eval]
eval_TMatch_PApp_inv [lemma, in SMTLIB.Eval]
eval_TMatch_PVar_inv [lemma, in SMTLIB.Eval]
eval_TMatch_nil_inv [lemma, in SMTLIB.Eval]
eval_TLet_inv [lemma, in SMTLIB.Eval]
eval_TForall_true_inv [lemma, in SMTLIB.Eval]
eval_TForall_inv [lemma, in SMTLIB.Eval]
eval_TExists_true_inv [lemma, in SMTLIB.Eval]
eval_TExists_inv [lemma, in SMTLIB.Eval]
eval_TLambda_inv [lemma, in SMTLIB.Eval]
eval_TApp_inv [lemma, in SMTLIB.Eval]
eval_TFVar_inv [lemma, in SMTLIB.Eval]
eval_mind [definition, in SMTLIB.Eval]
eval_sind [definition, in SMTLIB.Eval]
eval_ind [definition, in SMTLIB.Eval]
eval_distinct_true [lemma, in SMTLIB.Theory.Core]
eval_distinct_true_inv [lemma, in SMTLIB.Theory.Core]
eval_ors_true [lemma, in SMTLIB.Theory.Core]
eval_ands_true [lemma, in SMTLIB.Theory.Core]
eval_ands_true_inv [lemma, in SMTLIB.Theory.Core]
eval_ors_true_inv [lemma, in SMTLIB.Theory.Core]
eval_true_true [lemma, in SMTLIB.Theory.Core]
eval_false_not_true [lemma, in SMTLIB.Theory.Core]
eval_or_true [lemma, in SMTLIB.Theory.Core]
eval_or_true_inv [lemma, in SMTLIB.Theory.Core]
eval_and_true_inv [lemma, in SMTLIB.Theory.Core]
eval_and [lemma, in SMTLIB.Theory.Core]
eval_eq_true_inv [lemma, in SMTLIB.Theory.Core]
eval_eq_false [lemma, in SMTLIB.Theory.Core]
eval_eq_true [lemma, in SMTLIB.Theory.Core]
eval_impl_true [lemma, in SMTLIB.Theory.Core]
eval_impl_true_consequent [lemma, in SMTLIB.Theory.Core]
eval_ite [lemma, in SMTLIB.Theory.Core]
eval_impl [lemma, in SMTLIB.Theory.Core]
eval_not [lemma, in SMTLIB.Theory.Core]
eval_zero_real [lemma, in SMTLIB.Theory.Reals_Ints]
eval_decimal_literal [lemma, in SMTLIB.Theory.Reals_Ints]
eval_zero_int [lemma, in SMTLIB.Theory.Reals_Ints]
eval_int_literal [lemma, in SMTLIB.Theory.Reals_Ints]
eval_is_int [lemma, in SMTLIB.Theory.Reals_Ints]
eval_to_int [lemma, in SMTLIB.Theory.Reals_Ints]
eval_to_real [lemma, in SMTLIB.Theory.Reals_Ints]
eval_gt_real_true [lemma, in SMTLIB.Theory.Reals_Ints]
eval_gt_real_true_inv [lemma, in SMTLIB.Theory.Reals_Ints]
eval_gt_real_interp [lemma, in SMTLIB.Theory.Reals_Ints]
eval_geq_real [lemma, in SMTLIB.Theory.Reals_Ints]
eval_div_real [lemma, in SMTLIB.Theory.Reals_Ints]
eval_times_real [lemma, in SMTLIB.Theory.Reals_Ints]
eval_geq_int [lemma, in SMTLIB.Theory.Reals_Ints]
eval_geq_int_interp [lemma, in SMTLIB.Theory.Reals_Ints]
eval_leq_int [lemma, in SMTLIB.Theory.Reals_Ints]
eval_lt_int [lemma, in SMTLIB.Theory.Reals_Ints]
eval_times_int [lemma, in SMTLIB.Theory.Reals_Ints]
eval_plus_int [lemma, in SMTLIB.Theory.Reals_Ints]
eval_app [lemma, in SMTLIB.Theory.HO_Core]
eval_seq_nth [lemma, in SMTLIB.Theory.Seq]
eval_seq_len [lemma, in SMTLIB.Theory.Seq]
eval_seq_concat [lemma, in SMTLIB.Theory.Seq]
eval_f_at_zero [lemma, in SMTLIB.Tests.TestTheory]
eval_zero_over_zero [lemma, in SMTLIB.Tests.TestTheory]
exact_coverage_no_PVar [lemma, in SMTLIB.Term]
excluded_middle_int_has_sort [lemma, in SMTLIB.Tests.UnitTests]
excluded_middle_has_sort [lemma, in SMTLIB.Tests.UnitTests]
extends_rank_with_sorts [lemma, in SMTLIB.Signature]
extends_rank_add_sorts [lemma, in SMTLIB.Signature]
extends_rank_of_signature_expansion [lemma, in SMTLIB.Signature]
extends_rank_trans [instance, in SMTLIB.Signature]
extends_rank_refl [instance, in SMTLIB.Signature]
extends_rank [definition, in SMTLIB.Signature]
E_TMatch_PApp_false [constructor, in SMTLIB.Eval]
E_TMatch_PApp_true [constructor, in SMTLIB.Eval]
E_TMatch_PVar [constructor, in SMTLIB.Eval]
E_TLet [constructor, in SMTLIB.Eval]
E_TLambda [constructor, in SMTLIB.Eval]
E_TForall_false [constructor, in SMTLIB.Eval]
E_TForall_true [constructor, in SMTLIB.Eval]
E_TExists_false [constructor, in SMTLIB.Eval]
E_TExists_true [constructor, in SMTLIB.Eval]
E_TApp [constructor, in SMTLIB.Eval]
E_TFVar [constructor, in SMTLIB.Eval]
F
false_has_sort [lemma, in SMTLIB.Theory.Core]false_ [definition, in SMTLIB.Theory.Core]
fmap_projT1_hlist_to_list [lemma, in SMTLIB.Theory]
fmap_list_to_map_zip [lemma, in SMTLIB.Utils]
Forall_embeddable_sort_of_hlist [lemma, in SMTLIB.Theory]
forall_int_is_zero_has_sort [lemma, in SMTLIB.Tests.UnitTests]
Forall_cons_tail [definition, in SMTLIB.Utils]
Forall_cons_head [definition, in SMTLIB.Utils]
Forall_dec_elem [lemma, in SMTLIB.Utils]
Forall2_monomorphic_instance_of_mono [lemma, in SMTLIB.Symbols]
fresh_strings_of_set_fresh [lemma, in SMTLIB.Utils]
func [abbreviation, in SMTLIB.Symbols]
funcs [projection, in SMTLIB.Signature]
funcs_extends [projection, in SMTLIB.Signature]
funcs_dec [projection, in SMTLIB.Signature]
fv [definition, in SMTLIB.Term]
fv_term_open_close_image_nil [lemma, in SMTLIB.Term]
fv_term_open_close_image [lemma, in SMTLIB.Term]
fv_term_subst_singleton_TFVar_subseteq [lemma, in SMTLIB.Term]
fv_term_subst_zip_TFVar_subseteq [lemma, in SMTLIB.Term]
fv_term_subst_subseteq [lemma, in SMTLIB.Term]
fv_term_close_subseteq [lemma, in SMTLIB.Term]
fv_term_close [lemma, in SMTLIB.Term]
fv_term_open_TFVar1_subseteq [lemma, in SMTLIB.Term]
fv_term_open_TFVar_subseteq [lemma, in SMTLIB.Term]
fv_map_TFVar_eq_list_to_set [lemma, in SMTLIB.Term]
fv_subseteq_fv_term_open [lemma, in SMTLIB.Term]
fv_term_open_subseteq [lemma, in SMTLIB.Term]
fv_TLet_selectors_subseteq [lemma, in SMTLIB.Term]
f_string_literal_ne_op [lemma, in SMTLIB.Theory.Strings]
f_string_literal_inj [lemma, in SMTLIB.Theory.Strings]
f_string_literal [definition, in SMTLIB.Theory.Strings]
f_str_lt [definition, in SMTLIB.Theory.Strings]
f_str_len [definition, in SMTLIB.Theory.Strings]
f_str_concat [definition, in SMTLIB.Theory.Strings]
f_ite [definition, in SMTLIB.Theory.Core]
f_distinct [definition, in SMTLIB.Theory.Core]
f_eq [definition, in SMTLIB.Theory.Core]
f_xor [definition, in SMTLIB.Theory.Core]
f_or [definition, in SMTLIB.Theory.Core]
f_and [definition, in SMTLIB.Theory.Core]
f_impl [definition, in SMTLIB.Theory.Core]
f_not [definition, in SMTLIB.Theory.Core]
f_false [definition, in SMTLIB.Theory.Core]
f_true [definition, in SMTLIB.Theory.Core]
f_decimal_literal_inj [lemma, in SMTLIB.Theory.Reals_Ints]
f_int_literal_inj [lemma, in SMTLIB.Theory.Reals_Ints]
f_divisible_inj [lemma, in SMTLIB.Theory.Reals_Ints]
f_decimal_literal [definition, in SMTLIB.Theory.Reals_Ints]
f_int_literal [definition, in SMTLIB.Theory.Reals_Ints]
f_divisible [definition, in SMTLIB.Theory.Reals_Ints]
f_is_int [definition, in SMTLIB.Theory.Reals_Ints]
f_to_int [definition, in SMTLIB.Theory.Reals_Ints]
f_to_real [definition, in SMTLIB.Theory.Reals_Ints]
f_gt [definition, in SMTLIB.Theory.Reals_Ints]
f_geq [definition, in SMTLIB.Theory.Reals_Ints]
f_lt [definition, in SMTLIB.Theory.Reals_Ints]
f_leq [definition, in SMTLIB.Theory.Reals_Ints]
f_abs [definition, in SMTLIB.Theory.Reals_Ints]
f_mod [definition, in SMTLIB.Theory.Reals_Ints]
f_div [definition, in SMTLIB.Theory.Reals_Ints]
f_idiv [definition, in SMTLIB.Theory.Reals_Ints]
f_times [definition, in SMTLIB.Theory.Reals_Ints]
f_plus [definition, in SMTLIB.Theory.Reals_Ints]
f_minus [definition, in SMTLIB.Theory.Reals_Ints]
f_app [definition, in SMTLIB.Theory.HO_Core]
f_seq_map [definition, in SMTLIB.Theory.Seq]
f_seq_contains [definition, in SMTLIB.Theory.Seq]
f_seq_nth [definition, in SMTLIB.Theory.Seq]
f_seq_len [definition, in SMTLIB.Theory.Seq]
f_seq_concat [definition, in SMTLIB.Theory.Seq]
f_seq_unit [definition, in SMTLIB.Theory.Seq]
f_seq_empty [definition, in SMTLIB.Theory.Seq]
f_f_not_reals_ints_func [lemma, in SMTLIB.Tests.TestTheory]
f_f_not_core_func [lemma, in SMTLIB.Tests.TestTheory]
f_f [definition, in SMTLIB.Tests.TestTheory]
G
G [abbreviation, in SMTLIB.Theory.Seq]GConstr [constructor, in SMTLIB.Theory]
generator_sort_of_seq_embeddable [lemma, in SMTLIB.Theory.Seq]
generator_sort_irrelevant [lemma, in SMTLIB.Theory.Seq]
generator_sort [definition, in SMTLIB.Theory.Seq]
gen_tree_to_sort [definition, in SMTLIB.Symbols]
geq_has_sort_real [lemma, in SMTLIB.Theory.Reals_Ints]
geq_has_sort_int [lemma, in SMTLIB.Theory.Reals_Ints]
geq_ [definition, in SMTLIB.Theory.Reals_Ints]
GGen [constructor, in SMTLIB.Theory]
GroundTerm [section, in SMTLIB.Theory]
GroundTermRect [section, in SMTLIB.Theory]
GroundTermRect.gen [variable, in SMTLIB.Theory]
GroundTermRect.Hconstr [variable, in SMTLIB.Theory]
GroundTermRect.Hgen [variable, in SMTLIB.Theory]
GroundTermRect.P [variable, in SMTLIB.Theory]
GroundTermRect.Σ [variable, in SMTLIB.Theory]
GroundTerm.gen [variable, in SMTLIB.Theory]
GroundTerm.Σ [variable, in SMTLIB.Theory]
ground_term_embed_inj [lemma, in SMTLIB.Theory]
ground_term_embed_project [lemma, in SMTLIB.Theory]
ground_term_project_embed [lemma, in SMTLIB.Theory]
ground_term_project_adt [lemma, in SMTLIB.Theory]
ground_term_embed_gen [lemma, in SMTLIB.Theory]
ground_term_embed_adt [lemma, in SMTLIB.Theory]
ground_term_project [definition, in SMTLIB.Theory]
ground_term_embed [definition, in SMTLIB.Theory]
ground_term_ind [lemma, in SMTLIB.Theory]
ground_term_rect [definition, in SMTLIB.Theory]
ground_term_constructor [definition, in SMTLIB.Theory]
ground_term [inductive, in SMTLIB.Theory]
gt_has_sort_real [lemma, in SMTLIB.Theory.Reals_Ints]
gt_has_sort_int [lemma, in SMTLIB.Theory.Reals_Ints]
gt_ [definition, in SMTLIB.Theory.Reals_Ints]
H
HCons [constructor, in SMTLIB.Theory]heq_eq_rect_l [lemma, in SMTLIB.Utils]
hex_value_digit [lemma, in SMTLIB.Theory.Strings]
hex_value [definition, in SMTLIB.Theory.Strings]
hex_digit_inj [lemma, in SMTLIB.Theory.Strings]
hex_digit_code [lemma, in SMTLIB.Theory.Strings]
hex_digit [definition, in SMTLIB.Theory.Strings]
hlist [inductive, in SMTLIB.Theory]
hlist_map_embed_project [lemma, in SMTLIB.Theory]
hlist_map_embed [definition, in SMTLIB.Theory]
hlist_map_id [lemma, in SMTLIB.Theory]
hlist_lookup_map [lemma, in SMTLIB.Theory]
hlist_map_map [lemma, in SMTLIB.Theory]
hlist_map [definition, in SMTLIB.Theory]
hlist_ForallT_lookup [lemma, in SMTLIB.Theory]
hlist_ForallT [definition, in SMTLIB.Theory]
hlist_to_list [definition, in SMTLIB.Theory]
hlist_lookup_is_Some [lemma, in SMTLIB.Theory]
hlist_lookup_Some_1 [lemma, in SMTLIB.Theory]
hlist_lookup_Some [lemma, in SMTLIB.Theory]
hlist_lookup [definition, in SMTLIB.Theory]
hlist_cons_eq [lemma, in SMTLIB.Theory]
hlist_nil_eq [lemma, in SMTLIB.Theory]
hlist_sind [definition, in SMTLIB.Theory]
hlist_rec [definition, in SMTLIB.Theory]
hlist_ind [definition, in SMTLIB.Theory]
hlist_rect [definition, in SMTLIB.Theory]
hlist_map_seq_embed_project [lemma, in SMTLIB.Theory.Seq]
hlist_map_project_seq_embed [lemma, in SMTLIB.Theory.Seq]
hlist_lookup_seq_embed [lemma, in SMTLIB.Theory.Seq]
hlist_map_seq_embed [definition, in SMTLIB.Theory.Seq]
HNil [constructor, in SMTLIB.Theory]
holds [definition, in SMTLIB.Eval]
holds_iff_eval [lemma, in SMTLIB.Eval]
ho_core_interp_models [lemma, in SMTLIB.Theory.HO_Core]
ho_core_interp [definition, in SMTLIB.Theory.HO_Core]
ho_app [definition, in SMTLIB.Theory.HO_Core]
HO_CoreInterpretable.Hmap [variable, in SMTLIB.Theory.HO_Core]
HO_CoreInterpretable.Hbool [variable, in SMTLIB.Theory.HO_Core]
HO_CoreInterpretable.witness [variable, in SMTLIB.Theory.HO_Core]
HO_CoreInterpretable.D [variable, in SMTLIB.Theory.HO_Core]
HO_CoreInterpretable [section, in SMTLIB.Theory.HO_Core]
HO_CoreModels.A [variable, in SMTLIB.Theory.HO_Core]
HO_CoreModels [section, in SMTLIB.Theory.HO_Core]
ho_core_funcs [definition, in SMTLIB.Theory.HO_Core]
ho_interp [definition, in SMTLIB.Tests.TestTheory]
HO_Core [library]
I
identifier [inductive, in SMTLIB.Symbols]identifier_eqb_iff [lemma, in SMTLIB.Symbols]
identifier_eqb [definition, in SMTLIB.Symbols]
identifier_add_prefix [definition, in SMTLIB.Symbols]
identifier_infinite [instance, in SMTLIB.Symbols]
identifier_countable [instance, in SMTLIB.Symbols]
identifier_eq_decision [instance, in SMTLIB.Symbols]
identifier_sind [definition, in SMTLIB.Symbols]
identifier_rec [definition, in SMTLIB.Symbols]
identifier_ind [definition, in SMTLIB.Symbols]
identifier_rect [definition, in SMTLIB.Symbols]
IdIndexed [constructor, in SMTLIB.Symbols]
idiv_has_sort [lemma, in SMTLIB.Theory.Reals_Ints]
idiv_ [definition, in SMTLIB.Theory.Reals_Ints]
IdSimple [constructor, in SMTLIB.Symbols]
IdxNum [constructor, in SMTLIB.Symbols]
IdxSym [constructor, in SMTLIB.Symbols]
id_bool [definition, in SMTLIB.Tests.UnitTests]
impl_has_sort [lemma, in SMTLIB.Theory.Core]
impl_ [definition, in SMTLIB.Theory.Core]
index [inductive, in SMTLIB.Symbols]
index_eqb_iff [lemma, in SMTLIB.Symbols]
index_eqb [definition, in SMTLIB.Symbols]
index_countable [instance, in SMTLIB.Symbols]
index_eq_decision [instance, in SMTLIB.Symbols]
index_sind [definition, in SMTLIB.Symbols]
index_rec [definition, in SMTLIB.Symbols]
index_ind [definition, in SMTLIB.Symbols]
index_rect [definition, in SMTLIB.Symbols]
infix [definition, in SMTLIB.Utils]
infix_of_singleton [lemma, in SMTLIB.Utils]
instance_of_refl [lemma, in SMTLIB.Symbols]
instance_of_functional [lemma, in SMTLIB.Symbols]
instance_of [definition, in SMTLIB.Symbols]
interp [projection, in SMTLIB.Theory]
interpretation [definition, in SMTLIB.Theory]
Interpretation [section, in SMTLIB.Theory]
Interpretation.domain [variable, in SMTLIB.Theory]
interp_insert_func_ne [lemma, in SMTLIB.Theory]
interp_insert_func_eq [lemma, in SMTLIB.Theory]
interp_insert_func [definition, in SMTLIB.Theory]
interp_insert_rank_ne [lemma, in SMTLIB.Theory]
interp_insert_rank_eq [lemma, in SMTLIB.Theory]
interp_insert_rank [definition, in SMTLIB.Theory]
interp_const [definition, in SMTLIB.Theory]
interp_agree_on [definition, in SMTLIB.Theory]
interp_apply_curry [lemma, in SMTLIB.Theory]
interp_curry [definition, in SMTLIB.Theory]
interp_apply [definition, in SMTLIB.Theory]
int_literal_has_sort [lemma, in SMTLIB.Theory.Reals_Ints]
int_literal_value_eq [lemma, in SMTLIB.Theory.Reals_Ints]
int_literal_value [definition, in SMTLIB.Theory.Reals_Ints]
int_literal [definition, in SMTLIB.Theory.Reals_Ints]
int_literals_dec [instance, in SMTLIB.Theory.Reals_Ints]
int_literals [definition, in SMTLIB.Theory.Reals_Ints]
Inversion [section, in SMTLIB.Eval]
Inversion.A [variable, in SMTLIB.Eval]
Inversion.Σ [variable, in SMTLIB.Eval]
is_hex_digit [definition, in SMTLIB.Theory.Strings]
is_int_has_sort [lemma, in SMTLIB.Theory.Reals_Ints]
is_int [definition, in SMTLIB.Theory.Reals_Ints]
is_seqb_false [lemma, in SMTLIB.Theory.Seq]
is_seqb [definition, in SMTLIB.Theory.Seq]
ite_has_sort [lemma, in SMTLIB.Theory.Core]
ite_ [definition, in SMTLIB.Theory.Core]
L
lc [inductive, in SMTLIB.Term]LCA_TMatch [constructor, in SMTLIB.Term]
LCA_TLet [constructor, in SMTLIB.Term]
LCA_TForall [constructor, in SMTLIB.Term]
LCA_TExists [constructor, in SMTLIB.Term]
LCA_TLambda [constructor, in SMTLIB.Term]
LCA_TApp [constructor, in SMTLIB.Term]
LCA_TBVar [constructor, in SMTLIB.Term]
LCA_TFVar [constructor, in SMTLIB.Term]
LCT_TMatch [constructor, in SMTLIB.Term]
LCT_TLet [constructor, in SMTLIB.Term]
LCT_TForall [constructor, in SMTLIB.Term]
LCT_TExists [constructor, in SMTLIB.Term]
LCT_TLambda [constructor, in SMTLIB.Term]
LCT_TApp [constructor, in SMTLIB.Term]
LCT_TFVar [constructor, in SMTLIB.Term]
lc_at_term_close1 [lemma, in SMTLIB.Term]
lc_at_term_close [lemma, in SMTLIB.Term]
lc_at_term_subst_TFVar [lemma, in SMTLIB.Term]
lc_at_term_subst [lemma, in SMTLIB.Term]
lc_at_of_lc_term_open_TFVar [lemma, in SMTLIB.Term]
lc_lc_at [lemma, in SMTLIB.Term]
lc_at_term_open_nil [lemma, in SMTLIB.Term]
lc_at_term_open [lemma, in SMTLIB.Term]
lc_at_app_r [lemma, in SMTLIB.Term]
lc_at_TMatch_cons [lemma, in SMTLIB.Term]
lc_at_TLet_cons [lemma, in SMTLIB.Term]
lc_at_TApp_cons [lemma, in SMTLIB.Term]
lc_term_open_term_close [lemma, in SMTLIB.Term]
lc_term_open_rename [lemma, in SMTLIB.Term]
lc_term_open [lemma, in SMTLIB.Term]
lc_at_sind [definition, in SMTLIB.Term]
lc_at_ind [definition, in SMTLIB.Term]
lc_at [inductive, in SMTLIB.Term]
lc_sind [definition, in SMTLIB.Term]
lc_ind [definition, in SMTLIB.Term]
length_hlist_to_list [lemma, in SMTLIB.Theory]
length_fresh_strings_of_set [lemma, in SMTLIB.Utils]
length_omap_lt [lemma, in SMTLIB.Utils]
length_omap_le [lemma, in SMTLIB.Utils]
leq_has_sort_real [lemma, in SMTLIB.Theory.Reals_Ints]
leq_has_sort_int [lemma, in SMTLIB.Theory.Reals_Ints]
leq_ [definition, in SMTLIB.Theory.Reals_Ints]
list_lookup_hlist_to_list [lemma, in SMTLIB.Theory]
list_find_eq_list_to_map_zip [lemma, in SMTLIB.Utils]
list_to_map_zip_singleton_union [lemma, in SMTLIB.Utils]
list_eq_dec_elem_of [lemma, in SMTLIB.Utils]
list_eqb_iff [lemma, in SMTLIB.Utils]
list_eqb [definition, in SMTLIB.Utils]
list_ForallT_lookup [lemma, in SMTLIB.Utils]
list_ForallT [definition, in SMTLIB.Utils]
literal_payload_f_string_literal [lemma, in SMTLIB.Theory.Strings]
literal_payload [definition, in SMTLIB.Theory.Strings]
lookup_union_agree [lemma, in SMTLIB.Utils]
lookup_insert_agree [lemma, in SMTLIB.Utils]
lookup_list_to_map_zip_None [lemma, in SMTLIB.Utils]
lt_has_sort_real [lemma, in SMTLIB.Theory.Reals_Ints]
lt_has_sort_int [lemma, in SMTLIB.Theory.Reals_Ints]
lt_ [definition, in SMTLIB.Theory.Reals_Ints]
M
map_fst_map_second [lemma, in SMTLIB.Utils]match_pattern_constructor_in_constructors [lemma, in SMTLIB.Signature]
mc_ite [projection, in SMTLIB.Theory.Core]
mc_distinct [projection, in SMTLIB.Theory.Core]
mc_eq [projection, in SMTLIB.Theory.Core]
mc_xor [projection, in SMTLIB.Theory.Core]
mc_or [projection, in SMTLIB.Theory.Core]
mc_and [projection, in SMTLIB.Theory.Core]
mc_impl [projection, in SMTLIB.Theory.Core]
mc_not [projection, in SMTLIB.Theory.Core]
mc_false [projection, in SMTLIB.Theory.Core]
mc_true [projection, in SMTLIB.Theory.Core]
mhc_app [projection, in SMTLIB.Theory.HO_Core]
minus_has_sort_real [lemma, in SMTLIB.Theory.Reals_Ints]
minus_has_sort_int [lemma, in SMTLIB.Theory.Reals_Ints]
minus_ [definition, in SMTLIB.Theory.Reals_Ints]
models [projection, in SMTLIB.Theory]
models_strings [record, in SMTLIB.Theory.Strings]
models_f_string_literal [definition, in SMTLIB.Theory.Strings]
models_f_str_lt [definition, in SMTLIB.Theory.Strings]
models_f_str_len [definition, in SMTLIB.Theory.Strings]
models_f_str_concat [definition, in SMTLIB.Theory.Strings]
models_core [record, in SMTLIB.Theory.Core]
models_f_ite [definition, in SMTLIB.Theory.Core]
models_f_distinct [definition, in SMTLIB.Theory.Core]
models_f_eq [definition, in SMTLIB.Theory.Core]
models_f_xor [definition, in SMTLIB.Theory.Core]
models_f_or [definition, in SMTLIB.Theory.Core]
models_f_and [definition, in SMTLIB.Theory.Core]
models_f_impl [definition, in SMTLIB.Theory.Core]
models_f_not [definition, in SMTLIB.Theory.Core]
models_f_false [definition, in SMTLIB.Theory.Core]
models_f_true [definition, in SMTLIB.Theory.Core]
models_reals_ints [record, in SMTLIB.Theory.Reals_Ints]
models_f_decimal_literal [definition, in SMTLIB.Theory.Reals_Ints]
models_f_int_literal [definition, in SMTLIB.Theory.Reals_Ints]
models_f_divisible [definition, in SMTLIB.Theory.Reals_Ints]
models_f_is_int [definition, in SMTLIB.Theory.Reals_Ints]
models_f_to_int [definition, in SMTLIB.Theory.Reals_Ints]
models_f_to_real [definition, in SMTLIB.Theory.Reals_Ints]
models_f_gt_real [definition, in SMTLIB.Theory.Reals_Ints]
models_f_geq_real [definition, in SMTLIB.Theory.Reals_Ints]
models_f_lt_real [definition, in SMTLIB.Theory.Reals_Ints]
models_f_leq_real [definition, in SMTLIB.Theory.Reals_Ints]
models_f_div [definition, in SMTLIB.Theory.Reals_Ints]
models_f_times_real [definition, in SMTLIB.Theory.Reals_Ints]
models_f_plus_real [definition, in SMTLIB.Theory.Reals_Ints]
models_f_minus_sub_real [definition, in SMTLIB.Theory.Reals_Ints]
models_f_minus_neg_real [definition, in SMTLIB.Theory.Reals_Ints]
models_f_gt_int [definition, in SMTLIB.Theory.Reals_Ints]
models_f_geq_int [definition, in SMTLIB.Theory.Reals_Ints]
models_f_lt_int [definition, in SMTLIB.Theory.Reals_Ints]
models_f_leq_int [definition, in SMTLIB.Theory.Reals_Ints]
models_f_abs [definition, in SMTLIB.Theory.Reals_Ints]
models_f_mod [definition, in SMTLIB.Theory.Reals_Ints]
models_f_idiv [definition, in SMTLIB.Theory.Reals_Ints]
models_f_times_int [definition, in SMTLIB.Theory.Reals_Ints]
models_f_plus_int [definition, in SMTLIB.Theory.Reals_Ints]
models_f_minus_sub_int [definition, in SMTLIB.Theory.Reals_Ints]
models_f_minus_neg_int [definition, in SMTLIB.Theory.Reals_Ints]
models_ho_core [record, in SMTLIB.Theory.HO_Core]
models_f_app [definition, in SMTLIB.Theory.HO_Core]
models_seq [record, in SMTLIB.Theory.Seq]
models_f_seq_map [definition, in SMTLIB.Theory.Seq]
models_f_seq_contains [definition, in SMTLIB.Theory.Seq]
models_f_seq_nth [definition, in SMTLIB.Theory.Seq]
models_f_seq_len [definition, in SMTLIB.Theory.Seq]
models_f_seq_concat [definition, in SMTLIB.Theory.Seq]
models_f_seq_unit [definition, in SMTLIB.Theory.Seq]
models_f_seq_empty [definition, in SMTLIB.Theory.Seq]
mod_has_sort [lemma, in SMTLIB.Theory.Reals_Ints]
mod_ [definition, in SMTLIB.Theory.Reals_Ints]
monomorphic [inductive, in SMTLIB.Symbols]
monomorphic_sort_subst_at_most_two [lemma, in SMTLIB.Tests.UnitTests]
monomorphic_τ_map_bool [lemma, in SMTLIB.Tests.UnitTests]
monomorphic_entails [definition, in SMTLIB.Eval]
monomorphic_sat [definition, in SMTLIB.Eval]
monomorphic_rank_f_or_inv [lemma, in SMTLIB.Theory.Core]
monomorphic_rank_f_and_inv [lemma, in SMTLIB.Theory.Core]
monomorphic_rank_f_eq_inv [lemma, in SMTLIB.Theory.Core]
monomorphic_rank_signatures_agree_except_sorts [lemma, in SMTLIB.Signature]
monomorphic_rank_extends [lemma, in SMTLIB.Signature]
monomorphic_rank_conservative [lemma, in SMTLIB.Signature]
monomorphic_rank_constructor_args_eq [lemma, in SMTLIB.Signature]
monomorphic_rank_constructor_length [lemma, in SMTLIB.Signature]
monomorphic_rank_selector_length [lemma, in SMTLIB.Signature]
monomorphic_rank_selector [lemma, in SMTLIB.Signature]
monomorphic_rank [definition, in SMTLIB.Signature]
monomorphic_rank_base [abbreviation, in SMTLIB.Signature]
monomorphic_sort_subst [definition, in SMTLIB.Sorting]
monomorphic_instance_of_mono [lemma, in SMTLIB.Symbols]
monomorphic_instance_of_σ_bool [lemma, in SMTLIB.Symbols]
monomorphic_instance_of_SApp_const [lemma, in SMTLIB.Symbols]
monomorphic_instance_of_refl [lemma, in SMTLIB.Symbols]
monomorphic_instance_of_functional [lemma, in SMTLIB.Symbols]
monomorphic_instance_of [definition, in SMTLIB.Symbols]
monomorphic_iff_sort_params_empty [lemma, in SMTLIB.Symbols]
monomorphic_σ_bool [lemma, in SMTLIB.Symbols]
monomorphic_SApp_const [lemma, in SMTLIB.Symbols]
monomorphic_sind [definition, in SMTLIB.Symbols]
monomorphic_ind [definition, in SMTLIB.Symbols]
mri_decimal_literal [projection, in SMTLIB.Theory.Reals_Ints]
mri_int_literal [projection, in SMTLIB.Theory.Reals_Ints]
mri_divisible [projection, in SMTLIB.Theory.Reals_Ints]
mri_is_int [projection, in SMTLIB.Theory.Reals_Ints]
mri_to_int [projection, in SMTLIB.Theory.Reals_Ints]
mri_to_real [projection, in SMTLIB.Theory.Reals_Ints]
mri_gt_real [projection, in SMTLIB.Theory.Reals_Ints]
mri_geq_real [projection, in SMTLIB.Theory.Reals_Ints]
mri_lt_real [projection, in SMTLIB.Theory.Reals_Ints]
mri_leq_real [projection, in SMTLIB.Theory.Reals_Ints]
mri_div [projection, in SMTLIB.Theory.Reals_Ints]
mri_times_real [projection, in SMTLIB.Theory.Reals_Ints]
mri_plus_real [projection, in SMTLIB.Theory.Reals_Ints]
mri_minus_sub_real [projection, in SMTLIB.Theory.Reals_Ints]
mri_minus_neg_real [projection, in SMTLIB.Theory.Reals_Ints]
mri_gt_int [projection, in SMTLIB.Theory.Reals_Ints]
mri_geq_int [projection, in SMTLIB.Theory.Reals_Ints]
mri_lt_int [projection, in SMTLIB.Theory.Reals_Ints]
mri_leq_int [projection, in SMTLIB.Theory.Reals_Ints]
mri_abs [projection, in SMTLIB.Theory.Reals_Ints]
mri_mod [projection, in SMTLIB.Theory.Reals_Ints]
mri_idiv [projection, in SMTLIB.Theory.Reals_Ints]
mri_times_int [projection, in SMTLIB.Theory.Reals_Ints]
mri_plus_int [projection, in SMTLIB.Theory.Reals_Ints]
mri_minus_sub_int [projection, in SMTLIB.Theory.Reals_Ints]
mri_minus_neg_int [projection, in SMTLIB.Theory.Reals_Ints]
ms_string_literal [projection, in SMTLIB.Theory.Strings]
ms_str_lt [projection, in SMTLIB.Theory.Strings]
ms_str_len [projection, in SMTLIB.Theory.Strings]
ms_str_concat [projection, in SMTLIB.Theory.Strings]
ms_map [projection, in SMTLIB.Theory.Seq]
ms_contains [projection, in SMTLIB.Theory.Seq]
ms_nth [projection, in SMTLIB.Theory.Seq]
ms_len [projection, in SMTLIB.Theory.Seq]
ms_concat [projection, in SMTLIB.Theory.Seq]
ms_unit [projection, in SMTLIB.Theory.Seq]
ms_empty [projection, in SMTLIB.Theory.Seq]
M_SApp [constructor, in SMTLIB.Symbols]
N
neg_bool [definition, in SMTLIB.Tests.UnitTests]neg_has_sort_real [lemma, in SMTLIB.Theory.Reals_Ints]
neg_has_sort_int [lemma, in SMTLIB.Theory.Reals_Ints]
neg_ [definition, in SMTLIB.Theory.Reals_Ints]
nn_bool [definition, in SMTLIB.Tests.UnitTests]
NoDup_fresh_strings_of_set [lemma, in SMTLIB.Utils]
not_sat_not_at_most_two [lemma, in SMTLIB.Tests.UnitTests]
not_valid_at_most_two [lemma, in SMTLIB.Tests.UnitTests]
not_valid_forall_int_is_zero [lemma, in SMTLIB.Tests.UnitTests]
not_sat_forall_int_is_zero [lemma, in SMTLIB.Tests.UnitTests]
not_valid_one_eq_two [lemma, in SMTLIB.Tests.UnitTests]
not_sat_one_eq_two [lemma, in SMTLIB.Tests.UnitTests]
not_valid_uninterpreted_f_at_zero_is_four [lemma, in SMTLIB.Tests.UnitTests]
not_valid_zero_over_zero_is_four [lemma, in SMTLIB.Tests.UnitTests]
not_sat_not_entails [lemma, in SMTLIB.Eval]
not_has_sort [lemma, in SMTLIB.Theory.Core]
not_ [definition, in SMTLIB.Theory.Core]
not_adt_of_no_constructors [lemma, in SMTLIB.Signature]
not_elem_of_fv_term_open_close1 [lemma, in SMTLIB.Term]
not_elem_of_fv_term_subst_zip [lemma, in SMTLIB.Term]
not_elem_of_fresh_strings_of_set [lemma, in SMTLIB.Utils]
not_τ_seq_symb [lemma, in SMTLIB.Theory.Seq]
not_τ_seq_cons2 [lemma, in SMTLIB.Theory.Seq]
not_τ_seq_nil [lemma, in SMTLIB.Theory.Seq]
not_τ_seq_SParam [lemma, in SMTLIB.Theory.Seq]
not_entails_of_not_sat [lemma, in SMTLIB.Tests.TestTheory]
O
one_eq_two_has_sort [lemma, in SMTLIB.Tests.UnitTests]one_plus_one_has_sort [lemma, in SMTLIB.Tests.UnitTests]
open [definition, in SMTLIB.Term]
option_Forall_None [lemma, in SMTLIB.Utils]
option_Forall_Some [lemma, in SMTLIB.Utils]
ors_has_sort [lemma, in SMTLIB.Theory.Core]
ors_ [definition, in SMTLIB.Theory.Core]
or_has_sort [lemma, in SMTLIB.Theory.Core]
or_ [definition, in SMTLIB.Theory.Core]
P
PApp [constructor, in SMTLIB.Term]pars [definition, in SMTLIB.Term]
parse_string_literal_eq [lemma, in SMTLIB.Theory.Strings]
parse_string_literal [definition, in SMTLIB.Theory.Strings]
parse_decimal_literal_eq [lemma, in SMTLIB.Theory.Reals_Ints]
parse_decimal_literal [definition, in SMTLIB.Theory.Reals_Ints]
parse_int_literal_eq [lemma, in SMTLIB.Theory.Reals_Ints]
parse_int_literal [definition, in SMTLIB.Theory.Reals_Ints]
parse_divisible_eq [lemma, in SMTLIB.Theory.Reals_Ints]
parse_divisible [definition, in SMTLIB.Theory.Reals_Ints]
parse_Z_pretty [lemma, in SMTLIB.Utils]
parse_Z [definition, in SMTLIB.Utils]
parse_positive_pretty [lemma, in SMTLIB.Utils]
parse_positive [definition, in SMTLIB.Utils]
parse_N_pretty [lemma, in SMTLIB.Utils]
parse_N [definition, in SMTLIB.Utils]
parse_N_go_pretty [lemma, in SMTLIB.Utils]
parse_N_go [definition, in SMTLIB.Utils]
parse_N_char_pretty [lemma, in SMTLIB.Utils]
parse_N_char [definition, in SMTLIB.Utils]
pars_subseteq_pars_term_open [lemma, in SMTLIB.Term]
pattern [inductive, in SMTLIB.Term]
pattern_binders [definition, in SMTLIB.Term]
pattern_constructor [definition, in SMTLIB.Term]
pattern_countable [instance, in SMTLIB.Term]
pattern_eq_dec [instance, in SMTLIB.Term]
pattern_sind [definition, in SMTLIB.Term]
pattern_rec [definition, in SMTLIB.Term]
pattern_ind [definition, in SMTLIB.Term]
pattern_rect [definition, in SMTLIB.Term]
plain_char [definition, in SMTLIB.Theory.Strings]
plus_has_sort_real [lemma, in SMTLIB.Theory.Reals_Ints]
plus_has_sort_int [lemma, in SMTLIB.Theory.Reals_Ints]
plus_ [definition, in SMTLIB.Theory.Reals_Ints]
pmodels [projection, in SMTLIB.Theory]
polymorphic_term_has_sort_of_term_has_sort [lemma, in SMTLIB.Sorting]
polymorphic_term_has_sort [definition, in SMTLIB.Sorting]
pretheories_composable [record, in SMTLIB.Theory]
pretheory [record, in SMTLIB.Theory]
pretheory_add_sorts_interpretable [lemma, in SMTLIB.Theory]
pretheory_add_sorts_local [lemma, in SMTLIB.Theory]
pretheory_compose_interpretable [lemma, in SMTLIB.Theory]
pretheory_compose_local [lemma, in SMTLIB.Theory]
pretheory_interpretable [definition, in SMTLIB.Theory]
pretheory_local [definition, in SMTLIB.Theory]
pretheory_add_sorts [definition, in SMTLIB.Theory]
pretheory_compose_compose [instance, in SMTLIB.Theory]
pretheory_compose [definition, in SMTLIB.Theory]
pretty_positive_slash_free [lemma, in SMTLIB.Theory.Reals_Ints]
pretty_Z_slash_free [lemma, in SMTLIB.Theory.Reals_Ints]
pretty_N_slash_free [lemma, in SMTLIB.Theory.Reals_Ints]
pretty_N_go_slash_free [lemma, in SMTLIB.Theory.Reals_Ints]
ptc_signatures_composable [projection, in SMTLIB.Theory]
PVar [constructor, in SMTLIB.Term]
pΣ [projection, in SMTLIB.Theory]
Q
Qc_of_Z [abbreviation, in SMTLIB.Tests.UnitTests]quote_string [definition, in SMTLIB.Theory.Strings]
quote_char [definition, in SMTLIB.Theory.Strings]
R
rank [projection, in SMTLIB.Signature]rank_strings_sind [definition, in SMTLIB.Theory.Strings]
rank_strings_ind [definition, in SMTLIB.Theory.Strings]
rank_f_string_literal [constructor, in SMTLIB.Theory.Strings]
rank_f_str_lt [constructor, in SMTLIB.Theory.Strings]
rank_f_str_len [constructor, in SMTLIB.Theory.Strings]
rank_f_str_concat [constructor, in SMTLIB.Theory.Strings]
rank_strings [inductive, in SMTLIB.Theory.Strings]
rank_core_sind [definition, in SMTLIB.Theory.Core]
rank_core_ind [definition, in SMTLIB.Theory.Core]
rank_f_ite [constructor, in SMTLIB.Theory.Core]
rank_f_distinct [constructor, in SMTLIB.Theory.Core]
rank_f_eq [constructor, in SMTLIB.Theory.Core]
rank_f_xor [constructor, in SMTLIB.Theory.Core]
rank_f_or [constructor, in SMTLIB.Theory.Core]
rank_f_and [constructor, in SMTLIB.Theory.Core]
rank_f_impl [constructor, in SMTLIB.Theory.Core]
rank_f_not [constructor, in SMTLIB.Theory.Core]
rank_f_false [constructor, in SMTLIB.Theory.Core]
rank_f_true [constructor, in SMTLIB.Theory.Core]
rank_core [inductive, in SMTLIB.Theory.Core]
rank_consistent [definition, in SMTLIB.Signature]
rank_constructor_consistent [projection, in SMTLIB.Signature]
rank_conservative [projection, in SMTLIB.Signature]
rank_extends [projection, in SMTLIB.Signature]
rank_extension [record, in SMTLIB.Signature]
rank_constructor_args_determined_intro [lemma, in SMTLIB.Signature]
rank_monomorphic [lemma, in SMTLIB.Signature]
rank_tester [projection, in SMTLIB.Signature]
rank_selectors [projection, in SMTLIB.Signature]
rank_constructor_args_determined [projection, in SMTLIB.Signature]
rank_constructor [projection, in SMTLIB.Signature]
rank_left_total [projection, in SMTLIB.Signature]
rank_domain [projection, in SMTLIB.Signature]
rank_wf [projection, in SMTLIB.Signature]
rank_reals_ints_sind [definition, in SMTLIB.Theory.Reals_Ints]
rank_reals_ints_ind [definition, in SMTLIB.Theory.Reals_Ints]
rank_f_decimal_literal [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_int_literal [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_divisible [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_is_int [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_to_int [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_to_real [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_gt_real [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_geq_real [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_lt_real [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_leq_real [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_div [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_times_real [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_plus_real [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_minus_sub_real [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_minus_neg_real [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_gt_int [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_geq_int [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_lt_int [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_leq_int [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_abs [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_mod [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_idiv [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_times_int [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_plus_int [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_minus_sub_int [constructor, in SMTLIB.Theory.Reals_Ints]
rank_f_minus_neg_int [constructor, in SMTLIB.Theory.Reals_Ints]
rank_reals_ints [inductive, in SMTLIB.Theory.Reals_Ints]
rank_ho_core_sind [definition, in SMTLIB.Theory.HO_Core]
rank_ho_core_rec [definition, in SMTLIB.Theory.HO_Core]
rank_ho_core_ind [definition, in SMTLIB.Theory.HO_Core]
rank_ho_core_rect [definition, in SMTLIB.Theory.HO_Core]
rank_f_app [constructor, in SMTLIB.Theory.HO_Core]
rank_ho_core [inductive, in SMTLIB.Theory.HO_Core]
rank_seq_sind [definition, in SMTLIB.Theory.Seq]
rank_seq_ind [definition, in SMTLIB.Theory.Seq]
rank_f_seq_map [constructor, in SMTLIB.Theory.Seq]
rank_f_seq_contains [constructor, in SMTLIB.Theory.Seq]
rank_f_seq_nth [constructor, in SMTLIB.Theory.Seq]
rank_f_seq_len [constructor, in SMTLIB.Theory.Seq]
rank_f_seq_concat [constructor, in SMTLIB.Theory.Seq]
rank_f_seq_unit [constructor, in SMTLIB.Theory.Seq]
rank_f_seq_empty [constructor, in SMTLIB.Theory.Seq]
rank_seq [inductive, in SMTLIB.Theory.Seq]
rank_uninterp_sind [definition, in SMTLIB.Tests.TestTheory]
rank_uninterp_rec [definition, in SMTLIB.Tests.TestTheory]
rank_uninterp_ind [definition, in SMTLIB.Tests.TestTheory]
rank_uninterp_rect [definition, in SMTLIB.Tests.TestTheory]
rank_f_f [constructor, in SMTLIB.Tests.TestTheory]
rank_uninterp [inductive, in SMTLIB.Tests.TestTheory]
Rcmp [abbreviation, in SMTLIB.Theory.Reals_Ints]
reals_ints_interp_models [lemma, in SMTLIB.Theory.Reals_Ints]
reals_ints_interp [definition, in SMTLIB.Theory.Reals_Ints]
Reals_IntsInterpretable.HR [variable, in SMTLIB.Theory.Reals_Ints]
Reals_IntsInterpretable.HZ [variable, in SMTLIB.Theory.Reals_Ints]
Reals_IntsInterpretable.Hmap [variable, in SMTLIB.Theory.Reals_Ints]
Reals_IntsInterpretable.Hbool [variable, in SMTLIB.Theory.Reals_Ints]
Reals_IntsInterpretable.witness [variable, in SMTLIB.Theory.Reals_Ints]
Reals_IntsInterpretable.D [variable, in SMTLIB.Theory.Reals_Ints]
Reals_IntsInterpretable [section, in SMTLIB.Theory.Reals_Ints]
Reals_IntsModels.domain_σ_real [variable, in SMTLIB.Theory.Reals_Ints]
Reals_IntsModels.domain_σ_int [variable, in SMTLIB.Theory.Reals_Ints]
Reals_IntsModels.A [variable, in SMTLIB.Theory.Reals_Ints]
Reals_IntsModels [section, in SMTLIB.Theory.Reals_Ints]
reals_ints_funcs [definition, in SMTLIB.Theory.Reals_Ints]
Reals_Ints [library]
real_is_int_decision [instance, in SMTLIB.Theory.Reals_Ints]
refl_A_not_well_sorted [lemma, in SMTLIB.Tests.UnitTests]
refl_A [definition, in SMTLIB.Tests.UnitTests]
Rge_decision [instance, in SMTLIB.Theory.Reals_Ints]
Rgt_decision [instance, in SMTLIB.Theory.Reals_Ints]
ri_literals [definition, in SMTLIB.Theory.Reals_Ints]
Rle_decision [instance, in SMTLIB.Theory.Reals_Ints]
Rlt_decision [instance, in SMTLIB.Theory.Reals_Ints]
Rop1 [abbreviation, in SMTLIB.Theory.Reals_Ints]
Rop2 [abbreviation, in SMTLIB.Theory.Reals_Ints]
R_of_Qc [abbreviation, in SMTLIB.Tests.UnitTests]
S
SApp [constructor, in SMTLIB.Symbols]sat [definition, in SMTLIB.Eval]
sat_refl_A [lemma, in SMTLIB.Tests.UnitTests]
sat_ho_app [lemma, in SMTLIB.Tests.UnitTests]
sat_fun_distinct [lemma, in SMTLIB.Tests.UnitTests]
sat_fun_eq [lemma, in SMTLIB.Tests.UnitTests]
sat_excluded_middle_int [lemma, in SMTLIB.Tests.UnitTests]
sat_uninterpreted_f_at_zero_is_four [lemma, in SMTLIB.Tests.UnitTests]
sat_zero_over_zero_is_four [lemma, in SMTLIB.Tests.UnitTests]
sat_zero_over_zero [lemma, in SMTLIB.Tests.UnitTests]
sat_excluded_middle [lemma, in SMTLIB.Tests.UnitTests]
sat_one_plus_one [lemma, in SMTLIB.Tests.UnitTests]
sat_iff_monomorphic_sat [lemma, in SMTLIB.Eval]
sat_of_entails [lemma, in SMTLIB.Tests.TestTheory]
selectors [projection, in SMTLIB.Signature]
selectors_for_constructor_consistent [projection, in SMTLIB.Signature]
selectors_mutually_disj [projection, in SMTLIB.Signature]
selectors_for_constructor_wf [projection, in SMTLIB.Signature]
selectors_for_constructor [projection, in SMTLIB.Signature]
selectors_disj [projection, in SMTLIB.Signature]
selectors_wf [projection, in SMTLIB.Signature]
Seq [library]
SeqAdtConditions [section, in SMTLIB.Theory.Seq]
SeqAdtConditions.A [variable, in SMTLIB.Theory.Seq]
SeqAdtConditions.Hdom [variable, in SMTLIB.Theory.Seq]
SeqAdtConditions.Hlist [variable, in SMTLIB.Theory.Seq]
SeqAdtConditions.Σ [variable, in SMTLIB.Theory.Seq]
SeqAdtInterp [section, in SMTLIB.Theory.Seq]
SeqAdtInterp.base [variable, in SMTLIB.Theory.Seq]
SeqAdtInterp.D [variable, in SMTLIB.Theory.Seq]
SeqAdtInterp.Hbool [variable, in SMTLIB.Theory.Seq]
SeqAdtInterp.Hdom [variable, in SMTLIB.Theory.Seq]
SeqAdtInterp.Hlist [variable, in SMTLIB.Theory.Seq]
SeqAdtInterp.Hmap [variable, in SMTLIB.Theory.Seq]
SeqAdtInterp.Hranks [variable, in SMTLIB.Theory.Seq]
SeqAdtInterp.Hsel_nodup [variable, in SMTLIB.Theory.Seq]
SeqAdtInterp.Hseq_not_adt [variable, in SMTLIB.Theory.Seq]
SeqAdtInterp.Σ [variable, in SMTLIB.Theory.Seq]
SeqEmbedProject [section, in SMTLIB.Theory.Seq]
SeqEmbedProject.A [variable, in SMTLIB.Theory.Seq]
SeqEmbedProject.Hdom [variable, in SMTLIB.Theory.Seq]
SeqEmbedProject.Hlist [variable, in SMTLIB.Theory.Seq]
SeqEmbedProject.Hseq_not_adt [variable, in SMTLIB.Theory.Seq]
SeqEmbedProject.Σ [variable, in SMTLIB.Theory.Seq]
SeqGroundTerm [section, in SMTLIB.Theory.Seq]
SeqGroundTermRect [section, in SMTLIB.Theory.Seq]
SeqGroundTermRect.gen [variable, in SMTLIB.Theory.Seq]
SeqGroundTermRect.Hconstr [variable, in SMTLIB.Theory.Seq]
SeqGroundTermRect.Hgen [variable, in SMTLIB.Theory.Seq]
SeqGroundTermRect.Hseq [variable, in SMTLIB.Theory.Seq]
SeqGroundTermRect.P [variable, in SMTLIB.Theory.Seq]
SeqGroundTermRect.Σ [variable, in SMTLIB.Theory.Seq]
SeqGroundTermSize [section, in SMTLIB.Theory.Seq]
SeqGroundTermSize.gen [variable, in SMTLIB.Theory.Seq]
SeqGroundTermSize.Σ [variable, in SMTLIB.Theory.Seq]
SeqGroundTerm.gen [variable, in SMTLIB.Theory.Seq]
SeqGroundTerm.Σ [variable, in SMTLIB.Theory.Seq]
SeqInterpretable [section, in SMTLIB.Theory.Seq]
SeqInterpretable.D [variable, in SMTLIB.Theory.Seq]
SeqInterpretable.Hbool [variable, in SMTLIB.Theory.Seq]
SeqInterpretable.Hlist [variable, in SMTLIB.Theory.Seq]
SeqInterpretable.Hmap [variable, in SMTLIB.Theory.Seq]
SeqInterpretable.HZ [variable, in SMTLIB.Theory.Seq]
SeqInterpretable.witness [variable, in SMTLIB.Theory.Seq]
SeqModels [section, in SMTLIB.Theory.Seq]
SeqModels.A [variable, in SMTLIB.Theory.Seq]
SeqModels.domain_σ_seq [variable, in SMTLIB.Theory.Seq]
SeqModels.domain_σ_int [variable, in SMTLIB.Theory.Seq]
seq_adt_interpretation_axioms [lemma, in SMTLIB.Theory.Seq]
seq_adt_interpretation_conditions [lemma, in SMTLIB.Theory.Seq]
seq_adt_interpretation_other [lemma, in SMTLIB.Theory.Seq]
seq_constructor_interp_apply [lemma, in SMTLIB.Theory.Seq]
seq_adt_interpretation_tester [lemma, in SMTLIB.Theory.Seq]
seq_adt_interpretation_selector [lemma, in SMTLIB.Theory.Seq]
seq_adt_interpretation_constructor [lemma, in SMTLIB.Theory.Seq]
seq_adt_interpretation [definition, in SMTLIB.Theory.Seq]
seq_tester_interp [definition, in SMTLIB.Theory.Seq]
seq_selector_interp [definition, in SMTLIB.Theory.Seq]
seq_tester_value [definition, in SMTLIB.Theory.Seq]
seq_selector_value [definition, in SMTLIB.Theory.Seq]
seq_constructor_interp [definition, in SMTLIB.Theory.Seq]
seq_constructor_rank_ok [definition, in SMTLIB.Theory.Seq]
seq_adt_interp_constructor_disjoint [lemma, in SMTLIB.Theory.Seq]
seq_adt_axioms [definition, in SMTLIB.Theory.Seq]
seq_adt_interp_tester [projection, in SMTLIB.Theory.Seq]
seq_adt_interp_selector [projection, in SMTLIB.Theory.Seq]
seq_adt_interp_constructor [projection, in SMTLIB.Theory.Seq]
seq_adt_conditions [record, in SMTLIB.Theory.Seq]
seq_adt_constructor_condition [definition, in SMTLIB.Theory.Seq]
seq_ground_term_embed_irrel [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_embed_inj [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_embed_project [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_project_embed [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_project_leaf [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_project_seq [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_project_adt [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_embed_gen [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_embed_adt [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_embed_not_seq [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_embed_seq [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_project [definition, in SMTLIB.Theory.Seq]
seq_ground_term_embed [definition, in SMTLIB.Theory.Seq]
seq_ground_term_leaf [definition, in SMTLIB.Theory.Seq]
seq_domain_gen [definition, in SMTLIB.Theory.Seq]
seq_ground_term_size_SGConstr [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_size_SGSeq [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_size [definition, in SMTLIB.Theory.Seq]
seq_ground_term_ind [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_rect [definition, in SMTLIB.Theory.Seq]
seq_ground_term_constructor_Some [lemma, in SMTLIB.Theory.Seq]
seq_ground_term_constructor [definition, in SMTLIB.Theory.Seq]
seq_ground_term [inductive, in SMTLIB.Theory.Seq]
seq_embeddable_sort_app_nil [lemma, in SMTLIB.Theory.Seq]
seq_embeddable_sort_elem [lemma, in SMTLIB.Theory.Seq]
seq_embeddable_seq [lemma, in SMTLIB.Theory.Seq]
seq_embeddable_leaf [lemma, in SMTLIB.Theory.Seq]
seq_embeddable_sort_dec [instance, in SMTLIB.Theory.Seq]
seq_embeddable_sort_irrelevant [lemma, in SMTLIB.Theory.Seq]
seq_embeddable_sort [definition, in SMTLIB.Theory.Seq]
seq_embeddableb [definition, in SMTLIB.Theory.Seq]
seq_sorts_not_adt [definition, in SMTLIB.Theory.Seq]
seq_map_has_sort [lemma, in SMTLIB.Theory.Seq]
seq_contains_has_sort [lemma, in SMTLIB.Theory.Seq]
seq_nth_has_sort [lemma, in SMTLIB.Theory.Seq]
seq_len_has_sort [lemma, in SMTLIB.Theory.Seq]
seq_concat_has_sort [lemma, in SMTLIB.Theory.Seq]
seq_unit_has_sort [lemma, in SMTLIB.Theory.Seq]
seq_empty_has_sort [lemma, in SMTLIB.Theory.Seq]
seq_interp [definition, in SMTLIB.Theory.Seq]
seq_map_interp [definition, in SMTLIB.Theory.Seq]
seq_contains_interp [definition, in SMTLIB.Theory.Seq]
seq_nth_interp [definition, in SMTLIB.Theory.Seq]
seq_len_interp [definition, in SMTLIB.Theory.Seq]
seq_concat_interp [definition, in SMTLIB.Theory.Seq]
seq_unit_interp [definition, in SMTLIB.Theory.Seq]
seq_empty_interp [definition, in SMTLIB.Theory.Seq]
seq_at_τ_seq [lemma, in SMTLIB.Theory.Seq]
seq_at [definition, in SMTLIB.Theory.Seq]
seq_map [definition, in SMTLIB.Theory.Seq]
seq_contains [definition, in SMTLIB.Theory.Seq]
seq_nth [definition, in SMTLIB.Theory.Seq]
seq_len [definition, in SMTLIB.Theory.Seq]
seq_concat [definition, in SMTLIB.Theory.Seq]
seq_unit [definition, in SMTLIB.Theory.Seq]
seq_empty [definition, in SMTLIB.Theory.Seq]
seq_funcs [definition, in SMTLIB.Theory.Seq]
set_map_term_subst_insert_zip_TFVar [lemma, in SMTLIB.Term]
set_map_term_subst_zip_id [lemma, in SMTLIB.Term]
set_map_term_subst_TFVar_id [lemma, in SMTLIB.Term]
SGConstr [constructor, in SMTLIB.Theory.Seq]
SGGen [constructor, in SMTLIB.Theory.Seq]
SGSeq [constructor, in SMTLIB.Theory.Seq]
signature [record, in SMTLIB.Signature]
Signature [library]
signatures_agree_except_sorts_add_sorts_mono [lemma, in SMTLIB.Signature]
signatures_agree_except_sorts_insert_mono [lemma, in SMTLIB.Signature]
signatures_agree_except_sorts_add_sorts [lemma, in SMTLIB.Signature]
signatures_agree_except_sorts_insert [lemma, in SMTLIB.Signature]
signatures_agree_except_sorts_with_sorts [lemma, in SMTLIB.Signature]
signatures_agree_except_sorts_trans [lemma, in SMTLIB.Signature]
signatures_agree_except_sorts_sym [lemma, in SMTLIB.Signature]
signatures_agree_except_sorts_refl [lemma, in SMTLIB.Signature]
signatures_agree_except_sorts_rank [projection, in SMTLIB.Signature]
signatures_agree_except_sorts_constructor_for_tester [projection, in SMTLIB.Signature]
signatures_agree_except_sorts_tester_for_constructor [projection, in SMTLIB.Signature]
signatures_agree_except_sorts_selectors_for_constructor [projection, in SMTLIB.Signature]
signatures_agree_except_sorts_arity [projection, in SMTLIB.Signature]
signatures_agree_except_sorts_constructors_for_sort [projection, in SMTLIB.Signature]
signatures_agree_except_sorts_testers [projection, in SMTLIB.Signature]
signatures_agree_except_sorts_selectors [projection, in SMTLIB.Signature]
signatures_agree_except_sorts_constructors [projection, in SMTLIB.Signature]
signatures_agree_except_sorts_funcs [projection, in SMTLIB.Signature]
signatures_agree_except_sorts_sort_symbols [projection, in SMTLIB.Signature]
signatures_agree_except_sorts [record, in SMTLIB.Signature]
signatures_composable [record, in SMTLIB.Signature]
signature_add_sorts_adt [lemma, in SMTLIB.Signature]
signature_compose_adt_right [lemma, in SMTLIB.Signature]
signature_compose_adt_left [lemma, in SMTLIB.Signature]
signature_compose_tester_for_constructor_right [lemma, in SMTLIB.Signature]
signature_compose_selectors_for_constructor_right [lemma, in SMTLIB.Signature]
signature_compose_constructors_for_sort_right [lemma, in SMTLIB.Signature]
signature_compose_constructors_for_sort_left [lemma, in SMTLIB.Signature]
signature_lookup_add_sorts [lemma, in SMTLIB.Signature]
signature_lookup_with_sorts [lemma, in SMTLIB.Signature]
signature_add_sorts_sorts [lemma, in SMTLIB.Signature]
signature_insert_sorts [lemma, in SMTLIB.Signature]
signature_lookup_insert_ne [lemma, in SMTLIB.Signature]
signature_lookup_insert_eq [lemma, in SMTLIB.Signature]
signature_insert [instance, in SMTLIB.Signature]
signature_lookup [instance, in SMTLIB.Signature]
signature_add_sorts [definition, in SMTLIB.Signature]
signature_with_sorts [definition, in SMTLIB.Signature]
signature_compose_extends_rank_right [lemma, in SMTLIB.Signature]
signature_compose_extends_rank_left [lemma, in SMTLIB.Signature]
signature_compose_signature_expansion_right [lemma, in SMTLIB.Signature]
signature_compose_signature_expansion_left [lemma, in SMTLIB.Signature]
signature_compose_sort_wf_right [lemma, in SMTLIB.Signature]
signature_compose_sort_wf_left [lemma, in SMTLIB.Signature]
signature_compose_compose [instance, in SMTLIB.Signature]
signature_compose [definition, in SMTLIB.Signature]
signature_expansion_rank [projection, in SMTLIB.Signature]
signature_expansion_sorts [projection, in SMTLIB.Signature]
signature_expansion_tester_for_constructor [projection, in SMTLIB.Signature]
signature_expansion_selectors_for_constructor [projection, in SMTLIB.Signature]
signature_expansion_constructors [projection, in SMTLIB.Signature]
signature_expansion_constructors_for_sort [projection, in SMTLIB.Signature]
signature_expansion_arity [projection, in SMTLIB.Signature]
signature_expansion_funcs [projection, in SMTLIB.Signature]
signature_expansion_sort_symbols [projection, in SMTLIB.Signature]
signature_expansion [record, in SMTLIB.Signature]
size_list_to_set_le [lemma, in SMTLIB.Utils]
slash_free [definition, in SMTLIB.Theory.Reals_Ints]
smt_compose [projection, in SMTLIB.Signature]
smt_compose [constructor, in SMTLIB.Signature]
smt_mod_pos [lemma, in SMTLIB.Theory.Reals_Ints]
smt_mod [definition, in SMTLIB.Theory.Reals_Ints]
smt_div_pos [lemma, in SMTLIB.Theory.Reals_Ints]
smt_div [definition, in SMTLIB.Theory.Reals_Ints]
sort [inductive, in SMTLIB.Symbols]
sorting [abbreviation, in SMTLIB.Signature]
Sorting [library]
sortparam [abbreviation, in SMTLIB.Symbols]
sorts [projection, in SMTLIB.Signature]
sortsymb [abbreviation, in SMTLIB.Symbols]
sorts_consistent [projection, in SMTLIB.Signature]
sort_wf_with_sorts [lemma, in SMTLIB.Signature]
sort_wf_add_sorts [lemma, in SMTLIB.Signature]
sort_wf_signatures_agree_except_sorts [lemma, in SMTLIB.Signature]
sort_wf_inherit_right [lemma, in SMTLIB.Signature]
sort_wf_inherit_left [lemma, in SMTLIB.Signature]
sort_wf_extends [projection, in SMTLIB.Signature]
sort_wf_signature_expansion [lemma, in SMTLIB.Signature]
sort_wf_σ_bool [lemma, in SMTLIB.Signature]
sort_wf [definition, in SMTLIB.Signature]
sort_symbols_wf [projection, in SMTLIB.Signature]
sort_symbols [projection, in SMTLIB.Signature]
sort_wf_Σ_test_σ_int [lemma, in SMTLIB.Tests.TestTheory]
sort_subst_eq_subset [lemma, in SMTLIB.Symbols]
sort_subst_eq_param_agree [lemma, in SMTLIB.Symbols]
sort_subst_empty [lemma, in SMTLIB.Symbols]
sort_subst [definition, in SMTLIB.Symbols]
sort_subst_map_monomorphic [definition, in SMTLIB.Symbols]
sort_subst_map [abbreviation, in SMTLIB.Symbols]
sort_wf_base_dec [instance, in SMTLIB.Symbols]
sort_wf_base_sind [definition, in SMTLIB.Symbols]
sort_wf_base_ind [definition, in SMTLIB.Symbols]
sort_wf_base [inductive, in SMTLIB.Symbols]
sort_top_symbol [definition, in SMTLIB.Symbols]
sort_params [definition, in SMTLIB.Symbols]
sort_countable [instance, in SMTLIB.Symbols]
sort_gen_tree_cancel [lemma, in SMTLIB.Symbols]
sort_to_gen_tree [definition, in SMTLIB.Symbols]
sort_eq_decision [instance, in SMTLIB.Symbols]
sort_rec [definition, in SMTLIB.Symbols]
sort_rect [definition, in SMTLIB.Symbols]
sort_rect.HP_SApp [variable, in SMTLIB.Symbols]
sort_rect.HP_SParam [variable, in SMTLIB.Symbols]
sort_rect.P [variable, in SMTLIB.Symbols]
sort_rect [section, in SMTLIB.Symbols]
sort_ind [definition, in SMTLIB.Symbols]
sort_ind.HP_SApp [variable, in SMTLIB.Symbols]
sort_ind.HP_SParam [variable, in SMTLIB.Symbols]
sort_ind.P [variable, in SMTLIB.Symbols]
sort_ind [section, in SMTLIB.Symbols]
sort_domain_witness [definition, in SMTLIB.Domain]
sort_domain_adt [lemma, in SMTLIB.Domain]
sort_domain_τ_seq [lemma, in SMTLIB.Domain]
sort_domain_τ_map [lemma, in SMTLIB.Domain]
sort_domain_base [lemma, in SMTLIB.Domain]
sort_domain_adt_free [lemma, in SMTLIB.Domain]
sort_domain [definition, in SMTLIB.Domain]
SParam [constructor, in SMTLIB.Symbols]
Strings [library]
StringsInterpretable [section, in SMTLIB.Theory.Strings]
StringsInterpretable.D [variable, in SMTLIB.Theory.Strings]
StringsInterpretable.Hbool [variable, in SMTLIB.Theory.Strings]
StringsInterpretable.Hint [variable, in SMTLIB.Theory.Strings]
StringsInterpretable.Hmap [variable, in SMTLIB.Theory.Strings]
StringsInterpretable.Hstring [variable, in SMTLIB.Theory.Strings]
StringsInterpretable.witness [variable, in SMTLIB.Theory.Strings]
StringsModels [section, in SMTLIB.Theory.Strings]
StringsModels.A [variable, in SMTLIB.Theory.Strings]
StringsModels.domain_σ_int [variable, in SMTLIB.Theory.Strings]
StringsModels.domain_σ_string [variable, in SMTLIB.Theory.Strings]
strings_interp [definition, in SMTLIB.Theory.Strings]
strings_funcs [definition, in SMTLIB.Theory.Strings]
string_literal_has_sort [lemma, in SMTLIB.Theory.Strings]
string_literals_dec [instance, in SMTLIB.Theory.Strings]
string_occurs_quote_escape_string [lemma, in SMTLIB.Theory.Strings]
string_occurs_quote_escape_ascii [lemma, in SMTLIB.Theory.Strings]
string_literals [definition, in SMTLIB.Theory.Strings]
string_literal [definition, in SMTLIB.Theory.Strings]
string_occurs_pretty_Z [lemma, in SMTLIB.Utils]
string_occurs_pretty_N [lemma, in SMTLIB.Utils]
string_occurs_pretty_N_go [lemma, in SMTLIB.Utils]
string_split_at_app [lemma, in SMTLIB.Utils]
string_split_at [definition, in SMTLIB.Utils]
string_occurs [definition, in SMTLIB.Utils]
string_strip_prefix_app [lemma, in SMTLIB.Utils]
string_strip_prefix [definition, in SMTLIB.Utils]
string_app_inj_tail [lemma, in SMTLIB.Utils]
string_length_append [lemma, in SMTLIB.Utils]
structure [record, in SMTLIB.Theory]
Structure [section, in SMTLIB.Theory]
structure_of [definition, in SMTLIB.Theory]
Structure.EmbedProject [section, in SMTLIB.Theory]
Structure.EmbedProject.A [variable, in SMTLIB.Theory]
Structure.EmbedProject.Hdom [variable, in SMTLIB.Theory]
Structure.Σ [variable, in SMTLIB.Theory]
str_lt_has_sort [lemma, in SMTLIB.Theory.Strings]
str_len_has_sort [lemma, in SMTLIB.Theory.Strings]
str_concat_has_sort [lemma, in SMTLIB.Theory.Strings]
sub_term [definition, in SMTLIB.Term]
sub_sort [definition, in SMTLIB.Symbols]
symbol [abbreviation, in SMTLIB.Symbols]
Symbols [library]
s_string [definition, in SMTLIB.Theory.Strings]
s_real [definition, in SMTLIB.Theory.Reals_Ints]
s_int [definition, in SMTLIB.Theory.Reals_Ints]
s_seq [definition, in SMTLIB.Theory.Seq]
S_TMatch_PVar [constructor, in SMTLIB.Sorting]
S_TMatch_PApp [constructor, in SMTLIB.Sorting]
S_TLet [constructor, in SMTLIB.Sorting]
S_TForall [constructor, in SMTLIB.Sorting]
S_TExists [constructor, in SMTLIB.Sorting]
S_TLambda [constructor, in SMTLIB.Sorting]
S_TApp_annotated [constructor, in SMTLIB.Sorting]
S_TApp [constructor, in SMTLIB.Sorting]
S_TFVar [constructor, in SMTLIB.Sorting]
s_map [definition, in SMTLIB.Symbols]
s_bool [definition, in SMTLIB.Symbols]
T
TApp [constructor, in SMTLIB.Term]TBVar [constructor, in SMTLIB.Term]
term [inductive, in SMTLIB.Term]
Term [library]
term_sort_subst_at_most_two [lemma, in SMTLIB.Tests.UnitTests]
term_subst_ands [lemma, in SMTLIB.Theory.Core]
term_sort_subst_empty [lemma, in SMTLIB.Term]
term_sort_subst [definition, in SMTLIB.Term]
term_open_close_as_open_subst [lemma, in SMTLIB.Term]
term_open_close_subst1_nil [lemma, in SMTLIB.Term]
term_open_close_subst1 [lemma, in SMTLIB.Term]
term_open_close_subst_nil [lemma, in SMTLIB.Term]
term_open_close_subst [lemma, in SMTLIB.Term]
term_subst_singleton_open_TFVar1_comm [lemma, in SMTLIB.Term]
term_subst_singleton_open_TFVar_comm [lemma, in SMTLIB.Term]
term_subst_open_TFVar_rename [lemma, in SMTLIB.Term]
term_subst_open_TFVar_comm [lemma, in SMTLIB.Term]
term_subst_open [lemma, in SMTLIB.Term]
term_subst_insert_zip_TFVar [lemma, in SMTLIB.Term]
term_subst_insert [lemma, in SMTLIB.Term]
term_subst_subst_fresh_singleton [lemma, in SMTLIB.Term]
term_subst_subst_fresh [lemma, in SMTLIB.Term]
term_subst_subst [lemma, in SMTLIB.Term]
term_subst_ext [lemma, in SMTLIB.Term]
term_subst_fresh_singleton [lemma, in SMTLIB.Term]
term_subst_fresh [lemma, in SMTLIB.Term]
term_subst_id_singleton [lemma, in SMTLIB.Term]
term_subst_id_zip [lemma, in SMTLIB.Term]
term_subst_id [lemma, in SMTLIB.Term]
term_open_close_comm [lemma, in SMTLIB.Term]
term_close_fresh [lemma, in SMTLIB.Term]
term_close_nth_TFVar [lemma, in SMTLIB.Term]
term_size_term_open_TFVar [lemma, in SMTLIB.Term]
term_open_comm [lemma, in SMTLIB.Term]
term_open_lem [lemma, in SMTLIB.Term]
term_open_nth_TFVar [lemma, in SMTLIB.Term]
term_subst [definition, in SMTLIB.Term]
term_close [definition, in SMTLIB.Term]
term_open [definition, in SMTLIB.Term]
term_size_cases [lemma, in SMTLIB.Term]
term_size_list [lemma, in SMTLIB.Term]
term_size [definition, in SMTLIB.Term]
term_countable [instance, in SMTLIB.Term]
term_encode_decode [lemma, in SMTLIB.Term]
term_decode_encode_app [lemma, in SMTLIB.Term]
term_decode_encode_list [lemma, in SMTLIB.Term]
term_encode_bind_snd [lemma, in SMTLIB.Term]
term_decode [definition, in SMTLIB.Term]
term_encode [definition, in SMTLIB.Term]
term_eq_decision [instance, in SMTLIB.Term]
term_rec [definition, in SMTLIB.Term]
term_rect [definition, in SMTLIB.Term]
term_rect.HP_Match [variable, in SMTLIB.Term]
term_rect.HP_Let [variable, in SMTLIB.Term]
term_rect.HP_Forall [variable, in SMTLIB.Term]
term_rect.HP_Exists [variable, in SMTLIB.Term]
term_rect.HP_Fun [variable, in SMTLIB.Term]
term_rect.HP_App [variable, in SMTLIB.Term]
term_rect.HP_BVar [variable, in SMTLIB.Term]
term_rect.HP_FVar [variable, in SMTLIB.Term]
term_rect.P [variable, in SMTLIB.Term]
term_rect [section, in SMTLIB.Term]
term_ind [definition, in SMTLIB.Term]
term_ind.HP_Match [variable, in SMTLIB.Term]
term_ind.HP_Let [variable, in SMTLIB.Term]
term_ind.HP_Forall [variable, in SMTLIB.Term]
term_ind.HP_Exists [variable, in SMTLIB.Term]
term_ind.HP_App [variable, in SMTLIB.Term]
term_ind.HP_Fun [variable, in SMTLIB.Term]
term_ind.HP_BVar [variable, in SMTLIB.Term]
term_ind.HP_FVar [variable, in SMTLIB.Term]
term_ind.P [variable, in SMTLIB.Term]
term_ind [section, in SMTLIB.Term]
term_has_sort_term_open_term_close1 [lemma, in SMTLIB.Sorting]
term_has_sort_term_open_term_close [lemma, in SMTLIB.Sorting]
term_has_sort_term_subst1 [lemma, in SMTLIB.Sorting]
term_has_sort_rename [lemma, in SMTLIB.Sorting]
term_has_sort_term_subst_fv [lemma, in SMTLIB.Sorting]
term_has_sort_term_subst [lemma, in SMTLIB.Sorting]
term_has_sort_pars_empty [lemma, in SMTLIB.Sorting]
term_has_sort_map_TFVar_lookup [lemma, in SMTLIB.Sorting]
term_has_sort_fv_subseteq_dom [lemma, in SMTLIB.Sorting]
term_has_sort_fv_lookup [lemma, in SMTLIB.Sorting]
term_has_sort_lc [lemma, in SMTLIB.Sorting]
term_has_sort_strengthen1 [lemma, in SMTLIB.Sorting]
term_has_sort_strengthen [lemma, in SMTLIB.Sorting]
term_has_sort_weaken1 [lemma, in SMTLIB.Sorting]
term_has_sort_weaken [lemma, in SMTLIB.Sorting]
term_has_sort_add_sorts_with_sorts [lemma, in SMTLIB.Sorting]
term_has_sort_insert_with_sorts [lemma, in SMTLIB.Sorting]
term_has_sort_sorts_eq [lemma, in SMTLIB.Sorting]
term_has_sort_cong [lemma, in SMTLIB.Sorting]
term_has_sort_sind [definition, in SMTLIB.Sorting]
term_has_sort_ind [definition, in SMTLIB.Sorting]
term_has_sort [inductive, in SMTLIB.Sorting]
testers [projection, in SMTLIB.Signature]
testers_mutually_disj [projection, in SMTLIB.Signature]
testers_disj [projection, in SMTLIB.Signature]
testers_wf [projection, in SMTLIB.Signature]
tester_for_constructor_consistent [projection, in SMTLIB.Signature]
tester_constructor_bijection [projection, in SMTLIB.Signature]
tester_for_constructor_wf [projection, in SMTLIB.Signature]
tester_for_constructor [projection, in SMTLIB.Signature]
TestTheory [library]
test_interp [definition, in SMTLIB.Tests.TestTheory]
test_witness [definition, in SMTLIB.Tests.TestTheory]
test_base_witness [definition, in SMTLIB.Tests.TestTheory]
test_base [definition, in SMTLIB.Tests.TestTheory]
TExists [constructor, in SMTLIB.Term]
TExistss [definition, in SMTLIB.Term]
TForall [constructor, in SMTLIB.Term]
TFVar [constructor, in SMTLIB.Term]
theory [record, in SMTLIB.Theory]
Theory [library]
theory_init [definition, in SMTLIB.Theory]
theory_init_seq [definition, in SMTLIB.Theory.Seq]
times_has_sort_real [lemma, in SMTLIB.Theory.Reals_Ints]
times_has_sort_int [lemma, in SMTLIB.Theory.Reals_Ints]
times_ [definition, in SMTLIB.Theory.Reals_Ints]
TLambda [constructor, in SMTLIB.Term]
TLet [constructor, in SMTLIB.Term]
TMatch [constructor, in SMTLIB.Term]
to_int_has_sort [lemma, in SMTLIB.Theory.Reals_Ints]
to_real_has_sort [lemma, in SMTLIB.Theory.Reals_Ints]
to_int [definition, in SMTLIB.Theory.Reals_Ints]
to_real [definition, in SMTLIB.Theory.Reals_Ints]
true_has_sort [lemma, in SMTLIB.Theory.Core]
true_ [definition, in SMTLIB.Theory.Core]
T_strings_interpretable [lemma, in SMTLIB.Theory.Strings]
T_strings_local [lemma, in SMTLIB.Theory.Strings]
T_strings [definition, in SMTLIB.Theory.Strings]
T_core_interpretable [lemma, in SMTLIB.Theory.Core]
T_core_local [lemma, in SMTLIB.Theory.Core]
T_core [definition, in SMTLIB.Theory.Core]
T_reals_ints_interpretable [lemma, in SMTLIB.Theory.Reals_Ints]
T_reals_ints_local [lemma, in SMTLIB.Theory.Reals_Ints]
T_reals_ints [definition, in SMTLIB.Theory.Reals_Ints]
T_ho_core_interpretable [lemma, in SMTLIB.Theory.HO_Core]
T_ho_core_local [lemma, in SMTLIB.Theory.HO_Core]
T_ho_core [definition, in SMTLIB.Theory.HO_Core]
T_seq_interpretable [lemma, in SMTLIB.Theory.Seq]
T_seq_local [lemma, in SMTLIB.Theory.Seq]
T_seq [definition, in SMTLIB.Theory.Seq]
T_ho [definition, in SMTLIB.Tests.TestTheory]
T_ho_pre [definition, in SMTLIB.Tests.TestTheory]
T_test_consistent [lemma, in SMTLIB.Tests.TestTheory]
T_test [definition, in SMTLIB.Tests.TestTheory]
T_arith [definition, in SMTLIB.Tests.TestTheory]
T_uninterp [definition, in SMTLIB.Tests.TestTheory]
U
unescape_escape_string [lemma, in SMTLIB.Theory.Strings]unescape_string [definition, in SMTLIB.Theory.Strings]
uninterpreted_f_at_zero_has_sort [lemma, in SMTLIB.Tests.UnitTests]
uninterp_f [definition, in SMTLIB.Tests.TestTheory]
union_lookup_list_to_map_agree [lemma, in SMTLIB.Sorting]
UnitTests [library]
Utils [library]
u_B [definition, in SMTLIB.Symbols]
u_A [definition, in SMTLIB.Symbols]
V
valid_refl_A [lemma, in SMTLIB.Tests.UnitTests]valid_ho_app [lemma, in SMTLIB.Tests.UnitTests]
valid_ho_ext [lemma, in SMTLIB.Tests.UnitTests]
valid_fun_ext [lemma, in SMTLIB.Tests.UnitTests]
valid_excluded_middle_int [lemma, in SMTLIB.Tests.UnitTests]
valid_excluded_middle [lemma, in SMTLIB.Tests.UnitTests]
valid_one_plus_one [lemma, in SMTLIB.Tests.UnitTests]
valuation [abbreviation, in SMTLIB.Eval]
valuation_sorting_lookup [lemma, in SMTLIB.Eval]
valuation_sorting_insert [lemma, in SMTLIB.Eval]
valuation_well_sorted_refl [lemma, in SMTLIB.Eval]
valuation_well_sorted_union_lookup_list_to_map [lemma, in SMTLIB.Eval]
valuation_well_sorted_insert [lemma, in SMTLIB.Eval]
valuation_well_sorted_lookup [lemma, in SMTLIB.Eval]
valuation_well_sorted [definition, in SMTLIB.Eval]
valuation_sorting [definition, in SMTLIB.Eval]
var [abbreviation, in SMTLIB.Symbols]
V_ho [definition, in SMTLIB.Tests.UnitTests]
V_free [definition, in SMTLIB.Tests.TestTheory]
W
wf_sub_term [lemma, in SMTLIB.Term]WF_SApp [constructor, in SMTLIB.Symbols]
WF_SParam [constructor, in SMTLIB.Symbols]
wf_sub_sort [lemma, in SMTLIB.Symbols]
WhereTheFreedomIs [section, in SMTLIB.Tests.TestTheory]
WhereTheFreedomIs.d [variable, in SMTLIB.Tests.TestTheory]
WhereTheFreedomIs.k [variable, in SMTLIB.Tests.TestTheory]
X
xor_has_sort [lemma, in SMTLIB.Theory.Core]xor_ [definition, in SMTLIB.Theory.Core]
Z
Zcmp [abbreviation, in SMTLIB.Theory.Reals_Ints]Zdivide_decision [instance, in SMTLIB.Theory.Reals_Ints]
zero_over_zero_has_sort [lemma, in SMTLIB.Tests.UnitTests]
zero_real [definition, in SMTLIB.Theory.Reals_Ints]
zero_int [definition, in SMTLIB.Theory.Reals_Ints]
Zop1 [abbreviation, in SMTLIB.Theory.Reals_Ints]
Zop2 [abbreviation, in SMTLIB.Theory.Reals_Ints]
other
_ ⊨[ _ ] _ (smt_scope) [notation, in SMTLIB.Eval]_ ⊑ _ (smt_scope) [notation, in SMTLIB.Signature]
_ ⊢p _ : _ (smt_scope) [notation, in SMTLIB.Sorting]
_ ⊢ _ : _ (smt_scope) [notation, in SMTLIB.Sorting]
_ `infix_of` _ (stdpp_scope) [notation, in SMTLIB.Utils]
_ ≅ _ (type_scope) [notation, in SMTLIB.Utils]
_ ⊍ _ [notation, in SMTLIB.Signature]
_ ⊕[ _ ] _ [notation, in SMTLIB.Signature]
⟦ _ : _ ⟧*( _ , _ , _ ) ⇓ _ [notation, in SMTLIB.Eval]
⟦ _ : _ ⟧( _ , _ , _ ) ⇓ _ [notation, in SMTLIB.Eval]
Σ [projection, in SMTLIB.Theory]
Σ_strings [definition, in SMTLIB.Theory.Strings]
Σ_core [definition, in SMTLIB.Theory.Core]
Σ_reals_ints [definition, in SMTLIB.Theory.Reals_Ints]
Σ_ho_core [definition, in SMTLIB.Theory.HO_Core]
Σ_seq [definition, in SMTLIB.Theory.Seq]
Σ_ho_no_adt [lemma, in SMTLIB.Tests.TestTheory]
Σ_ho_core_extends_Σ_ho [lemma, in SMTLIB.Tests.TestTheory]
Σ_core_extends_Σ_ho [lemma, in SMTLIB.Tests.TestTheory]
Σ_ho [definition, in SMTLIB.Tests.TestTheory]
Σ_core_Σ_ho_core_composable [lemma, in SMTLIB.Tests.TestTheory]
Σ_test_no_adt [lemma, in SMTLIB.Tests.TestTheory]
Σ_reals_ints_extends_Σ_test [lemma, in SMTLIB.Tests.TestTheory]
Σ_core_extends_Σ_test [lemma, in SMTLIB.Tests.TestTheory]
Σ_uninterp_extends_Σ_test [lemma, in SMTLIB.Tests.TestTheory]
Σ_arith_extends_Σ_test [lemma, in SMTLIB.Tests.TestTheory]
Σ_reals_ints_extends_Σ_arith [lemma, in SMTLIB.Tests.TestTheory]
Σ_core_extends_Σ_arith [lemma, in SMTLIB.Tests.TestTheory]
Σ_test [definition, in SMTLIB.Tests.TestTheory]
Σ_arith_Σ_uninterp_composable [lemma, in SMTLIB.Tests.TestTheory]
Σ_core_Σ_reals_ints_composable [lemma, in SMTLIB.Tests.TestTheory]
Σ_uninterp [definition, in SMTLIB.Tests.TestTheory]
σ_string [definition, in SMTLIB.Theory.Strings]
σ_real [definition, in SMTLIB.Theory.Reals_Ints]
σ_int [definition, in SMTLIB.Theory.Reals_Ints]
σ_bool [definition, in SMTLIB.Symbols]
τ_seq [definition, in SMTLIB.Theory.Seq]
τ_B [definition, in SMTLIB.Symbols]
τ_A [definition, in SMTLIB.Symbols]
τ_map [definition, in SMTLIB.Symbols]
Notation Index
other
_ ⊨[ _ ] _ (smt_scope) [in SMTLIB.Eval]_ ⊑ _ (smt_scope) [in SMTLIB.Signature]
_ ⊢p _ : _ (smt_scope) [in SMTLIB.Sorting]
_ ⊢ _ : _ (smt_scope) [in SMTLIB.Sorting]
_ `infix_of` _ (stdpp_scope) [in SMTLIB.Utils]
_ ≅ _ (type_scope) [in SMTLIB.Utils]
_ ⊍ _ [in SMTLIB.Signature]
_ ⊕[ _ ] _ [in SMTLIB.Signature]
⟦ _ : _ ⟧*( _ , _ , _ ) ⇓ _ [in SMTLIB.Eval]
⟦ _ : _ ⟧( _ , _ , _ ) ⇓ _ [in SMTLIB.Eval]
Variable Index
B
BuildInterp.D [in SMTLIB.Theory]C
CoreInterpretable.D [in SMTLIB.Theory.Core]CoreInterpretable.Hbool [in SMTLIB.Theory.Core]
CoreInterpretable.witness [in SMTLIB.Theory.Core]
CoreModels.A [in SMTLIB.Theory.Core]
D
DomainConstruction.base [in SMTLIB.Domain]DomainConstruction.base_witness [in SMTLIB.Domain]
DomainConstruction.Σ [in SMTLIB.Domain]
G
GroundTermRect.gen [in SMTLIB.Theory]GroundTermRect.Hconstr [in SMTLIB.Theory]
GroundTermRect.Hgen [in SMTLIB.Theory]
GroundTermRect.P [in SMTLIB.Theory]
GroundTermRect.Σ [in SMTLIB.Theory]
GroundTerm.gen [in SMTLIB.Theory]
GroundTerm.Σ [in SMTLIB.Theory]
H
HO_CoreInterpretable.Hmap [in SMTLIB.Theory.HO_Core]HO_CoreInterpretable.Hbool [in SMTLIB.Theory.HO_Core]
HO_CoreInterpretable.witness [in SMTLIB.Theory.HO_Core]
HO_CoreInterpretable.D [in SMTLIB.Theory.HO_Core]
HO_CoreModels.A [in SMTLIB.Theory.HO_Core]
I
Interpretation.domain [in SMTLIB.Theory]Inversion.A [in SMTLIB.Eval]
Inversion.Σ [in SMTLIB.Eval]
R
Reals_IntsInterpretable.HR [in SMTLIB.Theory.Reals_Ints]Reals_IntsInterpretable.HZ [in SMTLIB.Theory.Reals_Ints]
Reals_IntsInterpretable.Hmap [in SMTLIB.Theory.Reals_Ints]
Reals_IntsInterpretable.Hbool [in SMTLIB.Theory.Reals_Ints]
Reals_IntsInterpretable.witness [in SMTLIB.Theory.Reals_Ints]
Reals_IntsInterpretable.D [in SMTLIB.Theory.Reals_Ints]
Reals_IntsModels.domain_σ_real [in SMTLIB.Theory.Reals_Ints]
Reals_IntsModels.domain_σ_int [in SMTLIB.Theory.Reals_Ints]
Reals_IntsModels.A [in SMTLIB.Theory.Reals_Ints]
S
SeqAdtConditions.A [in SMTLIB.Theory.Seq]SeqAdtConditions.Hdom [in SMTLIB.Theory.Seq]
SeqAdtConditions.Hlist [in SMTLIB.Theory.Seq]
SeqAdtConditions.Σ [in SMTLIB.Theory.Seq]
SeqAdtInterp.base [in SMTLIB.Theory.Seq]
SeqAdtInterp.D [in SMTLIB.Theory.Seq]
SeqAdtInterp.Hbool [in SMTLIB.Theory.Seq]
SeqAdtInterp.Hdom [in SMTLIB.Theory.Seq]
SeqAdtInterp.Hlist [in SMTLIB.Theory.Seq]
SeqAdtInterp.Hmap [in SMTLIB.Theory.Seq]
SeqAdtInterp.Hranks [in SMTLIB.Theory.Seq]
SeqAdtInterp.Hsel_nodup [in SMTLIB.Theory.Seq]
SeqAdtInterp.Hseq_not_adt [in SMTLIB.Theory.Seq]
SeqAdtInterp.Σ [in SMTLIB.Theory.Seq]
SeqEmbedProject.A [in SMTLIB.Theory.Seq]
SeqEmbedProject.Hdom [in SMTLIB.Theory.Seq]
SeqEmbedProject.Hlist [in SMTLIB.Theory.Seq]
SeqEmbedProject.Hseq_not_adt [in SMTLIB.Theory.Seq]
SeqEmbedProject.Σ [in SMTLIB.Theory.Seq]
SeqGroundTermRect.gen [in SMTLIB.Theory.Seq]
SeqGroundTermRect.Hconstr [in SMTLIB.Theory.Seq]
SeqGroundTermRect.Hgen [in SMTLIB.Theory.Seq]
SeqGroundTermRect.Hseq [in SMTLIB.Theory.Seq]
SeqGroundTermRect.P [in SMTLIB.Theory.Seq]
SeqGroundTermRect.Σ [in SMTLIB.Theory.Seq]
SeqGroundTermSize.gen [in SMTLIB.Theory.Seq]
SeqGroundTermSize.Σ [in SMTLIB.Theory.Seq]
SeqGroundTerm.gen [in SMTLIB.Theory.Seq]
SeqGroundTerm.Σ [in SMTLIB.Theory.Seq]
SeqInterpretable.D [in SMTLIB.Theory.Seq]
SeqInterpretable.Hbool [in SMTLIB.Theory.Seq]
SeqInterpretable.Hlist [in SMTLIB.Theory.Seq]
SeqInterpretable.Hmap [in SMTLIB.Theory.Seq]
SeqInterpretable.HZ [in SMTLIB.Theory.Seq]
SeqInterpretable.witness [in SMTLIB.Theory.Seq]
SeqModels.A [in SMTLIB.Theory.Seq]
SeqModels.domain_σ_seq [in SMTLIB.Theory.Seq]
SeqModels.domain_σ_int [in SMTLIB.Theory.Seq]
sort_rect.HP_SApp [in SMTLIB.Symbols]
sort_rect.HP_SParam [in SMTLIB.Symbols]
sort_rect.P [in SMTLIB.Symbols]
sort_ind.HP_SApp [in SMTLIB.Symbols]
sort_ind.HP_SParam [in SMTLIB.Symbols]
sort_ind.P [in SMTLIB.Symbols]
StringsInterpretable.D [in SMTLIB.Theory.Strings]
StringsInterpretable.Hbool [in SMTLIB.Theory.Strings]
StringsInterpretable.Hint [in SMTLIB.Theory.Strings]
StringsInterpretable.Hmap [in SMTLIB.Theory.Strings]
StringsInterpretable.Hstring [in SMTLIB.Theory.Strings]
StringsInterpretable.witness [in SMTLIB.Theory.Strings]
StringsModels.A [in SMTLIB.Theory.Strings]
StringsModels.domain_σ_int [in SMTLIB.Theory.Strings]
StringsModels.domain_σ_string [in SMTLIB.Theory.Strings]
Structure.EmbedProject.A [in SMTLIB.Theory]
Structure.EmbedProject.Hdom [in SMTLIB.Theory]
Structure.Σ [in SMTLIB.Theory]
T
term_rect.HP_Match [in SMTLIB.Term]term_rect.HP_Let [in SMTLIB.Term]
term_rect.HP_Forall [in SMTLIB.Term]
term_rect.HP_Exists [in SMTLIB.Term]
term_rect.HP_Fun [in SMTLIB.Term]
term_rect.HP_App [in SMTLIB.Term]
term_rect.HP_BVar [in SMTLIB.Term]
term_rect.HP_FVar [in SMTLIB.Term]
term_rect.P [in SMTLIB.Term]
term_ind.HP_Match [in SMTLIB.Term]
term_ind.HP_Let [in SMTLIB.Term]
term_ind.HP_Forall [in SMTLIB.Term]
term_ind.HP_Exists [in SMTLIB.Term]
term_ind.HP_App [in SMTLIB.Term]
term_ind.HP_Fun [in SMTLIB.Term]
term_ind.HP_BVar [in SMTLIB.Term]
term_ind.HP_FVar [in SMTLIB.Term]
term_ind.P [in SMTLIB.Term]
W
WhereTheFreedomIs.d [in SMTLIB.Tests.TestTheory]WhereTheFreedomIs.k [in SMTLIB.Tests.TestTheory]
Library Index
C
CoreD
DomainE
EvalH
HO_CoreR
Reals_IntsS
SeqSignature
Sorting
Strings
Symbols
T
TermTestTheory
Theory
U
UnitTestsUtils
Lemma Index
A
abs_has_sort [in SMTLIB.Theory.Reals_Ints]adt_interp_tester_false_off_constructor [in SMTLIB.Theory]
adt_constructed_of_adt_axioms [in SMTLIB.Theory]
adt_constructed_signatures_agree_except_sorts [in SMTLIB.Theory]
adt_interp_constructor_disjoint [in SMTLIB.Theory]
adt_interp_tester_at_rank [in SMTLIB.Theory]
adt_signatures_agree_except_sorts [in SMTLIB.Signature]
adt_free_of_embeddable [in SMTLIB.Signature]
adt_free_app_intro [in SMTLIB.Signature]
adt_free_param_intro [in SMTLIB.Signature]
adt_free_not_adt [in SMTLIB.Signature]
adt_free_param_inv [in SMTLIB.Signature]
adt_free_app_inv [in SMTLIB.Signature]
adt_free_app [in SMTLIB.Signature]
adt_free_param [in SMTLIB.Signature]
adt_freeb_args_true [in SMTLIB.Signature]
adt_free_irrelevant [in SMTLIB.Signature]
adt_freeb_args_unfold [in SMTLIB.Signature]
adt_intro [in SMTLIB.Signature]
adt_irrelevant [in SMTLIB.Signature]
adt_of_adt_spec [in SMTLIB.Signature]
adt_spec_of_adt [in SMTLIB.Signature]
adt_constructed_of_seq_adt_axioms [in SMTLIB.Theory.Seq]
ands_has_sort [in SMTLIB.Theory.Core]
and_has_sort [in SMTLIB.Theory.Core]
app_slash [in SMTLIB.Theory.Reals_Ints]
app_empty_l [in SMTLIB.Theory.Reals_Ints]
app_slash_inj [in SMTLIB.Theory.Reals_Ints]
app_has_sort [in SMTLIB.Theory.HO_Core]
at_most_two_has_sort [in SMTLIB.Tests.UnitTests]
A_ho_models [in SMTLIB.Tests.TestTheory]
A_ho_adt_axioms [in SMTLIB.Tests.TestTheory]
A_ho_models_ho_core [in SMTLIB.Tests.TestTheory]
A_ho_models_core [in SMTLIB.Tests.TestTheory]
A_free_models [in SMTLIB.Tests.TestTheory]
A_free_adt_axioms [in SMTLIB.Tests.TestTheory]
A_free_models_reals_ints [in SMTLIB.Tests.TestTheory]
A_free_models_core [in SMTLIB.Tests.TestTheory]
B
bool_has_sort [in SMTLIB.Theory.Core]C
cast_sym_true_neq_false [in SMTLIB.Utils]cast_sym_true_or_false [in SMTLIB.Utils]
cast_cast_sym [in SMTLIB.Utils]
cast_sym_cast [in SMTLIB.Utils]
cast_eq_iff_eq_cast_sym [in SMTLIB.Utils]
cast_sym_inj [in SMTLIB.Tests.TestTheory]
constant_body_printable [in SMTLIB.Theory.Strings]
core_interp_models [in SMTLIB.Theory.Core]
core_interp_ite [in SMTLIB.Theory.Core]
core_interp_distinct [in SMTLIB.Theory.Core]
core_interp_eq [in SMTLIB.Theory.Core]
core_interp_xor [in SMTLIB.Theory.Core]
core_interp_or [in SMTLIB.Theory.Core]
core_interp_and [in SMTLIB.Theory.Core]
core_interp_impl [in SMTLIB.Theory.Core]
core_interp_not [in SMTLIB.Theory.Core]
core_interp_false [in SMTLIB.Theory.Core]
core_interp_true [in SMTLIB.Theory.Core]
core_funcs_ho_core_funcs_disjoint [in SMTLIB.Tests.TestTheory]
core_funcs_reals_ints_funcs_disjoint [in SMTLIB.Tests.TestTheory]
D
decimal_literal_has_sort [in SMTLIB.Theory.Reals_Ints]decimal_literal_value_eq [in SMTLIB.Theory.Reals_Ints]
define_fun_eval_inserts [in SMTLIB.Theory.Core]
define_fun_eval_instantiate_inv [in SMTLIB.Theory.Core]
define_fun_eval_instantiate [in SMTLIB.Theory.Core]
define_fun_eval_intro [in SMTLIB.Theory.Core]
define_fun_intro_forall_telescope [in SMTLIB.Theory.Core]
define_fun_strip_forall_telescope [in SMTLIB.Theory.Core]
define_fun_forall_telescope_lc [in SMTLIB.Theory.Core]
distinct_has_sort [in SMTLIB.Theory.Core]
divisible_has_sort [in SMTLIB.Theory.Reals_Ints]
divisible_value_eq [in SMTLIB.Theory.Reals_Ints]
div_has_sort [in SMTLIB.Theory.Reals_Ints]
div_mod_euclidean [in SMTLIB.Theory.Reals_Ints]
D_test_τ_map [in SMTLIB.Tests.TestTheory]
D_test_σ_real [in SMTLIB.Tests.TestTheory]
D_test_σ_int [in SMTLIB.Tests.TestTheory]
D_test_σ_bool [in SMTLIB.Tests.TestTheory]
E
elem_of_fv_term_open_TFVar1 [in SMTLIB.Term]elem_of_fv_term_open_TFVar [in SMTLIB.Term]
embeddable_sort_app_nil [in SMTLIB.Signature]
embeddable_sort_adt_free [in SMTLIB.Signature]
embeddable_sort_adt [in SMTLIB.Signature]
embeddable_sort_of_seq_embeddable [in SMTLIB.Theory.Seq]
entails_trichotomy [in SMTLIB.Eval]
entails_sat [in SMTLIB.Eval]
entails_iff_monomorphic_entails [in SMTLIB.Eval]
eq_has_sort [in SMTLIB.Theory.Core]
eq_of_existT [in SMTLIB.Utils]
eq_of_heq [in SMTLIB.Utils]
escape_string_inj [in SMTLIB.Theory.Strings]
escape_ascii_head [in SMTLIB.Theory.Strings]
escape_ascii_nonempty [in SMTLIB.Theory.Strings]
escape_string_wf [in SMTLIB.Theory.Strings]
escape_ascii_escaped [in SMTLIB.Theory.Strings]
escape_ascii_plain [in SMTLIB.Theory.Strings]
evals_deterministic [in SMTLIB.Eval]
evals_vals_eq [in SMTLIB.Eval]
evals_sorts_eq [in SMTLIB.Eval]
evals_selector_sorts [in SMTLIB.Eval]
evals_cong_signature [in SMTLIB.Eval]
evals_cong [in SMTLIB.Eval]
evals_map_TFVar_deterministic [in SMTLIB.Eval]
evals_map_TFVar [in SMTLIB.Eval]
evals_intro [in SMTLIB.Eval]
evals_lookup [in SMTLIB.Eval]
evals_nth [in SMTLIB.Eval]
evals_length [in SMTLIB.Eval]
evals_cons_inv [in SMTLIB.Eval]
evals_cons_sigT [in SMTLIB.Eval]
evals_nil_sorts [in SMTLIB.Eval]
eval_at_most_two_body [in SMTLIB.Tests.UnitTests]
eval_app_lambda [in SMTLIB.Tests.UnitTests]
eval_nn_bool [in SMTLIB.Tests.UnitTests]
eval_neg_bool [in SMTLIB.Tests.UnitTests]
eval_id_bool [in SMTLIB.Tests.UnitTests]
eval_lambda_bool [in SMTLIB.Tests.UnitTests]
eval_forall_int_is_zero_false [in SMTLIB.Tests.UnitTests]
eval_total [in SMTLIB.Eval]
eval_total_signatures_agree_except_sorts [in SMTLIB.Eval]
eval_TMatch_total [in SMTLIB.Eval]
eval_term_open_alpha [in SMTLIB.Eval]
eval_term_open_alpha_disjoint [in SMTLIB.Eval]
eval_term_open_close_inserts [in SMTLIB.Eval]
eval_term_subst_TFVar_alpha [in SMTLIB.Eval]
eval_term_subst_TFVar1_alpha_inv [in SMTLIB.Eval]
eval_term_subst_TFVar1_alpha [in SMTLIB.Eval]
eval_term_subst_singleton_insert [in SMTLIB.Eval]
eval_term_subst_singleton_insert_mut_aux [in SMTLIB.Eval]
eval_term_open_alpha1 [in SMTLIB.Eval]
eval_rename [in SMTLIB.Eval]
eval_rename_mut_aux [in SMTLIB.Eval]
eval_TApp_args_value [in SMTLIB.Eval]
eval_deterministic [in SMTLIB.Eval]
eval_deterministic_TMatch [in SMTLIB.Eval]
eval_deterministic_TExists_arm [in SMTLIB.Eval]
eval_deterministic_TLet_arm [in SMTLIB.Eval]
eval_deterministic_TApp_arm_typed [in SMTLIB.Eval]
eval_deterministic_TApp_arm [in SMTLIB.Eval]
eval_deterministic_selector_app_arm [in SMTLIB.Eval]
eval_sort_of_well_sorted [in SMTLIB.Eval]
eval_sort_TMatch_PApp [in SMTLIB.Eval]
eval_sort_TMatch_PVar [in SMTLIB.Eval]
eval_cong_signature [in SMTLIB.Eval]
eval_cong_signature_mut_aux [in SMTLIB.Eval]
eval_strengthen1 [in SMTLIB.Eval]
eval_strengthen [in SMTLIB.Eval]
eval_weaken1 [in SMTLIB.Eval]
eval_weaken [in SMTLIB.Eval]
eval_closed_cong [in SMTLIB.Eval]
eval_cong [in SMTLIB.Eval]
eval_cong_mut_aux [in SMTLIB.Eval]
eval_term_open_map_TFVar [in SMTLIB.Eval]
eval_term_open_map_TFVar_mut_aux [in SMTLIB.Eval]
eval_TLet_NoDup_intro [in SMTLIB.Eval]
eval_value_heq [in SMTLIB.Eval]
eval_inserted_TFVar [in SMTLIB.Eval]
eval_TFVar_has_sort [in SMTLIB.Eval]
eval_TMatch_PApp_inv [in SMTLIB.Eval]
eval_TMatch_PVar_inv [in SMTLIB.Eval]
eval_TMatch_nil_inv [in SMTLIB.Eval]
eval_TLet_inv [in SMTLIB.Eval]
eval_TForall_true_inv [in SMTLIB.Eval]
eval_TForall_inv [in SMTLIB.Eval]
eval_TExists_true_inv [in SMTLIB.Eval]
eval_TExists_inv [in SMTLIB.Eval]
eval_TLambda_inv [in SMTLIB.Eval]
eval_TApp_inv [in SMTLIB.Eval]
eval_TFVar_inv [in SMTLIB.Eval]
eval_distinct_true [in SMTLIB.Theory.Core]
eval_distinct_true_inv [in SMTLIB.Theory.Core]
eval_ors_true [in SMTLIB.Theory.Core]
eval_ands_true [in SMTLIB.Theory.Core]
eval_ands_true_inv [in SMTLIB.Theory.Core]
eval_ors_true_inv [in SMTLIB.Theory.Core]
eval_true_true [in SMTLIB.Theory.Core]
eval_false_not_true [in SMTLIB.Theory.Core]
eval_or_true [in SMTLIB.Theory.Core]
eval_or_true_inv [in SMTLIB.Theory.Core]
eval_and_true_inv [in SMTLIB.Theory.Core]
eval_and [in SMTLIB.Theory.Core]
eval_eq_true_inv [in SMTLIB.Theory.Core]
eval_eq_false [in SMTLIB.Theory.Core]
eval_eq_true [in SMTLIB.Theory.Core]
eval_impl_true [in SMTLIB.Theory.Core]
eval_impl_true_consequent [in SMTLIB.Theory.Core]
eval_ite [in SMTLIB.Theory.Core]
eval_impl [in SMTLIB.Theory.Core]
eval_not [in SMTLIB.Theory.Core]
eval_zero_real [in SMTLIB.Theory.Reals_Ints]
eval_decimal_literal [in SMTLIB.Theory.Reals_Ints]
eval_zero_int [in SMTLIB.Theory.Reals_Ints]
eval_int_literal [in SMTLIB.Theory.Reals_Ints]
eval_is_int [in SMTLIB.Theory.Reals_Ints]
eval_to_int [in SMTLIB.Theory.Reals_Ints]
eval_to_real [in SMTLIB.Theory.Reals_Ints]
eval_gt_real_true [in SMTLIB.Theory.Reals_Ints]
eval_gt_real_true_inv [in SMTLIB.Theory.Reals_Ints]
eval_gt_real_interp [in SMTLIB.Theory.Reals_Ints]
eval_geq_real [in SMTLIB.Theory.Reals_Ints]
eval_div_real [in SMTLIB.Theory.Reals_Ints]
eval_times_real [in SMTLIB.Theory.Reals_Ints]
eval_geq_int [in SMTLIB.Theory.Reals_Ints]
eval_geq_int_interp [in SMTLIB.Theory.Reals_Ints]
eval_leq_int [in SMTLIB.Theory.Reals_Ints]
eval_lt_int [in SMTLIB.Theory.Reals_Ints]
eval_times_int [in SMTLIB.Theory.Reals_Ints]
eval_plus_int [in SMTLIB.Theory.Reals_Ints]
eval_app [in SMTLIB.Theory.HO_Core]
eval_seq_nth [in SMTLIB.Theory.Seq]
eval_seq_len [in SMTLIB.Theory.Seq]
eval_seq_concat [in SMTLIB.Theory.Seq]
eval_f_at_zero [in SMTLIB.Tests.TestTheory]
eval_zero_over_zero [in SMTLIB.Tests.TestTheory]
exact_coverage_no_PVar [in SMTLIB.Term]
excluded_middle_int_has_sort [in SMTLIB.Tests.UnitTests]
excluded_middle_has_sort [in SMTLIB.Tests.UnitTests]
extends_rank_with_sorts [in SMTLIB.Signature]
extends_rank_add_sorts [in SMTLIB.Signature]
extends_rank_of_signature_expansion [in SMTLIB.Signature]
F
false_has_sort [in SMTLIB.Theory.Core]fmap_projT1_hlist_to_list [in SMTLIB.Theory]
fmap_list_to_map_zip [in SMTLIB.Utils]
Forall_embeddable_sort_of_hlist [in SMTLIB.Theory]
forall_int_is_zero_has_sort [in SMTLIB.Tests.UnitTests]
Forall_dec_elem [in SMTLIB.Utils]
Forall2_monomorphic_instance_of_mono [in SMTLIB.Symbols]
fresh_strings_of_set_fresh [in SMTLIB.Utils]
fv_term_open_close_image_nil [in SMTLIB.Term]
fv_term_open_close_image [in SMTLIB.Term]
fv_term_subst_singleton_TFVar_subseteq [in SMTLIB.Term]
fv_term_subst_zip_TFVar_subseteq [in SMTLIB.Term]
fv_term_subst_subseteq [in SMTLIB.Term]
fv_term_close_subseteq [in SMTLIB.Term]
fv_term_close [in SMTLIB.Term]
fv_term_open_TFVar1_subseteq [in SMTLIB.Term]
fv_term_open_TFVar_subseteq [in SMTLIB.Term]
fv_map_TFVar_eq_list_to_set [in SMTLIB.Term]
fv_subseteq_fv_term_open [in SMTLIB.Term]
fv_term_open_subseteq [in SMTLIB.Term]
fv_TLet_selectors_subseteq [in SMTLIB.Term]
f_string_literal_ne_op [in SMTLIB.Theory.Strings]
f_string_literal_inj [in SMTLIB.Theory.Strings]
f_decimal_literal_inj [in SMTLIB.Theory.Reals_Ints]
f_int_literal_inj [in SMTLIB.Theory.Reals_Ints]
f_divisible_inj [in SMTLIB.Theory.Reals_Ints]
f_f_not_reals_ints_func [in SMTLIB.Tests.TestTheory]
f_f_not_core_func [in SMTLIB.Tests.TestTheory]
G
generator_sort_of_seq_embeddable [in SMTLIB.Theory.Seq]generator_sort_irrelevant [in SMTLIB.Theory.Seq]
geq_has_sort_real [in SMTLIB.Theory.Reals_Ints]
geq_has_sort_int [in SMTLIB.Theory.Reals_Ints]
ground_term_embed_inj [in SMTLIB.Theory]
ground_term_embed_project [in SMTLIB.Theory]
ground_term_project_embed [in SMTLIB.Theory]
ground_term_project_adt [in SMTLIB.Theory]
ground_term_embed_gen [in SMTLIB.Theory]
ground_term_embed_adt [in SMTLIB.Theory]
ground_term_ind [in SMTLIB.Theory]
gt_has_sort_real [in SMTLIB.Theory.Reals_Ints]
gt_has_sort_int [in SMTLIB.Theory.Reals_Ints]
H
heq_eq_rect_l [in SMTLIB.Utils]hex_value_digit [in SMTLIB.Theory.Strings]
hex_digit_inj [in SMTLIB.Theory.Strings]
hex_digit_code [in SMTLIB.Theory.Strings]
hlist_map_embed_project [in SMTLIB.Theory]
hlist_map_id [in SMTLIB.Theory]
hlist_lookup_map [in SMTLIB.Theory]
hlist_map_map [in SMTLIB.Theory]
hlist_ForallT_lookup [in SMTLIB.Theory]
hlist_lookup_is_Some [in SMTLIB.Theory]
hlist_lookup_Some_1 [in SMTLIB.Theory]
hlist_lookup_Some [in SMTLIB.Theory]
hlist_cons_eq [in SMTLIB.Theory]
hlist_nil_eq [in SMTLIB.Theory]
hlist_map_seq_embed_project [in SMTLIB.Theory.Seq]
hlist_map_project_seq_embed [in SMTLIB.Theory.Seq]
hlist_lookup_seq_embed [in SMTLIB.Theory.Seq]
holds_iff_eval [in SMTLIB.Eval]
ho_core_interp_models [in SMTLIB.Theory.HO_Core]
I
identifier_eqb_iff [in SMTLIB.Symbols]idiv_has_sort [in SMTLIB.Theory.Reals_Ints]
impl_has_sort [in SMTLIB.Theory.Core]
index_eqb_iff [in SMTLIB.Symbols]
infix_of_singleton [in SMTLIB.Utils]
instance_of_refl [in SMTLIB.Symbols]
instance_of_functional [in SMTLIB.Symbols]
interp_insert_func_ne [in SMTLIB.Theory]
interp_insert_func_eq [in SMTLIB.Theory]
interp_insert_rank_ne [in SMTLIB.Theory]
interp_insert_rank_eq [in SMTLIB.Theory]
interp_apply_curry [in SMTLIB.Theory]
int_literal_has_sort [in SMTLIB.Theory.Reals_Ints]
int_literal_value_eq [in SMTLIB.Theory.Reals_Ints]
is_int_has_sort [in SMTLIB.Theory.Reals_Ints]
is_seqb_false [in SMTLIB.Theory.Seq]
ite_has_sort [in SMTLIB.Theory.Core]
L
lc_at_term_close1 [in SMTLIB.Term]lc_at_term_close [in SMTLIB.Term]
lc_at_term_subst_TFVar [in SMTLIB.Term]
lc_at_term_subst [in SMTLIB.Term]
lc_at_of_lc_term_open_TFVar [in SMTLIB.Term]
lc_lc_at [in SMTLIB.Term]
lc_at_term_open_nil [in SMTLIB.Term]
lc_at_term_open [in SMTLIB.Term]
lc_at_app_r [in SMTLIB.Term]
lc_at_TMatch_cons [in SMTLIB.Term]
lc_at_TLet_cons [in SMTLIB.Term]
lc_at_TApp_cons [in SMTLIB.Term]
lc_term_open_term_close [in SMTLIB.Term]
lc_term_open_rename [in SMTLIB.Term]
lc_term_open [in SMTLIB.Term]
length_hlist_to_list [in SMTLIB.Theory]
length_fresh_strings_of_set [in SMTLIB.Utils]
length_omap_lt [in SMTLIB.Utils]
length_omap_le [in SMTLIB.Utils]
leq_has_sort_real [in SMTLIB.Theory.Reals_Ints]
leq_has_sort_int [in SMTLIB.Theory.Reals_Ints]
list_lookup_hlist_to_list [in SMTLIB.Theory]
list_find_eq_list_to_map_zip [in SMTLIB.Utils]
list_to_map_zip_singleton_union [in SMTLIB.Utils]
list_eq_dec_elem_of [in SMTLIB.Utils]
list_eqb_iff [in SMTLIB.Utils]
list_ForallT_lookup [in SMTLIB.Utils]
literal_payload_f_string_literal [in SMTLIB.Theory.Strings]
lookup_union_agree [in SMTLIB.Utils]
lookup_insert_agree [in SMTLIB.Utils]
lookup_list_to_map_zip_None [in SMTLIB.Utils]
lt_has_sort_real [in SMTLIB.Theory.Reals_Ints]
lt_has_sort_int [in SMTLIB.Theory.Reals_Ints]
M
map_fst_map_second [in SMTLIB.Utils]match_pattern_constructor_in_constructors [in SMTLIB.Signature]
minus_has_sort_real [in SMTLIB.Theory.Reals_Ints]
minus_has_sort_int [in SMTLIB.Theory.Reals_Ints]
mod_has_sort [in SMTLIB.Theory.Reals_Ints]
monomorphic_sort_subst_at_most_two [in SMTLIB.Tests.UnitTests]
monomorphic_τ_map_bool [in SMTLIB.Tests.UnitTests]
monomorphic_rank_f_or_inv [in SMTLIB.Theory.Core]
monomorphic_rank_f_and_inv [in SMTLIB.Theory.Core]
monomorphic_rank_f_eq_inv [in SMTLIB.Theory.Core]
monomorphic_rank_signatures_agree_except_sorts [in SMTLIB.Signature]
monomorphic_rank_extends [in SMTLIB.Signature]
monomorphic_rank_conservative [in SMTLIB.Signature]
monomorphic_rank_constructor_args_eq [in SMTLIB.Signature]
monomorphic_rank_constructor_length [in SMTLIB.Signature]
monomorphic_rank_selector_length [in SMTLIB.Signature]
monomorphic_rank_selector [in SMTLIB.Signature]
monomorphic_instance_of_mono [in SMTLIB.Symbols]
monomorphic_instance_of_σ_bool [in SMTLIB.Symbols]
monomorphic_instance_of_SApp_const [in SMTLIB.Symbols]
monomorphic_instance_of_refl [in SMTLIB.Symbols]
monomorphic_instance_of_functional [in SMTLIB.Symbols]
monomorphic_iff_sort_params_empty [in SMTLIB.Symbols]
monomorphic_σ_bool [in SMTLIB.Symbols]
monomorphic_SApp_const [in SMTLIB.Symbols]
N
neg_has_sort_real [in SMTLIB.Theory.Reals_Ints]neg_has_sort_int [in SMTLIB.Theory.Reals_Ints]
NoDup_fresh_strings_of_set [in SMTLIB.Utils]
not_sat_not_at_most_two [in SMTLIB.Tests.UnitTests]
not_valid_at_most_two [in SMTLIB.Tests.UnitTests]
not_valid_forall_int_is_zero [in SMTLIB.Tests.UnitTests]
not_sat_forall_int_is_zero [in SMTLIB.Tests.UnitTests]
not_valid_one_eq_two [in SMTLIB.Tests.UnitTests]
not_sat_one_eq_two [in SMTLIB.Tests.UnitTests]
not_valid_uninterpreted_f_at_zero_is_four [in SMTLIB.Tests.UnitTests]
not_valid_zero_over_zero_is_four [in SMTLIB.Tests.UnitTests]
not_sat_not_entails [in SMTLIB.Eval]
not_has_sort [in SMTLIB.Theory.Core]
not_adt_of_no_constructors [in SMTLIB.Signature]
not_elem_of_fv_term_open_close1 [in SMTLIB.Term]
not_elem_of_fv_term_subst_zip [in SMTLIB.Term]
not_elem_of_fresh_strings_of_set [in SMTLIB.Utils]
not_τ_seq_symb [in SMTLIB.Theory.Seq]
not_τ_seq_cons2 [in SMTLIB.Theory.Seq]
not_τ_seq_nil [in SMTLIB.Theory.Seq]
not_τ_seq_SParam [in SMTLIB.Theory.Seq]
not_entails_of_not_sat [in SMTLIB.Tests.TestTheory]
O
one_eq_two_has_sort [in SMTLIB.Tests.UnitTests]one_plus_one_has_sort [in SMTLIB.Tests.UnitTests]
option_Forall_None [in SMTLIB.Utils]
option_Forall_Some [in SMTLIB.Utils]
ors_has_sort [in SMTLIB.Theory.Core]
or_has_sort [in SMTLIB.Theory.Core]
P
parse_string_literal_eq [in SMTLIB.Theory.Strings]parse_decimal_literal_eq [in SMTLIB.Theory.Reals_Ints]
parse_int_literal_eq [in SMTLIB.Theory.Reals_Ints]
parse_divisible_eq [in SMTLIB.Theory.Reals_Ints]
parse_Z_pretty [in SMTLIB.Utils]
parse_positive_pretty [in SMTLIB.Utils]
parse_N_pretty [in SMTLIB.Utils]
parse_N_go_pretty [in SMTLIB.Utils]
parse_N_char_pretty [in SMTLIB.Utils]
pars_subseteq_pars_term_open [in SMTLIB.Term]
plus_has_sort_real [in SMTLIB.Theory.Reals_Ints]
plus_has_sort_int [in SMTLIB.Theory.Reals_Ints]
polymorphic_term_has_sort_of_term_has_sort [in SMTLIB.Sorting]
pretheory_add_sorts_interpretable [in SMTLIB.Theory]
pretheory_add_sorts_local [in SMTLIB.Theory]
pretheory_compose_interpretable [in SMTLIB.Theory]
pretheory_compose_local [in SMTLIB.Theory]
pretty_positive_slash_free [in SMTLIB.Theory.Reals_Ints]
pretty_Z_slash_free [in SMTLIB.Theory.Reals_Ints]
pretty_N_slash_free [in SMTLIB.Theory.Reals_Ints]
pretty_N_go_slash_free [in SMTLIB.Theory.Reals_Ints]
R
rank_constructor_args_determined_intro [in SMTLIB.Signature]rank_monomorphic [in SMTLIB.Signature]
reals_ints_interp_models [in SMTLIB.Theory.Reals_Ints]
refl_A_not_well_sorted [in SMTLIB.Tests.UnitTests]
S
sat_refl_A [in SMTLIB.Tests.UnitTests]sat_ho_app [in SMTLIB.Tests.UnitTests]
sat_fun_distinct [in SMTLIB.Tests.UnitTests]
sat_fun_eq [in SMTLIB.Tests.UnitTests]
sat_excluded_middle_int [in SMTLIB.Tests.UnitTests]
sat_uninterpreted_f_at_zero_is_four [in SMTLIB.Tests.UnitTests]
sat_zero_over_zero_is_four [in SMTLIB.Tests.UnitTests]
sat_zero_over_zero [in SMTLIB.Tests.UnitTests]
sat_excluded_middle [in SMTLIB.Tests.UnitTests]
sat_one_plus_one [in SMTLIB.Tests.UnitTests]
sat_iff_monomorphic_sat [in SMTLIB.Eval]
sat_of_entails [in SMTLIB.Tests.TestTheory]
seq_adt_interpretation_axioms [in SMTLIB.Theory.Seq]
seq_adt_interpretation_conditions [in SMTLIB.Theory.Seq]
seq_adt_interpretation_other [in SMTLIB.Theory.Seq]
seq_constructor_interp_apply [in SMTLIB.Theory.Seq]
seq_adt_interpretation_tester [in SMTLIB.Theory.Seq]
seq_adt_interpretation_selector [in SMTLIB.Theory.Seq]
seq_adt_interpretation_constructor [in SMTLIB.Theory.Seq]
seq_adt_interp_constructor_disjoint [in SMTLIB.Theory.Seq]
seq_ground_term_embed_irrel [in SMTLIB.Theory.Seq]
seq_ground_term_embed_inj [in SMTLIB.Theory.Seq]
seq_ground_term_embed_project [in SMTLIB.Theory.Seq]
seq_ground_term_project_embed [in SMTLIB.Theory.Seq]
seq_ground_term_project_leaf [in SMTLIB.Theory.Seq]
seq_ground_term_project_seq [in SMTLIB.Theory.Seq]
seq_ground_term_project_adt [in SMTLIB.Theory.Seq]
seq_ground_term_embed_gen [in SMTLIB.Theory.Seq]
seq_ground_term_embed_adt [in SMTLIB.Theory.Seq]
seq_ground_term_embed_not_seq [in SMTLIB.Theory.Seq]
seq_ground_term_embed_seq [in SMTLIB.Theory.Seq]
seq_ground_term_size_SGConstr [in SMTLIB.Theory.Seq]
seq_ground_term_size_SGSeq [in SMTLIB.Theory.Seq]
seq_ground_term_ind [in SMTLIB.Theory.Seq]
seq_ground_term_constructor_Some [in SMTLIB.Theory.Seq]
seq_embeddable_sort_app_nil [in SMTLIB.Theory.Seq]
seq_embeddable_sort_elem [in SMTLIB.Theory.Seq]
seq_embeddable_seq [in SMTLIB.Theory.Seq]
seq_embeddable_leaf [in SMTLIB.Theory.Seq]
seq_embeddable_sort_irrelevant [in SMTLIB.Theory.Seq]
seq_map_has_sort [in SMTLIB.Theory.Seq]
seq_contains_has_sort [in SMTLIB.Theory.Seq]
seq_nth_has_sort [in SMTLIB.Theory.Seq]
seq_len_has_sort [in SMTLIB.Theory.Seq]
seq_concat_has_sort [in SMTLIB.Theory.Seq]
seq_unit_has_sort [in SMTLIB.Theory.Seq]
seq_empty_has_sort [in SMTLIB.Theory.Seq]
seq_at_τ_seq [in SMTLIB.Theory.Seq]
set_map_term_subst_insert_zip_TFVar [in SMTLIB.Term]
set_map_term_subst_zip_id [in SMTLIB.Term]
set_map_term_subst_TFVar_id [in SMTLIB.Term]
signatures_agree_except_sorts_add_sorts_mono [in SMTLIB.Signature]
signatures_agree_except_sorts_insert_mono [in SMTLIB.Signature]
signatures_agree_except_sorts_add_sorts [in SMTLIB.Signature]
signatures_agree_except_sorts_insert [in SMTLIB.Signature]
signatures_agree_except_sorts_with_sorts [in SMTLIB.Signature]
signatures_agree_except_sorts_trans [in SMTLIB.Signature]
signatures_agree_except_sorts_sym [in SMTLIB.Signature]
signatures_agree_except_sorts_refl [in SMTLIB.Signature]
signature_add_sorts_adt [in SMTLIB.Signature]
signature_compose_adt_right [in SMTLIB.Signature]
signature_compose_adt_left [in SMTLIB.Signature]
signature_compose_tester_for_constructor_right [in SMTLIB.Signature]
signature_compose_selectors_for_constructor_right [in SMTLIB.Signature]
signature_compose_constructors_for_sort_right [in SMTLIB.Signature]
signature_compose_constructors_for_sort_left [in SMTLIB.Signature]
signature_lookup_add_sorts [in SMTLIB.Signature]
signature_lookup_with_sorts [in SMTLIB.Signature]
signature_add_sorts_sorts [in SMTLIB.Signature]
signature_insert_sorts [in SMTLIB.Signature]
signature_lookup_insert_ne [in SMTLIB.Signature]
signature_lookup_insert_eq [in SMTLIB.Signature]
signature_compose_extends_rank_right [in SMTLIB.Signature]
signature_compose_extends_rank_left [in SMTLIB.Signature]
signature_compose_signature_expansion_right [in SMTLIB.Signature]
signature_compose_signature_expansion_left [in SMTLIB.Signature]
signature_compose_sort_wf_right [in SMTLIB.Signature]
signature_compose_sort_wf_left [in SMTLIB.Signature]
size_list_to_set_le [in SMTLIB.Utils]
smt_mod_pos [in SMTLIB.Theory.Reals_Ints]
smt_div_pos [in SMTLIB.Theory.Reals_Ints]
sort_wf_with_sorts [in SMTLIB.Signature]
sort_wf_add_sorts [in SMTLIB.Signature]
sort_wf_signatures_agree_except_sorts [in SMTLIB.Signature]
sort_wf_inherit_right [in SMTLIB.Signature]
sort_wf_inherit_left [in SMTLIB.Signature]
sort_wf_signature_expansion [in SMTLIB.Signature]
sort_wf_σ_bool [in SMTLIB.Signature]
sort_wf_Σ_test_σ_int [in SMTLIB.Tests.TestTheory]
sort_subst_eq_subset [in SMTLIB.Symbols]
sort_subst_eq_param_agree [in SMTLIB.Symbols]
sort_subst_empty [in SMTLIB.Symbols]
sort_gen_tree_cancel [in SMTLIB.Symbols]
sort_domain_adt [in SMTLIB.Domain]
sort_domain_τ_seq [in SMTLIB.Domain]
sort_domain_τ_map [in SMTLIB.Domain]
sort_domain_base [in SMTLIB.Domain]
sort_domain_adt_free [in SMTLIB.Domain]
string_literal_has_sort [in SMTLIB.Theory.Strings]
string_occurs_quote_escape_string [in SMTLIB.Theory.Strings]
string_occurs_quote_escape_ascii [in SMTLIB.Theory.Strings]
string_occurs_pretty_Z [in SMTLIB.Utils]
string_occurs_pretty_N [in SMTLIB.Utils]
string_occurs_pretty_N_go [in SMTLIB.Utils]
string_split_at_app [in SMTLIB.Utils]
string_strip_prefix_app [in SMTLIB.Utils]
string_app_inj_tail [in SMTLIB.Utils]
string_length_append [in SMTLIB.Utils]
str_lt_has_sort [in SMTLIB.Theory.Strings]
str_len_has_sort [in SMTLIB.Theory.Strings]
str_concat_has_sort [in SMTLIB.Theory.Strings]
T
term_sort_subst_at_most_two [in SMTLIB.Tests.UnitTests]term_subst_ands [in SMTLIB.Theory.Core]
term_sort_subst_empty [in SMTLIB.Term]
term_open_close_as_open_subst [in SMTLIB.Term]
term_open_close_subst1_nil [in SMTLIB.Term]
term_open_close_subst1 [in SMTLIB.Term]
term_open_close_subst_nil [in SMTLIB.Term]
term_open_close_subst [in SMTLIB.Term]
term_subst_singleton_open_TFVar1_comm [in SMTLIB.Term]
term_subst_singleton_open_TFVar_comm [in SMTLIB.Term]
term_subst_open_TFVar_rename [in SMTLIB.Term]
term_subst_open_TFVar_comm [in SMTLIB.Term]
term_subst_open [in SMTLIB.Term]
term_subst_insert_zip_TFVar [in SMTLIB.Term]
term_subst_insert [in SMTLIB.Term]
term_subst_subst_fresh_singleton [in SMTLIB.Term]
term_subst_subst_fresh [in SMTLIB.Term]
term_subst_subst [in SMTLIB.Term]
term_subst_ext [in SMTLIB.Term]
term_subst_fresh_singleton [in SMTLIB.Term]
term_subst_fresh [in SMTLIB.Term]
term_subst_id_singleton [in SMTLIB.Term]
term_subst_id_zip [in SMTLIB.Term]
term_subst_id [in SMTLIB.Term]
term_open_close_comm [in SMTLIB.Term]
term_close_fresh [in SMTLIB.Term]
term_close_nth_TFVar [in SMTLIB.Term]
term_size_term_open_TFVar [in SMTLIB.Term]
term_open_comm [in SMTLIB.Term]
term_open_lem [in SMTLIB.Term]
term_open_nth_TFVar [in SMTLIB.Term]
term_size_cases [in SMTLIB.Term]
term_size_list [in SMTLIB.Term]
term_encode_decode [in SMTLIB.Term]
term_decode_encode_app [in SMTLIB.Term]
term_decode_encode_list [in SMTLIB.Term]
term_encode_bind_snd [in SMTLIB.Term]
term_has_sort_term_open_term_close1 [in SMTLIB.Sorting]
term_has_sort_term_open_term_close [in SMTLIB.Sorting]
term_has_sort_term_subst1 [in SMTLIB.Sorting]
term_has_sort_rename [in SMTLIB.Sorting]
term_has_sort_term_subst_fv [in SMTLIB.Sorting]
term_has_sort_term_subst [in SMTLIB.Sorting]
term_has_sort_pars_empty [in SMTLIB.Sorting]
term_has_sort_map_TFVar_lookup [in SMTLIB.Sorting]
term_has_sort_fv_subseteq_dom [in SMTLIB.Sorting]
term_has_sort_fv_lookup [in SMTLIB.Sorting]
term_has_sort_lc [in SMTLIB.Sorting]
term_has_sort_strengthen1 [in SMTLIB.Sorting]
term_has_sort_strengthen [in SMTLIB.Sorting]
term_has_sort_weaken1 [in SMTLIB.Sorting]
term_has_sort_weaken [in SMTLIB.Sorting]
term_has_sort_add_sorts_with_sorts [in SMTLIB.Sorting]
term_has_sort_insert_with_sorts [in SMTLIB.Sorting]
term_has_sort_sorts_eq [in SMTLIB.Sorting]
term_has_sort_cong [in SMTLIB.Sorting]
times_has_sort_real [in SMTLIB.Theory.Reals_Ints]
times_has_sort_int [in SMTLIB.Theory.Reals_Ints]
to_int_has_sort [in SMTLIB.Theory.Reals_Ints]
to_real_has_sort [in SMTLIB.Theory.Reals_Ints]
true_has_sort [in SMTLIB.Theory.Core]
T_strings_interpretable [in SMTLIB.Theory.Strings]
T_strings_local [in SMTLIB.Theory.Strings]
T_core_interpretable [in SMTLIB.Theory.Core]
T_core_local [in SMTLIB.Theory.Core]
T_reals_ints_interpretable [in SMTLIB.Theory.Reals_Ints]
T_reals_ints_local [in SMTLIB.Theory.Reals_Ints]
T_ho_core_interpretable [in SMTLIB.Theory.HO_Core]
T_ho_core_local [in SMTLIB.Theory.HO_Core]
T_seq_interpretable [in SMTLIB.Theory.Seq]
T_seq_local [in SMTLIB.Theory.Seq]
T_test_consistent [in SMTLIB.Tests.TestTheory]
U
unescape_escape_string [in SMTLIB.Theory.Strings]uninterpreted_f_at_zero_has_sort [in SMTLIB.Tests.UnitTests]
union_lookup_list_to_map_agree [in SMTLIB.Sorting]
V
valid_refl_A [in SMTLIB.Tests.UnitTests]valid_ho_app [in SMTLIB.Tests.UnitTests]
valid_ho_ext [in SMTLIB.Tests.UnitTests]
valid_fun_ext [in SMTLIB.Tests.UnitTests]
valid_excluded_middle_int [in SMTLIB.Tests.UnitTests]
valid_excluded_middle [in SMTLIB.Tests.UnitTests]
valid_one_plus_one [in SMTLIB.Tests.UnitTests]
valuation_sorting_lookup [in SMTLIB.Eval]
valuation_sorting_insert [in SMTLIB.Eval]
valuation_well_sorted_refl [in SMTLIB.Eval]
valuation_well_sorted_union_lookup_list_to_map [in SMTLIB.Eval]
valuation_well_sorted_insert [in SMTLIB.Eval]
valuation_well_sorted_lookup [in SMTLIB.Eval]
W
wf_sub_term [in SMTLIB.Term]wf_sub_sort [in SMTLIB.Symbols]
X
xor_has_sort [in SMTLIB.Theory.Core]Z
zero_over_zero_has_sort [in SMTLIB.Tests.UnitTests]other
Σ_ho_no_adt [in SMTLIB.Tests.TestTheory]Σ_ho_core_extends_Σ_ho [in SMTLIB.Tests.TestTheory]
Σ_core_extends_Σ_ho [in SMTLIB.Tests.TestTheory]
Σ_core_Σ_ho_core_composable [in SMTLIB.Tests.TestTheory]
Σ_test_no_adt [in SMTLIB.Tests.TestTheory]
Σ_reals_ints_extends_Σ_test [in SMTLIB.Tests.TestTheory]
Σ_core_extends_Σ_test [in SMTLIB.Tests.TestTheory]
Σ_uninterp_extends_Σ_test [in SMTLIB.Tests.TestTheory]
Σ_arith_extends_Σ_test [in SMTLIB.Tests.TestTheory]
Σ_reals_ints_extends_Σ_arith [in SMTLIB.Tests.TestTheory]
Σ_core_extends_Σ_arith [in SMTLIB.Tests.TestTheory]
Σ_arith_Σ_uninterp_composable [in SMTLIB.Tests.TestTheory]
Σ_core_Σ_reals_ints_composable [in SMTLIB.Tests.TestTheory]
Constructor Index
C
cb_escape [in SMTLIB.Theory.Strings]cb_plain [in SMTLIB.Theory.Strings]
cb_empty [in SMTLIB.Theory.Strings]
E
ES_cons [in SMTLIB.Eval]ES_nil [in SMTLIB.Eval]
E_TMatch_PApp_false [in SMTLIB.Eval]
E_TMatch_PApp_true [in SMTLIB.Eval]
E_TMatch_PVar [in SMTLIB.Eval]
E_TLet [in SMTLIB.Eval]
E_TLambda [in SMTLIB.Eval]
E_TForall_false [in SMTLIB.Eval]
E_TForall_true [in SMTLIB.Eval]
E_TExists_false [in SMTLIB.Eval]
E_TExists_true [in SMTLIB.Eval]
E_TApp [in SMTLIB.Eval]
E_TFVar [in SMTLIB.Eval]
G
GConstr [in SMTLIB.Theory]GGen [in SMTLIB.Theory]
H
HCons [in SMTLIB.Theory]HNil [in SMTLIB.Theory]
I
IdIndexed [in SMTLIB.Symbols]IdSimple [in SMTLIB.Symbols]
IdxNum [in SMTLIB.Symbols]
IdxSym [in SMTLIB.Symbols]
L
LCA_TMatch [in SMTLIB.Term]LCA_TLet [in SMTLIB.Term]
LCA_TForall [in SMTLIB.Term]
LCA_TExists [in SMTLIB.Term]
LCA_TLambda [in SMTLIB.Term]
LCA_TApp [in SMTLIB.Term]
LCA_TBVar [in SMTLIB.Term]
LCA_TFVar [in SMTLIB.Term]
LCT_TMatch [in SMTLIB.Term]
LCT_TLet [in SMTLIB.Term]
LCT_TForall [in SMTLIB.Term]
LCT_TExists [in SMTLIB.Term]
LCT_TLambda [in SMTLIB.Term]
LCT_TApp [in SMTLIB.Term]
LCT_TFVar [in SMTLIB.Term]
M
M_SApp [in SMTLIB.Symbols]P
PApp [in SMTLIB.Term]PVar [in SMTLIB.Term]
R
rank_f_string_literal [in SMTLIB.Theory.Strings]rank_f_str_lt [in SMTLIB.Theory.Strings]
rank_f_str_len [in SMTLIB.Theory.Strings]
rank_f_str_concat [in SMTLIB.Theory.Strings]
rank_f_ite [in SMTLIB.Theory.Core]
rank_f_distinct [in SMTLIB.Theory.Core]
rank_f_eq [in SMTLIB.Theory.Core]
rank_f_xor [in SMTLIB.Theory.Core]
rank_f_or [in SMTLIB.Theory.Core]
rank_f_and [in SMTLIB.Theory.Core]
rank_f_impl [in SMTLIB.Theory.Core]
rank_f_not [in SMTLIB.Theory.Core]
rank_f_false [in SMTLIB.Theory.Core]
rank_f_true [in SMTLIB.Theory.Core]
rank_f_decimal_literal [in SMTLIB.Theory.Reals_Ints]
rank_f_int_literal [in SMTLIB.Theory.Reals_Ints]
rank_f_divisible [in SMTLIB.Theory.Reals_Ints]
rank_f_is_int [in SMTLIB.Theory.Reals_Ints]
rank_f_to_int [in SMTLIB.Theory.Reals_Ints]
rank_f_to_real [in SMTLIB.Theory.Reals_Ints]
rank_f_gt_real [in SMTLIB.Theory.Reals_Ints]
rank_f_geq_real [in SMTLIB.Theory.Reals_Ints]
rank_f_lt_real [in SMTLIB.Theory.Reals_Ints]
rank_f_leq_real [in SMTLIB.Theory.Reals_Ints]
rank_f_div [in SMTLIB.Theory.Reals_Ints]
rank_f_times_real [in SMTLIB.Theory.Reals_Ints]
rank_f_plus_real [in SMTLIB.Theory.Reals_Ints]
rank_f_minus_sub_real [in SMTLIB.Theory.Reals_Ints]
rank_f_minus_neg_real [in SMTLIB.Theory.Reals_Ints]
rank_f_gt_int [in SMTLIB.Theory.Reals_Ints]
rank_f_geq_int [in SMTLIB.Theory.Reals_Ints]
rank_f_lt_int [in SMTLIB.Theory.Reals_Ints]
rank_f_leq_int [in SMTLIB.Theory.Reals_Ints]
rank_f_abs [in SMTLIB.Theory.Reals_Ints]
rank_f_mod [in SMTLIB.Theory.Reals_Ints]
rank_f_idiv [in SMTLIB.Theory.Reals_Ints]
rank_f_times_int [in SMTLIB.Theory.Reals_Ints]
rank_f_plus_int [in SMTLIB.Theory.Reals_Ints]
rank_f_minus_sub_int [in SMTLIB.Theory.Reals_Ints]
rank_f_minus_neg_int [in SMTLIB.Theory.Reals_Ints]
rank_f_app [in SMTLIB.Theory.HO_Core]
rank_f_seq_map [in SMTLIB.Theory.Seq]
rank_f_seq_contains [in SMTLIB.Theory.Seq]
rank_f_seq_nth [in SMTLIB.Theory.Seq]
rank_f_seq_len [in SMTLIB.Theory.Seq]
rank_f_seq_concat [in SMTLIB.Theory.Seq]
rank_f_seq_unit [in SMTLIB.Theory.Seq]
rank_f_seq_empty [in SMTLIB.Theory.Seq]
rank_f_f [in SMTLIB.Tests.TestTheory]
S
SApp [in SMTLIB.Symbols]SGConstr [in SMTLIB.Theory.Seq]
SGGen [in SMTLIB.Theory.Seq]
SGSeq [in SMTLIB.Theory.Seq]
smt_compose [in SMTLIB.Signature]
SParam [in SMTLIB.Symbols]
S_TMatch_PVar [in SMTLIB.Sorting]
S_TMatch_PApp [in SMTLIB.Sorting]
S_TLet [in SMTLIB.Sorting]
S_TForall [in SMTLIB.Sorting]
S_TExists [in SMTLIB.Sorting]
S_TLambda [in SMTLIB.Sorting]
S_TApp_annotated [in SMTLIB.Sorting]
S_TApp [in SMTLIB.Sorting]
S_TFVar [in SMTLIB.Sorting]
T
TApp [in SMTLIB.Term]TBVar [in SMTLIB.Term]
TExists [in SMTLIB.Term]
TForall [in SMTLIB.Term]
TFVar [in SMTLIB.Term]
TLambda [in SMTLIB.Term]
TLet [in SMTLIB.Term]
TMatch [in SMTLIB.Term]
W
WF_SApp [in SMTLIB.Symbols]WF_SParam [in SMTLIB.Symbols]
Projection Index
A
adt_constructed_disjoint [in SMTLIB.Theory]adt_constructed_domain [in SMTLIB.Theory]
adt_interp_tester [in SMTLIB.Theory]
adt_interp_selector [in SMTLIB.Theory]
adt_interp_constructor [in SMTLIB.Theory]
adt_domain [in SMTLIB.Theory]
arities_consistent [in SMTLIB.Signature]
arity [in SMTLIB.Signature]
arity_s_map [in SMTLIB.Signature]
arity_s_bool [in SMTLIB.Signature]
C
constructors [in SMTLIB.Signature]constructors_consistent_right [in SMTLIB.Signature]
constructors_consistent_left [in SMTLIB.Signature]
constructors_for_sort_consistent [in SMTLIB.Signature]
constructors_for_sort_wf [in SMTLIB.Signature]
constructors_for_sort [in SMTLIB.Signature]
constructors_wf [in SMTLIB.Signature]
constructor_for_tester_consistent [in SMTLIB.Signature]
constructor_tester_bijection [in SMTLIB.Signature]
constructor_for_tester_wf [in SMTLIB.Signature]
constructor_for_tester [in SMTLIB.Signature]
D
domain [in SMTLIB.Theory]domain_σ_map [in SMTLIB.Theory]
domain_σ_bool [in SMTLIB.Theory]
F
funcs [in SMTLIB.Signature]funcs_extends [in SMTLIB.Signature]
funcs_dec [in SMTLIB.Signature]
I
interp [in SMTLIB.Theory]M
mc_ite [in SMTLIB.Theory.Core]mc_distinct [in SMTLIB.Theory.Core]
mc_eq [in SMTLIB.Theory.Core]
mc_xor [in SMTLIB.Theory.Core]
mc_or [in SMTLIB.Theory.Core]
mc_and [in SMTLIB.Theory.Core]
mc_impl [in SMTLIB.Theory.Core]
mc_not [in SMTLIB.Theory.Core]
mc_false [in SMTLIB.Theory.Core]
mc_true [in SMTLIB.Theory.Core]
mhc_app [in SMTLIB.Theory.HO_Core]
models [in SMTLIB.Theory]
mri_decimal_literal [in SMTLIB.Theory.Reals_Ints]
mri_int_literal [in SMTLIB.Theory.Reals_Ints]
mri_divisible [in SMTLIB.Theory.Reals_Ints]
mri_is_int [in SMTLIB.Theory.Reals_Ints]
mri_to_int [in SMTLIB.Theory.Reals_Ints]
mri_to_real [in SMTLIB.Theory.Reals_Ints]
mri_gt_real [in SMTLIB.Theory.Reals_Ints]
mri_geq_real [in SMTLIB.Theory.Reals_Ints]
mri_lt_real [in SMTLIB.Theory.Reals_Ints]
mri_leq_real [in SMTLIB.Theory.Reals_Ints]
mri_div [in SMTLIB.Theory.Reals_Ints]
mri_times_real [in SMTLIB.Theory.Reals_Ints]
mri_plus_real [in SMTLIB.Theory.Reals_Ints]
mri_minus_sub_real [in SMTLIB.Theory.Reals_Ints]
mri_minus_neg_real [in SMTLIB.Theory.Reals_Ints]
mri_gt_int [in SMTLIB.Theory.Reals_Ints]
mri_geq_int [in SMTLIB.Theory.Reals_Ints]
mri_lt_int [in SMTLIB.Theory.Reals_Ints]
mri_leq_int [in SMTLIB.Theory.Reals_Ints]
mri_abs [in SMTLIB.Theory.Reals_Ints]
mri_mod [in SMTLIB.Theory.Reals_Ints]
mri_idiv [in SMTLIB.Theory.Reals_Ints]
mri_times_int [in SMTLIB.Theory.Reals_Ints]
mri_plus_int [in SMTLIB.Theory.Reals_Ints]
mri_minus_sub_int [in SMTLIB.Theory.Reals_Ints]
mri_minus_neg_int [in SMTLIB.Theory.Reals_Ints]
ms_string_literal [in SMTLIB.Theory.Strings]
ms_str_lt [in SMTLIB.Theory.Strings]
ms_str_len [in SMTLIB.Theory.Strings]
ms_str_concat [in SMTLIB.Theory.Strings]
ms_map [in SMTLIB.Theory.Seq]
ms_contains [in SMTLIB.Theory.Seq]
ms_nth [in SMTLIB.Theory.Seq]
ms_len [in SMTLIB.Theory.Seq]
ms_concat [in SMTLIB.Theory.Seq]
ms_unit [in SMTLIB.Theory.Seq]
ms_empty [in SMTLIB.Theory.Seq]
P
pmodels [in SMTLIB.Theory]ptc_signatures_composable [in SMTLIB.Theory]
pΣ [in SMTLIB.Theory]
R
rank [in SMTLIB.Signature]rank_constructor_consistent [in SMTLIB.Signature]
rank_conservative [in SMTLIB.Signature]
rank_extends [in SMTLIB.Signature]
rank_tester [in SMTLIB.Signature]
rank_selectors [in SMTLIB.Signature]
rank_constructor_args_determined [in SMTLIB.Signature]
rank_constructor [in SMTLIB.Signature]
rank_left_total [in SMTLIB.Signature]
rank_domain [in SMTLIB.Signature]
rank_wf [in SMTLIB.Signature]
S
selectors [in SMTLIB.Signature]selectors_for_constructor_consistent [in SMTLIB.Signature]
selectors_mutually_disj [in SMTLIB.Signature]
selectors_for_constructor_wf [in SMTLIB.Signature]
selectors_for_constructor [in SMTLIB.Signature]
selectors_disj [in SMTLIB.Signature]
selectors_wf [in SMTLIB.Signature]
seq_adt_interp_tester [in SMTLIB.Theory.Seq]
seq_adt_interp_selector [in SMTLIB.Theory.Seq]
seq_adt_interp_constructor [in SMTLIB.Theory.Seq]
signatures_agree_except_sorts_rank [in SMTLIB.Signature]
signatures_agree_except_sorts_constructor_for_tester [in SMTLIB.Signature]
signatures_agree_except_sorts_tester_for_constructor [in SMTLIB.Signature]
signatures_agree_except_sorts_selectors_for_constructor [in SMTLIB.Signature]
signatures_agree_except_sorts_arity [in SMTLIB.Signature]
signatures_agree_except_sorts_constructors_for_sort [in SMTLIB.Signature]
signatures_agree_except_sorts_testers [in SMTLIB.Signature]
signatures_agree_except_sorts_selectors [in SMTLIB.Signature]
signatures_agree_except_sorts_constructors [in SMTLIB.Signature]
signatures_agree_except_sorts_funcs [in SMTLIB.Signature]
signatures_agree_except_sorts_sort_symbols [in SMTLIB.Signature]
signature_expansion_rank [in SMTLIB.Signature]
signature_expansion_sorts [in SMTLIB.Signature]
signature_expansion_tester_for_constructor [in SMTLIB.Signature]
signature_expansion_selectors_for_constructor [in SMTLIB.Signature]
signature_expansion_constructors [in SMTLIB.Signature]
signature_expansion_constructors_for_sort [in SMTLIB.Signature]
signature_expansion_arity [in SMTLIB.Signature]
signature_expansion_funcs [in SMTLIB.Signature]
signature_expansion_sort_symbols [in SMTLIB.Signature]
smt_compose [in SMTLIB.Signature]
sorts [in SMTLIB.Signature]
sorts_consistent [in SMTLIB.Signature]
sort_wf_extends [in SMTLIB.Signature]
sort_symbols_wf [in SMTLIB.Signature]
sort_symbols [in SMTLIB.Signature]
T
testers [in SMTLIB.Signature]testers_mutually_disj [in SMTLIB.Signature]
testers_disj [in SMTLIB.Signature]
testers_wf [in SMTLIB.Signature]
tester_for_constructor_consistent [in SMTLIB.Signature]
tester_constructor_bijection [in SMTLIB.Signature]
tester_for_constructor_wf [in SMTLIB.Signature]
tester_for_constructor [in SMTLIB.Signature]
other
Σ [in SMTLIB.Theory]Inductive Index
C
Compose [in SMTLIB.Signature]constant_body [in SMTLIB.Theory.Strings]
E
eval [in SMTLIB.Eval]evals [in SMTLIB.Eval]
G
ground_term [in SMTLIB.Theory]H
hlist [in SMTLIB.Theory]I
identifier [in SMTLIB.Symbols]index [in SMTLIB.Symbols]
L
lc [in SMTLIB.Term]lc_at [in SMTLIB.Term]
M
monomorphic [in SMTLIB.Symbols]P
pattern [in SMTLIB.Term]R
rank_strings [in SMTLIB.Theory.Strings]rank_core [in SMTLIB.Theory.Core]
rank_reals_ints [in SMTLIB.Theory.Reals_Ints]
rank_ho_core [in SMTLIB.Theory.HO_Core]
rank_seq [in SMTLIB.Theory.Seq]
rank_uninterp [in SMTLIB.Tests.TestTheory]
S
seq_ground_term [in SMTLIB.Theory.Seq]sort [in SMTLIB.Symbols]
sort_wf_base [in SMTLIB.Symbols]
T
term [in SMTLIB.Term]term_has_sort [in SMTLIB.Sorting]
Section Index
B
BuildInterp [in SMTLIB.Theory]C
CoreInterpretable [in SMTLIB.Theory.Core]CoreModels [in SMTLIB.Theory.Core]
D
DomainConstruction [in SMTLIB.Domain]G
GroundTerm [in SMTLIB.Theory]GroundTermRect [in SMTLIB.Theory]
H
HO_CoreInterpretable [in SMTLIB.Theory.HO_Core]HO_CoreModels [in SMTLIB.Theory.HO_Core]
I
Interpretation [in SMTLIB.Theory]Inversion [in SMTLIB.Eval]
R
Reals_IntsInterpretable [in SMTLIB.Theory.Reals_Ints]Reals_IntsModels [in SMTLIB.Theory.Reals_Ints]
S
SeqAdtConditions [in SMTLIB.Theory.Seq]SeqAdtInterp [in SMTLIB.Theory.Seq]
SeqEmbedProject [in SMTLIB.Theory.Seq]
SeqGroundTerm [in SMTLIB.Theory.Seq]
SeqGroundTermRect [in SMTLIB.Theory.Seq]
SeqGroundTermSize [in SMTLIB.Theory.Seq]
SeqInterpretable [in SMTLIB.Theory.Seq]
SeqModels [in SMTLIB.Theory.Seq]
sort_rect [in SMTLIB.Symbols]
sort_ind [in SMTLIB.Symbols]
StringsInterpretable [in SMTLIB.Theory.Strings]
StringsModels [in SMTLIB.Theory.Strings]
Structure [in SMTLIB.Theory]
Structure.EmbedProject [in SMTLIB.Theory]
T
term_rect [in SMTLIB.Term]term_ind [in SMTLIB.Term]
W
WhereTheFreedomIs [in SMTLIB.Tests.TestTheory]Instance Index
A
adt_free_dec [in SMTLIB.Signature]adt_dec [in SMTLIB.Signature]
adt_spec_dec [in SMTLIB.Signature]
D
decimal_literals_dec [in SMTLIB.Theory.Reals_Ints]divisible_func_dec [in SMTLIB.Theory.Reals_Ints]
E
embeddable_sort_dec [in SMTLIB.Signature]extends_rank_trans [in SMTLIB.Signature]
extends_rank_refl [in SMTLIB.Signature]
I
identifier_infinite [in SMTLIB.Symbols]identifier_countable [in SMTLIB.Symbols]
identifier_eq_decision [in SMTLIB.Symbols]
index_countable [in SMTLIB.Symbols]
index_eq_decision [in SMTLIB.Symbols]
int_literals_dec [in SMTLIB.Theory.Reals_Ints]
P
pattern_countable [in SMTLIB.Term]pattern_eq_dec [in SMTLIB.Term]
pretheory_compose_compose [in SMTLIB.Theory]
R
real_is_int_decision [in SMTLIB.Theory.Reals_Ints]Rge_decision [in SMTLIB.Theory.Reals_Ints]
Rgt_decision [in SMTLIB.Theory.Reals_Ints]
Rle_decision [in SMTLIB.Theory.Reals_Ints]
Rlt_decision [in SMTLIB.Theory.Reals_Ints]
S
seq_embeddable_sort_dec [in SMTLIB.Theory.Seq]signature_insert [in SMTLIB.Signature]
signature_lookup [in SMTLIB.Signature]
signature_compose_compose [in SMTLIB.Signature]
sort_wf_base_dec [in SMTLIB.Symbols]
sort_countable [in SMTLIB.Symbols]
sort_eq_decision [in SMTLIB.Symbols]
string_literals_dec [in SMTLIB.Theory.Strings]
T
term_countable [in SMTLIB.Term]term_eq_decision [in SMTLIB.Term]
Z
Zdivide_decision [in SMTLIB.Theory.Reals_Ints]Abbreviation Index
A
A [in SMTLIB.Theory.Seq]A0 [in SMTLIB.Theory.Seq]
B
base [in SMTLIB.Theory.Strings]base [in SMTLIB.Theory.Core]
base [in SMTLIB.Theory.Reals_Ints]
base [in SMTLIB.Theory.Seq]
D
decimal_of_Z [in SMTLIB.Tests.UnitTests]F
func [in SMTLIB.Symbols]G
G [in SMTLIB.Theory.Seq]M
monomorphic_rank_base [in SMTLIB.Signature]Q
Qc_of_Z [in SMTLIB.Tests.UnitTests]R
Rcmp [in SMTLIB.Theory.Reals_Ints]Rop1 [in SMTLIB.Theory.Reals_Ints]
Rop2 [in SMTLIB.Theory.Reals_Ints]
R_of_Qc [in SMTLIB.Tests.UnitTests]
S
sorting [in SMTLIB.Signature]sortparam [in SMTLIB.Symbols]
sortsymb [in SMTLIB.Symbols]
sort_subst_map [in SMTLIB.Symbols]
symbol [in SMTLIB.Symbols]
V
valuation [in SMTLIB.Eval]var [in SMTLIB.Symbols]
Z
Zcmp [in SMTLIB.Theory.Reals_Ints]Zop1 [in SMTLIB.Theory.Reals_Ints]
Zop2 [in SMTLIB.Theory.Reals_Ints]
Definition Index
A
abs_ [in SMTLIB.Theory.Reals_Ints]adt [in SMTLIB.Signature]
adt_constructor_condition [in SMTLIB.Theory]
adt_tester_condition [in SMTLIB.Theory]
adt_selector_condition [in SMTLIB.Theory]
adt_free [in SMTLIB.Signature]
adt_freeb_args [in SMTLIB.Signature]
adt_freeb [in SMTLIB.Signature]
adt_spec [in SMTLIB.Signature]
adt_free_domain_witness [in SMTLIB.Domain]
adt_free_domain [in SMTLIB.Domain]
ands_ [in SMTLIB.Theory.Core]
and_ [in SMTLIB.Theory.Core]
app_ [in SMTLIB.Theory.HO_Core]
at_most_two [in SMTLIB.Tests.UnitTests]
at_most_two_body [in SMTLIB.Tests.UnitTests]
A_ho [in SMTLIB.Tests.TestTheory]
A_free [in SMTLIB.Tests.TestTheory]
B
base_interp [in SMTLIB.Tests.TestTheory]bool_ [in SMTLIB.Theory.Core]
C
cast [in SMTLIB.Utils]cast_to_bool [in SMTLIB.Theory.Strings]
cast_to_Z [in SMTLIB.Theory.Strings]
cast_to_string [in SMTLIB.Theory.Strings]
cast_to_bool [in SMTLIB.Theory.Core]
cast_to_bool [in SMTLIB.Theory.Reals_Ints]
cast_to_R [in SMTLIB.Theory.Reals_Ints]
cast_to_Z [in SMTLIB.Theory.Reals_Ints]
cast_sym [in SMTLIB.Utils]
cast_to_map [in SMTLIB.Theory.HO_Core]
cast_to_bool [in SMTLIB.Theory.Seq]
cast_to_map [in SMTLIB.Theory.Seq]
cast_to_Z [in SMTLIB.Theory.Seq]
cast_to_list [in SMTLIB.Theory.Seq]
closed [in SMTLIB.Term]
constant_body_sind [in SMTLIB.Theory.Strings]
constant_body_ind [in SMTLIB.Theory.Strings]
constructor_args_embeddable [in SMTLIB.Signature]
constructor_args_seq_embeddable [in SMTLIB.Theory.Seq]
core_interp [in SMTLIB.Theory.Core]
core_ite [in SMTLIB.Theory.Core]
core_cmp [in SMTLIB.Theory.Core]
core_binop [in SMTLIB.Theory.Core]
core_unop [in SMTLIB.Theory.Core]
core_lit [in SMTLIB.Theory.Core]
core_funcs [in SMTLIB.Theory.Core]
C_ho [in SMTLIB.Tests.TestTheory]
C_test [in SMTLIB.Tests.TestTheory]
C_arith [in SMTLIB.Tests.TestTheory]
D
decimal_literal_value [in SMTLIB.Theory.Reals_Ints]decimal_literal [in SMTLIB.Theory.Reals_Ints]
decimal_literals [in SMTLIB.Theory.Reals_Ints]
define_fun [in SMTLIB.Theory.Core]
distinct_ [in SMTLIB.Theory.Core]
divisible [in SMTLIB.Theory.Reals_Ints]
divisible_value [in SMTLIB.Theory.Reals_Ints]
divisible_func [in SMTLIB.Theory.Reals_Ints]
div_ [in SMTLIB.Theory.Reals_Ints]
div_by_zero [in SMTLIB.Tests.TestTheory]
domain_witness [in SMTLIB.Theory]
domain_gen [in SMTLIB.Theory]
dom_fun [in SMTLIB.Tests.UnitTests]
D_test [in SMTLIB.Tests.TestTheory]
E
embeddable_sort_of_ground_term [in SMTLIB.Theory]embeddable_sort [in SMTLIB.Signature]
entails [in SMTLIB.Eval]
eq_ [in SMTLIB.Theory.Core]
escape_string [in SMTLIB.Theory.Strings]
escape_ascii [in SMTLIB.Theory.Strings]
evals_mind [in SMTLIB.Eval]
evals_sind [in SMTLIB.Eval]
evals_ind [in SMTLIB.Eval]
eval_mind [in SMTLIB.Eval]
eval_sind [in SMTLIB.Eval]
eval_ind [in SMTLIB.Eval]
extends_rank [in SMTLIB.Signature]
F
false_ [in SMTLIB.Theory.Core]Forall_cons_tail [in SMTLIB.Utils]
Forall_cons_head [in SMTLIB.Utils]
fv [in SMTLIB.Term]
f_string_literal [in SMTLIB.Theory.Strings]
f_str_lt [in SMTLIB.Theory.Strings]
f_str_len [in SMTLIB.Theory.Strings]
f_str_concat [in SMTLIB.Theory.Strings]
f_ite [in SMTLIB.Theory.Core]
f_distinct [in SMTLIB.Theory.Core]
f_eq [in SMTLIB.Theory.Core]
f_xor [in SMTLIB.Theory.Core]
f_or [in SMTLIB.Theory.Core]
f_and [in SMTLIB.Theory.Core]
f_impl [in SMTLIB.Theory.Core]
f_not [in SMTLIB.Theory.Core]
f_false [in SMTLIB.Theory.Core]
f_true [in SMTLIB.Theory.Core]
f_decimal_literal [in SMTLIB.Theory.Reals_Ints]
f_int_literal [in SMTLIB.Theory.Reals_Ints]
f_divisible [in SMTLIB.Theory.Reals_Ints]
f_is_int [in SMTLIB.Theory.Reals_Ints]
f_to_int [in SMTLIB.Theory.Reals_Ints]
f_to_real [in SMTLIB.Theory.Reals_Ints]
f_gt [in SMTLIB.Theory.Reals_Ints]
f_geq [in SMTLIB.Theory.Reals_Ints]
f_lt [in SMTLIB.Theory.Reals_Ints]
f_leq [in SMTLIB.Theory.Reals_Ints]
f_abs [in SMTLIB.Theory.Reals_Ints]
f_mod [in SMTLIB.Theory.Reals_Ints]
f_div [in SMTLIB.Theory.Reals_Ints]
f_idiv [in SMTLIB.Theory.Reals_Ints]
f_times [in SMTLIB.Theory.Reals_Ints]
f_plus [in SMTLIB.Theory.Reals_Ints]
f_minus [in SMTLIB.Theory.Reals_Ints]
f_app [in SMTLIB.Theory.HO_Core]
f_seq_map [in SMTLIB.Theory.Seq]
f_seq_contains [in SMTLIB.Theory.Seq]
f_seq_nth [in SMTLIB.Theory.Seq]
f_seq_len [in SMTLIB.Theory.Seq]
f_seq_concat [in SMTLIB.Theory.Seq]
f_seq_unit [in SMTLIB.Theory.Seq]
f_seq_empty [in SMTLIB.Theory.Seq]
f_f [in SMTLIB.Tests.TestTheory]
G
generator_sort [in SMTLIB.Theory.Seq]gen_tree_to_sort [in SMTLIB.Symbols]
geq_ [in SMTLIB.Theory.Reals_Ints]
ground_term_project [in SMTLIB.Theory]
ground_term_embed [in SMTLIB.Theory]
ground_term_rect [in SMTLIB.Theory]
ground_term_constructor [in SMTLIB.Theory]
gt_ [in SMTLIB.Theory.Reals_Ints]
H
hex_value [in SMTLIB.Theory.Strings]hex_digit [in SMTLIB.Theory.Strings]
hlist_map_embed [in SMTLIB.Theory]
hlist_map [in SMTLIB.Theory]
hlist_ForallT [in SMTLIB.Theory]
hlist_to_list [in SMTLIB.Theory]
hlist_lookup [in SMTLIB.Theory]
hlist_sind [in SMTLIB.Theory]
hlist_rec [in SMTLIB.Theory]
hlist_ind [in SMTLIB.Theory]
hlist_rect [in SMTLIB.Theory]
hlist_map_seq_embed [in SMTLIB.Theory.Seq]
holds [in SMTLIB.Eval]
ho_core_interp [in SMTLIB.Theory.HO_Core]
ho_app [in SMTLIB.Theory.HO_Core]
ho_core_funcs [in SMTLIB.Theory.HO_Core]
ho_interp [in SMTLIB.Tests.TestTheory]
I
identifier_eqb [in SMTLIB.Symbols]identifier_add_prefix [in SMTLIB.Symbols]
identifier_sind [in SMTLIB.Symbols]
identifier_rec [in SMTLIB.Symbols]
identifier_ind [in SMTLIB.Symbols]
identifier_rect [in SMTLIB.Symbols]
idiv_ [in SMTLIB.Theory.Reals_Ints]
id_bool [in SMTLIB.Tests.UnitTests]
impl_ [in SMTLIB.Theory.Core]
index_eqb [in SMTLIB.Symbols]
index_sind [in SMTLIB.Symbols]
index_rec [in SMTLIB.Symbols]
index_ind [in SMTLIB.Symbols]
index_rect [in SMTLIB.Symbols]
infix [in SMTLIB.Utils]
instance_of [in SMTLIB.Symbols]
interpretation [in SMTLIB.Theory]
interp_insert_func [in SMTLIB.Theory]
interp_insert_rank [in SMTLIB.Theory]
interp_const [in SMTLIB.Theory]
interp_agree_on [in SMTLIB.Theory]
interp_curry [in SMTLIB.Theory]
interp_apply [in SMTLIB.Theory]
int_literal_value [in SMTLIB.Theory.Reals_Ints]
int_literal [in SMTLIB.Theory.Reals_Ints]
int_literals [in SMTLIB.Theory.Reals_Ints]
is_hex_digit [in SMTLIB.Theory.Strings]
is_int [in SMTLIB.Theory.Reals_Ints]
is_seqb [in SMTLIB.Theory.Seq]
ite_ [in SMTLIB.Theory.Core]
L
lc_at_sind [in SMTLIB.Term]lc_at_ind [in SMTLIB.Term]
lc_sind [in SMTLIB.Term]
lc_ind [in SMTLIB.Term]
leq_ [in SMTLIB.Theory.Reals_Ints]
list_eqb [in SMTLIB.Utils]
list_ForallT [in SMTLIB.Utils]
literal_payload [in SMTLIB.Theory.Strings]
lt_ [in SMTLIB.Theory.Reals_Ints]
M
minus_ [in SMTLIB.Theory.Reals_Ints]models_f_string_literal [in SMTLIB.Theory.Strings]
models_f_str_lt [in SMTLIB.Theory.Strings]
models_f_str_len [in SMTLIB.Theory.Strings]
models_f_str_concat [in SMTLIB.Theory.Strings]
models_f_ite [in SMTLIB.Theory.Core]
models_f_distinct [in SMTLIB.Theory.Core]
models_f_eq [in SMTLIB.Theory.Core]
models_f_xor [in SMTLIB.Theory.Core]
models_f_or [in SMTLIB.Theory.Core]
models_f_and [in SMTLIB.Theory.Core]
models_f_impl [in SMTLIB.Theory.Core]
models_f_not [in SMTLIB.Theory.Core]
models_f_false [in SMTLIB.Theory.Core]
models_f_true [in SMTLIB.Theory.Core]
models_f_decimal_literal [in SMTLIB.Theory.Reals_Ints]
models_f_int_literal [in SMTLIB.Theory.Reals_Ints]
models_f_divisible [in SMTLIB.Theory.Reals_Ints]
models_f_is_int [in SMTLIB.Theory.Reals_Ints]
models_f_to_int [in SMTLIB.Theory.Reals_Ints]
models_f_to_real [in SMTLIB.Theory.Reals_Ints]
models_f_gt_real [in SMTLIB.Theory.Reals_Ints]
models_f_geq_real [in SMTLIB.Theory.Reals_Ints]
models_f_lt_real [in SMTLIB.Theory.Reals_Ints]
models_f_leq_real [in SMTLIB.Theory.Reals_Ints]
models_f_div [in SMTLIB.Theory.Reals_Ints]
models_f_times_real [in SMTLIB.Theory.Reals_Ints]
models_f_plus_real [in SMTLIB.Theory.Reals_Ints]
models_f_minus_sub_real [in SMTLIB.Theory.Reals_Ints]
models_f_minus_neg_real [in SMTLIB.Theory.Reals_Ints]
models_f_gt_int [in SMTLIB.Theory.Reals_Ints]
models_f_geq_int [in SMTLIB.Theory.Reals_Ints]
models_f_lt_int [in SMTLIB.Theory.Reals_Ints]
models_f_leq_int [in SMTLIB.Theory.Reals_Ints]
models_f_abs [in SMTLIB.Theory.Reals_Ints]
models_f_mod [in SMTLIB.Theory.Reals_Ints]
models_f_idiv [in SMTLIB.Theory.Reals_Ints]
models_f_times_int [in SMTLIB.Theory.Reals_Ints]
models_f_plus_int [in SMTLIB.Theory.Reals_Ints]
models_f_minus_sub_int [in SMTLIB.Theory.Reals_Ints]
models_f_minus_neg_int [in SMTLIB.Theory.Reals_Ints]
models_f_app [in SMTLIB.Theory.HO_Core]
models_f_seq_map [in SMTLIB.Theory.Seq]
models_f_seq_contains [in SMTLIB.Theory.Seq]
models_f_seq_nth [in SMTLIB.Theory.Seq]
models_f_seq_len [in SMTLIB.Theory.Seq]
models_f_seq_concat [in SMTLIB.Theory.Seq]
models_f_seq_unit [in SMTLIB.Theory.Seq]
models_f_seq_empty [in SMTLIB.Theory.Seq]
mod_ [in SMTLIB.Theory.Reals_Ints]
monomorphic_entails [in SMTLIB.Eval]
monomorphic_sat [in SMTLIB.Eval]
monomorphic_rank [in SMTLIB.Signature]
monomorphic_sort_subst [in SMTLIB.Sorting]
monomorphic_instance_of [in SMTLIB.Symbols]
monomorphic_sind [in SMTLIB.Symbols]
monomorphic_ind [in SMTLIB.Symbols]
N
neg_bool [in SMTLIB.Tests.UnitTests]neg_ [in SMTLIB.Theory.Reals_Ints]
nn_bool [in SMTLIB.Tests.UnitTests]
not_ [in SMTLIB.Theory.Core]
O
open [in SMTLIB.Term]ors_ [in SMTLIB.Theory.Core]
or_ [in SMTLIB.Theory.Core]
P
pars [in SMTLIB.Term]parse_string_literal [in SMTLIB.Theory.Strings]
parse_decimal_literal [in SMTLIB.Theory.Reals_Ints]
parse_int_literal [in SMTLIB.Theory.Reals_Ints]
parse_divisible [in SMTLIB.Theory.Reals_Ints]
parse_Z [in SMTLIB.Utils]
parse_positive [in SMTLIB.Utils]
parse_N [in SMTLIB.Utils]
parse_N_go [in SMTLIB.Utils]
parse_N_char [in SMTLIB.Utils]
pattern_binders [in SMTLIB.Term]
pattern_constructor [in SMTLIB.Term]
pattern_sind [in SMTLIB.Term]
pattern_rec [in SMTLIB.Term]
pattern_ind [in SMTLIB.Term]
pattern_rect [in SMTLIB.Term]
plain_char [in SMTLIB.Theory.Strings]
plus_ [in SMTLIB.Theory.Reals_Ints]
polymorphic_term_has_sort [in SMTLIB.Sorting]
pretheory_interpretable [in SMTLIB.Theory]
pretheory_local [in SMTLIB.Theory]
pretheory_add_sorts [in SMTLIB.Theory]
pretheory_compose [in SMTLIB.Theory]
Q
quote_string [in SMTLIB.Theory.Strings]quote_char [in SMTLIB.Theory.Strings]
R
rank_strings_sind [in SMTLIB.Theory.Strings]rank_strings_ind [in SMTLIB.Theory.Strings]
rank_core_sind [in SMTLIB.Theory.Core]
rank_core_ind [in SMTLIB.Theory.Core]
rank_consistent [in SMTLIB.Signature]
rank_reals_ints_sind [in SMTLIB.Theory.Reals_Ints]
rank_reals_ints_ind [in SMTLIB.Theory.Reals_Ints]
rank_ho_core_sind [in SMTLIB.Theory.HO_Core]
rank_ho_core_rec [in SMTLIB.Theory.HO_Core]
rank_ho_core_ind [in SMTLIB.Theory.HO_Core]
rank_ho_core_rect [in SMTLIB.Theory.HO_Core]
rank_seq_sind [in SMTLIB.Theory.Seq]
rank_seq_ind [in SMTLIB.Theory.Seq]
rank_uninterp_sind [in SMTLIB.Tests.TestTheory]
rank_uninterp_rec [in SMTLIB.Tests.TestTheory]
rank_uninterp_ind [in SMTLIB.Tests.TestTheory]
rank_uninterp_rect [in SMTLIB.Tests.TestTheory]
reals_ints_interp [in SMTLIB.Theory.Reals_Ints]
reals_ints_funcs [in SMTLIB.Theory.Reals_Ints]
refl_A [in SMTLIB.Tests.UnitTests]
ri_literals [in SMTLIB.Theory.Reals_Ints]
S
sat [in SMTLIB.Eval]seq_adt_interpretation [in SMTLIB.Theory.Seq]
seq_tester_interp [in SMTLIB.Theory.Seq]
seq_selector_interp [in SMTLIB.Theory.Seq]
seq_tester_value [in SMTLIB.Theory.Seq]
seq_selector_value [in SMTLIB.Theory.Seq]
seq_constructor_interp [in SMTLIB.Theory.Seq]
seq_constructor_rank_ok [in SMTLIB.Theory.Seq]
seq_adt_axioms [in SMTLIB.Theory.Seq]
seq_adt_constructor_condition [in SMTLIB.Theory.Seq]
seq_ground_term_project [in SMTLIB.Theory.Seq]
seq_ground_term_embed [in SMTLIB.Theory.Seq]
seq_ground_term_leaf [in SMTLIB.Theory.Seq]
seq_domain_gen [in SMTLIB.Theory.Seq]
seq_ground_term_size [in SMTLIB.Theory.Seq]
seq_ground_term_rect [in SMTLIB.Theory.Seq]
seq_ground_term_constructor [in SMTLIB.Theory.Seq]
seq_embeddable_sort [in SMTLIB.Theory.Seq]
seq_embeddableb [in SMTLIB.Theory.Seq]
seq_sorts_not_adt [in SMTLIB.Theory.Seq]
seq_interp [in SMTLIB.Theory.Seq]
seq_map_interp [in SMTLIB.Theory.Seq]
seq_contains_interp [in SMTLIB.Theory.Seq]
seq_nth_interp [in SMTLIB.Theory.Seq]
seq_len_interp [in SMTLIB.Theory.Seq]
seq_concat_interp [in SMTLIB.Theory.Seq]
seq_unit_interp [in SMTLIB.Theory.Seq]
seq_empty_interp [in SMTLIB.Theory.Seq]
seq_at [in SMTLIB.Theory.Seq]
seq_map [in SMTLIB.Theory.Seq]
seq_contains [in SMTLIB.Theory.Seq]
seq_nth [in SMTLIB.Theory.Seq]
seq_len [in SMTLIB.Theory.Seq]
seq_concat [in SMTLIB.Theory.Seq]
seq_unit [in SMTLIB.Theory.Seq]
seq_empty [in SMTLIB.Theory.Seq]
seq_funcs [in SMTLIB.Theory.Seq]
signature_add_sorts [in SMTLIB.Signature]
signature_with_sorts [in SMTLIB.Signature]
signature_compose [in SMTLIB.Signature]
slash_free [in SMTLIB.Theory.Reals_Ints]
smt_mod [in SMTLIB.Theory.Reals_Ints]
smt_div [in SMTLIB.Theory.Reals_Ints]
sort_wf [in SMTLIB.Signature]
sort_subst [in SMTLIB.Symbols]
sort_subst_map_monomorphic [in SMTLIB.Symbols]
sort_wf_base_sind [in SMTLIB.Symbols]
sort_wf_base_ind [in SMTLIB.Symbols]
sort_top_symbol [in SMTLIB.Symbols]
sort_params [in SMTLIB.Symbols]
sort_to_gen_tree [in SMTLIB.Symbols]
sort_rec [in SMTLIB.Symbols]
sort_rect [in SMTLIB.Symbols]
sort_ind [in SMTLIB.Symbols]
sort_domain_witness [in SMTLIB.Domain]
sort_domain [in SMTLIB.Domain]
strings_interp [in SMTLIB.Theory.Strings]
strings_funcs [in SMTLIB.Theory.Strings]
string_literals [in SMTLIB.Theory.Strings]
string_literal [in SMTLIB.Theory.Strings]
string_split_at [in SMTLIB.Utils]
string_occurs [in SMTLIB.Utils]
string_strip_prefix [in SMTLIB.Utils]
structure_of [in SMTLIB.Theory]
sub_term [in SMTLIB.Term]
sub_sort [in SMTLIB.Symbols]
s_string [in SMTLIB.Theory.Strings]
s_real [in SMTLIB.Theory.Reals_Ints]
s_int [in SMTLIB.Theory.Reals_Ints]
s_seq [in SMTLIB.Theory.Seq]
s_map [in SMTLIB.Symbols]
s_bool [in SMTLIB.Symbols]
T
term_sort_subst [in SMTLIB.Term]term_subst [in SMTLIB.Term]
term_close [in SMTLIB.Term]
term_open [in SMTLIB.Term]
term_size [in SMTLIB.Term]
term_decode [in SMTLIB.Term]
term_encode [in SMTLIB.Term]
term_rec [in SMTLIB.Term]
term_rect [in SMTLIB.Term]
term_ind [in SMTLIB.Term]
term_has_sort_sind [in SMTLIB.Sorting]
term_has_sort_ind [in SMTLIB.Sorting]
test_interp [in SMTLIB.Tests.TestTheory]
test_witness [in SMTLIB.Tests.TestTheory]
test_base_witness [in SMTLIB.Tests.TestTheory]
test_base [in SMTLIB.Tests.TestTheory]
TExistss [in SMTLIB.Term]
theory_init [in SMTLIB.Theory]
theory_init_seq [in SMTLIB.Theory.Seq]
times_ [in SMTLIB.Theory.Reals_Ints]
to_int [in SMTLIB.Theory.Reals_Ints]
to_real [in SMTLIB.Theory.Reals_Ints]
true_ [in SMTLIB.Theory.Core]
T_strings [in SMTLIB.Theory.Strings]
T_core [in SMTLIB.Theory.Core]
T_reals_ints [in SMTLIB.Theory.Reals_Ints]
T_ho_core [in SMTLIB.Theory.HO_Core]
T_seq [in SMTLIB.Theory.Seq]
T_ho [in SMTLIB.Tests.TestTheory]
T_ho_pre [in SMTLIB.Tests.TestTheory]
T_test [in SMTLIB.Tests.TestTheory]
T_arith [in SMTLIB.Tests.TestTheory]
T_uninterp [in SMTLIB.Tests.TestTheory]
U
unescape_string [in SMTLIB.Theory.Strings]uninterp_f [in SMTLIB.Tests.TestTheory]
u_B [in SMTLIB.Symbols]
u_A [in SMTLIB.Symbols]
V
valuation_well_sorted [in SMTLIB.Eval]valuation_sorting [in SMTLIB.Eval]
V_ho [in SMTLIB.Tests.UnitTests]
V_free [in SMTLIB.Tests.TestTheory]
X
xor_ [in SMTLIB.Theory.Core]Z
zero_real [in SMTLIB.Theory.Reals_Ints]zero_int [in SMTLIB.Theory.Reals_Ints]
other
Σ_strings [in SMTLIB.Theory.Strings]Σ_core [in SMTLIB.Theory.Core]
Σ_reals_ints [in SMTLIB.Theory.Reals_Ints]
Σ_ho_core [in SMTLIB.Theory.HO_Core]
Σ_seq [in SMTLIB.Theory.Seq]
Σ_ho [in SMTLIB.Tests.TestTheory]
Σ_test [in SMTLIB.Tests.TestTheory]
Σ_uninterp [in SMTLIB.Tests.TestTheory]
σ_string [in SMTLIB.Theory.Strings]
σ_real [in SMTLIB.Theory.Reals_Ints]
σ_int [in SMTLIB.Theory.Reals_Ints]
σ_bool [in SMTLIB.Symbols]
τ_seq [in SMTLIB.Theory.Seq]
τ_B [in SMTLIB.Symbols]
τ_A [in SMTLIB.Symbols]
τ_map [in SMTLIB.Symbols]
Record Index
A
adt_constructed [in SMTLIB.Theory]adt_axioms [in SMTLIB.Theory]
C
Compose [in SMTLIB.Signature]M
models_strings [in SMTLIB.Theory.Strings]models_core [in SMTLIB.Theory.Core]
models_reals_ints [in SMTLIB.Theory.Reals_Ints]
models_ho_core [in SMTLIB.Theory.HO_Core]
models_seq [in SMTLIB.Theory.Seq]
P
pretheories_composable [in SMTLIB.Theory]pretheory [in SMTLIB.Theory]
R
rank_extension [in SMTLIB.Signature]S
seq_adt_conditions [in SMTLIB.Theory.Seq]signature [in SMTLIB.Signature]
signatures_agree_except_sorts [in SMTLIB.Signature]
signatures_composable [in SMTLIB.Signature]
signature_expansion [in SMTLIB.Signature]
structure [in SMTLIB.Theory]
T
theory [in SMTLIB.Theory]| 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 | (1562 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 | (10 entries) |
| 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 | (108 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 | (15 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 | (623 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 | (116 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) |
| 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 | (23 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 | (29 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 | (33 entries) |
| Abbreviation 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 | (25 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 | (426 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 | (18 entries) |
This page has been generated by coqdoc