Schedule/ProofCafe_20

• 04/28 Schedule/ProofCafe_20
• 時間: 14:30 - 17:30
• 場所: 名古屋大学 理学部1号館(多元数理科学棟) 307
• 参加登録: PARTAKE: 第20回 ProofCafe
• ソフトウェアの基礎のポリモルフィズム(多相性)の「rememberタクティック」から
• 参加者: 7人

#remember - remember T. destruct t. はcase_eq T. と似ている。 - destruct (式). の式の部分が変数一つならばrememberやcase_eqは必要ない。 - そもそもboolを使わずsumboolを使っていればよい。

#apply with - apply … with … は使う補題(定理)の引数が多いときなど有用。 - ↑引数名がないときはどうする？ - eapplyを使うという方法もある。