fact: Definition eval_rec (eval : nat -> reccode -> list nat -> option (nat + list nat)) (min : nat) (c : reccode) (v : list nat) : option (nat + list nat) := match c with | rc_cst n => Some (inl n) | rc_zero => Some (inl 0) | rc_succ => match v with | x :: _ => Some (inl (S x)) | _ => None end | rc_proj n => option_map inl (nth_error v n) | rc_comp f g => match eval min g v with | Some (inr g) => id_Some_inl (eval min f g) | _ => None end | rc_cons f g => match eval min f v, eval min g v with | Some (inl f), Some (inr g) => Some (inr (f :: g)) | _, _ => None end | rc_nil => Some (inr nil) | rc_rec f g => match v with | 0 :: v => id_Some_inl (eval min f v) | S n :: v => match eval min (rc_rec f g) (n :: v) with | Some (inl y) => id_Some_inl (eval min g (n :: y :: v)) | _ => None end | _ => None end | rc_min f => match eval 0 f (min :: v) with | Some (inl 0) => Some (inl min) | Some (inl _) => id_Some_inl (eval (S min) (rc_min f) v) | _ => None end end.
imports: Undecidability.L.Datatypes(LNat LOptions LSum List.List_nat) Undecidability.L.Tactics.GenEncode