2015-06-26から1日間の記事一覧
式の変形その1 Reserved Notation "e '==>' e'" (at level 50, left associativity). Inductive ReduceNatExpR : Exp -> Exp -> Prop := | R_Plus : forall n1 n2 n3, n1 plus n2 is n3 -> (ExpConst n1) +_ (ExpConst n2) ==> ExpConst n3 | R_Times : fora…