package rocq-partial

Rocq-partial provides a partial monad for representing partiality in Rocq. Resulting programs can be composed, reasoned about, and extracted. General recursion is supported through a recursion monad whose graph and domain are used to define the partial function.