coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Power function in Coq standard library?

From: Cao Qinxiang <caoqinxiang AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Power function in Coq standard library?
Date: Mon, 26 Feb 2018 18:04:26 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f46.google.com
Ironport-phdr: 9a23:BSmYWhQjT6RSSiV5BvKLAkMx0dpsv+yvbD5Q0YIujvd0So/mwa68bRaN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6kcYYAFe0BNvtDoYn8oVsPohq+ChOqBOPg1zRFgWP50rc90+Q4EAHG2gMhH9MUv3TSo9X4L6gSUeWvw6nJyTXPde9Z2TD46IXRdB0qvPKCXapofMbP1UUiExnJg1aQpID/IT+Zy+QAv3KU4udhU++klnQppBtroje1w8chkonJiZwRylDD7Sh5xZw6Jdy8SEJiZd6kHodcuziUN4Z5Q84uWW5ouCE9yr0JvZ60YjIGx4ggxx7ac/CHco6I7Qz/VOuJPzt0mHZodKi8ihuy60Ss1PDwW8mu3FtFrydJitzMuWoM1xzX5MiHUPx9/kK51DmTzQ/T7fhEIUEylavUKp4u2LgwlpUIvETMGy/5gkT2jKuMeko4/eio7vzrYq/6qZ+EK490lgb+P7wylcy4GOQ0KxQBX2yG+eunz7Dj5k34QLBSjvIsiKXZsZbaJd4apqGjGQNV3JwjuF6DCGKt181dln0aJnpEfgiGhs7nIQLgOvf9WNy2hByVkTF7xvnAMfW1CZzKN3nFgLboe7lV5EtVyQ51xtdascEHQoodKe7+Dxei/OfTCQU0ZlTtkrTXTe5l34ZbYlqhR6qQMafcq1iNv7t9LOyFZYtTszH4eaF8u6zeyEQhkFpYRpGHmIMNYSnhTPtjKkSdJ3Hrh4VZSDpYjk8FVOXvzWa6f3tTanK1Bf9u4zg6DMeiA9+GSNzzxrOG2yi/E9tdYWUUUl0=

Is power function like the following one defined in Coq standard library?

Fixpoint pow_func {A : Type} (f : A -> A) (n : nat) (a : A) : A :=
 match n with
  | O   => a
  | S n => f (pow_func f n a)
end.

I could only find power for natural numbers, Z and ring theory.

Thanks,

Qinxiang

[Coq-Club] Power function in Coq standard library?, Cao Qinxiang, 02/27/2018
- Re: [Coq-Club] Power function in Coq standard library?, Dominique Larchey-Wendling, 02/27/2018
- Re: [Coq-Club] Power function in Coq standard library?, Frédéric Besson, 02/27/2018