-
Notifications
You must be signed in to change notification settings - Fork 6
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Meaning of eato 10
?
#156
Comments
Tactic Notation "normalize" :=
repeat (print_goal; eapply multi_step ;
[ (eauto 10; fail) | (instantiate; simpl)]);
apply multi_refl. Now you may see the reason. The definition of Tactic Notation "deep_normalize" :=
repeat (print_goal; eapply multi_step ;
[ (eauto 20; fail) | (instantiate; simpl)]);
apply multi_refl.
Example halve_30: tapp halve (tnat 30) ==>* tnat 15.
Proof.
unfold halve; deep_normalize.
Qed. |
Wow... |
For a simpler example, try the following:
|
At 12_05 assignment, I believe my
halve
is well-defined.I passed
Example halve_type: empty |- halve \in TArrow TNat TNat. Proof. unfold halve; eauto 10. Qed.
Example halve_10: tapp halve (tnat 10) ==>* tnat 5. Proof. unfold halve; normalize. Qed.
Example halve_11: tapp halve (tnat 11) ==>* tnat 5. Proof. unfold halve; normalize. Qed.
All of those examples.
eauto 10
at first example?Example halve_30: tapp halve (tnat 11) ==>* tnat 15. Proof. unfold halve; normalize. Qed.
with this error,
In nested Ltac calls to "normalize" and "apply multi_refl" (expanded to "apply multi_refl"), last call failed.
?Is there limit of stack depth when using
normalize
?The text was updated successfully, but these errors were encountered: