fact: Fixpoint p_countdown (fuel : nat) : program unit := match fuel with | O => p_ret tt | S fuel' => p_do n <- p_get ; p_cond (n == 0) ( p_mark true ) ( p_do _ <- p_mark false ; p_do _ <- p_put (n-1) ; p_countdown fuel' ) end.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model