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$ 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

0

Reset to default

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.