CODEWITHSUNDEEP
coq
Someone
Someone

Reputation: 1

Can I use functions in Coq as constructors?

I am trying to write a function to determine whether a number is odd and return it if it is, and not if it is not. In order to do this, I have matched the number with an odd function that returns true if it is odd. How can I use this as a constructor? enter image description here

Upvotes: 0

Views: 89

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23612

You cannot use any function as if it were a constructor in a match clause. Only the constructors that appear in the declaration of a data type can be used in this fashion. However, the oddb function returns a boolean, which is a data type defined by constructors, and thus you are allowed to match on its result:

match oddb n with
| true  => (* return something *)
| false => (* return something else *)
end

You can actually write this more verbose form as a regular if-then-else expression as found in other functional programming languages. When you write

if oddb n then
  (* return something *)
else 
  (* return something else *)

Coq automatically translates your input into the form above.

Upvotes: 1

Related Questions