aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/kernel/inds.mv
blob: bd1cc49f868be6a3c8843038a9c37c4786465c81 (plain)
1
2
3
Inductive [] nat : Set := O : nat | S : nat->nat.
Check Construct nat 0 1.
Check Construct nat 0 2.