Ema

[Yaboku19]

pull request for true false nand zero and add

[shilangyu]

What is "ema" in the PR title?

[shilangyu]

Let's be consistent with the other rules

Suggested change

	| nand_true :
	Reduce (.nand .btrue .btrue) (.bfalse)
	| nand_false1 :
	Reduce (.nand .bfalse _) (.btrue)
	| nand_false2 :
	Reduce (.nand _ .bfalse) (.btrue)
	| successor :
	Reduce t t' ->
	Reduce (.succ t) (.succ t')
	| ctx_add1 :
	Reduce t t' ->
	Reduce (.add t t2) (.add t' t2)
	| ctx_add2 :
	Reduce t t' ->
	IsValue v ->
	Reduce (.add v t) (.add v t')
	| add_zero :
	Reduce (.add .zero t) (t)
	| add_succ :
	Reduce (.add (Term.succ t) (t2)) (Term.succ (.add t t2))
	| nand_true :
	Reduce (.nand .btrue .btrue) .bfalse
	| nand_false1 :
	Reduce (.nand .bfalse _) .btrue
	| nand_false2 :
	Reduce (.nand _ .bfalse) .btrue
	| ctx_succ :
	Reduce t t' ->
	Reduce (.succ t) (.succ t')
	| ctx_add1 :
	Reduce t1 t1' ->
	Reduce (.add t1 t2) (.add t1' t2)
	| ctx_add2 :
	IsValue v1 ->
	Reduce t2 t2' ->
	Reduce (.add v1 t2) (.add v1 t2')
	| add_zero :
	Reduce (.add .zero t2) t2
	| add_succ :
	Reduce (.add (Term.succ t1) t2) (Term.succ (.add t1 t2))

[shilangyu]

Looks good!