2015-06-25から1日間の記事一覧
式の定義 Inductive Exp : Type := | ExpConst : nat -> Exp | ExpPlus : Exp -> Exp -> Exp | ExpMult : Exp -> Exp -> Exp. Notation "x '+_' y" := (ExpPlus x y) (at level 50): type_scope. Notation "x '*_' y" := (ExpMult x y) (at level 40): type_…