Library Imp_LangTrick.Examples.SeriesExampleProofInputs

From Coq Require Import List String Arith Psatz.

From Imp_LangTrick Require Import Imp_LangTrickLanguage StackLanguage FactEnvTranslator ProofCompAuto TerminatesForSure ProofCompCodeCompAgnosticMod ProofCompAutoAnother.
From Imp_LangTrick Require Import StackLangTheorems ImpVarMap ProofCompilerBase Imp_LangLogProp LogicProp ProofCompilerHelpers Imp_LangHoareWF Imp_LangLogHoare ProofCompilerPostHelpers FunctionWellFormed ParamsWellFormed TranslationPure.
From Imp_LangTrick Require Import SeriesExample.
From Imp_LangTrick Require Import EnvToStackLTtoLEQ.

Module Type SeriesProgramInputs.
  Parameter x : nat.   Parameter dn : nat.   Parameter dd : nat. End SeriesProgramInputs.

Fixpoint stk_fenv_ify (funs : list fun_stk) : fun_env_stk :=
  match funs with
  | nil => init_fenv_stk
  | f :: funs' =>
      update (Name f) f (stk_fenv_ify funs')
  end.