inds.mv « kernel « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

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.