index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
misc
/
redirect_printing.out
blob: 4f45c4d4c2474e227feebf132accc8a724dd33a2 (
plain
)
1
2
nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
