MCPcopy Create free account
hub / github.com/argumentcomputer/ix / mk_id

Function mk_id

crates/kernel/src/check.rs:936–938  ·  view source on GitHub ↗
(s: &str)

Source from the content-addressed store, hash-verified

934 }
935
936 let refl_c = self
937 .env
938 .iter()
939 .find(|(id, _)| id.addr == self.prims.eq_refl.addr)
940 .map(|(_, c)| c.clone())
941 .ok_or_else(|| {

Callers 11

test_envFunction · 0.70
check_clears_cachesFunction · 0.70
check_theorem_with_type_in_prop_okFunction · 0.70
check_theorem_with_non_prop_type_rejectedFunction · 0.70
check_axiom_with_non_sort_type_rejectedFunction · 0.70
check_loose_var_in_decl_rejected_before_inferFunction · 0.70
check_out_of_range_universe_param_rejectedFunction · 0.70
check_const_idempotentFunction · 0.70
safe_definition_rejects_unsafe_inductive_refFunction · 0.70
checking_one_definition_checks_sibling_blockFunction · 0.70
check_axiom_referencing_unknown_const_errorsFunction · 0.70

Calls 1

mk_addrFunction · 0.70

Tested by 11

test_envFunction · 0.56
check_clears_cachesFunction · 0.56
check_theorem_with_type_in_prop_okFunction · 0.56
check_theorem_with_non_prop_type_rejectedFunction · 0.56
check_axiom_with_non_sort_type_rejectedFunction · 0.56
check_loose_var_in_decl_rejected_before_inferFunction · 0.56
check_out_of_range_universe_param_rejectedFunction · 0.56
check_const_idempotentFunction · 0.56
safe_definition_rejects_unsafe_inductive_refFunction · 0.56
checking_one_definition_checks_sibling_blockFunction · 0.56
check_axiom_referencing_unknown_const_errorsFunction · 0.56