δ-reduction δ-reduction は変数をその定義で置き換える。まず何か定義して、 Coq < Definition hoge := fun x:nat => 2+x. hoge is definedcbvを実行してみる。 Coq < Eval cbv delta [hoge] in (hoge 3). = (fun x : nat => 2 + x) 3 : natこの場合は「hog…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。