aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/InitSyntax.v
blob: eb39782ecd26eabbbddb48444821fb6d1242fdde (plain)
1
2
3
4
(* Soumis par Pierre *)
Print sig2.
Check (exists x : nat, x = x).
Check (fun b : bool => if b then b else b).