状態のところを読む。 Definition mystate : state := fun i => match i with | Id n => n // id nに対応するなんらかのnatを返すことが出来る。 end. Definition myid5 := Id 5. Eval simpl in update mystate myid5 10. (* Id 5に対応する値を 10にすると…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。