gpt4 book ai didi

coq - Coq 证明中的省略号是什么意思?

转载 作者:行者123 更新时间:2023-12-04 18:19:07 28 4
gpt4 key购买 nike

这是本在线类(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/

28 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com