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

  • $\begingroup$ This question might be better asked in Proof Assistants. $\endgroup$
    – Pseudonym
    Commented Aug 27, 2023 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$ Commented Aug 27, 2023 at 13:51


Your Answer

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

Browse other questions tagged or ask your own question.