[hcoop/debian/mlton.git] / regression / taut.sml

(* a tautology checker *)

datatype t =
   Base of bool
 | Fun of bool -> t

val rec taut =
   fn Base b => b
    | Fun f => taut (f true) andalso taut (f false)

val rec bigTrue =
   fn 0 => Base true
    | n => Fun (fn _ => bigTrue (n - 1))

val _ = taut (bigTrue 12)
Commit	Line	Data
7f918cf1 CE	1	(* a tautology checker *)
	2
	3	datatype t =
	4	Base of bool
	5	\| Fun of bool -> t
	6
	7	val rec taut =
	8	fn Base b => b
	9	\| Fun f => taut (f true) andalso taut (f false)
	10
	11	val rec bigTrue =
	12	fn 0 => Base true
	13	\| n => Fun (fn _ => bigTrue (n - 1))
	14
	15	val _ = taut (bigTrue 12)
	16