path: root/test-suite/kernel/inds.mv

Inductive [] nat : Set := O : nat | S : nat->nat.
Check Construct nat 0 1.
Check Construct nat 0 2.