Library MetaCoq.PCUIC.PCUICGeneration

Section Generation.
  Context `{cf : config.checker_flags}.

  Definition isWfArity_or_Type Σ Γ T : Type := (isWfArity typing Σ Γ T + isType Σ Γ T).

  Inductive typing_spine (Σ : global_env_ext) (Γ : context) :
    term → list term → term → Type :=
  | type_spine_nil ty ty' :
      isWfArity_or_Type Σ Γ ty' →
      Σ ;;; Γ |- ty ≤ ty' →
      typing_spine Σ Γ ty [] ty'

  | type_spine_cons hd tl na A B T B' :
      isWfArity_or_Type Σ Γ (tProd na A B) →
      Σ ;;; Γ |- T ≤ tProd na A B →
      Σ ;;; Γ |- hd : A →
      typing_spine Σ Γ (subst10 hd B) tl B' →
      typing_spine Σ Γ T (hd :: tl) B'.

  Lemma type_mkApps Σ Γ t u T t_ty :
    Σ ;;; Γ |- t : t_ty →
    typing_spine Σ Γ t_ty u T →
    Σ ;;; Γ |- mkApps t u : T.

  Lemma type_it_mkLambda_or_LetIn :
    ∀ Σ Γ Δ t A,
      Σ ;;; Γ ,,, Δ |- t : A →
      Σ ;;; Γ |- it_mkLambda_or_LetIn Δ t : it_mkProd_or_LetIn Δ A.

End Generation.