fact: Fixpoint cutoff (n : nat) `(fr : Free f a) : Free f (option a) := match n with | O => Pure None | S n' => match fr with | Pure x => Pure (Some x) | Join _ g h => Join (cutoff n \o g) h end end.
imports: Hask.Prelude Hask.Control.Monad