0
$\begingroup$

I need assistance in defining axioms for partial functions in total function theory that is available in Coq. Specifically, I'm looking for a constructive definition of a partial function that includes a constructor for obtaining a partial function from a smaller finite domain.

My use case involves formalizing the problem of counting the number of mappings from the set $\{0, 1, 2\}$ to $\{0, 1, \ldots, 4\}$. This can be represented as the size of the set of all such functions .Additionally, I am open to including the function extensionality axiom.

I formalized multiplication principles and solved the number of permutations problem using it.

assistance would be greatly appreciated

Improve this question
$\endgroup$
2
  • $\begingroup$ This question might be better asked in Proof Assistants. $\endgroup$
    – Pseudonym ♦
    Aug 27 at 5:54
  • $\begingroup$ There are $5^3 = 125$ such functions. You cannot literally mean that that is the problem you're trying to formalize. What is the real problem you'd like formalized? By the way, trying to formalize partial functions is the wrong way to approach this. $\endgroup$
    – Andrej Bauer
    Aug 27 at 13:51

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.