4f8db64e23
fix(simplifier): missing simp rule in prop simplifier fix(library/unfold_macros): do not look for untrusted macros when using sufficient trust level
26 lines
1.2 KiB
Text
26 lines
1.2 KiB
Text
[simplifier.prove] goal: ?m_1 : Q
|
|
[simplifier.prove] prove_fn succeeded but did not return a proof
|
|
simplifier_prove_failures.lean:13:15: error: simp tactic failed to simplify
|
|
state:
|
|
⊢ R
|
|
simplifier_prove_failures.lean:13:15: error: failed to add declaration 'example' to environment, value has metavariables
|
|
remark: set 'formatter.hide_full_terms' to false to see the complete term
|
|
?M_1
|
|
[simplifier.prove] goal: ?m_1 : Q
|
|
[simplifier.prove] prove_fn failed to prove Q
|
|
simplifier_prove_failures.lean:14:15: error: simp tactic failed to simplify
|
|
state:
|
|
⊢ R
|
|
simplifier_prove_failures.lean:14:15: error: failed to add declaration 'example' to environment, value has metavariables
|
|
remark: set 'formatter.hide_full_terms' to false to see the complete term
|
|
?M_1
|
|
[simplifier.prove] goal: ?m_1 : Q
|
|
[simplifier.prove] prove_fn succeeded but left an unrecognized metavariable of type P in proof
|
|
simplifier_prove_failures.lean:15:15: error: simp tactic failed to simplify
|
|
state:
|
|
⊢ R
|
|
simplifier_prove_failures.lean:15:15: error: failed to add declaration 'example' to environment, value has metavariables
|
|
remark: set 'formatter.hide_full_terms' to false to see the complete term
|
|
?M_1
|
|
[simplifier.prove] goal: ?m_1 : Q
|
|
[simplifier.prove] success: HPQ HP : Q
|