coq - Coq证明中的椭圆是什么意思？

这是在线类(class)https://softwarefoundations.cis.upenn.edu/plf-current/StlcProp.html#lab222中显示的证明。

Proof with eauto.
  remember (@empty ty) as Gamma.
  intros t t' T HT. generalize dependent t'.
  induction HT;
       intros t' HE; subst Gamma; subst;
       try solve [inversion HE; subst; auto].
  - (* T_App *)
    inversion HE; subst...
    (* Most of the cases are immediate by induction,
       and [eauto] takes care of them *)
    + (* ST_AppAbs *)
      apply substitution_preserves_typing with T11...
      inversion HT1...
Qed.

此行中的椭圆是做什么的？apply substitution_preserves_typing with T11...

最佳答案

椭圆采用某种预定义的策略。在此证明中，它是eauto，因为证明以Proof with eauto开头。有关更多信息，请参见reference manual。

关于coq - Coq证明中的椭圆是什么意思？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/54385439/