# A library for composable, extractable, partial programs

**URL:** <https://discourse.rocq-prover.org/t/a-library-for-composable-extractable-partial-programs/3131>\
**Category:** Announcements\
**Created:** [October 9, 2026, 7:37am UTC](https://discourse.rocq-prover.org/t/a-library-for-composable-extractable-partial-programs/3131 "2026-10-09T07:37:43Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![TheoWinterhalter](https://avatars.discourse-cdn.com/v4/letter/t/ea5d25/32.png) [@TheoWinterhalter](https://discourse.rocq-prover.org/u/TheoWinterhalter)\
**Post date:** [October 9, 2026, 7:37am UTC](https://discourse.rocq-prover.org/t/a-library-for-composable-extractable-partial-programs/3131/1 "2026-10-09T07:37:43Z")

</div>

It’s my pleasure to announce a new Rocq library for partial programs that was designed with Meven Lennon-Bertand and Kenji Maillard, and is now available on opam.

```sh
opam install rocq-partial

```

It lets you write and combine partial fixed points as follows:

```auto
Definition ack : nat → nat → partial nat :=
  #pfix ack (m : nat) (n : nat),
    match m, n with
    | 0, _ => ret (S n)
    | S m', 0 => ack m' 1
    | S m', S n' => k ← ack m n' ;; ack m' k
    end.

Definition ack_sum : nat → partial nat :=
  #pfix ack_sum n,
    if n =? 0 then ret 0
    else
      k ← lift (ack n n) ;;
      l ← ack_sum (n - 1) ;;
      ret (k + l).

```

It’s quite in the early stages, so there’s probably a lot missing compared to what one can find in the wild in Agda or Lean. It’s mostly driven from use cases, so if you have some that do not fit what is provided don’t hesitate to open issues or pull requests.

> **[GitHub - TheoWinterhalter/rocq-partial: A Rocq library for partial programs](https://github.com/TheoWinterhalter/rocq-partial)**
>
> A Rocq library for partial programs