aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Check.v
blob: 2c9fc7ada8280c6c75a3df762b02855025626695 (plain)
1
2
3
4
5
6
7
(* 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.