fact: Fixpoint countdown (fuel : nat) : [the stateTraceMonad nat bool of (StateMonad.acto (nat * seq bool)%type)] unit := match fuel with | O => Ret tt | S fuel' => do n <- st_get ; if (n == 0) then st_mark true else do _ <- st_mark false ; do _ <- st_put (n-1) ; countdown fuel' end.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model