(* Compiling the theories allows to test parsing and typing but not printing *)
(* This file tests that pretty-printing does not fail                        *)
(* Test of exact output is not specified                                     *)

Check O.
Check S.
Check nat.