我可以在 `coqtop -nois` 下使用策略吗？

Question

就像的op一样，我在-nois下重新开发Coq.Init.Prelude来练习。
我想用战术，但是没有用

我尝试了 Declare ML Module "ltac_plugin". 但没有用。

Welcome to Coq v8.8 (eccf1d50b020e87b4d19d0bda43361e1e82d01b1)

Coq < Declare ML Module "ltac_plugin".
[Loading ML file ltac_plugin.cmxs ... done]

Coq < Goal forall A:Prop, forall proof:A, A.
1 subgoal

  ============================
  forall (A : Prop) (_ : A), A

Unnamed_thm < intro.
Toplevel input, characters 0-5:
> intro.
> ^^^^^
Error: Syntax error: illegal begin of vernac.

Answer 1

您还需要Set Default Proof Mode "Classic" to have access to the standard tactics. This option is currently undocumented。

$ rlwrap coqtop -nois
Welcome to Coq 8.8.0 (May 2018)

Coq < Declare ML Module "ltac_plugin".
[Loading ML file ltac_plugin.cmxs ... done]

Coq < Set Default Proof Mode "Classic".

Coq < Goal forall A:Prop, forall proof:A, A.
1 subgoal

  ============================
  forall (A : Prop) (_ : A), A

Unnamed_thm < intros.
1 subgoal

  A : Prop
  proof : A
  ============================
  A

Unnamed_thm < assumption.
No more subgoals.

Unnamed_thm < Qed.
Unnamed_thm is defined

我可以在 `coqtop -nois` 下使用策略吗？

Can I use a tactics under `coqtop -nois`?

coq

coq-tactic