CODEWITHSUNDEEP
coq
xywang
xywang

Reputation: 951

Can I declare a 'polymorphic' axiom in Coq?

I'd like to have an axiom which accepts either a nat or a bool and returns a nat. Something like

Axiom poly_axiom {A : Set}: A -> nat.

But Coq refused to accept such a 'polymorphic' axiom. Is there any way to do that?

Irrelevant note: the purpose of defining such a weird axiom is to use poly_axiom to calculate the number of axioms used in term t, where t is of type A and t is 'wrapped' inside poly_axiom. There is another axiom defining how to reduce t inside axiom poly_axiom. It's also welcome to see a better solution to this problem.

Upvotes: 2

Views: 114

Answers (1)

gallais
gallais

Reputation: 12093

Unlike with Definitions (and Theorems, etc.), you cannot write variable names on the left hand side of the colon when declaring Axioms. You have to use a forall like so:

Axiom poly_axiom : forall {A : Set}, A -> nat.

Upvotes: 4

Related Questions