coq - Coq 证明中的省略号是什么意思?
问题描述
这是此在线课程中出现的证明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
。有关更多信息,请参阅参考手册。
推荐阅读
- c - 在 C 中使用指针时“需要左值作为赋值的左操作数”
- sql - 将身份号码添加到特定列
- swift - iOS oneTimeCode 在某些设备上不起作用
- vue.js - vuetify 'v-app' 标签让一切消失
- javascript - 如何在 Javascript 中观察 WeakMap 的垃圾收集?
- javascript - 我可以在完全不了解 JS 的情况下继续使用 React 吗?
- android - 每隔一段时间 BLE rssi 会减弱约 2 分钟 Android Beacon 库
- ruby-on-rails - Rails 6 - 强参数 - 允许数组
- node.js - 如何强制将用户路由到 HTTP
- python - 在打印语句中输出元组内容的更快方法