午前中時間が空いた。 Inductive ok_day : day -> Prop := | okd_gd : forall d:day, good_day d -> ok_day d | okd_before : forall d1 d2 : day, ok_day d2 -> day_before d2 d1 -> ok_day d1. という型定義において、 okd_gd は(コンストラクタ)関数で…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。