From MetaCoq.Template Require Import
        utils
        Ast
        Typing
        config
        Transform
        WcbvEval
        EtaExpand.

Import Transform.

Definition template_program := Ast.Env.program.

Definition wt_template_program {cf : checker_flags} (p : template_program) :=
  let Σ := Ast.Env.empty_ext p.1 in
  wf_ext Σ × ∑ T, Σ ;;; [] |- p.2 : T.

Definition eval_template_program (p : Ast.Env.program) (v : Ast.term) :=
  ∥ WcbvEval.eval p.1 p.2 v ∥.