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 |